completed conversion

README.md

@@ -4,9 +4,6 @@ A "proof assistant" with holes and implcit arguments. Developed to learn about e
 
 # TODO
 
-* evaluation
-* conversion
-
 * Raw syntax
   * Parser (BNFC)
 

lib/Convert.ml

@@ -20,7 +20,7 @@ let rec conv_tp (len : int) (v1 : V.value) (v2 : V.value) =
 
 and conv_tr (len : int) (ty : V.value) (v1 : V.value) (v2 : V.value) =
   match ty with
-  | Type -> conv_tp len v1 v2
+  | Type               -> conv_tp len v1 v2
   | T1                 -> () (* unit η-law, this still requires evaluation :/ *)
   | Pi (a, C (env, b)) ->
       let fresh = V.Stuck (V.Var (V.Lvl len), a) in
@@ -31,8 +31,22 @@ and conv_tr (len : int) (ty : V.value) (v1 : V.value) (v2 : V.value) =
       conv_tr len (E.eval (f1 :: env) b) (E.snd v1) (E.snd v2)
   | _ ->
       begin match v1, v2 with
-      | _ -> failwith "todo"
+      | Zero,  Zero  -> ()
+      | Suc n, Suc m -> conv_tr len ty n m
+      | True,  True  -> ()
+      | False, False -> ()
+      | Stuck (s1, _), Stuck (s2, _) -> conv_stuck len s1 s2
+      | _ -> raise Unequal
       end
 
 and conv_stuck (len : int) (s1 : V.stuck) (s2 : V.stuck) =
-  failwith "todo"
+  match s1, s2 with
+  | Var (Lvl i),       Var (Lvl j)       -> if i == j then () else raise Unequal
+  | Fst p1,            Fst p2            -> conv_stuck len p1 p2
+  | Snd p1,            Snd p2            -> conv_stuck len p1 p2
+  | App (f1, x1, ty1), App (f2, x2, ty2) -> begin
+    conv_stuck len f1 f2;
+    conv_tp len ty1 ty2;
+    conv_tr len ty1 x1 x2
+    end
+  | _ -> raise Unequal