From 43463df9899d00f0f86c3b655b84a5d5ce75402d Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 25 Mar 2023 16:52:15 +0000
Subject: Extract parsing and evaluation to new modules.

---
 src/CC/Term/Eval.idr | 42 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 src/CC/Term/Eval.idr

(limited to 'src/CC/Term/Eval.idr')

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
-- 
cgit v1.2.3