Optimizing some evar_maps manipulation. In particular, using a [map] instead

of a [fold] in [nf_*] normalizing functions.

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

4 files changed, 49 insertions, 16 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 84f7254b1b..1972aee28b 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -79,15 +79,11 @@ let nf_evar_info evc info =
     evar_body = match info.evar_body with
       | Evar_empty -> Evar_empty
       | Evar_defined c -> Evar_defined (Reductionops.nf_evar evc c) }
-let nf_evars evm =
-  Evd.fold
-    (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
-    evm Evd.empty
+
+let nf_evars evm = Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm
 
 let nf_evars_undefined evm =
-  Evd.fold_undefined
-    (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
-    evm (defined_evars evm)
+  Evd.raw_map_undefined (fun _ evi -> nf_evar_info evm evi) evm
 
 let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd
 let nf_evar_map_undefined evd = Evd.evars_reset_evd (nf_evars_undefined evd) evd
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c92f6a5b36..cebce3abea 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -260,6 +260,33 @@ let fold f d a =
 
 let fold_undefined f d a = ExMap.fold f d.undf_evars a
 
+let raw_map f d =
+  let f evk info =
+    let ans = f evk info in
+    let () = match info.evar_body, ans.evar_body with
+    | Evar_defined _, Evar_empty
+    | Evar_empty, Evar_defined _ ->
+      anomaly (str "Unrespectful mapping function.")
+    | _ -> ()
+    in
+    ans
+  in
+  let defn_evars = ExMap.mapi f d.defn_evars in
+  let undf_evars = ExMap.mapi f d.undf_evars in
+  { d with defn_evars; undf_evars; }
+
+let raw_map_undefined f d =
+  let f evk info =
+    let ans = f evk info in
+    let () = match ans.evar_body with
+    | Evar_defined _ ->
+      anomaly (str "Unrespectful mapping function.")
+    | _ -> ()
+    in
+    ans
+  in
+  { d with undf_evars = ExMap.mapi f d.undf_evars; }
+
 let is_evar = mem
 
 let is_defined d e = ExMap.mem e d.defn_evars
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 354a5b533f..0beb465713 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -127,6 +127,16 @@ val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
 (** Same as {!fold}, but restricted to undefined evars. For efficiency
     reasons. *)
 
+val raw_map : (evar -> evar_info -> evar_info) -> evar_map -> evar_map
+(** Apply the given function to all evars in the map. Beware: this function
+    expects the argument function to preserve the kind of [evar_body], i.e. it
+    must send [Evar_empty] to [Evar_empty] and [Evar_defined c] to some
+    [Evar_defined c']. *)
+
+val raw_map_undefined : (evar -> evar_info -> evar_info) -> evar_map -> evar_map
+(** Same as {!raw_map}, but restricted to undefined evars. For efficiency
+    reasons. *)
+
 val define : evar -> constr -> evar_map -> evar_map
 (** Set the body of an evar to the given constr. It is expected that:
     {ul
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index e917494315..a1cb232ca0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -493,20 +493,20 @@ let no_goals_or_obligations _ = function
   | _ -> true
 
 let mark_resolvability filter b sigma =
-  Evd.fold_undefined 
-    (fun ev evi evs ->
-     if filter ev (snd evi.evar_source) then
-       Evd.add evs ev (mark_resolvability_undef b evi)
-     else Evd.add evs ev evi)
-  sigma (Evd.defined_evars sigma)
+  let map ev evi =
+    if filter ev (snd evi.evar_source) then mark_resolvability_undef b evi
+    else evi
+  in
+  Evd.raw_map_undefined map sigma
 
 let mark_unresolvables ?(filter=all_evars) sigma = mark_resolvability filter false sigma
 let mark_resolvables sigma = mark_resolvability all_evars true sigma
 
 let has_typeclasses filter evd =
-  Evd.fold_undefined (fun ev evi has -> has ||
-    (filter ev (snd evi.evar_source) && is_class_evar evd evi && is_resolvable evi))
-    evd false
+  let check ev evi =
+    filter ev (snd evi.evar_source) && is_class_evar evd evi && is_resolvable evi
+  in
+  Evd.ExistentialMap.exists check (Evd.undefined_map evd)
 
 let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)