conversion of stuck induction

lib/Core/Convert.ml

@@ -22,6 +22,7 @@ and conv_tr (len : int) (ty : V.value) (v1 : V.value) (v2 : V.value) =
   match ty with
   | Type               -> conv_tp len v1 v2
   | T1                 -> () (* unit η-law, this still requires evaluation :/ *)
+  | T0                 -> () (* might be nice, why not? *)
   | Pi (a, C (env, b)) ->
       let fresh = V.Stuck (V.Var (V.Lvl len), a) in
       conv_tr (len+1) (E.eval (fresh :: env) b) (E.app v1 a) (E.app v2 a)
@@ -44,9 +45,27 @@ and conv_stuck (len : int) (s1 : V.stuck) (s2 : V.stuck) =
   | 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
+  | App (f1, x1, ty1), App (f2, x2, ty2) ->
     conv_stuck len f1 f2;
     conv_tp len ty1 ty2;
     conv_tr len ty1 x1 x2
-    end
+  | Ind0 (C (env1, a1), _), Ind0 (C (env2, a2), _) -> (* _ are definitionally equal *)
+    let fresh = V.Stuck (V.Var (V.Lvl len), V.T0) in
+    conv_tp (len+1) (E.eval (fresh :: env1) a1) (E.eval (fresh :: env2) a2)
+  | IndN (C (aenv1, a1), z1, C2 (senv1, s1), st1), IndN (C (aenv2, a2), z2, C2 (senv2, s2), st2) ->
+    conv_stuck len st1 st2;
+    let fresh1 = V.Stuck (V.Var (V.Lvl len), V.TNat) in
+    let ev1fr1 = E.eval (fresh1 :: aenv1) a1 in
+    conv_tp (len+1) ev1fr1 (E.eval (fresh1 :: aenv2) a2);
+    conv_tr len (E.eval (Zero :: aenv1) a1) z1 z2;
+    let fresh2 = V.Stuck (V.Var (V.Lvl len), ev1fr1) in
+    conv_tr (len+2) (E.eval (V.Suc fresh1 :: senv1) a1)
+                    (E.eval (fresh2 :: fresh1 :: senv1) s1)
+                    (E.eval (fresh2 :: fresh1 :: senv2) s2)
+  | IndB (C (env1, a1), t1, f1, st1), IndB (C (env2, a2), t2, f2, st2) ->
+    conv_stuck len st1 st2;
+    let fresh = V.Stuck (V.Var (V.Lvl len), V.TBool) in
+    conv_tp (len+1) (E.eval (fresh :: env1) a1) (E.eval (fresh :: env2) a2);
+    conv_tr len (E.eval (V.True  :: env1) a1) t1 t2;
+    conv_tr len (E.eval (V.False :: env1) a1) f1 f2
   | _ -> raise Unequal

lib/Core/Term.ml

@@ -21,7 +21,7 @@ type term
   | TBool
   | True
   | False
-  | IndB of term binder * term * term * term
+  | IndB of term binder * term * term * term (* ordered true, false *)
 
   | Pi   of term * term binder
   | Lam  of term binder

test/dune

@@ -1,2 +0,0 @@
-(test
- (name implicitt))