From ab7377de0a913ca6218bc7377fab33b8018f8f59 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Thu, 5 Sep 2013 17:28:56 +0000 Subject: 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 --- pretyping/evd.ml | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) (limited to 'pretyping/evd.ml') 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 -- cgit v1.2.3