Implemented autorewrite with ... in hyp [using ...].

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

5 files changed, 79 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index 60828b0537..dfdcf600c8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -23,6 +23,10 @@ Ltac
 
 Tactics
 
+- New implementation and generalization of [setoid_]* (setoid_rewrite,
+  setoid_symmetry, setoid_transitivity, setoid_reflexivity and autorewite).
+  New syntax for declaring relations and morphisms (old syntax still working
+  with minor modifications, but deprecated) (doc TODO)
 - Added "clear - id" to clear all hypotheses except the ones depending in id.
 - Added "dependent rewrite term" and "dependent rewrite term in hyp" (doc TODO)
 - The argument of Declare Left Step and Declare Right Step is now a term
@@ -31,6 +35,8 @@ Tactics
 - Idtac can now be left implicit in a [...|...] construct: for instance, 
   [ foo | | bar ] stands for [ foo | idtac | bar ]. (doc TODO). 
 - "Tactic Notation" extended to allow notations of tacticals (doc TODO).
+- Added "autorewrite with ... in hyp [using ...]" (doc TODO).
+- 
 
 Modules
 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 0f1611a82b..b79e6c6085 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -60,7 +60,7 @@ let print_rewrite_hintdb bas =
 type raw_rew_rule = constr * bool * raw_tactic_expr
 
 (* Applies all the rules of one base *)
-let one_base tac_main bas =
+let one_base general_rewrite_maybe_in tac_main bas =
   let lrul = 
     try 
       Stringmap.find bas !rewtab
@@ -72,14 +72,56 @@ let one_base tac_main bas =
     tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) ->
       tclTHEN tac
         (tclREPEAT_MAIN 
-	  (tclTHENSFIRSTn (general_rewrite dir csr) [|tac_main|] tc)))
+	  (tclTHENSFIRSTn (general_rewrite_maybe_in dir csr) [|tac_main|] tc)))
       tclIDTAC lrul))
 
 (* The AutoRewrite tactic *)
 let autorewrite tac_main lbas =
   tclREPEAT_MAIN (tclPROGRESS
     (List.fold_left (fun tac bas -> 
-       tclTHEN tac (one_base tac_main bas)) tclIDTAC lbas))
+       tclTHEN tac (one_base general_rewrite tac_main bas)) tclIDTAC lbas))
+
+let autorewrite_in id tac_main lbas gl =
+ (* let's check at once if id exists (to raise the appropriate error) *)
+ let _ = Tacmach.pf_get_hyp gl id in
+ let general_rewrite_in =
+  let id = ref id in
+  let to_be_cleared = ref false in
+   fun dir cstr gl ->
+    let last_hyp_id =
+     match gl.Evd.it.Evd.evar_hyps with
+        (last_hyp_id,_,_)::_ -> last_hyp_id
+      | _ -> (* even the hypothesis id is missing *)
+             error ("No such hypothesis : " ^ (string_of_id !id))
+    in
+    let gl' = general_rewrite_in dir !id cstr gl in
+    let gls = (fst gl').Evd.it in
+    match gls with
+       g::_ ->
+        (match g.Evd.evar_hyps with
+            (lastid,_,_)::_ ->
+              if last_hyp_id <> lastid then
+               begin
+                let gl'' =
+                  if !to_be_cleared then
+                   tclTHEN (fun _ -> gl') (tclTRY (clear [!id])) gl
+                  else gl' in
+                id := lastid ;
+                to_be_cleared := true ;
+                gl''
+               end
+              else
+               begin
+                to_be_cleared := false ;
+                gl'
+               end
+          | _ -> assert false) (* there must be at least an hypothesis *)
+     | _ -> assert false (* rewriting cannot complete a proof *)
+ in
+  tclREPEAT_MAIN (tclPROGRESS
+    (List.fold_left (fun tac bas -> 
+       tclTHEN tac (one_base general_rewrite_in tac_main bas)) tclIDTAC lbas))
+   gl
 
 (* Functions necessary to the library object declaration *)
 let cache_hintrewrite (_,(rbase,lrl)) =
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 8b18f23f2c..cc4c5ed37b 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -20,5 +20,6 @@ val add_rew_rules : string -> raw_rew_rule list -> unit
 
 (* The AutoRewrite tactic *)
 val autorewrite : tactic -> string list -> tactic
+val autorewrite_in : Names.identifier -> tactic -> string list -> tactic
 
 val print_rewrite_hintdb : string -> unit
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 4068289eb9..06493804f7 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -123,12 +123,20 @@ TACTIC EXTEND AutorewriteV7
     [ autorewrite Refiner.tclIDTAC l ]
 | [ "AutoRewrite" "[" ne_preident_list(l) "]" "using" tactic(t) ] ->
     [ autorewrite (snd t) l ]
+| [ "AutoRewrite" "[" ne_preident_list(l) "]" "in" ident(id) ] ->
+    [ autorewrite_in id Refiner.tclIDTAC l ]
+| [ "AutoRewrite" "[" ne_preident_list(l) "]" "in" ident(id) "using" tactic(t) ] ->
+    [ autorewrite_in id (snd t) l ]
 END
 TACTIC EXTEND AutorewriteV8
   [ "AutoRewrite" "with" ne_preident_list(l) ] ->
     [ autorewrite Refiner.tclIDTAC l ]
 | [ "AutoRewrite" "with" ne_preident_list(l) "using" tactic(t) ] ->
     [ autorewrite (snd t) l ]
+| [ "AutoRewrite" "with" ne_preident_list(l) "in" ident(id) ] ->
+    [ autorewrite_in id Refiner.tclIDTAC l ]
+| [ "AutoRewrite" "with" ne_preident_list(l) "in" ident(id) "using" tactic(t) ] ->
+    [ autorewrite_in id (snd t) l ]
 END
 
 let add_rewrite_hint name ort t lcsr =
diff --git a/test-suite/success/autorewritein.v8 b/test-suite/success/autorewritein.v8
new file mode 100644
index 0000000000..3e218099a0
--- /dev/null
+++ b/test-suite/success/autorewritein.v8
@@ -0,0 +1,19 @@
+Variable Ack : nat -> nat -> nat.
+
+Axiom Ack0 : forall m : nat, Ack 0 m = S m.
+Axiom Ack1 : forall n : nat, Ack (S n) 0 = Ack n 1.
+Axiom Ack2 : forall n m : nat, Ack (S n) (S m) = Ack n (Ack (S n) m).
+
+Hint Rewrite Ack0 Ack1 Ack2 : base0.
+
+Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False.
+Proof.
+  intros.
+  autorewrite with base0 in H using try (apply H; reflexivity).
+Qed.
+
+Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), H=H -> False.
+Proof.
+  intros.
+  autorewrite with base0 in H using try (apply H1; reflexivity).
+Qed.