Rework on rich forms of rewrite

 1) changed the semantics of rewrite H,H' : the earlier semantics 
    (rewrite H,H' == rewrite H; rewrite H') was poorly suited for 
    situations where first rewrite H generates side-conditions. 
    New semantics is tclTHENFIRST instead of tclTHEN, that is
    side-conditions are left untouched. 

    Note to myself: check if side-effect-come-first bug of 
    setoid rewrite is still alive, and do something if yes

 2) new syntax for rewriting something many times. This syntax is 
    shamelessly taken from ssreflect: 

    rewrite ?H  means "H as many times as possible" 
      (i.e. almost repeat rewrite H, except that 
       possible side-conditions are left apart as in 1)
    rewrite !H  means "at least once" (i.e. rewrite H; repeat rewrite H)
    rewrite 3?H means "up to 3 times", maybe less 
      (i.e. something like: do 3 (try rewrite H)).
    rewrite 3!H means "exactly 3 times" (i.e. almost do 3 rewrite H).

    For instance:  rewrite 3?foo, <-2!bar in H1,H2|-*

 3) By the way, for a try, I've enabled the syntax +/- as synonyms for 
    ->/<- in the orientation of rewrite. 
   
   Comments welcome ...




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

9 files changed, 89 insertions, 35 deletions

diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index 1becbbb94a..77d405e15d 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -363,7 +363,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     | TacTransitivity c -> depends_of_'constr c acc
 
     (* Equality and inversion *)
