Rewrite autorewrite to use a dnet indexed by the left-hand sides (or

rhs) of rewrite lemmas for efficient retrieval of matching lemmas.
Autorewrite's implementation is still unchanged but the dnet can be used
through the [hints] strategy of the new generalized rewrite. Now lemmas
are checked to actually be rewriting lemmas at declaration time hence
the change in DoubleSqrt where some unapplicable constants were declared
as lemmas.


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

5 files changed, 174 insertions, 80 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 130f7e7fc5..d1dc8d2e8b 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -25,15 +25,45 @@ open Tacexpr
 open Mod_subst
 
 (* Rewriting rules *)
-(* the type is the statement of the lemma constr. Used to elim duplicates. *)
-type rew_rule = constr * types * bool * glob_tactic_expr
+type rew_rule = { rew_lemma: constr;
+		  rew_type: types;
+		  rew_pat: constr;
+		  rew_l2r: bool;
+		  rew_tac: glob_tactic_expr }
 
+let subst_hint subst hint =
+  let cst' = subst_mps subst hint.rew_lemma in
+  let typ' = subst_mps subst hint.rew_type in
+  let pat' = subst_mps subst hint.rew_pat in
+  let t' = Tacinterp.subst_tactic subst hint.rew_tac in
+    if hint.rew_lemma == cst' && hint.rew_tac == t' then hint else
+      { hint with 
+	rew_lemma = cst'; rew_type = typ'; 
+	rew_pat = pat';	rew_tac = t' }
 
+module HintIdent = 
+struct
+  type t = rew_rule
+  
+  let compare t t' =
+    Pervasives.compare t.rew_lemma t'.rew_lemma
 
+  let subst = subst_hint
+
+  let constr_of t = t.rew_pat
+end
+
+module HintOpt =
+struct
+  let reduce c = c
+  let direction = true
+end
+
+module HintDN = Term_dnet.Make(HintIdent)(HintOpt)
 
 (* Summary and Object declaration *)
 let rewtab =
-  ref (Stringmap.empty : rew_rule list Stringmap.t)
+  ref (Stringmap.empty : HintDN.t Stringmap.t)
 
 let _ = 
   let init () = rewtab := Stringmap.empty in
@@ -53,36 +83,37 @@ let find_base bas =
    errorlabstrm "AutoRewrite" 
      (str ("Rewriting base "^(bas)^" does not exist."))
 
+let find_rewrites bas = 
+  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
+
 let print_rewrite_hintdb bas =
   let hints = find_base bas in
     ppnl (str "Database " ++ str bas ++ (Pp.cut ()) ++
 	     prlist_with_sep Pp.cut
-	     (fun (c,typ,d,t) ->
-	       str (if d then "rewrite -> " else "rewrite <- ") ++
-		 Printer.pr_lconstr c ++ str " of type " ++ Printer.pr_lconstr typ ++
+	     (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()) t) hints)
+		 Pptactic.pr_glob_tactic (Global.env()) h.rew_tac)
+	     (HintDN.find_all hints))
       
-type raw_rew_rule = constr * bool * raw_tactic_expr
+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 =
-    try
-      Stringmap.find bas !rewtab
-    with Not_found ->
-      errorlabstrm "AutoRewrite"
-        (str ("Rewriting base "^(bas)^" does not exist."))
-  in
-  let lrul = List.map (fun (c,_,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrul in
+  let lrul = HintDN.find_all (find_base 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
         (tclREPEAT_MAIN 
 	  (tclTHENSFIRSTn (general_rewrite_maybe_in dir csr) [|tac_main|] tc)))
       tclIDTAC lrul))
 
