Merge branch 'master' of gitlab.aliens-lyon.fr:savrillo/pieuvre
This commit is contained in:
Adrien Vannson
commit
7b69264e3f
233
main.ml
233
main.ml
@ -1,8 +1,14 @@
|
||||
open Structs;;
|
||||
open Pieuvre;;
|
||||
|
||||
let fail () =
|
||||
failwith "Unknown error";;
|
||||
open Tactic;;
|
||||
|
||||
(* Lorsqu'une tactique ne peut se lancer. Contient la tactique ainsi qu'un message contenant l'erreur.*)
|
||||
exception TacticException of tactic*string;;
|
||||
(* Lorsqu'une tactique est mal écrite*)
|
||||
exception TacticParseException;;
|
||||
(* Exception renvoyée lorsque la fonction de trou est appelée sur une liste trop grande. *)
|
||||
(* Ne devrait jamais être lancée *)
|
||||
exception TrouException;;
|
||||
|
||||
(* Parsage des arguments*)
|
||||
let filename = ref "" in
|
||||
@ -154,112 +160,125 @@ while !subgoals <> [] do
|
||||
Printf.printf "What do you want to do?\n"
|
||||
);
|
||||
|
||||
let tactic =
|
||||
let rec read_tactic () =
|
||||
try
|
||||
let lexbuf = Lexing.from_string (readline ()) in
|
||||
Parser.main_tactic Lexer.token lexbuf
|
||||
with e -> (
|
||||
Printf.printf "Can't parse tactic\n";
|
||||
if is_interactive then
|
||||
read_tactic ()
|
||||
else
|
||||
raise e
|
||||
)
|
||||
in
|
||||
read_tactic ()
|
||||
let rec read_tactic () =
|
||||
try
|
||||
let lexbuf = Lexing.from_string (readline ()) in
|
||||
Parser.main_tactic Lexer.token lexbuf
|
||||
with e -> raise TacticParseException
|
||||
in
|
||||
|
||||
let applyTactic tactic =
|
||||
begin
|
||||
let f = !fill_holes in
|
||||
match tactic with
|
||||
| Intro var -> (
|
||||
match ty with
|
||||
| TImpl (ty1, ty2) -> (
|
||||
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."))
|
||||
)
|
||||
| Assumption -> (
|
||||
let rec explore = function
|
||||
| (var, hyp) :: _ when hyp = ty -> (
|
||||
fill_holes := fun holes -> f ((LVar var) :: holes)
|
||||
)
|
||||
| [] -> raise (TacticException(tactic,"Cannot find a tactic that equals the goal."))
|
||||
| _ :: hyps -> explore hyps
|
||||
in
|
||||
explore hyps
|
||||
)
|
||||
| Apply var -> (
|
||||
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, hole)) :: holes)
|
||||
| [] -> raise TrouException
|
||||
)
|
||||
| None -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it does not exist."))
|
||||
| _ -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it is no implication."))
|
||||
)
|
||||
| Elim var -> (
|
||||
match find_hyp var with
|
||||
| Some TFalse -> fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes)
|
||||
| Some TAnd(tl,tr) -> (
|
||||
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 := (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)
|
||||
| _ -> raise TrouException
|
||||
)
|
||||
| None -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it does not exist."))
|
||||
| _ -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it is neither an implication, nor a /\\ or a \\/"))
|
||||
)
|
||||
(* Pour montrer A, on montre B -> A et B *)
|
||||
| Cut tint -> (
|
||||
subgoals := (TImpl (tint, ty), hyps) :: (tint, hyps) :: !subgoals;
|
||||
fill_holes := function
|
||||
| pf :: px :: s -> f ((LApp (pf, px)) :: s)
|
||||
| _ -> raise TrouException
|
||||
)
|
||||
|
||||
let f = !fill_holes in
|
||||
|
||||
match tactic with
|
||||
| Intro var -> (
|
||||
match ty with
|
||||
| TImpl (ty1, ty2) -> (
|
||||
subgoals := (ty2, (var, ty1) :: hyps) :: !subgoals;
|
||||
fill_holes := fun holes -> match holes with
|
||||
| h :: hs -> f (LFun (var, ty1, h) :: hs)
|
||||
| _ -> fail ()
|
||||
)
|
||||
| _ -> failwith "Can't intro"
|
||||
)
|
||||
| Assumption -> (
|
||||
let rec explore = function
|
||||
| (var, hyp) :: _ when hyp = ty -> (
|
||||
fill_holes := fun holes -> f ((LVar var) :: holes)
|
||||
)
|
||||
| [] -> failwith "No such hypothesis"
|
||||
| _ :: hyps -> explore hyps
|
||||
in
|
||||
explore hyps
|
||||
)
|
||||
| Apply var -> (
|
||||
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, hole)) :: holes)
|
||||
| [] -> fail ()
|
||||
)
|
||||
| None -> failwith ("Hypothesis " ^ var ^ " not found")
|
||||
| _ -> failwith ("Hypothesis " ^ var ^ " unusable")
|
||||
)
|
||||
| Elim var -> (
|
||||
match find_hyp var with
|
||||
| Some TFalse -> fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes)
|
||||
| Some TAnd(tl,tr) -> (
|
||||
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)
|
||||
| _ -> fail ()
|
||||
)
|
||||
| Some TOr(tl,tr) -> (
|
||||
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)
|
||||
| _ -> fail ()
|
||||
)
|
||||
| None -> failwith ("Hypothesis " ^ var ^ " not found")
|
||||
| _ -> failwith ("Hypothesis " ^ var ^ " unusable")
|
||||
)
|
||||
(* Pour montrer A, on montre B -> A et B *)
|
||||
| Cut tint -> (
|
||||
subgoals := (TImpl (tint, ty), hyps) :: (tint, hyps) :: !subgoals;
|
||||
fill_holes := function
|
||||
| pf :: px :: s -> f ((LApp (pf, px)) :: s)
|
||||
| _ -> fail ()
|
||||
)
|
||||
|
||||
| Split ovar -> (
|
||||
match ty with
|
||||
| TAnd(t1,t2) -> (
|
||||
subgoals := (t1, hyps) :: (t2, hyps) :: !subgoals;
|
||||
fill_holes := fun holes -> match holes with
|
||||
| h1 :: h2 :: hs -> f (LCouple(h1,h2) :: hs)
|
||||
| _ -> fail ()
|
||||
)
|
||||
| _ -> failwith "Target not a and clause"
|
||||
)
|
||||
| Left -> (
|
||||
match ty with
|
||||
| TOr(tl,tr) -> (
|
||||
subgoals := (tl, hyps) :: !subgoals;
|
||||
fill_holes := fun holes -> match holes with
|
||||
| hl :: hs -> f (LIg(hl,tr) :: hs)
|
||||
| _ -> fail ()
|
||||
)
|
||||
| _ -> failwith "Target not a or clause"
|
||||
)
|
||||
| Right -> (
|
||||
match ty with
|
||||
| TOr(tl,tr) -> (
|
||||
subgoals := (tr, hyps) :: !subgoals;
|
||||
fill_holes := fun holes -> match holes with
|
||||
| hr :: hs -> f (LId(hr,tl) :: hs)
|
||||
| _ -> fail ()
|
||||
)
|
||||
| _ -> failwith "Target not a or clause"
|
||||
)
|
||||
| Split -> (
|
||||
match ty with
|
||||
| TAnd(t1,t2) -> (
|
||||
subgoals := (t1, hyps) :: (t2, hyps) :: !subgoals;
|
||||
fill_holes := fun holes -> match holes with
|
||||
| h1 :: h2 :: hs -> f (LCouple(h1,h2) :: hs)
|
||||
| _ -> raise TrouException
|
||||
)
|
||||
| _ -> raise (TacticException(tactic,"Cannot split as the goal is no /\\ clause"))
|
||||
)
|
||||
| Left -> (
|
||||
match ty with
|
||||
| TOr(tl,tr) -> (
|
||||
subgoals := (tl, hyps) :: !subgoals;
|
||||
fill_holes := fun holes -> match holes with
|
||||
| hl :: hs -> f (LIg(hl,tr) :: hs)
|
||||
| _ -> raise TrouException
|
||||
)
|
||||
| _ -> raise (TacticException(tactic,"Cannot prove left as the goal is no \\/ clause"))
|
||||
)
|
||||
| Right -> (
|
||||
match ty with
|
||||
| TOr(tl,tr) -> (
|
||||
subgoals := (tr, hyps) :: !subgoals;
|
||||
fill_holes := fun holes -> match holes with
|
||||
| hr :: hs -> f (LId(hr,tl) :: hs)
|
||||
| _ -> raise TrouException
|
||||
)
|
||||
| _ -> raise (TacticException(tactic,"Cannot prove right as the goal is no \\/ clause"))
|
||||
)
|
||||
end
|
||||
in
|
||||
|
||||
let rec applyUntilWorking () =
|
||||
try
|
||||
(
|
||||
let readTactic = read_tactic () in
|
||||
applyTactic readTactic
|
||||
)
|
||||
with
|
||||
| TacticException(t,s) ->
|
||||
Printf.printf "\027[31mCannot apply the tactic: %s\027[0m\n" s;
|
||||
if(is_interactive) then applyUntilWorking () else raise (TacticException(t,s))
|
||||
| TacticParseException ->
|
||||
Printf.printf "\027[31mCannot parse the tactic, please refer to pieuvre documentation.\027[0m\n";
|
||||
if(is_interactive) then applyUntilWorking () else raise TacticParseException
|
||||
| e ->
|
||||
Printf.printf "\027[31mPieuvre Failed Unexpectedly !\027[0m\n";
|
||||
raise e
|
||||
in
|
||||
applyUntilWorking ()
|
||||
done;
|
||||
|
||||
let finalLam = !fill_holes [] in
|
||||
|
||||
@ -70,8 +70,7 @@ tactic:
|
||||
| APPLY VAR_NAME DOT { Apply $2 }
|
||||
| ELIM VAR_NAME DOT { Elim $2 }
|
||||
| CUT ty DOT { Cut $2 }
|
||||
| SPLIT DOT { Split None }
|
||||
| SPLIT VAR_NAME DOT { Split (Some $2) }
|
||||
| SPLIT DOT { Split }
|
||||
| LEFT DOT { Left }
|
||||
| RIGHT DOT { Right }
|
||||
|
||||
|
||||
@ -174,8 +174,8 @@ let rec betastep (l: lam) : lam option = match l with
|
||||
| (LCouple(lg,ld),None) -> Some ld
|
||||
| (_,None) -> None
|
||||
end
|
||||
| LIg(ll,t) -> Option.bind (betastep ll) (fun l' -> Some (LIg(ll,t)))
|
||||
| LId(ll,t) -> Option.bind (betastep ll) (fun l' -> Some (LId(ll,t)))
|
||||
| LIg(ll,t) -> Option.bind (betastep ll) (fun l' -> Some (LIg(l',t)))
|
||||
| LId(ll,t) -> Option.bind (betastep ll) (fun l' -> Some (LId(l',t)))
|
||||
| LCase(ll,lg,ld) -> begin
|
||||
match (ll,betastep ll) with
|
||||
| (_,Some ll') -> Some (LFst(ll'))
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user