diff options
| -rw-r--r-- | kernel/environ.ml | 26 | ||||
| -rw-r--r-- | kernel/environ.mli | 8 | ||||
| -rw-r--r-- | library/global.ml | 41 | ||||
| -rw-r--r-- | library/global.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
5 files changed, 39 insertions, 40 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 3b7e3ae544..e341412294 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -440,6 +440,16 @@ let constant_value_and_type env (kn, u) = | Undef _ -> None in b', cb.const_type, Univ.Constraint.empty +let body_of_constant_body env cb = + let otab = opaque_tables env in + match cb.const_body with + | Undef _ -> + None + | Def c -> + Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb) + | OpaqueDef o -> + Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb) + (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) @@ -694,6 +704,22 @@ let is_polymorphic env r = | IndRef ind -> polymorphic_ind ind env | ConstructRef cstr -> polymorphic_ind (inductive_of_constructor cstr) env +let is_template_polymorphic env r = + let open Names.GlobRef in + match r with + | VarRef _id -> false + | ConstRef _c -> false + | IndRef ind -> template_polymorphic_ind ind env + | ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env + +let is_type_in_type env r = + let open Names.GlobRef in + match r with + | VarRef _id -> false + | ConstRef c -> type_in_type_constant c env + | IndRef ind -> type_in_type_ind ind env + | ConstructRef cstr -> type_in_type_ind (inductive_of_constructor cstr) env + (*spiwack: the following functions assemble the pieces of the retroknowledge note that the "consistent" register function is available in the module Safetyping, Environ only synchronizes the proactive and the reactive parts*) diff --git a/kernel/environ.mli b/kernel/environ.mli index 43bfe7c2fb..0255581749 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -211,6 +211,12 @@ val constant_value_and_type : env -> Constant.t puniverses -> polymorphic *) val constant_context : env -> Constant.t -> Univ.AUContext.t +(** Returns the body of the constant if it has any, and the polymorphic context + it lives in. For monomorphic constant, the latter is empty, and for + polymorphic constants, the term contains De Bruijn universe variables that + need to be instantiated. *) +val body_of_constant_body : env -> constant_body -> (Constr.constr * Univ.AUContext.t) option + (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) @@ -320,6 +326,8 @@ val apply_to_hyp : named_context_val -> variable -> val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declaration) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val val is_polymorphic : env -> Names.GlobRef.t -> bool +val is_template_polymorphic : env -> GlobRef.t -> bool +val is_type_in_type : env -> GlobRef.t -> bool open Retroknowledge (** functions manipulating the retroknowledge diff --git a/library/global.ml b/library/global.ml index 3781ff3230..009f498a9e 100644 --- a/library/global.ml +++ b/library/global.ml @@ -128,19 +128,7 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) let opaque_tables () = Environ.opaque_tables (env ()) -let instantiate cb c = - let open Declarations in - match cb.const_universes with - | Monomorphic_const _ -> c, Univ.AUContext.empty - | Polymorphic_const ctx -> c, ctx - -let body_of_constant_body cb = - let open Declarations in - let otab = opaque_tables () in - match cb.const_body with - | Undef _ -> None - | Def c -> Some (instantiate cb (Mod_subst.force_constr c)) - | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o)) +let body_of_constant_body ce = body_of_constant_body (env ()) ce let body_of_constant cst = body_of_constant_body (lookup_constant cst) @@ -165,8 +153,6 @@ let import c u d = globalize (Safe_typing.import c u d) let env_of_context hyps = reset_with_named_context hyps (env()) -open Globnames - let constr_of_global_in_context = Typeops.constr_of_global_in_context let type_of_global_in_context = Typeops.type_of_global_in_context @@ -175,21 +161,9 @@ let universes_of_global gr = let is_polymorphic r = Environ.is_polymorphic (env()) r -let is_template_polymorphic r = - let env = env() in - match r with - | VarRef id -> false - | ConstRef c -> false - | IndRef ind -> Environ.template_polymorphic_ind ind env - | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env - -let is_type_in_type r = - let env = env() in - match r with - | VarRef id -> false - | ConstRef c -> Environ.type_in_type_constant c env - | IndRef ind -> Environ.type_in_type_ind ind env - | ConstructRef cstr -> Environ.type_in_type_ind (inductive_of_constructor cstr) env +let is_template_polymorphic r = is_template_polymorphic (env ()) r + +let is_type_in_type r = is_type_in_type (env ()) r let current_modpath () = Safe_typing.current_modpath (safe_env ()) @@ -209,10 +183,3 @@ let register_inline c = globalize0 (Safe_typing.register_inline c) let set_strategy k l = GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l) - -let set_reduction_sharing b = - let env = safe_env () in - let flags = Environ.typing_flags (Safe_typing.env_of_safe_env env) in - let flags = { flags with Declarations.share_reduction = b } in - let env = Safe_typing.set_typing_flags flags env in - GlobalSafeEnv.set_safe_env env diff --git a/library/global.mli b/library/global.mli index 42a8005a4f..5b0ff11b71 100644 --- a/library/global.mli +++ b/library/global.mli @@ -150,8 +150,6 @@ val register_inline : Constant.t -> unit val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit -val set_reduction_sharing : bool -> unit - (* Modifies the global state, registering new universes *) val current_modpath : unit -> ModPath.t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1190d73258..4df50a5e23 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1536,7 +1536,7 @@ let _ = optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction); - optwrite = (fun b -> Global.set_reduction_sharing b) } + optwrite = (fun b -> Global.set_typing_flags { (Global.typing_flags ()) with Declarations.share_reduction = b }) } let _ = declare_bool_option |