diff options
| -rw-r--r-- | kernel/environ.ml | 4 | ||||
| -rw-r--r-- | kernel/names.ml | 14 | ||||
| -rw-r--r-- | kernel/names.mli | 6 | ||||
| -rw-r--r-- | kernel/pre_env.ml | 50 | ||||
| -rw-r--r-- | kernel/pre_env.mli | 21 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
7 files changed, 25 insertions, 76 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index a25714d779..15db39328c 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 21d22baffb..03826cda7c 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 4b71766bb0..c85cfc433f 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 f584edc3b0..b655887d70 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 d6f0e7d1cd..964d709cff 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 670e115af8..bf758b96b1 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 29297058eb..3951190832 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) |