let id_tac =
let id_tac (proof,goal) =
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = 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, _subst, _ , _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
raise (PET.Fail (lazy "fail tactical"))
in
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
(HExtlib.list_concat ~sep:[ C.Semicolon ]
(List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
+let if_ ~start ~continuation ~fail =
+ S.mk_tactic
+ (fun istatus ->
+ let xostatus =
+ try
+ let res = C.eval (C.Tactical (C.Tactic start)) istatus in
+ info (lazy ("Tacticals.if_: succedeed!!!"));
+ Some res
+ with PET.Fail _ -> None
+ in
+ match xostatus with
+ | Some ostatus ->
+ let opened,closed = S.goals ostatus in
+ begin match opened with
+ | [] -> ostatus
+ | _ ->
+ fold_eval (S.focus ~-1 ostatus)
+ [ C.Semicolon; C.Tactical (C.Tactic continuation) ]
+ end
+ | None -> C.eval (C.Tactical (C.Tactic fail)) istatus
+ )
+
(* Tacticals that cannot be implemented on top of tynycals *)
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
(* 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,_subst,_,_,_),_) as istatus) =
+ let ((_,metasenv',_subst,_,_,_),_) as ostatus =
PET.apply_tactic tactic istatus
in
(*CSC: Warning