From b7125f02771727588fc641df70d75b9affe4c35d Mon Sep 17 00:00:00 2001 From: depsterr Date: Tue, 30 Aug 2022 18:08:51 +0200 Subject: [PATCH] did some work on conversion --- lib/Convert.ml | 38 ++++++++++++++++++++++++++++++++++++++ lib/Eval.ml | 19 ++++++++++++++++--- 2 files changed, 54 insertions(+), 3 deletions(-) create mode 100644 lib/Convert.ml diff --git a/lib/Convert.ml b/lib/Convert.ml new file mode 100644 index 0000000..0bdefd5 --- /dev/null +++ b/lib/Convert.ml @@ -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" diff --git a/lib/Eval.ml b/lib/Eval.ml index 99ca9a3..82df1ab 100644 --- a/lib/Eval.ml +++ b/lib/Eval.ml @@ -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"