From d1091555104e0198eaaa94a1bb69e96d5cc73447 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 29 Oct 2018 11:27:15 +0100 Subject: Seeing Global purely as a wrapper on top of kernel functions. --- kernel/environ.ml | 26 ++++++++++++++++++++++++++ kernel/environ.mli | 8 ++++++++ 2 files changed, 34 insertions(+) (limited to 'kernel') 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 -- cgit v1.2.3 From c3ea3cd8a2bd29fc0129e34af4a1689bbf7519a5 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 31 Oct 2018 16:09:43 +0100 Subject: Introduce Safe_typing.set_share_reduction --- kernel/safe_typing.ml | 4 ++++ kernel/safe_typing.mli | 1 + 2 files changed, 5 insertions(+) (limited to 'kernel') diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 12f9592ab7..90b89995ee 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -194,6 +194,10 @@ let set_engagement c senv = let set_typing_flags c senv = { senv with env = Environ.set_typing_flags c senv.env } +let set_share_reduction b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with share_reduction = b } senv + (** Check that the engagement [c] expected by a library matches the current (initial) one *) let check_engagement env expected_impredicative_set = diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 26fa91adbd..ea288b771e 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -137,6 +137,7 @@ val add_constraints : (** Setting the type theory flavor *) val set_engagement : Declarations.engagement -> safe_transformer0 val set_typing_flags : Declarations.typing_flags -> safe_transformer0 +val set_share_reduction : bool -> safe_transformer0 (** {6 Interactive module functions } *) -- cgit v1.2.3 From c367e7cd962089d2932b986e5764b8e3844ad4b0 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 31 Oct 2018 16:12:26 +0100 Subject: Use standard combinator for Global.set_strategy --- kernel/safe_typing.ml | 2 +- kernel/safe_typing.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 90b89995ee..779e05ee0c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1194,7 +1194,7 @@ loaded by side-effect once and for all (like it is done in OCaml). Would this be correct with respect to undo's and stuff ? *) -let set_strategy e k l = { e with env = +let set_strategy k l e = { e with env = (Environ.set_oracle e.env (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) } diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index ea288b771e..443b5cfd73 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -218,4 +218,4 @@ val register : val register_inline : Constant.t -> safe_transformer0 val set_strategy : - safe_environment -> Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_environment + Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0 -- cgit v1.2.3