Mysaa/pieuvre
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Merge remote-tracking branch 'origin/master'

Browse Source
This commit is contained in:
Mysaa 2022-05-10 15:00:38 +02:00
commit 98a9e6964f
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
1 changed files with 25 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
main.ml
View File

@ -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:";
@ -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
@ -75,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"
@ -120,27 +132,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")
)
| Cut tint -> (
subgoals := (TImpl(tint, ty), hyps)::(tint, hyps)::!subgoals;