diff options
| -rw-r--r-- | pretyping/evarutil.ml | 10 | ||||
| -rw-r--r-- | pretyping/evd.ml | 27 | ||||
| -rw-r--r-- | pretyping/evd.mli | 10 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 18 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 29 |
5 files changed, 63 insertions, 31 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 84f7254b1..1972aee28 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 c92f6a5b3..cebce3abe 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 354a5b533..0beb46571 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 e91749431..a1cb232ca 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) diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 646c57d95..c62499fdf 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -197,7 +197,7 @@ let rec catchable = function | e -> Logic.catchable_exception e let nb_empty_evars s = - Evd.fold_undefined (fun ev evi acc -> succ acc) s 0 + ExistentialMap.cardinal (undefined_map s) let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) (Evarutil.nf_evar evs (Goal.V82.concl evs ev)) @@ -629,26 +629,25 @@ let select_and_update_evars p oevd in_comp evd ev evi = (** Do we still have unresolved evars that should be resolved ? *) let has_undefined p oevd evd = - Evd.fold_undefined (fun ev evi has -> has || - snd (p oevd ev evi)) - evd false + let check ev evi = snd (p oevd ev evi) in + ExistentialMap.exists check (Evd.undefined_map evd) (** Revert the resolvability status of evars after resolution, potentially unprotecting some evars that were set unresolvable just for this call to resolution. *) let revert_resolvability oevd evd = - Evd.fold_undefined - (fun ev evi evm -> - try - if not (Typeclasses.is_resolvable evi) then - let evi' = Evd.find_undefined oevd ev in - if Typeclasses.is_resolvable evi' then - Evd.add evm ev (Typeclasses.mark_resolvable evi) - else evm - else evm - with Not_found -> evm) - evd evd + let map ev evi = + try + if not (Typeclasses.is_resolvable evi) then + let evi' = Evd.find_undefined oevd ev in + if Typeclasses.is_resolvable evi' then + Typeclasses.mark_resolvable evi + else evi + else evi + with Not_found -> evi + in + Evd.raw_map_undefined map evd (** If [do_split] is [true], we try to separate the problem in several components and then solve them separately *) |