72 lines
3.2 KiB
OCaml
72 lines
3.2 KiB
OCaml
module V = Value
|
|
module E = Eval
|
|
|
|
exception Unequal (* todo, better exception *)
|
|
|
|
let rec conv_tp (len : int) (v1 : V.value) (v2 : V.value) =
|
|
match v1, v2 with
|
|
| Type, Type -> ()
|
|
| T0, T0 -> ()
|
|
| T1, T1 -> ()
|
|
| TNat, TNat -> ()
|
|
| TBool, TBool -> ()
|
|
| Pi (a1, C (env1, b1)), Pi (a2, C (env2, b2)) (* fallthrough *)
|
|
| Sg (a1, C (env1, b1)), Sg (a2, C (env2, b2)) ->
|
|
conv_tp len a1 a2;
|
|
let fresh = V.Stuck (V.Var (V.Lvl len), a1) in
|
|
conv_tp (len+1) (E.eval (fresh :: env1) b1) (E.eval (fresh :: env2) b2)
|
|
| Stuck (s1, Type), Stuck (s2, Type) -> conv_stuck len s1 s2
|
|
| _ -> raise Unequal
|
|
|
|
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)
|
|
| Sg (a, C (env, b)) ->
|
|
let f1 = E.fst v1 in
|
|
conv_tr len a f1 (E.fst v2);
|
|
conv_tr len (E.eval (f1 :: env) b) (E.snd v1) (E.snd v2)
|
|
| _ ->
|
|
begin match v1, v2 with
|
|
| 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) =
|
|
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) ->
|
|
conv_stuck len f1 f2;
|
|
conv_tp len ty1 ty2;
|
|
conv_tr len ty1 x1 x2
|
|
| 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
|