Adds a tactical once.

[once t] does just as [t] but has exactly one success it [t] has at least one success.

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

10 files changed, 29 insertions, 0 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index fece99312..839294c0a 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -217,6 +217,8 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr =
   | TacOr of
       ('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
   | 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 96f4bc387..033de89df 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -66,6 +66,7 @@ GEXTEND Gram
       | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta)
       | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
       | IDENT "progress"; ta = tactic_expr -> TacProgress ta
+      | IDENT "once"; ta = tactic_expr -> TacOnce 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 61f758df0..f0d713be4 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -891,6 +891,10 @@ let rec pr_tac inherited tac =
       hov 1 (pr_tac (lorelse,L) t1 ++ str " +" ++ brk (1,1) ++
              pr_tac (lorelse,E) t2),
       lorelse
+  | TacOnce t ->
+      (* arnaud: vérifier qu'il s'agit bien de la syntaxe définitive. *)
+      hov 1 (str "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 8a3511651..167fedf7b 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -244,6 +244,15 @@ let tclIFCATCH a s f =
     | Util.Inr e -> f e
     | Util.Inl (x,a') -> Proof.plus (s x) (fun e -> (a' e) >>= fun x' -> (s x'))
 
+(* [tclONCE t] fails if [t] fails, otherwise it has exactly one
+   success. *)
+let tclONCE t =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  Proof.split t >>= function
+    | Util.Inr e -> tclZERO e
+    | Util.Inl (x,_) -> tclUNIT x
+
 (* 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 207df891e..c9296e694 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -156,6 +156,10 @@ val tclORELSE : 'a tactic -> (exn -> 'a tactic) -> 'a tactic
    fails with [e], then it behaves as [f e]. *)
 val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (exn -> 'b tactic) -> 'b tactic
 
+(* [tclONCE t] fails if [t] fails, otherwise it has exactly one
+   success. *)
+val tclONCE : '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 ddabb5d08..2f41ff2ae 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -689,6 +689,8 @@ and intern_tactic_seq onlytac ist = function
       ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic onlytac ist tac)
   | TacOr (tac1,tac2) ->
       ist.ltacvars, TacOr (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2)
+  | TacOnce tac ->
+      ist.ltacvars, TacOnce (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 2bf3c8e06..34ea3dc87 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1139,6 +1139,8 @@ and eval_tactic ist = function
   | TacRepeat tac -> Tacticals.New.tclREPEAT (interp_tactic ist tac)
   | TacOr (tac1,tac2) ->
       Tacticals.New.tclOR (interp_tactic ist tac1) (interp_tactic ist tac2)
+  | TacOnce tac ->
+      Tacticals.New.tclONCE (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 ba37c1019..44327abef 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -249,6 +249,8 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
   | TacRepeat tac -> TacRepeat (subst_tactic subst tac)
   | TacOr (tac1,tac2) ->
       TacOr (subst_tactic subst tac1,subst_tactic subst tac2)
+  | TacOnce tac ->
+      TacOnce (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 574e4c9a9..2131dc480 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -398,6 +398,8 @@ module New = struct
         end
     end
 
+  let tclONCE = Proofview.tclONCE
+
   let tclORELSE0 t1 t2 =
     tclINDEPENDENT begin
       tclORELSE
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index f7ba178a3..722cb8b13 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -184,6 +184,7 @@ module New : sig
      THIS MODULE. *)
   val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic
   val tclOR : unit tactic -> unit tactic -> unit tactic
+  val tclONCE : unit tactic -> unit tactic
   val tclORELSE0 : unit tactic -> unit tactic -> unit tactic
   val tclORELSE  : unit tactic -> unit tactic -> unit tactic