aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-29 10:05:56 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-29 10:05:56 +0200
commitfc4f18c84bfc421dff55c77aa564abc1ea20f528 (patch)
tree4a9656e44d957f17a8c342e794a8bf2276ea50f3
parent092b74035b73780432a1db9588a7ac54ec6a4721 (diff)
parente7e3714f0fd0e791501acccca3317ed8175c4815 (diff)
Merge PR #7745: Make type Environ.globals abstract + simplify Environ.retroknowledge
-rw-r--r--dev/top_printers.ml2
-rw-r--r--kernel/clambda.ml2
-rw-r--r--kernel/environ.ml8
-rw-r--r--kernel/environ.mli15
-rw-r--r--kernel/nativecode.ml4
-rw-r--r--kernel/nativelambda.ml2
-rw-r--r--kernel/safe_typing.ml4
-rw-r--r--kernel/safe_typing.mli1
-rw-r--r--pretyping/nativenorm.ml2
-rw-r--r--pretyping/vnorm.ml2
-rw-r--r--vernac/vernacentries.ml14
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