Change implementation of resolution for typeclasses to use a customized

eauto instead of an arbitrary tactic. Export more from eauto to allow
easier debugging.


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

3 files changed, 53 insertions, 33 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e30f553fe..399264859 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -362,7 +362,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	      (* If recursive argument was not given by user, we try all args.
 	         An earlier approach was to look only for inductive arguments,
 		 but doing it properly involves delta-reduction, and it finally 
-                 doesn't seem to worth the effort (except for huge mutual 
+                 doesn't seem worth the effort (except for huge mutual 
 		 fixpoints ?) *)
 	      let possible_indexes = Array.to_list (Array.mapi 
 		(fun i (n,_) -> match n with 
@@ -668,8 +668,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  (pretype_type empty_valcon env evdref lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !evdref in
     let evd = nf_evar_defs evd in
-    let c' = nf_evar (evars_of evd) c' in
-    let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in
+    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in
     let c' = nf_evar (evars_of evd) c' in
       evdref := evd;
       c'
@@ -684,7 +683,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let j = pretype empty_tycon env evdref ([],[]) c in
     let evd,_ = consider_remaining_unif_problems env !evdref in
     let j = j_nf_evar (evars_of evd) j in
-    let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in
+    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:true env (evars_of evd) evd in
     let j = j_nf_evar (evars_of evd) j in
     check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
     j
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index f9ab283ad..7a95f9c35 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -216,7 +216,7 @@ let instances r =
     with Not_found -> unbound_class (Global.env()) (loc_of_reference r, id)
 
 let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false)
-let solve_instanciations_problem = ref (fun _ _ -> assert false)
+let solve_instanciations_problem = ref (fun _ _ _ _ -> assert false)
 
 let resolve_typeclass env ev evi (evd, defined as acc) =
   try
@@ -278,34 +278,43 @@ let destClassApp c =
     | _ when isInd c -> Some (destInd c, [||])
     | _ -> None
 
-let resolve_typeclasses ?(check=true) env sigma evd =
+let is_independent evm ev = 
+  Evd.fold (fun ev' evi indep -> indep && 
+    (ev = ev' || 
+	evi.evar_body <> Evar_empty ||
+	not (Termops.occur_evar ev evi.evar_concl)))
+    evm true
+    
+
 (*   try !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) *)
 (*   with _ -> *)
-  let evm = Evd.evars_of evd in
-  let tc_evars = 
-    let f ev evi acc =
-      let (l, k) = Evd.evar_source ev evd in
-	if not check || is_implicit_arg k then
-	  match destClassApp evi.evar_concl with
-	    | Some (i, args) when is_class i -> 
-		Evd.add acc ev evi
-	    | _ -> acc
-	else acc
-    in Evd.fold f evm Evd.empty
-  in
-  let rec sat evars =
-    let (evars', progress) = 
-      Evd.fold 
-	(fun ev evi acc -> 
-	  if (Evd.mem tc_evars ev || not (Evd.mem evm ev)) && evi.evar_body = Evar_empty then
-	    resolve_typeclass env ev evi acc 
-	  else acc)
-	(Evd.evars_of evars) (evars, false) 
-    in
-      if not progress then evars'
-      else
-	sat (Evarutil.nf_evar_defs evars')
-  in sat (Evarutil.nf_evar_defs evd)
+(*   let evm = Evd.evars_of evd in *)
+(*   let tc_evars =  *)
+(*     let f ev evi acc = *)
+(*       let (l, k) = Evd.evar_source ev evd in *)
+(* 	if not check || is_implicit_arg k then *)
+(* 	  match destClassApp evi.evar_concl with *)
+(* 	    | Some (i, args) when is_class i ->  *)
+(* 		Evd.add acc ev evi *)
+(* 	    | _ -> acc *)
+(* 	else acc *)
+(*     in Evd.fold f evm Evd.empty *)
+(*   in *)
+(*   let rec sat evars = *)
+(*     let evm = Evd.evars_of evars in *)
+(*     let (evars', progress) =  *)
+(*       Evd.fold  *)
+(* 	(fun ev evi acc ->  *)
+(* 	  if (Evd.mem tc_evars ev || not (Evd.mem evm ev))  *)
+(* 	    && evi.evar_body = Evar_empty then *)
+(* 	    resolve_typeclass env ev evi acc  *)
+(* 	  else acc) *)
+(* 	evm (evars, false)  *)
+(*     in *)
+(*       if not progress then evars' *)
+(*       else *)
+(* 	sat (Evarutil.nf_evar_defs evars') *)
+(*   in sat (Evarutil.nf_evar_defs evd) *)
   
 let class_of_constr c = 
   let extract_ind c =
@@ -317,6 +326,16 @@ let class_of_constr c =
 	App (c, _) -> extract_ind c
       | _ -> extract_ind c
 
+let has_typeclasses evd =
+  Evd.fold (fun ev evi has -> has || 
+    (evi.evar_body = Evar_empty && class_of_constr evi.evar_concl <> None))
+    evd false
+
+let resolve_typeclasses ?(onlyargs=false) ?(all=true) env sigma evd =
+  if not (has_typeclasses sigma) then evd
+  else
+    !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs all
+
 type substitution = (identifier * constr) list
 
 let substitution_of_named_context isevars env id n subst l = 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index db408c889..f231c7406 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -61,10 +61,10 @@ val is_class : inductive -> bool
 val class_of_constr : constr -> typeclass option
 
 val resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_defs * bool
-val resolve_typeclasses : ?check:bool -> env -> evar_map -> evar_defs -> evar_defs
+val resolve_typeclasses : ?onlyargs:bool -> ?all:bool -> env -> evar_map -> evar_defs -> evar_defs
 
 val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref
-val solve_instanciations_problem : (env -> evar_defs -> evar_defs) ref
+val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> evar_defs) ref
 
 type substitution = (identifier * constr) list
 
@@ -73,3 +73,5 @@ val substitution_of_named_context :
   substitution -> named_context -> substitution
 
 val nf_substitution : evar_map -> substitution -> substitution
+
+val is_implicit_arg : hole_kind -> bool