did some work on conversion

This commit is contained in:
Rachel Lambda Samuelsson 2022-08-30 18:08:51 +02:00
parent 354705afe5
commit b7125f0277
2 changed files with 54 additions and 3 deletions

38
lib/Convert.ml Normal file
View File

@ -0,0 +1,38 @@
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 :/ *)
| 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
| _ -> failwith "todo"
end
and conv_stuck (len : int) (s1 : V.stuck) (s2 : V.stuck) =
failwith "todo"

View File

@ -49,10 +49,23 @@ and indN (env : V.env) (b : T.term) (tz : V.value) (ts : T.term) (n : V.value) =
| _ -> failwith "eval IndN impossible error"
and app (f : V.value) (x : V.value) =
failwith "todo"
match f with
| Lam (C (env, tr)) -> eval (x :: env) tr
| Stuck (s, t) -> begin
match t with
| Pi (_, C (env, tr)) -> V.Stuck (V.App (s, x, t), eval (x :: env) tr)
| _ -> failwith "eval app stuck f not of pi type"
end
| _ -> failwith "eval app impossible error"
and fst (p : V.value) =
failwith "todo"
match p with
| Pair (a, _) -> a
| Stuck (s, Sg (a, _)) -> V.Stuck (V.Fst s, a)
| _ -> failwith "eval fst impossible error"
and snd (p : V.value) =
failwith "todo"
match p with
| Pair (_, b) -> b
| Stuck (s, Sg (_, C (env, b))) -> V.Stuck (V.Snd s, (eval (fst p :: env) b))
| _ -> failwith "eval fst impossible error"