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

3 files changed, 20 insertions, 9 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 677039015..b6c3acfac 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 772f9cdc8..475304fb6 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 effd6f9af..8de4fcd10 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)