Extension syntaxique de rewrite in: au lieu de pouvoir faire

juste rewrite in <id>, on a maintenant rewrite in <clause>. 

Ainsi rewrite H in H1,H2 |- * === rewrite H in H1; rewrite H in H2; rewrite H

Pour l'instant rewrite H in * |- signifie: faire une fois 
"try rewrite H in Hi" sur toutes les hypotheses Hi du contexte sauf H
En particulier, n'echoue pour l'instant pas s'il n'y a rien a 
reecrire nulle part. 

NB: rewrite H in * === rewrite H in * |- * === rewrite H in * |- ; rewrite H

ATTENTION: la syntaxe de rewrite ayant changé, j'adapte interface en conséquence. 
 Est-ce la bonne facon de faire ? 




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

12 files changed, 72 insertions, 21 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index fb71288a97..8f880a767e 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -685,8 +685,8 @@ and ct_TACTIC_COM =
   | CT_rename of ct_ID * ct_ID
   | CT_repeat of ct_TACTIC_COM
   | CT_replace_with of ct_FORMULA * ct_FORMULA * ct_ID_OPT * ct_TACTIC_OPT
-  | CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT
-  | CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT
+  | CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_CLAUSE
+  | CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_CLAUSE
   | CT_right of ct_SPEC_LIST
   | CT_ring of ct_FORMULA_LIST
   | CT_simple_user_tac of ct_ID * ct_TACTIC_ARG_LIST
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 5a7ccc26b1..064d20abd4 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -1717,12 +1717,12 @@ and fTACTIC_COM = function
 | CT_rewrite_lr(x1, x2, x3) ->
    fFORMULA x1;
    fSPEC_LIST x2;
-   fID_OPT x3;
+   fCLAUSE x3;
    fNODE "rewrite_lr" 3
 | CT_rewrite_rl(x1, x2, x3) ->
    fFORMULA x1;
    fSPEC_LIST x2;
-   fID_OPT x3;
+   fCLAUSE x3;
    fNODE "rewrite_rl" 3
 | CT_right(x1) ->
    fSPEC_LIST x1;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 21138c85e4..b9cd78e0b2 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -978,19 +978,12 @@ and xlate_tac =
 		CT_coerce_TACTIC_COM_to_TACTIC_OPT tac
 	in 
 	CT_replace_with (c1, c2,id_opt,tac_opt)
-    | TacExtend (_,"rewrite", [b; cbindl]) ->
-     let b = out_gen Extraargs.rawwit_orient b in
-     let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
-     let c = xlate_formula c and bindl = xlate_bindings bindl in
-     if b then CT_rewrite_lr (c, bindl, ctv_ID_OPT_NONE)
-     else CT_rewrite_rl (c, bindl, ctv_ID_OPT_NONE)
-    | TacExtend (_,"rewrite_in", [b; cbindl; id]) ->
-     let b = out_gen Extraargs.rawwit_orient b in
-     let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
-     let c = xlate_formula c and bindl = xlate_bindings bindl in
-     let id = ctf_ID_OPT_SOME (xlate_ident (snd (out_gen rawwit_var id))) in
-     if b then CT_rewrite_lr (c, bindl, id)
-     else CT_rewrite_rl (c, bindl, id)
+    | TacRewrite(b,cbindl,cl) -> 
+     let cl = xlate_clause cl 
+     and c = xlate_formula (fst cbindl) 
+     and bindl = xlate_bindings (snd cbindl) in
+     if b then CT_rewrite_lr (c, bindl, cl)
+     else CT_rewrite_rl (c, bindl, cl)
     | TacExtend (_,"conditional_rewrite", [t; b; cbindl]) ->
      let t = out_gen rawwit_main_tactic t in
      let b = out_gen Extraargs.rawwit_orient b in
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 5c847f5a48..d87336b816 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -261,6 +261,11 @@ GEXTEND Gram
     [ [ "in"; idl = LIST1 id_or_meta -> idl
       | -> [] ] ]
   ;
