diff options
| -rw-r--r-- | proofs/proofview.ml | 12 | ||||
| -rw-r--r-- | proofs/proofview.mli | 7 |
2 files changed, 19 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index c478bd6635..0f118a7c6d 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -210,6 +210,10 @@ let unfocus c sp = module Proof = Proofview_monad.Logical type +'a tactic = 'a Proof.t +type 'a case = +| Fail of exn +| Next of 'a * (exn -> 'a tactic) + (* Applies a tactic to the current proofview. *) let apply env t sp = let (((next_r,next_state),status)) = Proofview_monad.NonLogical.run (Proof.run t env sp) in @@ -247,6 +251,14 @@ let tclOR t1 t2 = (* [tclZERO e] always fails with error message [e]*) let tclZERO = Proof.zero +(* [tclCASE t] observes the head of the tactic and returns it as a value *) +let tclCASE t = + let map = function + | Nil e -> Fail e + | Cons (x, t) -> Next (x, t) + in + Proof.map map (Proof.split t) + (* [tclORELSE t1 t2] behaves like [t1] if [t1] succeeds at least once or [t2] if [t1] fails. *) let tclORELSE t1 t2 = diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 6a2d815114..affe276800 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -124,6 +124,10 @@ val unfocus : focus_context -> proofview -> proofview type +'a tactic +type 'a case = +| Fail of exn +| Next of 'a * (exn -> 'a tactic) + (* Applies a tactic to the current proofview. *) (* the return boolean signals the use of an unsafe tactic, in which case it is [false]. *) @@ -160,6 +164,9 @@ val tclZERO : exn -> 'a tactic or [t2 e] if [t1] fails with [e]. *) val tclORELSE : 'a tactic -> (exn -> 'a tactic) -> 'a tactic +(* [tclCASE t] observes the head of the tactic and returns it as a value *) +val tclCASE : 'a tactic -> 'a case tactic + (* [tclIFCATCH a s f] is a generalisation of [tclORELSE]: if [a] succeeds at least once then it behaves as [tclBIND a s] otherwise, if [a] fails with [e], then it behaves as [f e]. *) |