Merge PR #7745: Make type Environ.globals abstract + simplify Environ.retroknowledge

11 files changed, 30 insertions, 26 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/clambda.ml b/kernel/clambda.ml
index b722e4200..f1b6f3dff 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -814,7 +814,7 @@ let optimize_lambda lam =
 
 let lambda_of_constr ~optimize genv c =
   let env = Renv.make genv in
-  let ids = List.rev_map Context.Rel.Declaration.get_name genv.env_rel_context.env_rel_ctx in
+  let ids = List.rev_map Context.Rel.Declaration.get_name (rel_context genv) in
   Renv.push_rels env (Array.of_list ids);
   let lam = lambda_of_constr env c in
   let lam = if optimize then optimize_lambda lam else lam in
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..084d3c4de 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 } *)
 
@@ -320,6 +318,7 @@ open Retroknowledge
 (** functions manipulating the retroknowledge 
     @author spiwack *)
 val retroknowledge : (retroknowledge->'a) -> env -> 'a
+[@@ocaml.deprecated "Use the record projection."]
 
 val registered : env -> field -> bool
 
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 74d12f3cd..1748e98a4 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1845,7 +1845,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml =
   in
   let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in
   let auxdefs = List.fold_right get_named_val fv_named auxdefs in
-  let lvl = Context.Rel.length env.env_rel_context.env_rel_ctx in
+  let lvl = Context.Rel.length (rel_context env) in
   let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in
   let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in
   let aux_name = fresh_lname Anonymous in
@@ -1854,7 +1854,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml =
 and compile_rel env sigma univ auxdefs n =
   let open Context.Rel.Declaration in
   let decl = lookup_rel n env in
-  let n = List.length env.env_rel_context.env_rel_ctx - n in
+  let n = List.length (rel_context env) - n in
   match decl with
   | LocalDef (_,t,_) ->
       let code = lambda_of_constr env sigma t in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 244e5e0dd..5843cd543 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -659,7 +659,7 @@ let optimize lam =
 let lambda_of_constr env sigma c =
   set_global_env env;
   let env = Renv.make () in
-  let ids = List.rev_map RelDecl.get_name !global_env.env_rel_context.env_rel_ctx in
+  let ids = List.rev_map RelDecl.get_name (rel_context !global_env) in
   Renv.push_rels env (Array.of_list ids);
   let lam = lambda_of_constr env sigma c in
 (*  if Flags.vm_draw_opt () then begin
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 12c82e20d..f87ec9e02 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -897,9 +897,11 @@ let typing senv = Typeops.infer (env_of_senv senv)
 
 (** {6 Retroknowledge / native compiler } *)
 
+[@@@ocaml.warning "-3"]
 (** universal lifting, used for the "get" operations mostly *)
 let retroknowledge f senv =
   Environ.retroknowledge f (env_of_senv senv)
+[@@@ocaml.warning "+3"]
 
 let register field value by_clause senv =
   (* todo : value closed, by_clause safe, by_clause of the proper type*)
@@ -918,7 +920,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/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 4078a9092..aca77ccd1 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -221,6 +221,7 @@ val delta_of_senv :
 open Retroknowledge
 
 val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a
+[@@ocaml.deprecated "Use the projection of Environ.env"]
 
 val register :
   field -> Retroknowledge.entry -> Constr.constr -> safe_transformer0
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 7319846fb..16d003f67 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -123,7 +123,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
   try
     if const then
       let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in
-      retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd ind) tag, ctyp
+      Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkInd ind) tag, ctyp
     else
       raise Not_found
   with Not_found ->
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 14c9f49b1..bd6062824 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -79,7 +79,7 @@ let construct_of_constr const env tag typ =
   (* spiwack : here be a branch for specific decompilation handled by retroknowledge *)
   try
     if const then
-      ((retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkIndU indu) tag),
+      ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkIndU indu) tag),
        typ) (*spiwack: this may need to be changed in case there are parameters in the
 	               type which may cause a constant value to have an arity.
 	               (type_constructor seems to be all about parameters actually)
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