Adds an experimental exactly_once tactical.

exactly_once t, will have a success if t has exactly once success.

There are a few caveats:
- The underlying effects of t may happen in an unpredictable order (hence it may be wise to use it only with "pure" tactics)
- The second success of a tactic is conditional on the exception thrown. In Ltac it doesn't show, but in the underlying code, the tactical also expects the exception you want to use to produce the second success.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17009 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 29 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 823082aced..bb1d5758d6 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -253,6 +253,28 @@ let tclONCE t =
     | Nil e -> tclZERO e
     | Cons (x,_) -> tclUNIT x
 
+exception MoreThanOneSuccess
+let _ = Errors.register_handler begin function
+  | MoreThanOneSuccess -> Errors.error "This tactic has more than one success."
+  | _ -> raise Errors.Unhandled
+end
+
+(* [tclONCE e t] succeeds as [t] if [t] has exactly one
+   success. Otherwise it fails.  It may behave differently than [t] as
+   there may be extra non-logical effects used to discover that [t]
+   does not have a second success. Moreover the second success may be
+   conditional on the error recieved: [e] is used. *)
+let tclEXACTLY_ONCE e t =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  Proof.split t >>= function
+    | Nil e -> tclZERO e
+    | Cons (x,k) ->
+        Proof.split (k e) >>= function
+          | Nil _ -> tclUNIT x
+          | _ -> tclZERO MoreThanOneSuccess
+
+
 (* Focuses a tactic at a range of subgoals, found by their indices. *)
 (* arnaud: bug if 0 goals ! *)
 let tclFOCUS i j t =
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 0504efea57..5b25c003d6 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -160,6 +160,13 @@ val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (exn -> 'b tactic) -> 'b tact
    success. *)
 val tclONCE : 'a tactic -> 'a tactic
 
+(* [tclONCE e t] succeeds as [t] if [t] has exactly one
+   success. Otherwise it fails.  It may behave differently than [t] as
+   there may be extra non-logical effects used to discover that [t]
+   does not have a second success. Moreover the second success may be
+   conditional on the error recieved: [e] is used. *)
+val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic
+
 (* Focuses a tactic at a range of subgoals, found by their indices. *)
 val tclFOCUS : int -> int -> 'a tactic -> 'a tactic