Fixes in typeclasses resolution. Avoid reducing instances types before

making the auto apply entry. Makes indexing better and avoid polution of
[auto with *] with many abstract lemmas comming from [typeclass_instances]. 
Quite a nice speedup again, even Field_theory has dropped to 58s from
70s.


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

9 files changed, 99 insertions, 48 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 767a7dd667..dcea487a97 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -473,7 +473,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	 let hintl = 
 	   try 
 	     [make_apply_entry (pf_env g') (project g')
-		(true,false) 
+		(true,true,false) 
 		None
 		(mkVar hid,htyp)]
 	   with Failure _ -> [] 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 09e61719ae..0516bd551d 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1770,7 +1770,7 @@ let rec xlate_vernac =
 		| HintsImmediate _ -> CT_hints_immediate(l', dblist)
 		| _ -> assert false)
         | HintsResolve l -> 
-	 let f1, formulas = match List.map xlate_formula (List.map snd l) with
+	 let f1, formulas = match List.map xlate_formula (List.map pi3 l) with
 	     a :: tl -> a, tl
 	   | _  -> failwith "" in
 	 let l' = CT_formula_ne_list(f1, formulas) in
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 32a2427ed1..486f80abc9 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -106,7 +106,7 @@ GEXTEND Gram
   ;
   hint:
     [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT [ n = natural -> n ] -> 
-          HintsResolve (List.map (fun x -> (n, x)) lc)
+          HintsResolve (List.map (fun x -> (n, true, x)) lc)
       | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc
       | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
       | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index bfcaf99164..646f697b6d 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -192,7 +192,7 @@ let pr_hints local db h pr_c pr_pat =
     match h with
     | HintsResolve l ->
         str "Resolve " ++ prlist_with_sep sep 
-	  (fun (pri, c) -> pr_c c ++ 
+	  (fun (pri, _, c) -> pr_c c ++ 
 	    match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ())
 	  l
     | HintsImmediate l ->
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 9a17af6aa8..a5778d45db 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -258,15 +258,15 @@ let make_exact_entry pri (c,cty) =
 	(head_of_constr_reference (List.hd (head_constr cty)),
 	   { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c })
 
-let make_apply_entry env sigma (eapply,verbose) pri (c,cty) =
-  let cty = hnf_constr env sigma cty in
-  match kind_of_term cty with
+let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
+  let cty = if hnf then hnf_constr env sigma cty else cty in
+    match kind_of_term cty with
     | Prod _ ->
         let ce = mk_clenv_from dummy_goal (c,cty) in
 	let c' = clenv_type ce in
 	let pat = Pattern.pattern_of_constr c' in
         let hd = (try head_pattern_bound pat
-                  with BoundPattern -> failwith "make_apply_entry") in
+          with BoundPattern -> failwith "make_apply_entry") in
         let nmiss = List.length (clenv_missing ce) in
 	if nmiss = 0 then 
 	  (hd,
@@ -285,7 +285,7 @@ let make_apply_entry env sigma (eapply,verbose) pri (c,cty) =
         end
     | _ -> failwith "make_apply_entry"
  
-(* flags is (e,v) with e=true if eapply and v=true if verbose 
+(* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose 
    c is a constr
    cty is the type of constr *)
 
@@ -299,14 +299,14 @@ let make_resolves env sigma flags pri c =
   if ents = [] then
     errorlabstrm "Hint" 
       (pr_lconstr c ++ spc() ++ 
-        (if fst flags then str"cannot be used as a hint."
+        (if pi1 flags then str"cannot be used as a hint."
 	else str "can be used as a hint only for eauto."));
   ents
 
 (* used to add an hypothesis to the local hint database *)
 let make_resolve_hyp env sigma (hname,_,htyp) = 
   try
-    [make_apply_entry env sigma (true, false) None
+    [make_apply_entry env sigma (true, true, false) None
        (mkVar hname, htyp)]
   with 
     | Failure _ -> []
@@ -457,8 +457,8 @@ let add_resolves env sigma clist local dbnames =
        Lib.add_anonymous_leaf
 	 (inAutoHint
 	    (local,dbname, AddTactic
-     	      (List.flatten (List.map (fun (x, y) ->
-		make_resolves env sigma (true,Flags.is_verbose()) x y) clist)))))
+     	      (List.flatten (List.map (fun (x, hnf, y) ->
+		make_resolves env sigma (true,hnf,Flags.is_verbose()) x y) clist)))))
     dbnames
 
 
@@ -507,7 +507,7 @@ let add_hints local dbnames0 h =
   let f = Constrintern.interp_constr sigma env in
   match h with
   | HintsResolve lhints ->	
-      add_resolves env sigma (List.map (fun (pri, x) -> pri, f x) lhints) local dbnames
+      add_resolves env sigma (List.map (fun (pri, b, x) -> pri, b, f x) lhints) local dbnames
   | HintsImmediate lhints ->
       add_trivials env sigma (List.map f lhints) local dbnames
   | HintsUnfold lhints ->
@@ -544,7 +544,7 @@ let add_hints local dbnames0 h =
         let isp = inductive_of_reference qid in
         let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in
         let lcons = list_tabulate
-          (fun i -> None, mkConstruct (isp,i+1)) (Array.length consnames) in
+          (fun i -> None, true, mkConstruct (isp,i+1)) (Array.length consnames) in
         add_resolves env sigma lcons local dbnames in
       List.iter add_one lqid
   | HintsExtern (pri, patcom, tacexp) ->
@@ -707,7 +707,7 @@ let unify_resolve flags (c,clenv) gls =
 let make_local_hint_db eapply lems g =
   let sign = pf_hyps g in
   let hintlist = list_map_append (pf_apply make_resolve_hyp g) sign in
-  let hintlist' = list_map_append (pf_apply make_resolves g (eapply,false) None) lems in
+  let hintlist' = list_map_append (pf_apply make_resolves g (eapply,true,false) None) lems in
     Hint_db.add_list hintlist' (Hint_db.add_list hintlist (Hint_db.empty empty_transparent_state false))
 
 (* Serait-ce possible de compiler d'abord la tactique puis de faire la
@@ -741,6 +741,10 @@ let conclPattern concl pat tac gl =
 (* Papageno : cette fonction a été pas mal simplifiée depuis que la base
   de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
 
+let flags_of_state st =
+  {auto_unif_flags with 
+    modulo_conv_on_closed_terms = Some st; modulo_delta = st}
+
 let rec trivial_fail_db mod_delta db_list local_db gl =
   let intro_tac = 
     tclTHEN intro 
@@ -788,19 +792,27 @@ and my_find_search_delta db_list local_db hdc concl =
     if occur_existential concl then 
       list_map_append
 	(fun db -> 
-	  let st = {flags with modulo_delta = Hint_db.transparent_state db} in
-	    List.map (fun x -> (st,x)) (Hint_db.map_all hdc db))
+	  if Hint_db.use_dn db then 
+	    let flags = flags_of_state (Hint_db.transparent_state db) in
+	      List.map (fun x -> (flags, x)) (Hint_db.map_auto (hdc,concl) db)
+	  else
+	    let st = {flags with modulo_delta = Hint_db.transparent_state db} in
+	      List.map (fun x -> (st,x)) (Hint_db.map_all hdc db))
 	(local_db::db_list)
     else
       list_map_append (fun db -> 
-	let (ids, csts as st) = Hint_db.transparent_state db in
-	let st, l = 
-	  let l =
-	    if (Idpred.is_empty ids && Cpred.is_empty csts)
-	    then Hint_db.map_auto (hdc,concl) db
-	    else Hint_db.map_all hdc db
-	  in {flags with modulo_delta = st}, l
-	in List.map (fun x -> (st,x)) l)
+	if Hint_db.use_dn db then 
+	  let flags = flags_of_state (Hint_db.transparent_state db) in
+	    List.map (fun x -> (flags, x)) (Hint_db.map_auto (hdc,concl) db)
+	else
+	  let (ids, csts as st) = Hint_db.transparent_state db in
+	  let st, l = 
+	    let l =
+	      if (Idpred.is_empty ids && Cpred.is_empty csts)
+	      then Hint_db.map_auto (hdc,concl) db
+	      else Hint_db.map_all hdc db
+	    in {flags with modulo_delta = st}, l
+	  in List.map (fun x -> (st,x)) l)
       	(local_db::db_list)
   in
     List.map 
@@ -910,7 +922,7 @@ let rec search_gen decomp n mod_delta db_list local_db extra_sign goal =
 	 let hintl = 
 	   try 
 	     [make_apply_entry (pf_env g') (project g')
-		(true,false) None
+		(true,true,false) None
 		(mkVar hid, htyp)]
 	   with Failure _ -> [] 
 	 in
@@ -1009,7 +1021,7 @@ let make_resolve_any_hyp env sigma (id,_,ty) =
   let ents = 
     map_succeed
       (fun f -> f (mkVar id,ty)) 
-      [make_exact_entry None; make_apply_entry env sigma (true,false) None]
+      [make_exact_entry None; make_apply_entry env sigma (true,true,false) None]
   in 
   ents
 
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 3efcc62815..b35f98ec1a 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -95,11 +95,13 @@ val make_exact_entry : int option -> constr * constr -> global_reference * pri_a
 
 (* [make_apply_entry (eapply,verbose) pri (c,cty)].
    [eapply] is true if this hint will be used only with EApply;
+   [hnf] should be true if we should expand the head of cty before searching for 
+   products;
    [c] is the term given as an exact proof to solve the goal;
-   [cty] is the type of [hc]. *)
-
+   [cty] is the type of [c]. *)
+  
 val make_apply_entry :
