Removing uses of Evar.add in class-related functions.

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

4 files changed, 47 insertions, 44 deletions

diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 89eb217d28..a6a9a75c5a 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -22,7 +22,8 @@ type typeclass_error =
     | NotAClass of constr
     | UnboundMethod of global_reference * Id.t Loc.located (* Class name, method *)
     | NoInstance of Id.t Loc.located * constr list
-    | UnsatisfiableConstraints of evar_map * (existential_key * Evar_kinds.t) option
+    | UnsatisfiableConstraints of
+      evar_map * (existential_key * Evar_kinds.t) option * Evar.Set.t option
     | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
@@ -35,14 +36,15 @@ let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
 
 let no_instance env id args = typeclass_error env (NoInstance (id, args))
 
-let unsatisfiable_constraints env evd ev =
+let unsatisfiable_constraints env evd ev comp =
   match ev with
   | None ->
-      raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
+    let err = UnsatisfiableConstraints (evd, None, comp) in
+    raise (TypeClassError (env, err))
   | Some ev ->
     let loc, kind = Evd.evar_source ev evd in
-    let err = TypeClassError (env, UnsatisfiableConstraints (evd, Some (ev, kind))) in
-    Loc.raise loc err
+    let err = UnsatisfiableConstraints (evd, Some (ev, kind), comp) in
+    Loc.raise loc (TypeClassError (env, err))
 
 let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
 
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index a55b9204ef..94bbfce00e 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -25,7 +25,9 @@ type typeclass_error =
   | NotAClass of constr
   | UnboundMethod of global_reference * Id.t located (** Class name, method *)
   | NoInstance of Id.t located * constr list
-  | UnsatisfiableConstraints of evar_map * (existential_key * Evar_kinds.t) option
+  | UnsatisfiableConstraints of
+    evar_map * (existential_key * Evar_kinds.t) option * Evar.Set.t option
+    (** evar map, unresolvable evar, connex component *)
   | MismatchedContextInstance of contexts * constr_expr list * rel_context (** found, expected *)
 
 exception TypeClassError of env * typeclass_error
@@ -36,7 +38,8 @@ val unbound_method : env -> global_reference -> Id.t located -> 'a
 
 val no_instance : env -> Id.t located -> constr list -> 'a
 
-val unsatisfiable_constraints : env -> evar_map -> evar option -> 'a
+val unsatisfiable_constraints : env -> evar_map -> evar option ->
+  Evar.Set.t option -> 'a
 
 val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index da6e123121..87086cfae8 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -36,18 +36,18 @@ exception Found of evar_map
 
 (** We transform the evars that are concerned by this resolution
     (according to predicate p) into goals.
-    Invariant: function p only manipulates undefined evars *)
+    Invariant: function p only manipulates and returns undefined evars *)
 
 let evars_to_goals p evm =
