diff options
Diffstat (limited to 'src/AST.hs')
| -rw-r--r-- | src/AST.hs | 29 |
1 files changed, 25 insertions, 4 deletions
@@ -11,6 +11,7 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveTraversable #-} module AST (module AST, module AST.Weaken) where import Data.Functor.Const @@ -30,11 +31,12 @@ data SNat n where deriving instance (Show (SNat n)) data Vec n t where - VNil :: Vec n t + VNil :: Vec Z t (:<) :: t -> Vec n t -> Vec (S n) t deriving instance Show t => Show (Vec n t) deriving instance Functor (Vec n) deriving instance Foldable (Vec n) +deriving instance Traversable (Vec n) data SList f l where SNil :: SList f '[] @@ -92,6 +94,9 @@ type family ConsN n x l where ConsN Z x l = l ConsN (S n) x l = x : ConsN n x l +-- General assumption: head of the list (whatever way it is associated) is the +-- inner variable / inner array dimension. In pretty printing, the inner +-- variable / inner dimension is printed on the _right_. type Expr :: (Ty -> Type) -> [Ty] -> Ty -> Type data Expr x env t where -- lambda calculus @@ -109,7 +114,7 @@ data Expr x env t where -- array operations EBuild1 :: x (TArr (S Z) t) -> Expr x env TIx -> Expr x (TIx : env) t -> Expr x env (TArr (S Z) t) - EBuild :: x (TArr n t) -> SNat n -> Vec n (Expr x env TIx) -> Expr x (ConsN n TIx env) t -> Expr x env (TArr n t) + EBuild :: x (TArr n t) -> Vec n (Expr x env TIx) -> Expr x (ConsN n TIx env) t -> Expr x env (TArr n t) EFold1 :: x (TArr n t) -> Expr x (t : t : env) t -> Expr x env (TArr (S n) t) -> Expr x env (TArr n t) -- expression operations @@ -168,7 +173,7 @@ typeOf = \case ECase _ _ a _ -> typeOf a EBuild1 _ _ e -> STArr (SS SZ) (typeOf e) - EBuild _ n _ e -> STArr n (typeOf e) + EBuild _ es e -> STArr (vecLength es) (typeOf e) EFold1 _ _ e | STArr (SS n) t <- typeOf e -> STArr n t EConst _ t _ -> STScal t @@ -212,6 +217,10 @@ fromNat :: Nat -> Int fromNat Z = 0 fromNat (S n) = succ (fromNat n) +vecLength :: Vec n t -> SNat n +vecLength VNil = SZ +vecLength (_ :< v) = SS (vecLength v) + infixr @> (@>) :: env :> env' -> Idx env t -> Idx env' t WId @> i = i @@ -233,7 +242,7 @@ weakenExpr w = \case EInr x t e -> EInr x t (weakenExpr w e) ECase x e1 e2 e3 -> ECase x (weakenExpr w e1) (weakenExpr (WCopy w) e2) (weakenExpr (WCopy w) e3) EBuild1 x e1 e2 -> EBuild1 x (weakenExpr w e1) (weakenExpr (WCopy w) e2) - EBuild x n es e -> EBuild x n (weakenVec w es) (weakenExpr (wcopyN n w) e) + EBuild x es e -> EBuild x (weakenVec w es) (weakenExpr (wcopyN (vecLength es) w) e) EFold1 x e1 e2 -> EFold1 x (weakenExpr (WCopy (WCopy w)) e1) (weakenExpr w e2) EConst x t v -> EConst x t v EIdx1 x e1 e2 -> EIdx1 x (weakenExpr w e1) (weakenExpr w e2) @@ -245,10 +254,18 @@ weakenExpr w = \case EMBind e1 e2 -> EMBind (weakenExpr w e1) (weakenExpr (WCopy w) e2) EError t s -> EError t s +wsinkN :: SNat n -> env :> ConsN n TIx env +wsinkN SZ = WId +wsinkN (SS n) = WSink .> wsinkN n + wcopyN :: SNat n -> env :> env' -> ConsN n TIx env :> ConsN n TIx env' wcopyN SZ w = w wcopyN (SS n) w = WCopy (wcopyN n w) +wpopN :: SNat n -> ConsN n TIx env :> env' -> env :> env' +wpopN SZ w = w +wpopN (SS n) w = wpopN n (WPop w) + weakenVec :: (env :> env') -> Vec n (Expr x env TIx) -> Vec n (Expr x env' TIx) weakenVec _ VNil = VNil weakenVec w (e :< v) = weakenExpr w e :< weakenVec w v @@ -256,3 +273,7 @@ weakenVec w (e :< v) = weakenExpr w e :< weakenVec w v slistMap :: (forall t. f t -> g t) -> SList f list -> SList g list slistMap _ SNil = SNil slistMap f (SCons x list) = SCons (f x) (slistMap f list) + +idx2int :: Idx env t -> Int +idx2int IZ = 0 +idx2int (IS n) = 1 + idx2int n |