Using HMaps in Safe_env.environments, hopefully improving performances.

5 files changed, 33 insertions, 9 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 15db39328c..0bf3923e45 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -168,7 +168,7 @@ let no_link_info () = ref NotLinked
 
 let add_constant_key kn cb linkinfo env =
   let new_constants =
-    Cmap_env.add kn (cb,(linkinfo, ref None)) env.env_globals.env_constants in
+    Constants.add kn (cb,(linkinfo, ref None)) env.env_globals.env_constants in
   let new_globals =
     { env.env_globals with
 	env_constants = new_constants } in
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index b655887d70..3509ccf0cc 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -38,8 +38,23 @@ type constant_key = constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
+module Constants =
+struct
+  module M =
+  struct
+    type t = Constant.t
+    include Constant.UserOrd
+  end
+  module CMap = HMap.Make(M)
+  type t = constant_key CMap.t
+  let empty = CMap.empty
+  let add = CMap.add
+  let find = CMap.find
+  let fold = CMap.fold
+end
+
 type globals = {
-  env_constants : constant_key Cmap_env.t;
+  env_constants : Constants.t;
   env_inductives : mind_key Mindmap_env.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}
@@ -81,7 +96,7 @@ let empty_named_context_val = [],[]
 
 let empty_env = {
   env_globals = {
-    env_constants = Cmap_env.empty;
+    env_constants = Constants.empty;
     env_inductives = Mindmap_env.empty;
     env_modules = MPmap.empty;
     env_modtypes = MPmap.empty};
@@ -150,10 +165,10 @@ let env_of_named id env = env
 (* Global constants *)
 
 let lookup_constant_key kn env =
-  Cmap_env.find kn env.env_globals.env_constants
+  Constants.find kn env.env_globals.env_constants
 
 let lookup_constant kn env =
-  fst (Cmap_env.find kn env.env_globals.env_constants)
+  fst (Constants.find kn env.env_globals.env_constants)
 
 (* Mutual Inductives *)
 let lookup_mind kn env =
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 964d709cff..4596b23aaa 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -25,8 +25,17 @@ type constant_key = constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
+module Constants :
+sig
+  type t
+  val empty : t
+  val add : Constant.t -> constant_key -> t -> t
+  val find : Constant.t -> t -> constant_key
+  val fold : (Constant.t -> constant_key -> 'a -> 'a) -> t -> 'a  -> 'a
+end
+
 type globals = {
-  env_constants : constant_key Cmap_env.t;
+  env_constants : Constants.t;
   env_inductives : mind_key Mindmap_env.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index bf758b96b1..670e115af8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -766,9 +766,9 @@ let register_inline kn senv =
   if not (evaluable_constant kn senv.env) then
     Errors.error "Register inline: an evaluable constant is expected";
   let env = pre_env senv.env in
-  let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in
+  let (cb,r) = Constants.find kn env.env_globals.env_constants in
   let cb = {cb with const_inline_code = true} in
-  let new_constants = Cmap_env.add kn (cb,r) env.env_globals.env_constants in
+  let new_constants = Constants.add kn (cb,r) env.env_globals.env_constants in
   let new_globals = { env.env_globals with env_constants = new_constants } in
   let env = { env with env_globals = new_globals } in
   { senv with env = env_of_pre_env env }
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3951190832..29297058eb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -264,7 +264,7 @@ let print_namespace ns =
   | _ -> false in
   let constants = (Environ.pre_env (Global.env ())).Pre_env.env_globals.Pre_env.env_constants in
   let constants_in_namespace =
-    Cmap_env.fold (fun c (body,_) acc ->
+    Pre_env.Constants.fold (fun c (body,_) acc ->
       let kn = user_con c in
       if matches (modpath kn) then
         acc++fnl()++hov 2 (print_constant kn body)