-  let goals, evm' =
-    Evd.fold_undefined
-      (fun ev evi (gls, evm') ->
-	let evi', goal = p evm ev evi in
-	let gls' = if goal then (ev,Goal.V82.build ev) :: gls else gls in
-	(gls', Evd.add evm' ev evi'))
-      evm ([], Evd.defined_evars evm)
+  let goals = ref Evar.Map.empty in
+  let map ev evi =
+    let evi, goal = p evm ev evi in
+    let () = if goal then goals := Evar.Map.add ev (Goal.V82.build ev) !goals in
+    evi
   in
-  if List.is_empty goals then None else Some (List.rev goals, evm')
+  let evm = Evd.raw_map_undefined map evm in
+  if Evar.Map.is_empty !goals then None
+  else Some (Evar.Map.bindings !goals, evm)
 
 (** Typeclasses instance search tactic / eauto *)
 
@@ -560,16 +560,6 @@ let split_evars evm =
   deps_of_constraints (snd (extract_all_conv_pbs evm)) evm p;
   Intpart.partition p
 
-(** [evars_in_comp] filters an [evar_map], keeping only evars
-    that belongs to a certain component *)
-
-let evars_in_comp comp evm =
-  try
-    evars_reset_evd
-      (Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evm ev))
-	 comp Evd.empty) evm
-  with Not_found -> assert false
-
 let is_inference_forced p evd ev =
   try
     let evi = Evd.find_undefined evd ev in
@@ -588,20 +578,23 @@ let is_mandatory p comp evd =
 
 (** In case of unsatisfiable constraints, build a nice error message *)
 
-let error_unresolvable env comp do_split evd =
+let error_unresolvable env comp evd =
   let evd = Evarutil.nf_evar_map_undefined evd in
-  let evm = if do_split then evars_in_comp comp evd else evd in
-  let _, ev = Evd.fold_undefined
-    (fun ev evi (b,acc) ->
-      (* focus on one instance if only one was searched for *)
-      if not (Option.is_empty (class_of_constr evi.evar_concl)) then
-	if not b (* || do_split *) then
-	  true, Some ev
-	else b, None
-      else b, acc) evm (false, None)
+  let is_part ev = match comp with
+  | None -> true
+  | Some s -> Evar.Set.mem ev s
   in
+  let fold ev evi (found, accu) =
+    let ev_class = class_of_constr evi.evar_concl in
+    if not (Option.is_empty ev_class) && is_part ev then
+      (* focus on one instance if only one was searched for *)
+      if not found then (true, Some ev)
+      else (found, None)
+    else (found, accu)
+   in
+  let (_, ev) = Evd.fold_undefined fold evd (true, None) in
   Typeclasses_errors.unsatisfiable_constraints
-    (Evarutil.nf_env_evar evm env) evm ev
+    (Evarutil.nf_env_evar evd env) evd ev comp
 
 (** Check if an evar is concerned by the current resolution attempt,
     (and in particular is in the current component), and also update
@@ -663,7 +656,8 @@ let resolve_all_evars debug m env p oevd do_split fail =
       with Unresolved | Not_found ->
 	if fail && (not do_split || is_mandatory (p evd) comp evd)
 	then (* Unable to satisfy the constraints. *)
-	  error_unresolvable env comp do_split evd
+          let comp = if do_split then Some comp else None in
+	  error_unresolvable env comp evd
 	else (* Best effort: do nothing on this component *)
 	  docomp evd comps
   in docomp oevd split
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index e70d0a0e8b..4d4002cff2 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -801,12 +801,16 @@ let pr_constraints printenv env evd evars cstrs =
       let filter evk _ = Evar.Map.mem evk evars in
       pr_evar_map_filter filter evd
 
-let explain_unsatisfiable_constraints env evd constr =
+let explain_unsatisfiable_constraints env evd constr comp =
   let (_, constraints) = Evd.extract_all_conv_pbs evd in
   let undef = Evd.undefined_map (Evarutil.nf_evar_map_undefined evd) in
-  (* Remove evars that are not subject to resolution. *)
-  let is_resolvable _ evi = Typeclasses.is_resolvable evi in
-  let undef = Evar.Map.filter is_resolvable undef in
+  (** Only keep evars that are subject to resolution and members of the given
+     component. *)
+  let is_kept evk evi = match comp with
+  | None -> Typeclasses.is_resolvable evi
+  | Some comp -> Typeclasses.is_resolvable evi && Evar.Set.mem evk comp
+  in
+  let undef = Evar.Map.filter is_kept undef in
   match constr with
   | None ->
     str "Unable to satisfy the following constraints:" ++ fnl () ++
@@ -832,8 +836,8 @@ let explain_typeclass_error env = function
   | NotAClass c -> explain_not_a_class env c
   | UnboundMethod (cid, id) -> explain_unbound_method env cid id
   | NoInstance (id, l) -> explain_no_instance env id l
-  | UnsatisfiableConstraints (evd, c) ->
-      explain_unsatisfiable_constraints env evd c
+  | UnsatisfiableConstraints (evd, c, comp) ->
+      explain_unsatisfiable_constraints env evd c comp
   | MismatchedContextInstance (c,i,j) -> explain_mismatched_contexts env c i j
 
 (* Refiner errors *)