1 files changed, 42 insertions, 0 deletions
diff --git a/src/CC/Term/Eval.idr b/src/CC/Term/Eval.idr
new file mode 100644
index 0000000..311bc34
--- /dev/null
+++ b/src/CC/Term/Eval.idr
@@ -0,0 +1,42 @@
+module CC.Term.Eval
+
+import CC.Name
+import CC.Term
+import CC.Thinning
+
+-- Evaluation ------------------------------------------------------------------
+
+export
+app : Closure ctx -> Lazy (Value ctx) -> Value ctx
+export
+eval : Env local global -> Term local -> Value global
+
+app (Close n env t) v = assert_total $ eval (env :< (n, v)) t
+
+eval env (Var k n prf) = index env k prf
+eval env (Abs n t) = VAbs (Close n env t)
+eval env (App t u) =
+  case eval env t of
+    Ntrl n => Ntrl $ VApp n (eval env u)
+    VAbs close => app close (eval env u)
+eval env (Let n t u) = eval (env :< (n, eval env t)) u
+
+-- Quoting ---------------------------------------------------------------------
+
+export
+quote : {ctx : _} -> Value ctx -> Term ctx
+quoteNtrl : {ctx : _} -> Neutral ctx -> Term ctx
+
+quote (Ntrl n) = quoteNtrl n
+quote (VAbs close@(Close n _ _)) =
+  Abs n $
+  assert_total $
+  quote $
+  app (wknClose close (drop id)) (Ntrl $ VVar 0 n $ Here $ reflexive {rel = (~~)})
+
+quoteNtrl (VVar k n prf) = Var k n prf
+quoteNtrl (VApp n v) = App (quoteNtrl n) (quote v)
+
+export
+normalise : {global : _} -> Env local global -> Term local -> Term global
+normalise env t = quote $ eval env t