Merge mutual definitions into a single function.

This is really bad style, but a useful step in making a fuel-powered
stack-based interpreter.

1 files changed, 44 insertions, 33 deletions

diff --git a/src/Level0.idr b/src/Level0.idr
index 51fd236..8bbf29b 100644
--- a/src/Level0.idr
+++ b/src/Level0.idr
@@ -45,39 +45,50 @@ restrict (sub :< t) Id = sub :< t
 restrict (sub :< t) (Drop thin) = restrict sub thin
 restrict (sub :< t) (Keep thin) = restrict sub thin :< t
 
--- Evaluates a term in a context of normal forms.
-partial
-eval : Term ctx ty -> NormSubst ctx' ctx -> Cont (Normal ctx' ty)
-partial
-evalSub : Subst ctx ctx'' -> NormSubst ctx' ctx -> Cont (NormSubst ctx' ctx'')
-partial
-rec : Normal ctx N -> Normal ctx ty -> Normal (ctx :< ty) ty -> Cont (Normal ctx ty)
+data Case : Type where
+  Eval : (0 ty : Ty) -> (0 ctx, ctx' : SnocList Ty) -> Case
+  EvalSub : (0 ctx, ctx', ctx'' : SnocList Ty) -> Case
+  App : (0 ty, ty' : Ty) -> (0 ctx : SnocList Ty) -> Case
+  Rec : (0 ty : Ty) -> (0 ctx : SnocList Ty) -> Case
 
-eval (Var i) sub = pure (index sub i)
-eval (Abs t) sub = [| Abs (eval t $ lift sub) |]
-eval (App t u) sub = do
-  t <- eval t sub
-  case t of
-    Abs t => do
-      u <- eval u sub
-      eval (forgetNorm t) (Base Id :< u)
-    Ntrl t => Ntrl <$> App t <$> eval u sub
-eval Zero sub = pure Zero
-eval (Succ t) sub = [| Succ (eval t sub) |]
-eval (Rec t u v) sub = do
-  t <- eval t sub
-  u <- eval u sub
-  v <- eval v (lift sub)
-  rec t u v
-eval (Sub t sub') sub = do
-  sub' <- evalSub sub' sub
-  eval t sub'
+0 Input : Case -> Type
+Input (Eval ty ctx ctx') = (Term ctx ty, NormSubst ctx' ctx)
+Input (EvalSub ctx ctx' ctx'') = (Subst ctx' ctx, NormSubst ctx'' ctx')
+Input (App ty ty' ctx) = (Normal ctx (ty ~> ty'), Normal ctx ty)
+Input (Rec ty ctx) = (Normal ctx N, Normal ctx ty, Normal (ctx :< ty) ty)
 
-evalSub (Base thin) sub' = pure (restrict sub' thin)
-evalSub (sub :< t) sub' = [| evalSub sub sub' :< eval t sub' |]
+0 Output : Case -> Type
+Output (Eval ty ctx ctx') = Normal ctx' ty
+Output (EvalSub ctx ctx' ctx'') = NormSubst ctx'' ctx
+Output (App ty ty' ctx) = Normal ctx ty'
+Output (Rec ty ctx) = Normal ctx ty
 
-rec Zero u v = pure u
-rec (Succ t) u v = do
-  val <- rec t u v
-  eval (forgetNorm v) (Base Id :< val)
-rec (Ntrl t) u v = pure (Ntrl $ Rec t u v)
+partial
+eval : (c : Case) -> Input c -> Cont (Output c)
+eval (Eval _ _ _) (Var i, sub) = pure (index sub i)
+eval (Eval _ _ _) (Abs t, sub) = [| Abs (eval (Eval _ _ _) (t, lift sub)) |]
+eval (Eval _ _ _) (App t u, sub) = do
+  t <- eval (Eval _ _ _) (t, sub)
+  u <- eval (Eval _ _ _) (u, sub)
+  eval (App _ _ _) (t, u)
+eval (Eval _ _ _) (Zero, sub) = pure Zero
+eval (Eval _ _ _) (Succ t, sub) = [| Succ (eval (Eval _ _ _) (t, sub)) |]
+eval (Eval _ _ _) (Rec t u v, sub) = do
+  t <- eval (Eval _ _ _) (t, sub)
+  u <- eval (Eval _ _ _) (u, sub)
+  v <- eval (Eval _ _ _) (v, lift sub)
+  eval (Rec _ _) (t, u, v)
+eval (Eval _ _ _) (Sub t sub', sub) = do
+  sub' <- eval (EvalSub _ _ _) (sub', sub)
+  eval (Eval _ _ _) (t, sub')
+eval (EvalSub _ _ _) (Base thin, sub') = pure (restrict sub' thin)
+eval (EvalSub _ _ _) (sub :< t, sub') =
+  [| eval (EvalSub _ _ _) (sub, sub') :< eval (Eval _ _ _) (t, sub') |]
+eval (App _ _ _) (Abs t, u) =
+  eval (Eval _ _ _) (forgetNorm t, Base Id :< u)
+eval (App _ _ _) (Ntrl t, u) = pure (Ntrl $ App t u)
+eval (Rec _ _) (Zero, u, v) = pure u
+eval (Rec _ _) (Succ t, u, v) = do
+  val <- eval (Rec _ _) (t, u, v)
+  eval (Eval _ _ _) (forgetNorm v, Base Id :< val)
+eval (Rec _ _) (Ntrl t, u, v) = pure (Ntrl $ Rec t u v)