From 5774bab7d825476cb5e3a642073d3ba1737e87f3 Mon Sep 17 00:00:00 2001 From: Adrien Vannson Date: Tue, 10 May 2022 14:31:34 +0200 Subject: [PATCH 1/3] Fonction find_hyp --- main.ml | 33 ++++++++++++++++++--------------- 1 file changed, 18 insertions(+), 15 deletions(-) diff --git a/main.ml b/main.ml index f982e23..cb9e6b7 100644 --- a/main.ml +++ b/main.ml @@ -65,6 +65,15 @@ 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 @@ -120,27 +129,21 @@ while !subgoals <> [] do explore hyps ) | Apply var -> ( - let rec explore = function - | (var_hyp, TImpl (t1, t2)) :: _ when var_hyp = var && t2 = ty -> ( + match find_hyp var with + | Some (TImpl (t1, t2)) when t2 = ty -> ( subgoals := (t1, hyps) :: !subgoals; fill_holes := function - | hole :: holes -> f ((LApp (LVar var_hyp, hole)) :: holes) + | hole :: holes -> f ((LApp (LVar var, hole)) :: holes) | [] -> fail () ) - | [] -> failwith ("Hypothesis " ^ var ^ " not found or unusable") - | _ :: hyps -> explore hyps - in - explore hyps; + | None -> failwith ("Hypothesis " ^ var ^ " not found") + | _ -> failwith ("Hypothesis " ^ var ^ " unusable") ) | Elim var -> ( - let rec explore = function - | (var_hyp, ty_hyp) :: _ when var_hyp = var && ty_hyp = TFalse -> ( - fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes) - ) - | [] -> failwith ("Hypothesis " ^ var ^ " not found or unusable") - | _ :: hyps -> explore hyps - in - explore hyps; + match find_hyp var with + | Some TFalse -> fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes) + | None -> failwith ("Hypothesis " ^ var ^ " not found") + | _ -> failwith ("Hypothesis " ^ var ^ " unusable") ) done; From dc29a939349b8a23b2fb75d89c72dcfa84e56bcb Mon Sep 17 00:00:00 2001 From: Adrien Vannson Date: Tue, 10 May 2022 14:44:07 +0200 Subject: [PATCH 2/3] Affichage des subgoals --- main.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/main.ml b/main.ml index cb9e6b7..0f15308 100644 --- a/main.ml +++ b/main.ml @@ -84,6 +84,9 @@ while !subgoals <> [] do (* 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; (* Lecture d'une tactique *) Printf.printf "What do you want to do?\n" From 93e1174ff3c351c2fc99e90d5d1343e6a31ca554 Mon Sep 17 00:00:00 2001 From: Adrien Vannson Date: Tue, 10 May 2022 14:50:13 +0200 Subject: [PATCH 3/3] Renommage --- main.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/main.ml b/main.ml index 0f15308..8560f2d 100644 --- a/main.ml +++ b/main.ml @@ -7,13 +7,13 @@ let fail () = (* Parsage des arguments*) let filename = ref "" in -let reduce = ref false in -let alpha = ref false in +let reduce_option = ref false in +let alpha_option = ref false in let typecheck_option = ref false in Arg.parse - [("-reduce", Arg.Set reduce, "Show the step-by-step reduction of a lambda-term"); - ("-alpha", Arg.Set alpha, "Check is two lambda-terms separated by '&' are alpha-convertible"); + [("-reduce", Arg.Set reduce_option, "Show the step-by-step reduction of a lambda-term"); + ("-alpha", Arg.Set alpha_option, "Check is two lambda-terms separated by '&' are alpha-convertible"); ("-typecheck", Arg.Set typecheck_option, "Check if a lambda term has a given type")] (fun s -> filename := s) "The available options are:";