(** debugging print *)
let info s = debug_print (lazy ("TACTICALS INFO: " ^ (Lazy.force s)))
+module PET = ProofEngineTypes
+
let id_tac =
let id_tac (proof,goal) =
let _, metasenv, _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
(proof,[goal])
in
- ProofEngineTypes.mk_tactic id_tac
+ PET.mk_tactic id_tac
let fail_tac =
let fail_tac (proof,goal) =
let _, metasenv, _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
- raise (ProofEngineTypes.Fail (lazy "fail tactical"))
+ raise (PET.Fail (lazy "fail tactical"))
in
- ProofEngineTypes.mk_tactic fail_tac
+ PET.mk_tactic fail_tac
-type goal = ProofEngineTypes.goal
+type goal = PET.goal
(** TODO needed until tactics start returning both opened and closed goals
* First part of the function performs a diff among goals ~before tactic
val do_tactic: n: int -> tactic: tactic -> tactic
val try_tactic: tactic: tactic -> tactic
val solve_tactics: tactics: (string * tactic) list -> tactic
+ val progress_tactic: tactic: tactic -> tactic
val tactic: tactic -> tactic
val skip: tactic
val semicolon: tactic
val branch: tactic
val shift: tactic
- val pos: int -> tactic
+ val pos: int list -> tactic
+ val wildcard: tactic
val merge: tactic
val focus: int list -> tactic
val unfocus: tactic
with
e ->
match e with
- | (ProofEngineTypes.Fail _)
+ | (PET.Fail _)
| (CicTypeChecker.TypeCheckerFailure _)
| (CicUnification.UnificationFailure _) ->
info (lazy (
Printexc.to_string e));
first ~tactics istatus
| _ -> raise e) (* [e] must not be caught ; let's re-raise it *)
- | [] -> raise (ProofEngineTypes.Fail (lazy "first: no tactics left"))
+ | [] -> raise (PET.Fail (lazy "first: no tactics left"))
in
S.mk_tactic (first ~tactics)
in
S.set_goals (opened', closed') output_status
with
- (ProofEngineTypes.Fail _) as e ->
+ (PET.Fail _) as e ->
info (lazy
("Tacticals.repeat_tactic failed after nth time with exception: "
^ Printexc.to_string e));
in
S.set_goals (opened', closed') output_status
with
- (ProofEngineTypes.Fail _) as e ->
+ (PET.Fail _) as e ->
info (lazy
("Tacticals.do_tactic failed after nth time with exception: "
^ Printexc.to_string e)) ;
(* This applies tactic and catches its possible failure *)
let try_tactic ~tactic =
- let rec try_tactic ~tactic status =
+ let try_tactic status =
info (lazy "in Tacticals.try_tactic");
try
S.apply_tactic tactic status
with
- (ProofEngineTypes.Fail _) as e ->
+ (PET.Fail _) as e ->
info (lazy (
"Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
S.apply_tactic S.id_tactic status
in
- S.mk_tactic (try_tactic ~tactic)
+ S.mk_tactic try_tactic
(* This tries tactics until one of them doesn't _solve_ the goal *)
(* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
| _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
solve_tactics ~tactics:(moretactics) status
with
- (ProofEngineTypes.Fail _) as e ->
+ (PET.Fail _) as e ->
info (lazy (
"Tacticals.solve_tactics: current tactic failed with exn: "
^ Printexc.to_string e));
solve_tactics ~tactics status
)
| [] ->
- raise (ProofEngineTypes.Fail
+ raise (PET.Fail
(lazy "solve_tactics cannot solve the goal"))
in
S.mk_tactic (solve_tactics ~tactics)
+ let progress_tactic ~tactic =
+ let msg = lazy "Failed to progress" in
+ let get_sequent (proof, goal) =
+ let (_, metasenv, _, _) = proof in
+ let _, context, ty = CicUtil.lookup_meta goal metasenv in
+ context, ty
+ in
+ let progress_tactic ist =
+ let before = get_sequent (S.get_status ist) in
+ let ost = S.apply_tactic tactic ist in
+ match S.goals ost with
+ | [goal], _ when before <> get_sequent (S.get_proof ost, goal) ->
+ raise (PET.Fail msg)
+ | _ -> ost
+ in
+ S.mk_tactic progress_tactic
+
let cont_proxy cont = S.mk_tactic (C.eval cont)
let tactic t = cont_proxy (C.Tactical (C.Tactic t))
let branch = cont_proxy C.Branch
let shift = cont_proxy C.Shift
let pos i = cont_proxy (C.Pos i)
+ let wildcard = cont_proxy C.Wildcard
let merge = cont_proxy C.Merge
let focus goals = cont_proxy (C.Focus goals)
let unfocus = cont_proxy C.Unfocus
module Stack = Continuationals.Stack
type input_status =
- ProofEngineTypes.status (* (proof, goal) *) * Stack.t
+ PET.status (* (proof, goal) *) * Stack.t
type output_status =
- (ProofEngineTypes.proof * goal list * goal list) * Stack.t
+ (PET.proof * goal list * goal list) * Stack.t
- type tactic = ProofEngineTypes.tactic
+ type tactic = PET.tactic
let id_tactic = id_tac
let mk_tactic f =
- ProofEngineTypes.mk_tactic
+ PET.mk_tactic
(fun (proof, goal) as pstatus ->
let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
let istatus = pstatus, stack in
proof, opened)
let apply_tactic tac ((proof, _) as pstatus, stack) =
- let proof', opened = ProofEngineTypes.apply_tactic tac pstatus in
+ let proof', opened = PET.apply_tactic tac pstatus in
(* let _ = prerr_endline ("goal aperti dalla tattica " ^ String.concat "," (List.map string_of_int opened)) in *)
- let before = ProofEngineTypes.goals_of_proof proof in
- let after = ProofEngineTypes.goals_of_proof proof' in
+ let before = PET.goals_of_proof proof in
+ let after = PET.goals_of_proof proof' in
let opened_goals, closed_goals = goals_diff ~before ~after ~opened in
(* let _ = prerr_endline ("goal ritornati dalla tattica " ^ String.concat "," (List.map string_of_int opened_goals)) in *)
(proof', opened_goals, closed_goals), stack
+ let get_status (status, _) = status
+ let get_proof ((proof, _, _), _) = proof
+
let goals ((_, opened, closed), _) = opened, closed
let set_goals (opened, closed) ((proof, _, _), stack) =
(proof, opened, closed), stack