diff options
-rw-r--r-- | kernel/environ.ml | 2 | ||||
-rw-r--r-- | kernel/names.mli | 2 | ||||
-rw-r--r-- | kernel/pre_env.ml | 51 | ||||
-rw-r--r-- | kernel/pre_env.mli | 18 |
4 files changed, 51 insertions, 22 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 0bf3923e4..a25714d77 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -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 = Mindmap_env.add kn mind_key env.env_globals.env_inductives in + let new_inds = Inductives.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.mli b/kernel/names.mli index 3b7de68d9..4b71766bb 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -363,11 +363,13 @@ sig module CanOrd : sig val compare : t -> t -> int val equal : t -> t -> bool + val hash : t -> int end module UserOrd : sig val compare : t -> t -> int val equal : t -> t -> bool + val hash : t -> int end val equal : t -> t -> bool diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 3509ccf0c..f584edc3b 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -38,24 +38,43 @@ type constant_key = constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref -module Constants = +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 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 + 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 : mind_key Mindmap_env.t; + env_inductives : Inductives.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t} @@ -97,7 +116,7 @@ let empty_named_context_val = [],[] let empty_env = { env_globals = { env_constants = Constants.empty; - env_inductives = Mindmap_env.empty; + env_inductives = Inductives.empty; env_modules = MPmap.empty; env_modtypes = MPmap.empty}; env_named_context = empty_named_context; @@ -172,7 +191,7 @@ let lookup_constant kn env = (* Mutual Inductives *) let lookup_mind kn env = - fst (Mindmap_env.find kn env.env_globals.env_inductives) + fst (Inductives.find kn env.env_globals.env_inductives) let lookup_mind_key kn env = - Mindmap_env.find kn env.env_globals.env_inductives + Inductives.find kn env.env_globals.env_inductives diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 4596b23aa..d6f0e7d1c 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -25,18 +25,26 @@ type constant_key = constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref -module Constants : +module type Map = sig type t + type key + type value 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 + 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 : mind_key Mindmap_env.t; + env_inductives : Inductives.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t} |