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

10 files changed, 45 insertions, 0 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 839294c0a1..0ddf58b74a 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -219,6 +219,8 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr =
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacOnce of
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
+  | TacExactlyOnce of
+      ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacOrelse of
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr *
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 033de89df3..d075a77904 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -67,6 +67,7 @@ GEXTEND Gram
       | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
       | IDENT "progress"; ta = tactic_expr -> TacProgress ta
       | IDENT "once"; ta = tactic_expr -> TacOnce ta
+      | IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta
       | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta
 (*To do: put Abstract in Refiner*)
       | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index f0d713be48..c5a8a380d6 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -895,6 +895,10 @@ let rec pr_tac inherited tac =
       (* arnaud: vérifier qu'il s'agit bien de la syntaxe définitive. *)
       hov 1 (str "once" ++ spc () ++ pr_tac (ltactical,E) t),
       ltactical
+  | TacExactlyOnce t ->
+      (* arnaud: vérifier qu'il s'agit bien de la syntaxe définitive. *)
+      hov 1 (str "exactly_once" ++ spc () ++ pr_tac (ltactical,E) t),
+      ltactical
   | TacOrelse (t1,t2) ->
       hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
              pr_tac (lorelse,E) t2),
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
 
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 2f41ff2aea..42ea649ecd 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -691,6 +691,8 @@ and intern_tactic_seq onlytac ist = function
       ist.ltacvars, TacOr (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2)
   | TacOnce tac ->
       ist.ltacvars, TacOnce (intern_pure_tactic ist tac)
+  | TacExactlyOnce tac ->
+      ist.ltacvars, TacExactlyOnce (intern_pure_tactic ist tac)
   | TacOrelse (tac1,tac2) ->
       ist.ltacvars, TacOrelse (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2)
   | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_pure_tactic ist) l)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2c64b669c5..edb9ab66d3 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1141,6 +1141,8 @@ and eval_tactic ist = function
       Tacticals.New.tclOR (interp_tactic ist tac1) (interp_tactic ist tac2)
   | TacOnce tac ->
       Tacticals.New.tclONCE (interp_tactic ist tac)
+  | TacExactlyOnce tac ->
+      Tacticals.New.tclEXACTLY_ONCE (interp_tactic ist tac)
   | TacOrelse (tac1,tac2) ->
       Tacticals.New.tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2)
   | TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l)
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 44327abef2..7c968865ac 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -251,6 +251,8 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
       TacOr (subst_tactic subst tac1,subst_tactic subst tac2)
   | TacOnce tac ->
       TacOnce (subst_tactic subst tac)
+  | TacExactlyOnce tac ->
+      TacExactlyOnce (subst_tactic subst tac)
   | TacOrelse (tac1,tac2) ->
       TacOrelse (subst_tactic subst tac1,subst_tactic subst tac2)
   | TacFirst l -> TacFirst (List.map (subst_tactic subst) l)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 1b8cf531bc..f25bae9bb8 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -400,6 +400,8 @@ module New = struct
 
   let tclONCE = Proofview.tclONCE
 
+  let tclEXACTLY_ONCE t = Proofview.tclEXACTLY_ONCE (Refiner.FailError(0,lazy (assert false))) t
+
   let tclORELSE0 t1 t2 =
     tclINDEPENDENT begin
       tclORELSE
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 722cb8b135..efeb4a7478 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -185,6 +185,7 @@ module New : sig
   val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic
   val tclOR : unit tactic -> unit tactic -> unit tactic
   val tclONCE : unit tactic -> unit tactic
+  val tclEXACTLY_ONCE : unit tactic -> unit tactic
   val tclORELSE0 : unit tactic -> unit tactic -> unit tactic
   val tclORELSE  : unit tactic -> unit tactic -> unit tactic