From b1ccb0ad713fd04c2774c8c1dd819b182393b4e5 Mon Sep 17 00:00:00 2001 From: Marwan Date: Fri, 17 May 2024 08:10:26 +0200 Subject: [PATCH] on force l'annotation sur le OU --- affichage.ml | 25 ++++++++++++++++--------- hlam.ml | 32 ++++++++++++++++---------------- lam.ml | 20 ++++++++++---------- parser.mly | 8 ++++---- proof.ml | 12 ++++++------ types.ml | 1 - typing.ml | 37 ++++++++++++++++++++++++++----------- 7 files changed, 78 insertions(+), 57 deletions(-) diff --git a/affichage.ml b/affichage.ml index ec929f9..3d68eb4 100644 --- a/affichage.ml +++ b/affichage.ml @@ -19,7 +19,6 @@ let rec string_of_ty = function 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) -> @@ -35,10 +34,14 @@ let rec string_of_expr = function "exf (" ^ s_e ^ " : " ^ s_ty ^ ")" | Pair (e1, e2) -> "("^(string_of_expr e1)^", "^(string_of_expr e2)^")" - | Left e -> - "l("^(string_of_expr e)^")" - | Right e -> - "r("^(string_of_expr e)^")" + | Left (e, t) -> + let s_e = string_of_expr e in + let s_ty = string_of_ty t in + "l (" ^ s_e ^ " : " ^ s_ty ^ ")" + | Right (e, t) -> + let s_e = string_of_expr e in + let s_ty = string_of_ty t in + "r (" ^ s_e ^ " : " ^ s_ty ^ ")" let rec string_of_hlam = function HFun ((s, t), e) -> @@ -54,10 +57,14 @@ let rec string_of_hlam = function "exf (" ^ s_e ^ " : " ^ s_ty ^ ")" | HPair (e1, e2) -> "("^(string_of_hlam e1)^", "^(string_of_hlam e2)^")" - | HLeft e -> - "l("^(string_of_hlam e)^")" - | HRight e -> - "r("^(string_of_hlam e)^")" + | HLeft (e, t) -> + let s_e = string_of_hlam e in + let s_ty = string_of_ty t in + "l (" ^ s_e ^ " : " ^ s_ty ^ ")" + | HRight (e, t) -> + let s_e = string_of_hlam e in + let s_ty = string_of_ty t in + "r (" ^ s_e ^ " : " ^ s_ty ^ ")" | Ref e -> "{"^(string_of_hlam !e)^"}" | Hole -> "?" diff --git a/hlam.ml b/hlam.ml index 5b3281c..9c61950 100644 --- a/hlam.ml +++ b/hlam.ml @@ -8,8 +8,8 @@ type hlam = (* hollow lam *) | HVar of id | HExf of hlam * Types.ty | HPair of hlam * hlam - | HLeft of hlam - | HRight of hlam + | HLeft of hlam * Types.ty + | HRight of hlam * Types.ty | Ref of hlam ref | Hole @@ -22,8 +22,8 @@ let clean_hlam assoc (h : hlam) : hlam = | 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) + | HLeft (h, t) -> HLeft (clean h, t) + | HRight (h, t) -> HRight (clean h, t) | Ref (hr) -> match List.assq_opt hr !assoc with None -> let new_h = ref (clean !hr) @@ -49,12 +49,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) + | Pair (e1, e2) -> + HPair (hlam_of_lam e1, hlam_of_lam e2) + | Left (e, t) -> + HLeft (hlam_of_lam e, t) + | Right (e, t) -> + HRight (hlam_of_lam e, t) let rec lam_of_hlam : hlam -> lam = function HFun ((x, t), e) -> @@ -68,11 +68,11 @@ 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) + | HPair (e1, e2) -> + Pair (lam_of_hlam e1, lam_of_hlam e2) + | HLeft (e, t) -> + Left (lam_of_hlam e, t) + | HRight (e, t) -> + Right (lam_of_hlam e, t) | Ref e_ref -> lam_of_hlam !e_ref | Hole -> raise (TacticFailed "can not translate unclosed terms") diff --git a/lam.ml b/lam.ml index d61b7ef..267b0ff 100644 --- a/lam.ml +++ b/lam.ml @@ -8,8 +8,8 @@ type lam = | Var of id | Exf of lam * Types.ty | Pair of lam * lam - | Left of lam - | Right of lam + | Left of lam * Types.ty + | Right of lam * Types.ty (** alpha renaming in a deterministic way if readable is set to true, original variable's names are used to rename *) @@ -33,8 +33,8 @@ let alpha_convert ?(readable=false) (e : lam) : lam = | 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) + | Left (e, t) -> Left (alpha_aux e g, t) + | Right (e, t) -> Right (alpha_aux e g, t) in alpha_aux e [] @@ -63,8 +63,8 @@ let rec subst (m : lam) (n : lam) (x : id) : lam = 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) + | Left (e, t) -> Left (subst e n x, t) + | Right (e, t) -> Right (subst e n x, t) (* INVARIANT : e has already been alpha-converted *) let rec betastep (e : lam) : lam option = @@ -100,15 +100,15 @@ let rec betastep (e : lam) : lam option = end | Some e1 -> Some (Pair (e1, e2)) end - | Left e -> + | Left (e, t) -> begin match betastep e with None -> None - | Some e -> Some (Left e) + | Some e -> Some (Left (e, t)) end - | Right e -> + | Right (e, t) -> begin match betastep e with None -> None - | Some e -> Some (Right e) + | Some e -> Some (Right (e, t)) end | Var _ -> None | Exf (e, t) -> diff --git a/parser.mly b/parser.mly index a30d5ed..bd59195 100644 --- a/parser.mly +++ b/parser.mly @@ -73,10 +73,10 @@ expression: { Exf (e, t) } | LPAREN e1=expression COMMA e2=expression RPAREN { Pair(e1, e2) } - | L LPAREN e=expression RPAREN - { Left(e) } - | R LPAREN e=expression RPAREN - { Right(e) } + | L LPAREN e=expression COLON t=ty RPAREN + { Left(e, t) } + | R LPAREN e=expression COLON t=ty RPAREN + { Right(e, t) } | e=app_expr { e } app_expr: diff --git a/proof.ml b/proof.ml index ed311c6..5f7b63e 100644 --- a/proof.ml +++ b/proof.ml @@ -199,10 +199,10 @@ let tact_right ((g, gs) : proof) : proof = None -> raise (TacticFailed "no current goal") | Some (h, goal_ty, cs) -> match goal_ty with - | Or(_, t) -> + | Or(_, t_r) as t -> let new_h = Ref (ref Hole) in - fill h (HRight new_h); - Some (new_h, t, cs), gs + fill h (HRight (new_h, t)); + Some (new_h, t_r, cs), gs | _ -> raise (TacticFailed "Not a disjunction") let tact_left ((g, gs) : proof) : proof = @@ -210,10 +210,10 @@ let tact_left ((g, gs) : proof) : proof = None -> raise (TacticFailed "no current goal") | Some (h, goal_ty, cs) -> match goal_ty with - | Or(t, _) -> + | Or(t_l, _) as t-> let new_h = Ref (ref Hole) in - fill h (HLeft new_h); - Some (new_h, t, cs), gs + fill h (HLeft (new_h, t)); + Some (new_h, t_l, cs), gs | _ -> raise (TacticFailed "Not a disjunction") let apply_tactic (p : proof) (t : tactic) : proof = diff --git a/types.ml b/types.ml index 0d1deb9..6b319be 100644 --- a/types.ml +++ b/types.ml @@ -6,6 +6,5 @@ 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 d7d8355..5430637 100644 --- a/typing.ml +++ b/typing.ml @@ -1,6 +1,8 @@ open Types open Lam +exception Could_not_infer + let rec typecheck (g : gam) (e : lam) (expected_t : ty) : bool = match e with Var x -> (List.assoc x g) = expected_t @@ -25,16 +27,17 @@ let rec typecheck (g : gam) (e : lam) (expected_t : ty) : bool = (typecheck g e1 t1) && (typecheck g e2 t2) | _ -> false end - | Left e -> + | Left (e, t) when t = expected_t -> begin match expected_t with - Or (t, _) -> typecheck g e t + Or (t_l, _) -> typecheck g e t_l | _ -> false end - | Right e -> + | Right (e, t) when t = expected_t -> begin match expected_t with - Or (_, t) -> typecheck g e t + Or (_, t_r) -> typecheck g e t_r | _ -> false end + | Left _ | Right _ -> false and typeinfer (g : gam) (e : lam) : ty = @@ -49,19 +52,31 @@ and typeinfer (g : gam) (e : lam) : ty = Arr (t1, t2) -> if typecheck g e2 t1 then t2 - else failwith "couldn't infer" - | _ -> failwith "couldn't infer" + else raise Could_not_infer + | _ -> raise Could_not_infer end | Exf (e, t) -> if typecheck g e t then Bot - else failwith "couldn't infer" + else raise Could_not_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) + | Left (e, t) -> + begin match t with + Or (t_l, _) -> + if typecheck g e t_l + then t + else raise Could_not_infer + | _ -> raise Could_not_infer + end + | Right (e, t) -> + begin match t with + Or (_, t_r) -> + if typecheck g e t_r + then t + else raise Could_not_infer + | _ -> raise Could_not_infer + end