let id_tac =
let id_tac (proof,goal) =
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _, _, _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
(proof,[goal])
in
let fail_tac =
let fail_tac (proof,goal) =
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _, _ , _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
raise (PET.Fail (lazy "fail tactical"))
in
type tactic = PET.tactic
- let id_tactic = id_tac
-
(* f is an eval function of a machine;
the machine is applied to a fresh stack and the final stack is read
back to obtain the result of the tactic *)
let mk_tactic f =
PET.mk_tactic
- (fun (proof, goal) as pstatus ->
+ (fun ((proof, goal) as pstatus) ->
let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
let istatus = pstatus, stack in
let (proof, _, _), stack = f istatus in
let opened_goals, closed_goals = goals_diff ~before ~after ~opened 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
(* Done only at the beginning of the eval of the machine *)
let get_stack = snd
(* Tacticals that cannot be implemented on top of tynycals *)
+let const_tac res = PET.mk_tactic (fun _ -> res)
+
+let if_ ~start ~continuation ~fail =
+ let if_ status =
+ let xoutput =
+ try
+ let result = PET.apply_tactic start status in
+ info (lazy ("Tacticals.if_: succedeed!!!"));
+ Some result
+ with PET.Fail _ -> None
+ in
+ let tactic = match xoutput with
+ | Some res -> then_ ~start:(const_tac res) ~continuation
+ | None -> fail
+ in
+ PET.apply_tactic tactic status
+ in
+ PET.mk_tactic if_
+
+let ifs ~start ~continuations ~fail =
+ let ifs status =
+ let xoutput =
+ try
+ let result = PET.apply_tactic start status in
+ info (lazy ("Tacticals.ifs: succedeed!!!"));
+ Some result
+ with PET.Fail _ -> None
+ in
+ let tactic = match xoutput with
+ | Some res -> thens ~start:(const_tac res) ~continuations
+ | None -> fail
+ in
+ PET.apply_tactic tactic status
+ in
+ PET.mk_tactic ifs
+
let first ~tactics =
- let rec first ~(tactics: (string * tactic) list) status =
+ let rec first ~(tactics: tactic list) status =
info (lazy "in Tacticals.first");
match tactics with
[] -> raise (PET.Fail (lazy "first: no tactics left"))
- | (descr, tac)::tactics ->
- info (lazy ("Tacticals.first IS TRYING " ^ descr));
+ | tac::tactics ->
try
let res = PET.apply_tactic tac status in
- info (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!"));
+ info (lazy ("Tacticals.first: succedeed!!!"));
res
with
PET.Fail _ -> first ~tactics status
in
PET.mk_tactic (first ~tactics)
-
let rec do_tactic ~n ~tactic =
PET.mk_tactic
(function status ->
(* This tries tactics until one of them solves the goal *)
let solve_tactics ~tactics =
- let rec solve_tactics ~(tactics: (string * tactic) list) status =
+ let rec solve_tactics ~(tactics: tactic list) status =
info (lazy "in Tacticals.solve_tactics");
match tactics with
- | (descr, currenttactic)::moretactics ->
- info (lazy ("Tacticals.solve_tactics is trying " ^ descr));
+ | currenttactic::moretactics ->
(try
let (proof, opened) as output_status =
PET.apply_tactic currenttactic status
in
match opened with
- | [] -> info (lazy ("Tacticals.solve_tactics: " ^ descr ^
- " solved the goal!!!"));
+ | [] -> info (lazy ("Tacticals.solve_tactics: solved the goal!!!"));
output_status
| _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
raise (PET.Fail (lazy "Goal not solved"))
let progress_tactic ~tactic =
let msg = lazy "Failed to progress" in
- let progress_tactic (((_,metasenv,_,_,_),_) as istatus) =
- let ((_,metasenv',_,_,_),_) as ostatus =
+ let progress_tactic (((_,metasenv,_,_,_,_),g) as istatus) =
+ let ((_,metasenv',_,_,_,_),opened) as ostatus =
PET.apply_tactic tactic istatus
in
- (*CSC: Warning
- If just the index of some metas changes the tactic is recognized
- as a progressing one. This is wrong. *)
- if metasenv' = metasenv then
- raise (PET.Fail msg)
- else
- ostatus
+ match opened with
+ | [g1] ->
+ let _,oc,oldty = CicUtil.lookup_meta g metasenv in
+ let _,nc,newty = CicUtil.lookup_meta g1 metasenv' in
+ if oldty = newty && oc = nc then
+ raise (PET.Fail msg)
+ else
+ ostatus
+ | _ -> ostatus
in
PET.mk_tactic progress_tactic