diff options
| -rw-r--r-- | kernel/environ.ml | 66 | ||||
| -rw-r--r-- | kernel/environ.mli | 16 |
2 files changed, 50 insertions, 32 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 4a2aeea22d..98d66cafa1 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -50,12 +50,19 @@ type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref -type globals = { - 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; -} +module Globals = struct + + type view = + { constants : constant_key Cmap_env.t + ; inductives : mind_key Mindmap_env.t + ; modules : module_body MPmap.t + ; modtypes : module_type_body MPmap.t + } + + type t = view + + let view x = x +end type stratification = { env_universes : UGraph.t; @@ -88,7 +95,7 @@ type rel_context_val = { } type env = { - env_globals : globals; + env_globals : Globals.t; env_named_context : named_context_val; (* section variables *) env_rel_context : rel_context_val; env_nb_rel : int; @@ -110,11 +117,12 @@ let empty_rel_context_val = { } let empty_env = { - env_globals = { - env_constants = Cmap_env.empty; - env_inductives = Mindmap_env.empty; - env_modules = MPmap.empty; - env_modtypes = MPmap.empty}; + env_globals = + { Globals.constants = Cmap_env.empty + ; inductives = Mindmap_env.empty + ; modules = MPmap.empty + ; modtypes = MPmap.empty + }; env_named_context = empty_named_context_val; env_rel_context = empty_rel_context_val; env_nb_rel = 0; @@ -215,29 +223,29 @@ let lookup_named_ctxt id ctxt = fst (Id.Map.find id ctxt.env_named_map) let fold_constants f env acc = - Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc + Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.Globals.constants acc let fold_inductives f env acc = - Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_inductives acc + Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.Globals.inductives acc (* Global constants *) let lookup_constant_key kn env = - Cmap_env.find kn env.env_globals.env_constants + Cmap_env.find kn env.env_globals.Globals.constants let lookup_constant kn env = - fst (Cmap_env.find kn env.env_globals.env_constants) + fst (Cmap_env.find kn env.env_globals.Globals.constants) (* Mutual Inductives *) let lookup_mind kn env = - fst (Mindmap_env.find kn env.env_globals.env_inductives) + fst (Mindmap_env.find kn env.env_globals.Globals.inductives) let mind_context env mind = let mib = lookup_mind mind env in Declareops.inductive_polymorphic_context mib let lookup_mind_key kn env = - Mindmap_env.find kn env.env_globals.env_inductives + Mindmap_env.find kn env.env_globals.Globals.inductives let oracle env = env.env_typing_flags.conv_oracle let set_oracle env o = @@ -468,10 +476,10 @@ let no_link_info = NotLinked let add_constant_key kn cb linkinfo env = let new_constants = - Cmap_env.add kn (cb,(ref linkinfo, ref None)) env.env_globals.env_constants in + Cmap_env.add kn (cb,(ref linkinfo, ref None)) env.env_globals.Globals.constants in let new_globals = { env.env_globals with - env_constants = new_constants } in + Globals.constants = new_constants } in { env with env_globals = new_globals } let add_constant kn cb env = @@ -598,10 +606,10 @@ let template_polymorphic_pind (ind,u) env = else template_polymorphic_ind ind env let add_mind_key kn (_mind, _ as mind_key) env = - let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in + let new_inds = Mindmap_env.add kn mind_key env.env_globals.Globals.inductives in let new_globals = { env.env_globals with - env_inductives = new_inds; } in + Globals.inductives = new_inds; } in { env with env_globals = new_globals } let add_mind kn mib env = @@ -688,22 +696,22 @@ let keep_hyps env needed = let add_modtype mtb env = let mp = mtb.mod_mp in - let new_modtypes = MPmap.add mp mtb env.env_globals.env_modtypes in - let new_globals = { env.env_globals with env_modtypes = new_modtypes } in + let new_modtypes = MPmap.add mp mtb env.env_globals.Globals.modtypes in + let new_globals = { env.env_globals with Globals.modtypes = new_modtypes } in { env with env_globals = new_globals } let shallow_add_module mb env = let mp = mb.mod_mp in - let new_mods = MPmap.add mp mb env.env_globals.env_modules in - let new_globals = { env.env_globals with env_modules = new_mods } in + let new_mods = MPmap.add mp mb env.env_globals.Globals.modules in + let new_globals = { env.env_globals with Globals.modules = new_mods } in { env with env_globals = new_globals } let lookup_module mp env = - MPmap.find mp env.env_globals.env_modules + MPmap.find mp env.env_globals.Globals.modules -let lookup_modtype mp env = - MPmap.find mp env.env_globals.env_modtypes +let lookup_modtype mp env = + MPmap.find mp env.env_globals.Globals.modtypes (*s Judgments. *) diff --git a/kernel/environ.mli b/kernel/environ.mli index f7de98dcfb..5af2a7288b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -46,8 +46,18 @@ type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref -type globals -(** globals = constants + projections + inductive types + modules + module-types *) +module Globals : sig + type t + + type view = + { constants : constant_key Cmap_env.t + ; inductives : mind_key Mindmap_env.t + ; modules : module_body MPmap.t + ; modtypes : module_type_body MPmap.t + } + + val view : t -> view +end type stratification = { env_universes : UGraph.t; @@ -67,7 +77,7 @@ type rel_context_val = private { } type env = private { - env_globals : globals; + env_globals : Globals.t; env_named_context : named_context_val; (* section variables *) env_rel_context : rel_context_val; env_nb_rel : int; |