1 files changed, 72 insertions, 0 deletions
diff --git a/src/Level0.idr b/src/Level0.idr
new file mode 100644
index 0000000..bccaa4f
--- /dev/null
+++ b/src/Level0.idr
@@ -0,0 +1,72 @@
+module Level0
+
+import Data.SnocList.Elem
+import NormalForm
+import Term
+import Thinning
+
+Res : Type -> Type
+Res = Pair ()
+
+public export
+data NormSubst : SnocList Ty -> SnocList Ty -> Type where
+  Base : ctx' `Thins` ctx -> NormSubst ctx ctx'
+  (:<) : NormSubst ctx ctx' -> Normal ctx ty -> NormSubst ctx (ctx' :< ty)
+
+%name NormSubst sub
+
+shift : NormSubst ctx ctx' -> NormSubst (ctx :< ty) ctx'
+shift (Base thin) = Base (Drop thin)
+shift (sub :< t) = shift sub :< wknNorm t (Drop Id)
+
+lift : NormSubst ctx ctx' -> NormSubst (ctx :< ty) (ctx' :< ty)
+lift (Base thin) = Base (keep thin)
+lift (sub :< t) = shift (sub :< t) :< Ntrl (Var Here)
+
+index : NormSubst ctx' ctx -> Elem ty ctx -> Normal ctx' ty
+index (Base thin) i = Ntrl (Var $ index thin i)
+index (sub :< t) Here = t
+index (sub :< t) (There i) = index sub i
+
+restrict : NormSubst ctx1 ctx2 -> ctx3 `Thins` ctx2 -> NormSubst ctx1 ctx3
+restrict (Base thin') thin = Base (thin' . thin)
+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 -> Res (Normal ctx' ty)
+partial
+evalSub : Subst ctx ctx'' -> NormSubst ctx' ctx -> Res (NormSubst ctx' ctx'')
+partial
+rec : Normal ctx N -> Normal ctx ty -> Normal (ctx :< ty) ty -> Res (Normal ctx ty)
+
+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'
+
+evalSub (Base thin) sub' = pure (restrict sub' thin)
+evalSub (sub :< t) sub' = [| evalSub sub sub' :< eval t sub' |]
+
+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)