Using Hashmaps by default in constant and inductive maps. This changes fold and

iter order, but it seems nobody was relying on it (contrarily to the string case).

7 files changed, 25 insertions, 76 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index a25714d77..15db39328 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 =
-    Constants.add kn (cb,(linkinfo, ref None)) env.env_globals.env_constants in
+    Cmap_env.add kn (cb,(linkinfo, ref None)) env.env_globals.env_constants in
   let new_globals =
     { env.env_globals with
 	env_constants = new_constants } in
@@ -206,7 +206,7 @@ let evaluable_constant cst env =
 let lookup_mind = lookup_mind
 
 let add_mind_key kn mind_key env =
-  let new_inds = Inductives.add kn mind_key env.env_globals.env_inductives in
+  let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
   let new_globals =
     { env.env_globals with
 	env_inductives = new_inds } in
diff --git a/kernel/names.ml b/kernel/names.ml
index 21d22baff..03826cda7 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -524,19 +524,19 @@ end
 
 module Constant = KerPair
 
-module Cmap = CMap.Make(Constant.CanOrd)
-module Cmap_env = CMap.Make(Constant.UserOrd)
+module Cmap = HMap.Make(Constant.CanOrd)
+module Cmap_env = HMap.Make(Constant.UserOrd)
 module Cpred = Predicate.Make(Constant.CanOrd)
-module Cset = Set.Make(Constant.CanOrd)
-module Cset_env = Set.Make(Constant.UserOrd)
+module Cset = Cmap.Set
+module Cset_env = Cmap_env.Set
 
 (** {6 Names of mutual inductive types } *)
 
 module MutInd = KerPair
 
-module Mindmap = CMap.Make(MutInd.CanOrd)
-module Mindset = Set.Make(MutInd.CanOrd)
-module Mindmap_env = Map.Make(MutInd.UserOrd)
+module Mindmap = HMap.Make(MutInd.CanOrd)
+module Mindset = Mindmap.Set
+module Mindmap_env = HMap.Make(MutInd.UserOrd)
 
 (** Beware: first inductive has index 0 *)
 (** Beware: first constructor has index 1 *)
diff --git a/kernel/names.mli b/kernel/names.mli
index 4b71766bb..c85cfc433 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -319,8 +319,8 @@ end
 (** The [*_env] modules consider an order on user part of names
    the others consider an order on canonical part of names*)
 module Cpred : Predicate.S with type elt = Constant.t
-module Cset : Set.S with type elt = Constant.t
-module Cset_env  : Set.S with type elt = Constant.t
+module Cset : CSig.SetS with type elt = Constant.t
+module Cset_env  : CSig.SetS with type elt = Constant.t
 module Cmap : Map.ExtS with type key = Constant.t and module Set := Cset
 module Cmap_env : Map.ExtS with type key = Constant.t  and module Set := Cset_env
 
@@ -386,7 +386,7 @@ sig
 
 end
 
-module Mindset : Set.S with type elt = MutInd.t
+module Mindset : CSig.SetS with type elt = MutInd.t
 module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset
 module Mindmap_env : Map.S with type key = MutInd.t
 
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index f584edc3b..b655887d7 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -38,43 +38,9 @@ type constant_key = constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
-module type Map =
-sig
-  type t
-  type key
-  type value
-  val empty : t
-  val add : key -> value -> t -> t
-  val find : key -> t -> value
-  val fold : (key -> value -> 'a -> 'a) -> t -> 'a -> 'a
-end
-
-module Make(M : sig include HMap.HashedType type value end) =
-struct
-  module Map = HMap.Make(M)
-  type t = M.value Map.t
-  let empty = Map.empty
-  let add = Map.add
-  let find = Map.find
-  let fold = Map.fold
-end
-
-module Constants = Make(struct
-  type t = Constant.t
-  type value = constant_key
-  include Constant.UserOrd
-end)
-
-module Inductives = Make(struct
-  type t = MutInd.t
-  type value = mind_key
-  include MutInd.UserOrd
-end)
-
-
 type globals = {
-  env_constants : Constants.t;
-  env_inductives : Inductives.t;
+  env_constants : constant_key Cmap_env.t;
+  env_inductives : mind_key Mindmap_env.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}
 
@@ -115,8 +81,8 @@ let empty_named_context_val = [],[]
 
 let empty_env = {
   env_globals = {
-    env_constants = Constants.empty;
-    env_inductives = Inductives.empty;
+    env_constants = Cmap_env.empty;
+    env_inductives = Mindmap_env.empty;
     env_modules = MPmap.empty;
     env_modtypes = MPmap.empty};
   env_named_context = empty_named_context;
@@ -184,14 +150,14 @@ let env_of_named id env = env
 (* Global constants *)
 
 let lookup_constant_key kn env =
-  Constants.find kn env.env_globals.env_constants
+  Cmap_env.find kn env.env_globals.env_constants
 
 let lookup_constant kn env =
-  fst (Constants.find kn env.env_globals.env_constants)
+  fst (Cmap_env.find kn env.env_globals.env_constants)
 
 (* Mutual Inductives *)
 let lookup_mind kn env =
-  fst (Inductives.find kn env.env_globals.env_inductives)
+  fst (Mindmap_env.find kn env.env_globals.env_inductives)
 
 let lookup_mind_key kn env =
-  Inductives.find kn env.env_globals.env_inductives
+  Mindmap_env.find kn env.env_globals.env_inductives
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index d6f0e7d1c..964d709cf 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -25,26 +25,9 @@ type constant_key = constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
-module type Map =
-sig
-  type t
-  type key
-  type value
-  val empty : t
-  val add : key -> value -> t -> t
-  val find : key -> t -> value
-  val fold : (key -> value -> 'a -> 'a) -> t -> 'a -> 'a
-end
-
-module Constants : Map
-  with type key := Constant.t and type value := constant_key
-
-module Inductives : Map
-  with type key := MutInd.t and type value := mind_key
-
 type globals = {
-  env_constants : Constants.t;
-  env_inductives : Inductives.t;
+  env_constants : constant_key Cmap_env.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 670e115af..bf758b96b 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) = Constants.find kn env.env_globals.env_constants in
+  let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in
   let cb = {cb with const_inline_code = true} in
-  let new_constants = Constants.add kn (cb,r) env.env_globals.env_constants in
+  let new_constants = Cmap_env.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 29297058e..395119083 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 =
-    Pre_env.Constants.fold (fun c (body,_) acc ->
+    Cmap_env.fold (fun c (body,_) acc ->
       let kn = user_con c in
       if matches (modpath kn) then
         acc++fnl()++hov 2 (print_constant kn body)