- Fix handling of clauses in setoid_rewrite to rewrite under binders

correctly.
- Fix the new autorewrite to implement the (unstated) invariant that the
last declared rules are applied first, which makes a difference for
non-confluent rewrite rules. Some scripts in CoLoR rely on that.


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

4 files changed, 47 insertions, 35 deletions

diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 656a90c70..4c6c5e631 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -367,6 +367,8 @@ struct
     possibly_under app_pat (search_pat pat (pat_of_constr pat)) dn init
 
   let find_all dn = Idset.elements (TDnet.find_all dn)
+
+  let map f dn = TDnet.map f (fun x -> x) dn
 end
     
 module type S =
@@ -385,4 +387,5 @@ sig
   val search_head_concl : t -> constr -> result list
   val search_eq_concl : t -> constr -> constr -> result list
   val find_all : t -> ident list
+  val map : (ident -> ident) -> t -> t
 end
diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli
index ccf962481..f6c1b5b61 100644
--- a/pretyping/term_dnet.mli
+++ b/pretyping/term_dnet.mli
@@ -102,6 +102,8 @@ sig
 
   (* [find_all dn] returns all idents contained in dn *)
   val find_all : t -> ident list
+
+  val map : (ident -> ident) -> t -> t
 end
 
 module Make :
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index d1dc8d2e8..2472c1274 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -43,14 +43,15 @@ let subst_hint subst hint =
 
 module HintIdent = 
 struct
-  type t = rew_rule
+  type t = int * rew_rule
   
-  let compare t t' =
-    Pervasives.compare t.rew_lemma t'.rew_lemma
+  let compare (i,t) (i',t') =
+    Pervasives.compare i i'
+(*     Pervasives.compare t.rew_lemma t'.rew_lemma *)
 
-  let subst = subst_hint
+  let subst s (i,t) = (i,subst_hint s t)
 
-  let constr_of t = t.rew_pat
+  let constr_of (i,t) = t.rew_pat
 end
 
 module HintOpt =
@@ -84,29 +85,28 @@ let find_base bas =
      (str ("Rewriting base "^(bas)^" does not exist."))
 
 let find_rewrites bas = 
-  HintDN.find_all (find_base bas)
+  List.rev_map snd (HintDN.find_all (find_base bas))
 
 let find_matches bas pat =
   let base = find_base bas in
   let res = HintDN.search_pattern base pat in
-    List.map (fun (rew, esubst, subst) -> rew) res
+    List.map (fun ((_,rew), esubst, subst) -> rew) res
 
 let print_rewrite_hintdb bas =
-  let hints = find_base bas in
-    ppnl (str "Database " ++ str bas ++ (Pp.cut ()) ++
-	     prlist_with_sep Pp.cut
-	     (fun h ->
-	       str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
-		 Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++
-		 str " then use tactic " ++ 
-		 Pptactic.pr_glob_tactic (Global.env()) h.rew_tac)
-	     (HintDN.find_all hints))
-      
+  ppnl (str "Database " ++ str bas ++ (Pp.cut ()) ++
+	   prlist_with_sep Pp.cut
+	   (fun h ->
+	     str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
+	       Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++
+	       str " then use tactic " ++ 
+	       Pptactic.pr_glob_tactic (Global.env()) h.rew_tac)
+	   (find_rewrites bas))
+    
 type raw_rew_rule = loc * constr * bool * raw_tactic_expr
 
 (* Applies all the rules of one base *)
 let one_base general_rewrite_maybe_in tac_main bas =
-  let lrul = HintDN.find_all (find_base bas) in
+  let lrul = find_rewrites bas in
   let lrul = List.map (fun h -> (h.rew_lemma,h.rew_l2r,Tacinterp.eval_tactic h.rew_tac)) lrul in
     tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) ->
       tclTHEN tac
