Migrate to accumulators (mostly removing EVM code)

1 files changed, 29 insertions, 16 deletions

diff --git a/src/AST.hs b/src/AST.hs
index aeab1b7..2267672 100644
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -30,7 +30,7 @@ data Ty
   | TEither Ty Ty
   | TArr Nat Ty  -- ^ rank, element type
   | TScal ScalTy
-  | TEVM [Ty] Ty
+  | TAccum Nat Ty  -- ^ rank and element type of the array being accumulated to
   deriving (Show, Eq, Ord)
 
 data ScalTy = TI32 | TI64 | TF32 | TF64 | TBool
@@ -43,7 +43,7 @@ data STy t where
   STEither :: STy a -> STy b -> STy (TEither a b)
   STArr :: SNat n -> STy t -> STy (TArr n t)
   STScal :: SScalTy t -> STy (TScal t)
-  STEVM :: SList STy env -> STy t -> STy (TEVM env t)
+  STAccum :: SNat n -> STy t -> STy (TAccum n t)
 deriving instance Show (STy t)
 
 data SScalTy t where
@@ -97,11 +97,9 @@ data Expr x env t where
   EIdx :: x t -> Expr x env (TArr n t) -> Vec n (Expr x env TIx) -> Expr x env t
   EOp :: x t -> SOp a t -> Expr x env a -> Expr x env t
 
-  -- EVM operations
-  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)
+  -- accumulation effect
+  EWith :: Expr x env (TArr n t) -> Expr x (TAccum n t : env) a -> Expr x env (TPair a (TArr n t))
+  EAccum :: Expr x env TIx -> Expr x env t -> Expr x env (TAccum n t) -> Expr x env TNil
 
   -- partiality
   EError :: STy a -> String -> Expr x env a
@@ -157,10 +155,8 @@ typeOf = \case
   EIdx _ e _ | STArr _ t <- typeOf e -> t
   EOp _ op _ -> opt2 op
 
-  EMOne t _ _ -> STEVM t STNil
-  EMScope e | STEVM (SCons t env) a <- typeOf e -> STEVM env (STPair a t)
-  EMReturn env e -> STEVM env (typeOf e)
-  EMBind _ e -> typeOf e
+  EWith e1 e2 -> STPair (typeOf e2) (typeOf e1)
+  EAccum _ _ _ -> STNil
 
   EError t _ -> t
 
@@ -175,7 +171,7 @@ unSTy = \case
   STEither a b -> TEither (unSTy a) (unSTy b)
   STArr n t -> TArr (unSNat n) (unSTy t)
   STScal t -> TScal (unSScalTy t)
-  STEVM l t -> TEVM (unSList l) (unSTy t)
+  STAccum n t -> TAccum (unSNat n) (unSTy t)
 
 unSList :: SList STy env -> [Ty]
 unSList SNil = []
@@ -207,10 +203,8 @@ weakenExpr w = \case
   EIdx1 x e1 e2 -> EIdx1 x (weakenExpr w e1) (weakenExpr w e2)
   EIdx x e1 es -> EIdx x (weakenExpr w e1) (weakenExpr w <$> es)
   EOp x op e -> EOp x op (weakenExpr w e)
-  EMOne t i e -> EMOne t i (weakenExpr w e)
-  EMScope e -> EMScope (weakenExpr w e)
-  EMReturn t e -> EMReturn t (weakenExpr w e)
-  EMBind e1 e2 -> EMBind (weakenExpr w e1) (weakenExpr (WCopy w) e2)
+  EWith e1 e2 -> EWith (weakenExpr w e1) (weakenExpr (WCopy w) e2)
+  EAccum e1 e2 e3 -> EAccum (weakenExpr w e1) (weakenExpr w e2) (weakenExpr w e3)
   EError t s -> EError t s
 
 wsinkN :: SNat n -> env :> ConsN n TIx env
@@ -233,3 +227,22 @@ slistIdx SNil i = case i of {}
 idx2int :: Idx env t -> Int
 idx2int IZ = 0
 idx2int (IS n) = 1 + idx2int n
+
+class KnownScalTy t where knownScalTy :: SScalTy t
+instance KnownScalTy TI32 where knownScalTy = STI32
+instance KnownScalTy TI64 where knownScalTy = STI64
+instance KnownScalTy TF32 where knownScalTy = STF32
+instance KnownScalTy TF64 where knownScalTy = STF64
+instance KnownScalTy TBool where knownScalTy = STBool
+
+class KnownTy t where knownTy :: STy t
+instance KnownTy TNil where knownTy = STNil
+instance (KnownTy s, KnownTy t) => KnownTy (TPair s t) where knownTy = STPair knownTy knownTy
+instance (KnownTy s, KnownTy t) => KnownTy (TEither s t) where knownTy = STEither knownTy knownTy
+instance (KnownNat n, KnownTy t) => KnownTy (TArr n t) where knownTy = STArr knownNat knownTy
+instance KnownScalTy t => KnownTy (TScal t) where knownTy = STScal knownScalTy
+instance (KnownNat n, KnownTy t) => KnownTy (TAccum n t) where knownTy = STAccum knownNat knownTy
+
+class KnownEnv env where knownEnv :: SList STy env
+instance KnownEnv '[] where knownEnv = SNil
+instance (KnownTy t, KnownEnv env) => KnownEnv (t : env) where knownEnv = SCons knownTy knownEnv