From d631cd3e93abb77401509273ab2f0d7f0c76e5b4 Mon Sep 17 00:00:00 2001 From: Adrien Vannson Date: Wed, 18 May 2022 16:36:02 +0200 Subject: [PATCH] Intros --- lexer.mll | 1 + main.ml | 62 +++++++++++++++++++++++++++++++---------------- parser.mly | 9 +++++-- tactic.ml | 1 + tests/intros.8pus | 4 +++ 5 files changed, 54 insertions(+), 23 deletions(-) create mode 100644 tests/intros.8pus diff --git a/lexer.mll b/lexer.mll index 50d8ad5..3e45c7d 100644 --- a/lexer.mll +++ b/lexer.mll @@ -15,6 +15,7 @@ rule token = parse | ',' { COMMA } | "intro" { INTRO } + | "intros" { INTROS } | "assumption" { ASSUMPTION } | "apply" { APPLY } | "elim" { ELIM } diff --git a/main.ml b/main.ml index 2fd67c4..d66a948 100644 --- a/main.ml +++ b/main.ml @@ -162,28 +162,17 @@ let subgoals: (ty * (var_lambda * ty) list) list ref = ref [(ty, [])] in let fill_holes = ref (fun holes -> List.hd holes) in while !subgoals <> [] do - let (ty, hyps) = List.hd !subgoals in - subgoals := List.tl !subgoals; - - let find_hyp (var: var_lambda) : ty option = - let rec explore = function - | [] -> None - | (var_hyp, hyp) :: hyps when var_hyp = var -> Some hyp - | _ :: hyps -> explore hyps - in - explore hyps - in - if is_interactive then ( (* Nettoyage du terminal *) let _ = Sys.command("clear -x") in (* Affichage des hypothèses *) - List.iter (fun (var, h) -> Printf.printf "%s: %s\n" var (string_of_ty h)) hyps; + List.iter + (fun (var, h) -> Printf.printf "%s: %s\n" var (string_of_ty h)) + (snd (List.hd !subgoals)); (* Affichage des sous-buts *) Printf.printf "================\n"; - Printf.printf "%s\n" (string_of_ty ty); List.iter (fun (ty, _) -> Printf.printf "%s\n" (string_of_ty ty) ) !subgoals; @@ -199,23 +188,40 @@ while !subgoals <> [] do with e -> raise TacticParseException in - let applyTactic tactic = - begin + let rec applyTactic tactic = ( + let (ty, hyps) = List.hd !subgoals in + + let find_hyp (var: var_lambda) : ty option = + let rec explore = function + | [] -> None + | (var_hyp, hyp) :: hyps when var_hyp = var -> Some hyp + | _ :: hyps -> explore hyps + in + explore hyps + in + let f = !fill_holes in match tactic with | Intro var -> ( match ty with | TImpl (ty1, ty2) -> ( + subgoals := List.tl !subgoals; subgoals := (ty2, (var, ty1) :: hyps) :: !subgoals; fill_holes := fun holes -> match holes with | h :: hs -> f (LFun (var, ty1, h) :: hs) | _ -> raise TrouException ) - | _ -> raise (TacticException(tactic,"Cannot intro when the goal is no implication.")) + | _ -> raise (TacticException(tactic, "Cannot intro when the goal is no implication.")) ) + | Intros [] -> () + | Intros (t :: ts) -> ( + applyTactic (Intro t); + applyTactic (Intros ts) + ) | Assumption -> ( let rec explore = function | (var, hyp) :: _ when hyp = ty -> ( + subgoals := List.tl !subgoals; fill_holes := fun holes -> f ((LVar var) :: holes) ) | [] -> raise (TacticException(tactic,"Cannot find a tactic that equals the goal.")) @@ -226,6 +232,7 @@ while !subgoals <> [] do | Apply var -> ( match find_hyp var with | Some (TImpl (t1, t2)) when t2 = ty -> ( + subgoals := List.tl !subgoals; subgoals := (t1, hyps) :: !subgoals; fill_holes := function | hole :: holes -> f ((LApp (LVar var, hole)) :: holes) @@ -236,14 +243,19 @@ while !subgoals <> [] do ) | Elim var -> ( match find_hyp var with - | Some TFalse -> fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes) + | Some TFalse -> ( + subgoals := List.tl !subgoals; + fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes) + ) | Some TAnd(tl,tr) -> ( + subgoals := List.tl !subgoals; subgoals := (TImpl(tl,TImpl(tr,ty)),hyps)::!subgoals; fill_holes := fun holes -> match holes with | h::r -> f ((LApp(LApp(h,LFst(LVar(var))),LSnd(LVar(var))))::r) | _ -> raise TrouException ) | Some TOr(tl,tr) -> ( + subgoals := List.tl !subgoals; subgoals := (TImpl(tl,ty),hyps)::(TImpl(tr,ty),hyps)::!subgoals; fill_holes := fun holes -> match holes with | hl::hr::r -> f (LCase(LVar(var),hl,hr)::r) @@ -254,6 +266,7 @@ while !subgoals <> [] do ) (* Pour montrer A, on montre B -> A et B *) | Cut tint -> ( + subgoals := List.tl !subgoals; subgoals := (TImpl (tint, ty), hyps) :: (tint, hyps) :: !subgoals; fill_holes := function | pf :: px :: s -> f ((LApp (pf, px)) :: s) @@ -263,6 +276,7 @@ while !subgoals <> [] do | Split -> ( match ty with | TAnd(t1,t2) -> ( + subgoals := List.tl !subgoals; subgoals := (t1, hyps) :: (t2, hyps) :: !subgoals; fill_holes := fun holes -> match holes with | h1 :: h2 :: hs -> f (LCouple(h1,h2) :: hs) @@ -273,6 +287,7 @@ while !subgoals <> [] do | Left -> ( match ty with | TOr(tl,tr) -> ( + subgoals := List.tl !subgoals; subgoals := (tl, hyps) :: !subgoals; fill_holes := fun holes -> match holes with | hl :: hs -> f (LIg(hl,tr) :: hs) @@ -283,6 +298,7 @@ while !subgoals <> [] do | Right -> ( match ty with | TOr(tl,tr) -> ( + subgoals := List.tl !subgoals; subgoals := (tr, hyps) :: !subgoals; fill_holes := fun holes -> match holes with | hr :: hs -> f (LId(hr,tl) :: hs) @@ -291,10 +307,14 @@ while !subgoals <> [] do | _ -> raise (TacticException(tactic,"Cannot prove right as the goal is no \\/ clause")) ) | Exact l -> ( - if not (typecheck hyps l ty) then raise (TacticException(tactic,"λ-term "^(string_of_lam l)^" cannot be typed with "^(string_of_ty ty)^" as its type is "^(match (computeType [] l) with None -> "None" | Some t -> string_of_ty t))) - else fill_holes := fun holes -> f (l::holes) + if not (typecheck hyps l ty) then + raise (TacticException(tactic,"λ-term "^(string_of_lam l)^" cannot be typed with "^(string_of_ty ty)^" as its type is "^(match (computeType [] l) with None -> "None" | Some t -> string_of_ty t))) + else ( + subgoals := List.tl !subgoals; + fill_holes := fun holes -> f (l::holes) + ) ) - end + ) in let rec applyUntilWorking () = diff --git a/parser.mly b/parser.mly index c6381f1..c421bc3 100644 --- a/parser.mly +++ b/parser.mly @@ -10,7 +10,7 @@ %token VAR_NAME %token TYPE_NAME -%token DOT INTRO ASSUMPTION APPLY ELIM CUT SPLIT LEFT RIGHT EXACT FST SND IG ID CASE I +%token DOT INTRO INTROS ASSUMPTION APPLY ELIM CUT SPLIT LEFT RIGHT EXACT FST SND IG ID CASE I %token FUN MAPS_TO COLON EXF %token AMPERSAND @@ -63,9 +63,14 @@ ty: | FALSE { TFalse } | TRUE { TTrue } +var_list: + | VAR_NAME { [$1] } + | VAR_NAME var_list { $1 :: $2 } + /* Tactiques */ tactic: | INTRO VAR_NAME DOT { Intro $2 } + | INTROS var_list DOT { Intros $2 } | ASSUMPTION DOT { Assumption } | APPLY VAR_NAME DOT { Apply $2 } | ELIM VAR_NAME DOT { Elim $2 } @@ -83,7 +88,7 @@ lambda_arg: /* Expression pouvant être en argument d'une fonction */ | SND LPAREN lambda RPAREN { LSnd ($3) } | IG LPAREN lambda COMMA ty RPAREN { LIg ($3, $5) } | ID LPAREN lambda COMMA ty RPAREN { LId ($3, $5) } - | CASE LPAREN lambda COMMA lambda COMMA lambda RPAREN + | CASE LPAREN lambda COMMA lambda COMMA lambda RPAREN { LCase ($3, $5,$7) } | I { LI } | LPAREN lambda COMMA lambda RPAREN { LCouple($2, $4) } diff --git a/tactic.ml b/tactic.ml index 1aa4aaa..141666e 100644 --- a/tactic.ml +++ b/tactic.ml @@ -2,6 +2,7 @@ open Structs;; type tactic = | Intro of var_lambda + | Intros of var_lambda list | Assumption | Apply of var_lambda | Elim of var_lambda diff --git a/tests/intros.8pus b/tests/intros.8pus new file mode 100644 index 0000000..d359019 --- /dev/null +++ b/tests/intros.8pus @@ -0,0 +1,4 @@ +A -> (A -> B) -> B +intros a f. +apply f. +assumption.