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

Fonction find_hyp

Browse Source
This commit is contained in:
Adrien Vannson 2022-05-10 14:31:34 +02:00
parent 2b98fd6407
commit 5774bab7d8
No known key found for this signature in database
GPG Key ID: FE2E66FD978C1A55
1 changed files with 18 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
main.ml
View File

@ -65,6 +65,15 @@ while !subgoals <> [] do
let (ty, hyps) = List.hd !subgoals in let (ty, hyps) = List.hd !subgoals in
subgoals := List.tl !subgoals; 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 ( if is_interactive then (
(* Nettoyage du terminal *) (* Nettoyage du terminal *)
let _ = Sys.command("clear -x") in let _ = Sys.command("clear -x") in
@ -120,27 +129,21 @@ while !subgoals <> [] do
explore hyps explore hyps
) )
| Apply var -> ( | Apply var -> (
let rec explore = function match find_hyp var with
| (var_hyp, TImpl (t1, t2)) :: _ when var_hyp = var && t2 = ty -> ( | Some (TImpl (t1, t2)) when t2 = ty -> (
subgoals := (t1, hyps) :: !subgoals; subgoals := (t1, hyps) :: !subgoals;
fill_holes := function fill_holes := function
| hole :: holes -> f ((LApp (LVar var_hyp, hole)) :: holes) | hole :: holes -> f ((LApp (LVar var, hole)) :: holes)
| [] -> fail () | [] -> fail ()
) )
| [] -> failwith ("Hypothesis " ^ var ^ " not found or unusable") | None -> failwith ("Hypothesis " ^ var ^ " not found")
| _ :: hyps -> explore hyps | _ -> failwith ("Hypothesis " ^ var ^ " unusable")
in
explore hyps;
) )
| Elim var -> ( | Elim var -> (
let rec explore = function match find_hyp var with
| (var_hyp, ty_hyp) :: _ when var_hyp = var && ty_hyp = TFalse -> ( | Some TFalse -> fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes)
fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes) | None -> failwith ("Hypothesis " ^ var ^ " not found")
) | _ -> failwith ("Hypothesis " ^ var ^ " unusable")
| [] -> failwith ("Hypothesis " ^ var ^ " not found or unusable")
| _ :: hyps -> explore hyps
in
explore hyps;
) )
done; done;