From 3984f3c1db51f7b788ad49eafb7647774e8d1f53 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Jun 2018 14:04:25 +0200 Subject: Make Environ.globals abstract. --- dev/top_printers.ml | 2 +- kernel/environ.ml | 8 ++++++-- kernel/environ.mli | 14 ++++++-------- kernel/safe_typing.ml | 2 +- vernac/vernacentries.ml | 14 ++++++-------- 5 files changed, 20 insertions(+), 20 deletions(-) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 811abd67f..ab679a71c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -232,7 +232,7 @@ let ppenv e = pp let ppenvwithcst e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ - str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).env_globals.env_constants (mt ()) ++ str "}") + str "{" ++ Environ.fold_constants (fun a _ s -> Constant.print a ++ spc () ++ s) e (mt ()) ++ str "}") let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x)) diff --git a/kernel/environ.ml b/kernel/environ.ml index 0e34a7165..224b6d5b8 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -55,7 +55,8 @@ type globals = { env_projections : projection_body Cmap_env.t; env_inductives : mind_key Mindmap_env.t; env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t} + env_modtypes : module_type_body MPmap.t; +} type stratification = { env_universes : UGraph.t; @@ -86,7 +87,7 @@ type rel_context_val = { } type env = { - env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_globals : globals; env_named_context : named_context_val; (* section variables *) env_rel_context : rel_context_val; env_nb_rel : int; @@ -208,6 +209,9 @@ let lookup_named_val id env = 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 + (* Global constants *) let lookup_constant_key kn env = diff --git a/kernel/environ.mli b/kernel/environ.mli index 8928b32f1..4c637bf78 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -46,13 +46,8 @@ type constant_key = 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_projections : projection_body Cmap_env.t; - env_inductives : mind_key Mindmap_env.t; - env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t -} +type globals +(** globals = constants + projections + inductive types + modules + module-types *) type stratification = { env_universes : UGraph.t; @@ -70,7 +65,7 @@ type rel_context_val = private { } type env = private { - env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_globals : globals; env_named_context : named_context_val; (* section variables *) env_rel_context : rel_context_val; env_nb_rel : int; @@ -175,6 +170,9 @@ val reset_with_named_context : named_context_val -> env -> env (** This removes the [n] last declarations from the rel context *) val pop_rel_context : int -> env -> env +(** Useful for printing *) +val fold_constants : (Constant.t -> constant_body -> 'a -> 'a) -> env -> 'a -> 'a + (** {5 Global constants } {6 Add entries to global environment } *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 12c82e20d..caa935506 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -918,7 +918,7 @@ let register_inline kn senv = if not (evaluable_constant kn senv.env) then CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected"); let env = senv.env in - let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in + let cb = lookup_constant kn env in let cb = {cb with const_inline_code = true} in let env = add_constant kn cb env in { senv with env} diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 43c974846..6d1abeca1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -263,15 +263,13 @@ let print_namespace ns = let matches mp = match match_modulepath ns mp with | Some [] -> true | _ -> false in - let constants = (Global.env ()).Environ.env_globals.Environ.env_constants in let constants_in_namespace = - Cmap_env.fold (fun c (body,_) acc -> - let kn = Constant.user c in - if matches (KerName.modpath kn) then - acc++fnl()++hov 2 (print_constant kn body) - else - acc - ) constants (str"") + Environ.fold_constants (fun c body acc -> + let kn = Constant.user c in + if matches (KerName.modpath kn) + then acc++fnl()++hov 2 (print_constant kn body) + else acc) + (Global.env ()) (str"") in (print_list Id.print ns)++str":"++fnl()++constants_in_namespace -- cgit v1.2.3