-  env -> evar_map -> bool * bool -> int option -> constr * constr
+  env -> evar_map -> bool * bool * bool -> int option -> constr * constr
       -> global_reference * pri_auto_tactic
 
 (* A constr which is Hint'ed will be:
@@ -110,7 +112,7 @@ val make_apply_entry :
        has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> bool * bool -> int option -> constr -> 
+  env -> evar_map -> bool * bool * bool -> int option -> constr -> 
       (global_reference * pri_auto_tactic) list
 
 (* [make_resolve_hyp hname htyp].
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index b50c591898..3cdf050c43 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -343,16 +343,24 @@ let is_transparent_gr (ids, csts) = function
   | ConstRef cst -> Cpred.mem cst csts
   | IndRef _ | ConstructRef _ -> false
 
+let make_resolve_hyp env sigma st flags pri (id, _, cty) =
+  let ctx, ar = decompose_prod cty in
+  let keep = 
+    match kind_of_term (fst (decompose_app ar)) with
+    | Const c -> is_class (ConstRef c)
+    | Ind i -> is_class (IndRef i)
+    | _ -> false
+  in
+    if keep then let c = mkVar id in
+      map_succeed 
+	(fun f -> f (c,cty)) 
+	[make_exact_entry pri; make_apply_entry env sigma flags pri]
+    else []
+
 let make_local_hint_db st eapply lems g =
   let sign = pf_hyps g in
-  let make_resolve_hyp env evar_map c = 
-    try 
-      let res = make_resolves env evar_map (eapply, false) None (mkVar c) in
-	List.filter (fun (gr, _) -> not (is_transparent_gr st gr)) res
-    with _ -> []
-  in
-  let hintlist = list_map_append (pf_apply make_resolve_hyp g) (ids_of_named_context sign) in
-  let hintlist' = list_map_append (pf_apply make_resolves g (eapply,false) None) lems in
+  let hintlist = list_map_append (pf_apply make_resolve_hyp g st (eapply,false,false) None) sign in
+  let hintlist' = list_map_append (pf_apply make_resolves g (eapply,false,false) None) lems in
     Hint_db.add_list hintlist' (Hint_db.add_list hintlist (Hint_db.empty st true))
 
 let e_search_auto debug (in_depth,p) lems st db_list gls = 
@@ -1715,7 +1723,7 @@ END
 
 let not_declared env ty rel =
   tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared " ++ 
-		str ty ++ str" relation. Maybe you need to import the Setoid library.")
+		str ty ++ str" relation. Maybe you need to import the Setoid library")
 
 let relation_of_constr env c = 
   match kind_of_term c with
