Add type checking.HEADmaster

Currently, there is Set in Set. Next step is to add universe levels.

1 files changed, 68 insertions, 10 deletions

diff --git a/src/CC/Term/Eval.idr b/src/CC/Term/Eval.idr
index 311bc34..7029893 100644
--- a/src/CC/Term/Eval.idr
+++ b/src/CC/Term/Eval.idr
@@ -4,22 +4,28 @@ import CC.Name
 import CC.Term
 import CC.Thinning
 
+import Data.SnocList.Elem
+
 -- Evaluation ------------------------------------------------------------------
 
 export
-app : Closure ctx -> Lazy (Value ctx) -> Value ctx
+app : (n : Name) -> Env local global -> Term (local :< n) -> Lazy (Value global) -> Value global
 export
 eval : Env local global -> Term local -> Value global
 
-app (Close n env t) v = assert_total $ eval (env :< (n, v)) t
+app n env t v = 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 (Let n ty val t) = eval (env :< (n, eval env val)) t
+eval env Set = VSet
+eval env (Pi Nothing t u) = VFunc env t u
+eval env (Pi (Just n) t u) = VPi n (eval env t) env u
+eval env (Abs n t) = VAbs env n 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
+    VAbs env' n t => assert_total $ app n env' t (eval env u)
+    _ => assert_total $ idris_crash "eval invariant broken"
 
 -- Quoting ---------------------------------------------------------------------
 
@@ -28,11 +34,17 @@ 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 = (~~)})
+quote VSet = Set
+quote (VPi n t env u) =
+  Pi (Just n)
+    (quote t)
+    (assert_total $ quote $ eval (liftEnv [<n] env) u)
+quote (VFunc env t u) =
+  Pi Nothing
+    (assert_total $ quote $ eval env t)
+    (assert_total $ quote $ eval env u)
+quote (VAbs env n t) =
+  Abs n $ assert_total $ quote $ app n (wknEnv env (drop id)) t (Ntrl $ VVar 0 _ $ fromElem Here)
 
 quoteNtrl (VVar k n prf) = Var k n prf
 quoteNtrl (VApp n v) = App (quoteNtrl n) (quote v)
@@ -40,3 +52,49 @@ 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
+
+-- Conversion ------------------------------------------------------------------
+
+export
+convert : {ctx : Context} -> Value ctx -> Value ctx -> Bool
+convertNtrl : {ctx : Context} -> Neutral ctx -> Neutral ctx -> Bool
+
+convert VSet VSet = True
+
+convert (VFunc env t u) (VFunc env' t' u') =
+  assert_total $
+  convert (eval env t) (eval env' t') &&
+  convert (eval env u) (eval env' u')
+convert (VFunc env t u) (VPi m t' env' u') =
+  assert_total $
+  convert (eval env t) t' &&
+  convert (eval (wknEnv env (drop id)) u) (eval (liftEnv [<m] env') u')
+convert (VPi n t env u) (VFunc env' t' u') =
+  assert_total $
+  convert t (eval env' t') &&
+  convert (eval (liftEnv [<n] env) u) (eval (wknEnv env' (drop id)) u')
+convert (VPi n t env u) (VPi m t' env' u') =
+  convert t t' &&
+  (assert_total $ convert (eval (liftEnv [<n] env) u) (eval (liftEnv [<n] env') $ renTerm Refl u'))
+
+convert (VAbs env n t) (VAbs env' m u) =
+  assert_total $
+  convert (eval (liftEnv [<n] env) t) (eval (liftEnv [<n] env') $ renTerm Refl u)
+convert (VAbs env n t) (Ntrl m) =
+  assert_total $
+  convert
+    (eval (liftEnv [<n] env) t)
+    (Ntrl (VApp (wknNtrl m (drop id)) (Ntrl $ VVar 0 _ $ fromElem Here)))
+convert (Ntrl n)  (VAbs env m t) =
+  assert_total $
+  convert
+    (Ntrl (VApp (wknNtrl n (drop id)) (Ntrl $ VVar 0 _ $ fromElem Here)))
+    (eval (liftEnv [<m] env) t)
+
+convert (Ntrl n) (Ntrl m) = convertNtrl n m
+
+convert _ _ = False
+
+convertNtrl (VVar k _ _) (VVar j _ _) = k == j
+convertNtrl (VApp n v) (VApp m u) = convertNtrl n m && convert v u
+convertNtrl _ _ = False