diff --git a/README.md b/README.md index 68685ad..987ac9f 100644 --- a/README.md +++ b/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) diff --git a/lib/Convert.ml b/lib/Convert.ml index 0bdefd5..88aa51f 100644 --- a/lib/Convert.ml +++ b/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