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
(* 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: tactic list) status =
info (lazy "in Tacticals.first");
in
PET.mk_tactic (first ~tactics)
-
let rec do_tactic ~n ~tactic =
PET.mk_tactic
(function status ->