diff options
Diffstat (limited to 'src/AST.hs')
| -rw-r--r-- | src/AST.hs | 16 |
1 files changed, 13 insertions, 3 deletions
@@ -91,6 +91,11 @@ data Expr x env t where EVar :: x t -> STy t -> Idx env t -> Expr x env t ELet :: x t -> Expr x env a -> Expr x (a : env) t -> Expr x env t + -- base types + EPair :: x (TPair a b) -> Expr x env a -> Expr x env b -> Expr x env (TPair a b) + EFst :: x a -> STy b -> Expr x env (TPair a b) -> Expr x env a + ESnd :: x b -> STy a -> Expr x env (TPair a b) -> Expr x env b + -- 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) @@ -103,7 +108,10 @@ data Expr x env t where EOp :: x t -> SOp a t -> Expr x env a -> Expr x env t -- EVM operations - EMOne :: Idx venv t -> Expr x env t -> Expr x env (TEVM venv TNil) + EMOne :: SList STy venv -> Idx venv t -> Expr x env t -> Expr x env (TEVM venv TNil) + EMScope :: Expr x env (TEVM (t : venv) a) -> Expr x env (TEVM venv (TPair a t)) + EMReturn :: SList STy venv -> Expr x env t -> Expr x env (TEVM venv t) + EMBind :: Expr x env (TEVM venv a) -> Expr x (a : env) (TEVM venv b) -> Expr x env (TEVM venv b) deriving instance (forall ty. Show (x ty)) => Show (Expr x env t) type SOp :: Ty -> Ty -> Type @@ -141,7 +149,7 @@ typeOf = \case EIdx _ e _ | STArr _ t <- typeOf e -> t EOp _ op _ -> opt2 op - EMOne _ _ -> STEVM _ STNil + EMOne t _ _ -> STEVM t STNil unSNat :: SNat n -> Nat unSNat SZ = Z @@ -175,6 +183,7 @@ data env :> env' where WId :: env :> env WSink :: env :> (t : env) WCopy :: env :> env' -> (t : env) :> (t : env') + WPop :: (t : env) :> env' -> env :> env' WThen :: env1 :> env2 -> env2 :> env3 -> env1 :> env3 deriving instance Show (env :> env') @@ -187,6 +196,7 @@ WId @> i = i WSink @> i = IS i WCopy _ @> IZ = IZ WCopy w @> (IS i) = IS (w @> i) +WPop w @> i = w @> IS i WThen w1 w2 @> i = w2 @> w1 @> i weakenExpr :: env :> env' -> Expr x env t -> Expr x env' t @@ -200,7 +210,7 @@ weakenExpr w = \case EIdx1 x e1 e2 -> EIdx1 x (weakenExpr w e1) (weakenExpr w e2) EIdx x e1 es -> EIdx x (weakenExpr w e1) (weakenVec w es) EOp x op e -> EOp x op (weakenExpr w e) - EMOne i e -> EMOne i (weakenExpr w e) + EMOne t i e -> EMOne t i (weakenExpr w e) wcopyN :: SNat n -> env :> env' -> ConsN n TIx env :> ConsN n TIx env' wcopyN SZ w = w |