@@ -208,10 +208,12 @@ let auto_multi_rewrite_with tac_main lbas cl gl =
 	    Util.errorlabstrm "autorewrite" 
 	      (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
 
-
 (* Functions necessary to the library object declaration *)
 let cache_hintrewrite (_,(rbase,lrl)) =
-  rewtab:=Stringmap.add rbase lrl !rewtab
+  let base = try find_base rbase with _ -> HintDN.empty in
+  let max = try fst (Util.list_last (HintDN.find_all base)) with _ -> 0 in
+  let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in
+    rewtab:=Stringmap.add rbase (HintDN.union lrl base) !rewtab
 
 let export_hintrewrite x = Some x
 
@@ -295,14 +297,16 @@ let find_applied_relation metas loc env sigma c left2right =
 	
 (* To add rewriting rules to a base *)
 let add_rew_rules base lrul =
+  let counter = ref 0 in
   let lrul =
-   List.fold_left
-     (fun dn (loc,c,b,t) ->
-       let info = find_applied_relation false loc (Global.env ()) Evd.empty c b in
-       let pat = if b then info.hyp_left else info.hyp_right in
-       let rul = { rew_lemma = c; rew_type = info.hyp_ty;
-		   rew_pat = pat; rew_l2r = b;
-		   rew_tac = Tacinterp.glob_tactic t}
-       in HintDN.add pat rul dn) 
-     (try find_base base with _ -> HintDN.empty) lrul
+    List.fold_left
+      (fun dn (loc,c,b,t) ->
+	let info = find_applied_relation false loc (Global.env ()) Evd.empty c b in
+	let pat = if b then info.hyp_left else info.hyp_right in
+	let rul = { rew_lemma = c; rew_type = info.hyp_ty;
+		    rew_pat = pat; rew_l2r = b;
+		    rew_tac = Tacinterp.glob_tactic t}
+	in incr counter;
+	  HintDN.add pat (!counter, rul) dn) HintDN.empty lrul
   in Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
+    
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 8efb0176e..df4851443 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -287,14 +287,14 @@ let convertible env evd x y =
 let allowK = true
 
 let refresh_hypinfo env sigma hypinfo = 
-  if !hypinfo.abs = None then
-    let {l2r=l2r; c = c;cl=cl} = !hypinfo in
+  if hypinfo.abs = None then
+    let {l2r=l2r; c=c;cl=cl} = hypinfo in
       match c with 
 	| Some c ->
 	    (* Refresh the clausenv to not get the same meta twice in the goal. *)
-	    hypinfo := decompose_applied_relation env ( cl.evd) c l2r;
-	| _ -> ()
-  else ()
+	    decompose_applied_relation env cl.evd c l2r;
+	| _ -> hypinfo
+  else hypinfo
 
 let unify_eqn env sigma hypinfo t = 
   if isEvar t then None
@@ -329,7 +329,7 @@ let unify_eqn env sigma hypinfo t =
 	      and ty2 = Typing.mtype_of env'.env env'.evd c2
 	      in
 		if convertible env env'.evd ty1 ty2 then (
-		  if occur_meta prf then refresh_hypinfo env sigma hypinfo;
+		  if occur_meta prf then hypinfo := refresh_hypinfo env sigma !hypinfo;
 		  env', prf, c1, c2, car, rel)
 		else raise Reduction.NotConvertible
     in
@@ -463,12 +463,15 @@ let apply_constraint env sigma car rel cstr res =
   | None -> res
   | Some r -> resolve_subrelation env sigma car rel r res
 
+let eq_env x y = x == y
+
 let apply_rule hypinfo loccs : strategy =
   let (nowhere_except_in,occs) = loccs in
   let is_occ occ = 
     if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in
   let occ = ref 0 in
     fun env sigma t ty cstr evars ->
+      if not (eq_env !hypinfo.cl.env env) then hypinfo := refresh_hypinfo env sigma !hypinfo;
       let unif = unify_eqn env sigma hypinfo t in
 	if unif <> None then incr occ;
 	match unif with