diff --git a/affichage.ml b/affichage.ml index c3df528..b570c00 100644 --- a/affichage.ml +++ b/affichage.ml @@ -10,14 +10,15 @@ let rec string_of_ty = function let s2 = string_of_ty t2 in "(" ^ s1 ^ " -> " ^ s2 ^ ")" | Bot -> "False" - | And(t1, t2) -> + | And (t1, t2) -> let s1 = string_of_ty t1 in let s2 = string_of_ty t2 in "(" ^ s1 ^ " /\\ " ^ s2 ^ ")" - | Or(t1, t2) -> + | Or (t1, t2) -> let s1 = string_of_ty t1 in let s2 = string_of_ty t2 in "(" ^ s1 ^ " \\/ " ^ s2 ^ ")" + | Unknown -> "Unknown" let rec string_of_expr = function Fun ((s, t), e) -> @@ -31,6 +32,11 @@ let rec string_of_expr = function let s_e = string_of_expr e in let s_ty = string_of_ty t in "exf (" ^ s_e ^ " : " ^ s_ty ^ ")" + | Pair (e1, e2) -> + "Pair("^(string_of_expr e1)^", "^(string_of_expr e2)^")" + | Left e | Right e -> + "["^(string_of_expr e)^"]" + let print_ty t = diff --git a/lam.ml b/lam.ml index 12caae1..d61b7ef 100644 --- a/lam.ml +++ b/lam.ml @@ -7,6 +7,9 @@ type lam = | App of lam * lam | Var of id | Exf of lam * Types.ty + | Pair of lam * lam + | Left of lam + | Right of lam (** alpha renaming in a deterministic way if readable is set to true, original variable's names are used to rename *) @@ -29,6 +32,9 @@ let alpha_convert ?(readable=false) (e : lam) : lam = | App (e1, e2) -> App (alpha_aux e1 g, alpha_aux e2 g) | Var v -> Var (get_ren_var v g) | Exf (e, t) -> Exf (alpha_aux e g, t) + | Pair (e1, e2) -> Pair (alpha_aux e1 g, alpha_aux e2 g) + | Left e -> Left (alpha_aux e g) + | Right e -> Right (alpha_aux e g) in alpha_aux e [] @@ -53,6 +59,12 @@ let rec subst (m : lam) (n : lam) (x : id) : lam = | Exf (e, t) -> let e = subst e n x in Exf (e, t) + | Pair (e1, e2) -> + let e1 = subst e1 n x in + let e2 = subst e2 n x in + Pair (e1, e2) + | Left e -> Left (subst e n x) + | Right e -> Right (subst e n x) (* INVARIANT : e has already been alpha-converted *) let rec betastep (e : lam) : lam option = @@ -79,6 +91,25 @@ let rec betastep (e : lam) : lam option = end | Some e1 -> Some (App (e1, e2)) end + | Pair (e1, e2) -> + begin match betastep e1 with + None -> + begin match betastep e2 with + None -> None + | Some e2 -> Some (Pair (e1, e2)) + end + | Some e1 -> Some (Pair (e1, e2)) + end + | Left e -> + begin match betastep e with + None -> None + | Some e -> Some (Left e) + end + | Right e -> + begin match betastep e with + None -> None + | Some e -> Some (Right e) + end | Var _ -> None | Exf (e, t) -> begin match betastep e with diff --git a/proof.ml b/proof.ml index e832183..b96f91a 100644 --- a/proof.ml +++ b/proof.ml @@ -8,6 +8,9 @@ type hlam = (* hollow lam *) | HApp of hlam * hlam | HVar of id | HExf of hlam * Types.ty + | HPair of hlam * hlam + | HLeft of hlam + | HRight of hlam | Ref of hlam ref | Hole @@ -43,6 +46,9 @@ let clean_hlam assoc (h : hlam) : hlam = | HApp (h1, h2) -> HApp (clean h1, clean h2) | HVar s -> HVar s | HExf (h, t) -> HExf (clean h, t) + | HPair (h1, h2) -> HPair (clean h1, clean h2) + | HLeft h -> HLeft (clean h) + | HRight h -> HRight (clean h) | Ref (hr) -> match List.assq_opt hr !assoc with None -> let new_h = ref (clean !hr) @@ -84,6 +90,12 @@ let rec hlam_of_lam : lam -> hlam = function | Exf (e, t) -> let e = hlam_of_lam e in HExf (e, t) + | Pair (l1, l2) -> + HPair (hlam_of_lam l1, hlam_of_lam l2) + | Left l -> + HLeft (hlam_of_lam l) + | Right l -> + HRight (hlam_of_lam l) let rec lam_of_hlam : hlam -> lam = function HFun ((x, t), e) -> @@ -97,6 +109,12 @@ let rec lam_of_hlam : hlam -> lam = function | HExf (e, t) -> let e = lam_of_hlam e in Exf (e, t) + | HPair (h1, h2) -> + Pair (lam_of_hlam h1, lam_of_hlam h2) + | HLeft h -> + Left (lam_of_hlam h) + | HRight h -> + Right (lam_of_hlam h) | Ref e_ref -> lam_of_hlam !e_ref | Hole -> raise (TacticFailed "can not translate unclosed terms") @@ -242,7 +260,10 @@ let tact_split ((g, gs) : proof) : proof = | Some (h, goal_ty, cs) -> match goal_ty with | And(t1, t2) -> - Some (h, t1, cs), (h, t2, cs)::gs + let h1 = Ref (ref Hole) in + let h2 = Ref (ref Hole) in + fill h (HPair (h1, h2)); + Some (h1, t1, cs), (h2, t2, cs)::gs | _ -> raise (TacticFailed "Not a conjonction") @@ -252,7 +273,9 @@ let tact_right ((g, gs) : proof) : proof = | Some (h, goal_ty, cs) -> match goal_ty with | Or(_, t) -> - Some (h, t, cs), gs + let new_h = Ref (ref Hole) in + fill h (HRight new_h); + Some (new_h, t, cs), gs | _ -> raise (TacticFailed "Not a disjunction") let tact_left ((g, gs) : proof) : proof = @@ -261,7 +284,9 @@ let tact_left ((g, gs) : proof) : proof = | Some (h, goal_ty, cs) -> match goal_ty with | Or(t, _) -> - Some (h, t, cs), gs + let new_h = Ref (ref Hole) in + fill h (HLeft new_h); + Some (new_h, t, cs), gs | _ -> raise (TacticFailed "Not a disjunction") let apply_tactic (p : proof) (t : tactic) : proof = diff --git a/types.ml b/types.ml index 6b319be..0d1deb9 100644 --- a/types.ml +++ b/types.ml @@ -6,5 +6,6 @@ type ty = | And of ty * ty | Or of ty * ty | Bot + | Unknown (* for Or *) type gam = (ty_id * ty) list diff --git a/typing.ml b/typing.ml index 4a3cb86..d7d8355 100644 --- a/typing.ml +++ b/typing.ml @@ -19,6 +19,23 @@ let rec typecheck (g : gam) (e : lam) (expected_t : ty) : bool = end | Exf (e, t) -> (expected_t = Bot) && (typecheck g e t) + | Pair (e1, e2) -> + begin match expected_t with + And (t1, t2) -> + (typecheck g e1 t1) && (typecheck g e2 t2) + | _ -> false + end + | Left e -> + begin match expected_t with + Or (t, _) -> typecheck g e t + | _ -> false + end + | Right e -> + begin match expected_t with + Or (_, t) -> typecheck g e t + | _ -> false + end + and typeinfer (g : gam) (e : lam) : ty = match e with @@ -39,3 +56,12 @@ and typeinfer (g : gam) (e : lam) : ty = if typecheck g e t then Bot else failwith "couldn't infer" + | Pair (e1, e2) -> + And ( + typeinfer g e1, + typeinfer g e2 + ) + | Left e -> + Or (typeinfer g e, Unknown) + | Right e -> + Or (Unknown, typeinfer g e)