-    | TacRewrite (_,cbl,_) -> list_union_map (o depends_of_'constr_with_bindings snd) cbl acc
+    | TacRewrite (_,cbl,_) -> list_union_map (o depends_of_'constr_with_bindings (fun (_,_,x)->x)) cbl acc
     | TacInversion (is, _)  -> depends_of_'a_'b_inversion_strength depends_of_'constr is acc
 
     (* For ML extensions *)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 0fbfa39b72..db8963554b 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1011,7 +1011,7 @@ and xlate_tac =
 		CT_coerce_TACTIC_COM_to_TACTIC_OPT tac
 	in 
 	CT_replace_with (c1, c2,cl,tac_opt)
-    | TacRewrite(false,[b,cbindl],cl) -> 
+    | TacRewrite(false,[b,Precisely 1,cbindl],cl) -> 
      let cl = xlate_clause cl 
      and c = xlate_formula (fst cbindl) 
      and bindl = xlate_bindings (snd cbindl) in
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a58125dc09..6a794e9eb3 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1756,7 +1756,7 @@ implicit type of $t$ and $u$.
 This tactic applies to any goal. The type of {\term}
 must have the form
 
-\texttt{(x$_1$:A$_1$) \dots\ (x$_n$:A$_n$)}\texttt{eq}\term$_1$ \term$_2$. 
+\texttt{(x$_1$:A$_1$) \dots\ (x$_n$:A$_n$)}\texttt{eq} \term$_1$ \term$_2$. 
 
 \noindent where \texttt{eq} is the Leibniz equality or a registered
 setoid equality.
@@ -1781,9 +1781,11 @@ This happens if \term$_1$ does not occur in the goal.
 
 \begin{Variants}
 \item {\tt rewrite -> {\term}}\tacindex{rewrite ->}\\
+  {\tt rewrite +{\term}}\tacindex{rewrite +}\\
   Is equivalent to {\tt rewrite \term}
 
 \item {\tt rewrite <- {\term}}\tacindex{rewrite <-}\\
+  {\tt rewrite -{\term}}\tacindex{rewrite -}\\
   Uses the equality \term$_1${\tt=}\term$_2$ from right to left
 
 \item {\tt rewrite {\term} in \textit{clause}}
@@ -1804,24 +1806,32 @@ This happens if \term$_1$ does not occur in the goal.
     and \texttt{rewrite H in * |-} that succeeds if at
     least one of these two tactics succeeds. 
   \end{itemize}
-
-\item {\tt rewrite -> {\term} in \textit{clause}}
-  \tacindex{rewrite -> \dots\ in}\\
-  Behaves as {\tt rewrite {\term} in \textit{clause}}.
- 
-\item {\tt rewrite <- {\term} in \textit{clause}}\\
-  \tacindex{rewrite <- \dots\ in}
-  Uses the equality \term$_1${\tt=}\term$_2$ from right to left to
-  rewrite in \textit{clause} as explained above.
+  Orientation {\tt ->} or {\tt <-} (or {\tt +} or {\tt -}) can be
+  inserted before the term to rewrite.
 
 \item {\tt rewrite $\term_1$, \ldots, $term_n$}\\
-  Is equivalent to {\tt rewrite $\term_1$; \ldots; rewrite $\term_n$}.
-  Orientation {\tt ->} or {\tt <-} can be inserted before each term. 
-  
-\item {\tt rewrite $\term_1$, \ldots, $term_n$ in \textit{clause}}\\
-  Is equivalent to {\tt rewrite $\term_1$ in \textit{clause}; \ldots; 
-  rewrite $\term_n$ in \textit{clause}}.
-  Orientation {\tt ->} or {\tt <-} can be inserted before each term. 
+  Is equivalent to the $n$ successive tactics {\tt rewrite $\term_1$}
+  up to {\tt rewrite $\term_n$}, each one working on the first subgoal
+  generated by the previous one.
+  Orientation {\tt ->} or {\tt <-} (or {\tt +} or {\tt -}) can be
+  inserted before each term to rewrite. One unique \textit{clause}
+  can be added at the end after the keyword {\tt in}, it will 
+  then affect all rewrite operations.
+
+\item In all forms of {\tt rewrite} described above, a term to rewrite
+  can be immediately prefixed by one of the following modifiers:
+  \begin{itemize}
+  \item {\tt ?} : the tactic {\tt rewrite ?$\term$} performs the
+    rewrite of $\term$  as many times as possible (perhaps zero time).
+    This form never fails. 
+  \item {\tt $n$?} : works similarly, except that it will do at most 
+   $n$ rewrites. 
+  \item {\tt !} : works as {\tt ?}, except that at least one rewrite 
+    should succeed, otherwise the tactic fails. 
+  \item {\tt $n$!} : precisely $n$ rewrites of $\term$ will be done, 
+    leading to failure if these $n$ rewrites are not possible. 
+  \end{itemize}
+
 
 \end{Variants}
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index f305ebd69e..724bb2da1b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -288,8 +288,10 @@ GEXTEND Gram
   orient: 
     [ [ "->" -> true 
       | "<-" -> false
+      | "+" -> true
+      | "-" -> false
       | -> true ]]
-  ; 
+  ;
   fixdecl:
     [ [ "("; id = ident; bl=LIST0 Constr.binder; ann=fixannot;
         ":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ]
@@ -319,9 +321,25 @@ GEXTEND Gram
   ;
   rename : 
     [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ]
-  ; 
+  ;
   rewriter : 
-    [ [ b = orient; c = constr_with_bindings -> (b,c) ] ]
+    [ [ c = constr_with_bindings -> (Precisely 1, c)
+      | "!"; c = constr_with_bindings -> (RepeatPlus,c)
+      |	"?"; c = constr_with_bindings -> (RepeatStar,c)
+      | n = natural; "!"; c = constr_with_bindings -> (Precisely n,c)
+      |	n = natural; "?"; c = constr_with_bindings -> (UpTo n,c)
+    (* hack for allowing "rewrite ?t" and "rewrite NN?t" that normally 
+       produce a pattern_ident *)
+      | c = pattern_ident -> 
+	  let c = (CRef (Libnames.Ident (dummy_loc,c)), NoBindings) in  
+	  (RepeatStar, c)
+      | n = natural; c = pattern_ident -> 
+	  let c = (CRef (Libnames.Ident (dummy_loc,c)), NoBindings) in  
+	  (UpTo n, c)
+      ] ]
+  ;
+  oriented_rewriter : 
+    [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ]
   ; 
   simple_tactic:
     [ [ 
@@ -451,9 +469,9 @@ GEXTEND Gram
       | IDENT "transitivity"; c = constr -> TacTransitivity c
 
       (* Equality and inversion *)
-      | IDENT "rewrite"; l = LIST1 rewriter SEP ","; cl = clause -> 
+      | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause ->
 	  TacRewrite (false,l,cl)
-      | IDENT "erewrite"; l = LIST1 rewriter SEP ","; cl = clause ->
+      | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause ->
 	  TacRewrite (true,l,cl)
       | IDENT "dependent"; k =
 	  [ IDENT "simple"; IDENT "inversion" -> SimpleInversion
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 67858b3c60..da915a5cc3 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -428,6 +428,13 @@ let pr_clause_pattern pr_id = function
 
 let pr_orient b = if b then mt () else str " <-"
 
+let pr_multi = function 
+  | Precisely 1 -> mt ()
+  | Precisely n -> pr_int n ++ str "!"
+  | UpTo n -> pr_int n ++ str "?"
+  | RepeatStar -> str "?"
+  | RepeatPlus -> str "!"
+
 let pr_induction_arg prlc prc = function
   | ElimOnConstr c -> pr_with_bindings prlc prc c
   | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
@@ -818,7 +825,8 @@ and pr_atom1 = function
       hov 1 (str (if ev then "erewrite" else "rewrite") ++ 
 	     prlist_with_sep
 	     (fun () -> str ","++spc())
-	     (fun (b,c) -> pr_orient b ++ spc() ++ pr_with_bindings c)
+	     (fun (b,m,c) -> 
+		pr_orient b ++ spc() ++ pr_multi m ++ pr_with_bindings c)
 	     l
 	     ++ pr_clauses pr_ident cl) 
   | TacInversion (DepInversion (k,c,ids),hyp) ->
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 09d5c05165..a63fd1aebb 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -99,6 +99,12 @@ let simple_clause_of = function
   | { onhyps = Some []; onconcl = true; concl_occs=[] } -> None
   | _ -> error "not a simple clause (one hypothesis or conclusion)"
 
+type multi = 
+  | Precisely of int
+  | UpTo of int
+  | RepeatStar
+  | RepeatPlus
+
 type pattern_expr = constr_expr
 
 (* Type of patterns *)
@@ -187,7 +193,8 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacTransitivity of 'constr 
 
   (* Equality and inversion *)
-  | TacRewrite of evars_flag * (bool * 'constr with_bindings) list * 'id gclause
+  | TacRewrite of 
+      evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause
   | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
       
   (* For ML extensions *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6770390152..b6c3acface 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -166,11 +166,21 @@ let general_multi_rewrite l2r with_evars c cl =
 	      (general_rewrite_ebindings l2r c with_evars)
 	      do_hyps
 
-let rec general_multi_multi_rewrite with_evars l cl = match l with 
-  | [] -> tclIDTAC
-  | (l2r,c)::l -> 
-      tclTHEN (general_multi_rewrite l2r with_evars c cl)
-	(general_multi_multi_rewrite with_evars l cl)
+let general_multi_multi_rewrite with_evars l cl = 
+  let do1 l2r c = general_multi_rewrite l2r with_evars c cl in
+  let rec doN l2r c = function 
+    | Precisely n when n <= 0 -> tclIDTAC
+    | Precisely 1 -> do1 l2r c
+    | Precisely n -> tclTHENFIRST (do1 l2r c) (doN l2r c (Precisely (n-1)))
+    | RepeatStar -> tclREPEAT_MAIN (do1 l2r c)
+    | RepeatPlus -> tclTHENFIRST (do1 l2r c) (doN l2r c RepeatStar)
+    | UpTo n when n<=0 -> tclIDTAC
+    | UpTo n -> tclTHENFIRST (tclTRY (do1 l2r c)) (doN l2r c (UpTo (n-1)))
+  in 
+  let rec loop = function
+    | [] -> tclIDTAC
+    | (l2r,m,c)::l -> tclTHENFIRST (doN l2r c m) (loop l)
+  in loop l
 
 (* Conditional rewriting, the success of a rewriting is related 
    to the resolution of the conditions by a given tactic *)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 772f9cdc8e..475304fb6c 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -49,7 +49,7 @@ val general_rewrite_in          :
 val general_multi_rewrite : 
   bool -> evars_flag -> constr with_ebindings -> clause -> tactic
 val general_multi_multi_rewrite : 
-  evars_flag -> (bool * constr with_ebindings) list -> clause -> tactic
+  evars_flag -> (bool * multi * constr with_ebindings) list -> clause -> tactic
 
 val conditional_rewrite : bool -> tactic -> constr with_ebindings -> tactic
 val conditional_rewrite_in :
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index effd6f9afb..8de4fcd10b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -745,7 +745,7 @@ let rec intern_atomic lf ist x =
   | TacRewrite (ev,l,cl) -> 
       TacRewrite 
 	(ev, 
-	 List.map (fun (b,c) -> (b,intern_constr_with_bindings ist c)) l,
+	 List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings ist c)) l,
 	 clause_app (intern_hyp_location ist) cl)
   | TacInversion (inv,hyp) ->
       TacInversion (intern_inversion_strength lf ist inv,
@@ -2107,7 +2107,7 @@ and interp_atomic ist gl = function
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl) -> 
       Equality.general_multi_multi_rewrite ev
-	(List.map (fun (b,c) -> (b, interp_constr_with_bindings ist gl c)) l)
+	(List.map (fun (b,m,c) -> (b,m,interp_constr_with_bindings ist gl c)) l)
 	(interp_clause ist gl cl)
   | TacInversion (DepInversion (k,c,ids),hyp) ->
       Inv.dinv k (Option.map (pf_interp_constr ist gl) c)
@@ -2405,7 +2405,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl) -> 
       TacRewrite (ev, 
-		  List.map (fun (b,c) ->b,subst_raw_with_bindings subst c) l,
+		  List.map (fun (b,m,c) ->
+			      b,m,subst_raw_with_bindings subst c) l,
 		  cl)
   | TacInversion (DepInversion (k,c,l),hyp) ->
      TacInversion (DepInversion (k,Option.map (subst_rawconstr subst) c,l),hyp)