+  orient: 
+    [ [ "->" -> true 
+      | "<-" -> false
+      | -> true ]]
+  ; 
   fixdecl:
     [ [ "("; id = ident; bl=LIST0 Constr.binder; ann=fixannot;
         ":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ]
@@ -411,6 +416,8 @@ GEXTEND Gram
       | IDENT "transitivity"; c = constr -> TacTransitivity c
 
       (* Equality and inversion *)
+      | IDENT "rewrite"; b = orient; c = constr_with_bindings ; cl = clause -> 
+	  TacRewrite (b,c,cl)
       | IDENT "dependent"; k =
 	  [ IDENT "simple"; IDENT "inversion" -> SimpleInversion
 	  | IDENT "inversion" -> FullInversion
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 76054c5996..f1388ab69c 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -418,6 +418,8 @@ let pr_clause_pattern pr_id = function
 	  ++ spc () ++ pr_id id) l ++
         pr_opt (fun nl -> prlist_with_sep spc int nl ++ str " Goal") glopt
 
+let pr_orient b = if b then mt () else str " <-"
+
 let pr_induction_arg prc = function
   | ElimOnConstr c -> prc c
   | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
@@ -787,6 +789,9 @@ and pr_atom1 env = function
   | TacTransitivity c -> str "transitivity" ++ pr_constrarg env c
 
   (* Equality and inversion *)
+  | TacRewrite (b,c,cl) -> 
+      hov 1 (str "rewrite" ++ pr_orient b ++ spc() ++ pr_with_bindings env c ++ 
+             pr_clauses pr_ident cl) 
   | TacInversion (DepInversion (k,c,ids),hyp) ->
       hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
       pr_quantified_hypothesis hyp ++
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index ea7c49f2bc..89060f9ccc 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -184,6 +184,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacTransitivity of 'constr 
 
   (* Equality and inversion *)
+  | TacRewrite of bool * 'constr with_bindings * 'id gclause
   | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
       
   (* For ML extensions *)
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 8a1c4e16a2..8aef9c50b2 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -103,7 +103,7 @@ let mkGenDecideEqGoal rectype g =
 
 let eqCase tac = 
   (tclTHEN intro  
-  (tclTHEN (tclLAST_HYP Extratactics.h_rewriteLR)
+  (tclTHEN (tclLAST_HYP Equality.rewriteLR)
   (tclTHEN clear_last 
   tac)))
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ddeed16d5b..1316e8aab7 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -119,6 +119,37 @@ let general_rewrite_bindings_in l2r id =
 let general_rewrite_in l2r id c = 
   general_rewrite_bindings_clause (Some id) l2r (c,NoBindings)
 
+
+let general_multi_rewrite l2r c cl = 
+  let rec do_hyps = function 
+    | [] -> tclIDTAC
+    | (id,_,_) :: l -> 
+	tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l)
+  in 
+  let rec try_do_hyps = function 
+    | [] -> tclIDTAC 
+    | id :: l -> 
+	tclTHENFIRST 
+	  (tclTRY (general_rewrite_bindings_in l2r id c)) 
+	  (try_do_hyps l)
+  in 
+  if cl.concl_occs <> [] then 
+    error "The \"at\" syntax isn't available yet for the rewrite tactic"
+  else 
+    tclTHENFIRST 
+      (if cl.onconcl then general_rewrite_bindings l2r c else tclIDTAC)
+      (match cl.onhyps with 
+	 | Some l -> do_hyps l
+	 | None -> 
+	     fun gl -> 
+	       (* try to rewrite in all hypothesis 
+		  (except maybe the rewritten one) *)
+	       let ids = match kind_of_term (fst c) with 
+		 | Var id -> list_remove id (pf_ids_of_hyps gl)
+		 | _ -> pf_ids_of_hyps gl
+	       in try_do_hyps ids gl)
+
+
 (* 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 7632fd36bd..12f9becbe8 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -43,6 +43,9 @@ val general_rewrite_bindings_in :
 val general_rewrite_in          :
   bool -> identifier -> constr -> tactic
 
+val general_multi_rewrite : 
+  bool -> constr with_bindings -> clause -> tactic
+
 val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic
 val conditional_rewrite_in :
   bool -> identifier -> tactic -> constr with_bindings -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 1c0e04276e..11bb71ca8c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -20,6 +20,9 @@ open Names
 (* Equality *)
 open Equality
 
+(* Pierre L: for an easy implementation of "rewrite ... in <clause>", rewrite
+  has moved to g_tactics.ml4
+
 TACTIC EXTEND rewrite
 | [ "rewrite" orient(b) constr_with_bindings(c) ] ->
     [general_rewrite_bindings b c]
@@ -30,7 +33,8 @@ TACTIC EXTEND rewrite_in
     [general_rewrite_bindings_in b h c]
 END
 
-let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings)
+let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings) 
+*)
 
 (* Julien: Mise en commun des differentes version de replace with in by 
    TODO: améliorer l'affichage et deplacer dans extraargs
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 0e47cf4f37..c9252d4e3a 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -15,7 +15,6 @@ open Rawterm
 
 val h_discrHyp : quantified_hypothesis -> tactic
 val h_injHyp : quantified_hypothesis -> tactic
-val h_rewriteLR : constr -> tactic
 
 val refine_tac : Genarg.open_constr -> tactic
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 56aaee4feb..ed9a4ecf8f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -720,6 +720,9 @@ let rec intern_atomic lf ist x =
   | TacTransitivity c -> TacTransitivity (intern_constr ist c)
 
   (* Equality and inversion *)
+  | TacRewrite (b,c,cl) -> 
+      TacRewrite (b,intern_constr_with_bindings ist c,
+		  clause_app (intern_hyp_location ist) cl)
   | TacInversion (inv,hyp) ->
       TacInversion (intern_inversion_strength lf ist inv,
         intern_quantified_hypothesis ist hyp)
@@ -1568,7 +1571,7 @@ and interp_match_context ist g lz lr lmr =
            db_matched_concl ist.debug (pf_env goal) concl;
            apply_hyps_context ist env lz goal mt [] lgoal mhyps hyps
         with e when is_match_catchable e ->
-          (match e with
+         (match e with
             | PatternMatchingFailure -> db_matching_failure ist.debug
             | Eval_fail s -> db_eval_failure ist.debug s
             | _ -> db_logic_failure ist.debug e);
@@ -1828,6 +1831,10 @@ and interp_atomic ist gl = function
   | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c)
 
   (* Equality and inversion *)
+  | TacRewrite (b,c,cl) -> 
+      Equality.general_multi_rewrite b 
+	(interp_constr_with_bindings ist gl c) 
+	(interp_clause ist gl cl)
   | TacInversion (DepInversion (k,c,ids),hyp) ->
       Inv.dinv k (option_map (pf_interp_constr ist gl) c)
         (interp_intro_pattern ist ids)
@@ -2073,6 +2080,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c)
 
   (* Equality and inversion *)
+  | TacRewrite (b,c,cl) -> TacRewrite (b, subst_raw_with_bindings subst c,cl)
   | TacInversion (DepInversion (k,c,l),hyp) ->
      TacInversion (DepInversion (k,option_map (subst_rawconstr subst) c,l),hyp)
   | TacInversion (NonDepInversion _,_) as x -> x