-
-
 (* The AutoRewrite tactic *)
 let autorewrite tac_main lbas =
   tclREPEAT_MAIN (tclPROGRESS
@@ -180,38 +211,12 @@ let auto_multi_rewrite_with tac_main lbas cl gl =
 
 (* Functions necessary to the library object declaration *)
 let cache_hintrewrite (_,(rbase,lrl)) =
-  let l = 
-    try 
-      let oldl = Stringmap.find rbase !rewtab in
-      let lrl =
-       List.map
-        (fun (c,dummy,b,t) ->
-          (* here we substitute the dummy value with the right one *)
-          c,Typing.type_of (Global.env ()) Evd.empty c,b,t) lrl in
-      (List.filter
-          (fun (_,typ,_,_) ->
-            not (List.exists (fun (_,typ',_,_) -> Term.eq_constr typ typ') oldl)
-          ) lrl) @ oldl
-    with
-      | Not_found -> lrl
-  in
-    rewtab:=Stringmap.add rbase l !rewtab
+  rewtab:=Stringmap.add rbase lrl !rewtab
 
 let export_hintrewrite x = Some x
 
 let subst_hintrewrite (_,subst,(rbase,list as node)) = 
-  let subst_first (cst,typ,b,t as pair) = 
-    let cst' = subst_mps subst cst in
-    let typ' =
-     (* here we do not have the environment and Global.env () is not the
-        one where cst' lives in. Thus we can just put a dummy value and
-        override it in cache_hintrewrite *)
-     typ (* dummy value, it will be recomputed by cache_hintrewrite *) in
-    let t' = Tacinterp.subst_tactic subst t in
-      if cst == cst' && t == t' then pair else
-	(cst',typ',b,t')
-  in
-  let list' = list_smartmap subst_first list in
+  let list' = HintDN.subst subst list in
     if list' == list then node else
       (rbase,list')
       
@@ -221,18 +226,83 @@ let classify_hintrewrite (_,x) = Libobject.Substitute x
 (* Declaration of the Hint Rewrite library object *)
 let (inHintRewrite,_)=
   Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with
-       Libobject.cache_function = cache_hintrewrite;
-       Libobject.load_function = (fun _ -> cache_hintrewrite);
-       Libobject.subst_function = subst_hintrewrite;
-       Libobject.classify_function = classify_hintrewrite;
-       Libobject.export_function = export_hintrewrite }
+    Libobject.cache_function = cache_hintrewrite;
+    Libobject.load_function = (fun _ -> cache_hintrewrite);
+    Libobject.subst_function = subst_hintrewrite;
+    Libobject.classify_function = classify_hintrewrite;
+    Libobject.export_function = export_hintrewrite }
+
+
+open Clenv
 
+type hypinfo = {
+  hyp_cl : clausenv;
+  hyp_prf : constr;
+  hyp_ty : types;
+  hyp_car : constr;
+  hyp_rel : constr;
+  hyp_l2r : bool;
+  hyp_left : constr;
+  hyp_right : constr;
+}
+
+let evd_convertible env evd x y =
+  try ignore(Evarconv.the_conv_x env x y evd); true 
+  with _ -> false
+  
+let decompose_applied_relation metas env sigma c ctype left2right =
+  let find_rel ty = 
+    let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in
+    let eqclause = 
+      if metas then eqclause
+      else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
+    in
+    let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
+    let rec split_last_two = function
+      | [c1;c2] -> [],(c1, c2)
+      | x::y::z ->
+	  let l,res = split_last_two (y::z) in x::l, res
+      | _ -> raise Not_found
+    in
+      try 
+	let others,(c1,c2) = split_last_two args in
+	let ty1, ty2 = 
+	  Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2
+	in
+	  if not (evd_convertible env eqclause.evd ty1 ty2) then None
+	  else
+	    Some { hyp_cl=eqclause; hyp_prf=(Clenv.clenv_value eqclause); hyp_ty = ty;
+		   hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others);
+		   hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; }
+      with Not_found -> None
+  in
+    match find_rel ctype with
+    | Some c -> Some c
+    | None -> 
+	let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *)
+	match find_rel (it_mkProd_or_LetIn t' ctx) with
+	| Some c -> Some c
+	| None -> None
+
+let find_applied_relation metas loc env sigma c left2right =
+  let ctype = Typing.type_of env sigma c in
+    match decompose_applied_relation metas env sigma c ctype left2right with
+    | Some c -> c
+    | None -> 
+	user_err_loc (loc, "decompose_applied_relation", 
+		     str"The type" ++ spc () ++ Printer.pr_constr_env env ctype ++
+		       spc () ++ str"of this term does not end with an applied relation.")
+	
 (* To add rewriting rules to a base *)
 let add_rew_rules base lrul =
   let lrul =
-   List.rev_map
-    (fun (c,b,t) ->
-      (c,mkProp (* dummy value *), b,Tacinterp.glob_tactic t)
-    ) lrul
-  in
-   Lib.add_anonymous_leaf (inHintRewrite (base,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
+  in Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 632a281709..c8b3410dcb 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -15,7 +15,7 @@ open Tacmach
 (*i*)
 
 (* Rewriting rules before tactic interpretation *)
-type raw_rew_rule = Term.constr * bool * Tacexpr.raw_tactic_expr
+type raw_rew_rule = Util.loc * Term.constr * bool * Tacexpr.raw_tactic_expr
 
 (* To add rewriting rules to a base *)
 val add_rew_rules : string -> raw_rew_rule list -> unit
@@ -25,13 +25,37 @@ val autorewrite : tactic -> string list -> tactic
 val autorewrite_in : Names.identifier -> tactic -> string list -> tactic
 
 (* Rewriting rules *)
-(* the type is the statement of the lemma constr. Used to elim duplicates. *)
-type rew_rule = constr * types * bool * glob_tactic_expr
+type rew_rule = { rew_lemma: constr;
+		  rew_type: types;
+		  rew_pat: constr;
+		  rew_l2r: bool;
+		  rew_tac: glob_tactic_expr }
 
-val find_base : string -> rew_rule list
+val find_rewrites : string -> rew_rule list
+
+val find_matches : string -> constr -> rew_rule list
 
 val auto_multi_rewrite : string list -> Tacticals.clause -> tactic
 
 val auto_multi_rewrite_with : tactic -> string list -> Tacticals.clause -> tactic
 
 val print_rewrite_hintdb : string -> unit
+
+open Clenv
+
+
+type hypinfo = {
+  hyp_cl : clausenv;
+  hyp_prf : constr;
+  hyp_ty : types;
+  hyp_car : constr;
+  hyp_rel : constr;
+  hyp_l2r : bool;
+  hyp_left : constr;
+  hyp_right : constr;
+}
+
+val find_applied_relation : bool ->
+  Util.loc ->
+  Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo
+
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index d3aba06899..28e3888453 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -195,7 +195,7 @@ END
 
 let add_rewrite_hint name ort t lcsr =
   let env = Global.env() and sigma = Evd.empty in
-  let f c = Constrintern.interp_constr sigma env c, ort, t in
+  let f c = Topconstr.constr_loc c, Constrintern.interp_constr sigma env c, ort, t in
   add_rew_rules name (List.map f lcsr)
 
 VERNAC COMMAND EXTEND HintRewrite
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 1bbb2324f3..147e5384e2 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -242,7 +242,7 @@ let evd_convertible env evd x y =
   try ignore(Evarconv.the_conv_x env x y evd); true 
   with _ -> false
   
-let decompose_setoid_eqhyp env sigma c left2right =
+let decompose_applied_relation env sigma c left2right =
   let ctype = Typing.type_of env sigma c in
   let find_rel ty = 
     let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in
@@ -295,7 +295,7 @@ let refresh_hypinfo env sigma hypinfo =
       match c with 
 	| Some c ->
 	    (* Refresh the clausenv to not get the same meta twice in the goal. *)
-	    hypinfo := decompose_setoid_eqhyp env ( cl.evd) c l2r;
+	    hypinfo := decompose_applied_relation env ( cl.evd) c l2r;
 	| _ -> ()
   else ()
 
@@ -489,7 +489,7 @@ let apply_rule hypinfo loccs : strategy =
 let apply_lemma (evm,c) left2right loccs : strategy =
   fun env sigma ->
     let evars = Evd.merge sigma evm in
-    let hypinfo = ref (decompose_setoid_eqhyp env evars c left2right) in
+    let hypinfo = ref (decompose_applied_relation env evars c left2right) in
       apply_rule hypinfo loccs env sigma
 
 let subterm all flags (s : strategy) : strategy =
@@ -588,11 +588,6 @@ let subterm all flags (s : strategy) : strategy =
 let all_subterms = subterm true default_flags
 let one_subterm = subterm false default_flags
 
-let morphism_proof env evars carrier relation x =
-  let goal =
-    mkApp (Lazy.force morphism_proxy_type, [| carrier ; relation; x |])
-  in Evarutil.e_new_evar evars env goal
-
 (** Requires transitivity of the rewrite step, not tail-recursive. *)
 
 let transitivity env sigma (res : rewrite_result_info) (next : strategy) : rewrite_result option =
@@ -660,10 +655,10 @@ module Strategies =
       seq s (any s)
 
     let bu (s : strategy) : strategy = 
-      fix (fun s' -> choice (seq (all_subterms s') (try_ s')) s)
+      fix (fun s' -> seq (choice (all_subterms s') s) (try_ s'))
 
     let td (s : strategy) : strategy = 
-      fix (fun s' -> choice s (seq (all_subterms s') (try_ s')))
+      fix (fun s' -> seq (choice s (all_subterms s')) (try_ s'))
 
     let innermost (s : strategy) : strategy =
       fix (fun ins -> choice (one_subterm ins) s)
@@ -676,9 +671,15 @@ module Strategies =
 	choice tac (apply_lemma l l2r (false,[])))
 	fail cs
 	
+    let old_hints (db : string) : strategy =
+      let rules = Autorewrite.find_rewrites db in
+	lemmas (List.map (fun hint -> (inj_open hint.Autorewrite.rew_lemma, hint.Autorewrite.rew_l2r)) rules)
+
     let hints (db : string) : strategy =
-      let rules = Autorewrite.find_base db in
-	lemmas (List.map (fun (b,_,l2r,_) -> (inj_open b, l2r)) rules)
+      fun env sigma t ty cstr evars ->
+	let rules = Autorewrite.find_matches db t in
+	  lemmas (List.map (fun hint -> (inj_open hint.Autorewrite.rew_lemma, hint.Autorewrite.rew_l2r)) rules)
+	    env sigma t ty cstr evars
 
 end
 
@@ -693,7 +694,7 @@ let rewrite_strat flags occs hyp =
 let rewrite_with (evm,c) left2right loccs : strategy =
   fun env sigma ->
     let evars = Evd.merge sigma evm in
-    let hypinfo = ref (decompose_setoid_eqhyp env evars c left2right) in
+    let hypinfo = ref (decompose_applied_relation env evars c left2right) in
       rewrite_strat default_flags loccs hypinfo env sigma
 
 let apply_strategy (s : strategy) env sigma concl cstr evars =
@@ -854,6 +855,7 @@ ARGUMENT EXTEND rewstrategy TYPED AS strategy
   | [ rewstrategy(h) ";" rewstrategy(h') ] -> [ Strategies.seq h h' ]
   | [ "(" rewstrategy(h) ")" ] -> [ h ]
   | [ "choice" rewstrategy(h) rewstrategy(h') ] -> [ Strategies.choice h h' ]
+  | [ "old_hints" preident(h) ] -> [ Strategies.old_hints h ]
   | [ "hints" preident(h) ] -> [ Strategies.hints h ]
   | [ "terms" constr_list(h) ] -> [ fun env sigma -> Strategies.lemmas (interp_constr_list env sigma h) env sigma ]
 END
@@ -1263,7 +1265,7 @@ let unification_rewrite l2r c1 c2 cl car rel but gl =
     {cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)}
 
 let get_hyp gl evars (evm,c) clause l2r = 
-  let hi = decompose_setoid_eqhyp (pf_env gl) evars c l2r in
+  let hi = decompose_applied_relation (pf_env gl) evars c l2r in
   let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in
     unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl
 	
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index 00c7aeec65..c72abed619 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
@@ -269,10 +269,8 @@ Section DoubleSqrt.
  Let spec_ww_Bm1 : [[wwBm1]] = wwB - 1.
  Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);auto. Qed.
 
- 
- Hint Rewrite spec_w_0 spec_w_1 w_Bm1 spec_w_WW spec_w_sub 
-              spec_w_div21 spec_w_add_mul_div spec_ww_Bm1
-              spec_w_add_c spec_w_sqrt2: w_rewrite.
+ Hint Rewrite spec_w_0 spec_w_1 spec_w_WW spec_w_sub
+   spec_w_add_mul_div spec_ww_Bm1 spec_w_add_c : w_rewrite.
 
  Lemma spec_ww_is_even : forall x,
       if ww_is_even x then [[x]] mod 2 = 0 else [[x]] mod 2 = 1.