@@ -1725,11 +1733,40 @@ let relation_of_constr env c =
     | _ -> errorlabstrm "relation_of_constr" 
 	(str "The term " ++ Printer.pr_constr_env env c ++ str" is not an applied relation.")
 	
-let setoid_proof gl ty ?(bindings=NoBindings) meth fallback =
+let setoid_proof gl ty fn fallback =
+  let env = pf_env gl in
+  let rel, args = relation_of_constr env (pf_concl gl) in
+  let evm, car = project gl, pf_type_of gl args.(0) in
+    try fn env evm car rel gl
+    with Not_found -> 
+      match fallback gl with
+      | Some tac -> tac gl
+      | None -> not_declared env ty rel gl
+	  
+let setoid_reflexivity gl =
+  setoid_proof gl "reflexive" 
+    (fun env evm car rel -> apply (get_reflexive_proof env evm car rel))
+    (reflexivity_red true)
+	  
+let setoid_symmetry gl =
+  setoid_proof gl "symmetric" 
+    (fun env evm car rel -> apply (get_symmetric_proof env evm car rel))
+    (symmetry_red true)
+    
+let setoid_transitivity c gl =
+  setoid_proof gl "transitive" 
+    (fun env evm car rel ->
+      apply_with_bindings
+	((get_transitive_proof env evm car rel),
+	Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp (id_of_string "y"), c ]))
+    (transitivity_red true c)
+    
+(*
+  let setoid_proof gl ty ?(bindings=NoBindings) meth fallback =
   try
-    typeclass_app_constrexpr 
-      (CRef (Qualid (dummy_loc, Nametab.shortest_qualid_of_global Idset.empty
-	(Lazy.force meth)))) ~bindings gl
+  typeclass_app_constrexpr 
+  (CRef (Qualid (dummy_loc, Nametab.shortest_qualid_of_global Idset.empty
+  (Lazy.force meth)))) ~bindings gl
   with Not_found | Typeclasses_errors.TypeClassError (_, _) |
       Stdpp.Exc_located (_, Typeclasses_errors.TypeClassError (_, _)) -> 
 	match fallback gl with 
@@ -1752,7 +1789,7 @@ let setoid_transitivity c gl =
     setoid_proof gl "transitive" 
       ~bindings:(Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp binding_name, constrIn c ])
       transitive_proof_global (transitivity_red true c)
-
+*)
 let setoid_symmetry_in id gl =
   let ctype = pf_type_of gl (mkVar id) in
   let binders,concl = Sign.decompose_prod_assum ctype in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 288574882b..8dcbf4b282 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -47,7 +47,7 @@ let _ =
       Flags.silently (fun () ->      
 	Auto.add_hints false [typeclasses_db] 
 	  (Vernacexpr.HintsResolve 
-	      [pri, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) ())
+	      [pri, false, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) ())
 
 let declare_instance_cst glob con =
   let instance = Typeops.type_of_constant (Global.env ()) con in
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 5bd8dc36eb..f87549706a 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -112,7 +112,7 @@ type comment =
   | CommentInt of int
 
 type hints =
-  | HintsResolve of (int option * constr_expr) list
+  | HintsResolve of (int option * bool * constr_expr) list
   | HintsImmediate of constr_expr list
   | HintsUnfold of reference list
   | HintsTransparency of reference list * bool