From 988aab80e03e593c76869b113c5bcc043209d952 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 9 Oct 2018 20:11:45 +0200 Subject: Cleaning layout typeops.mli. --- kernel/typeops.mli | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'kernel') diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 57acdfe4b5..515e22c99b 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -54,11 +54,10 @@ val type_of_variable : env -> variable -> types val judge_of_variable : env -> variable -> unsafe_judgment (** {6 type of a constant } *) - +val type_of_constant_in : env -> pconstant -> types val judge_of_constant : env -> pconstant -> unsafe_judgment (** {6 type of an applied projection } *) - val judge_of_projection : env -> Projection.t -> unsafe_judgment -> unsafe_judgment (** {6 Type of application. } *) @@ -89,9 +88,7 @@ val judge_of_cast : unsafe_judgment (** {6 Inductive types. } *) - val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment - val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) @@ -99,7 +96,7 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -val type_of_constant_in : env -> pconstant -> types +(** {6 Miscellaneous. } *) (** Check that hyps are included in env and fails with error otherwise *) val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit -- cgit v1.2.3 From df6b72e348543a289a2ef3f89f32c905add564bc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 9 Oct 2018 20:22:59 +0200 Subject: Moving Global.type_of_global_in_context to Typeops. It is purely functional, so no need for it to be in global now that GlobRef.t are in the kernel. Also updated the comments. --- kernel/typeops.ml | 24 ++++++++++++++++++++++++ kernel/typeops.mli | 10 ++++++++++ 2 files changed, 34 insertions(+) (limited to 'kernel') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 164a47dd9a..c3a964d2db 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -319,6 +319,30 @@ let check_fixpoint env lna lar vdef vdeft = with NotConvertibleVect i -> error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar +(* Global references *) + +let type_of_global_in_context env r = + let open Names.GlobRef in + match r with + | VarRef id -> Environ.named_type id env, Univ.AUContext.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + let univs = Declareops.constant_polymorphic_context cb in + cb.Declarations.const_type, univs + | IndRef ind -> + let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in + let univs = Declareops.inductive_polymorphic_context mib in + let inst = Univ.make_abstract_instance univs in + let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in + Inductive.type_of_inductive env (specif, inst), univs + | ConstructRef cstr -> + let (mib,_ as specif) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) + in + let univs = Declareops.inductive_polymorphic_context mib in + let inst = Univ.make_abstract_instance univs in + Inductive.type_of_constructor (cstr,inst) specif, univs + (************************************************************************) (************************************************************************) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 515e22c99b..e83c1b3dc5 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -96,6 +96,16 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment +(** {6 Type of global references. } *) + +val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t +(** Returns the type of the global reference, by creating a fresh + instance of polymorphic references and computing their + instantiated universe context. The type should not be used + without pushing it's universe context in the environmnent of + usage. For non-universe-polymorphic constants, it does not + matter. *) + (** {6 Miscellaneous. } *) (** Check that hyps are included in env and fails with error otherwise *) -- cgit v1.2.3 From 09d0ba708a96125632344f2f994b45e9075fc303 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 9 Oct 2018 20:46:15 +0200 Subject: Moving Global.constr_of_global_in_context to Typeops. It is purely functional, so no need for it to be in global now that GlobRef.t are in the kernel. --- kernel/typeops.ml | 22 ++++++++++++++++++++++ kernel/typeops.mli | 8 ++++++++ 2 files changed, 30 insertions(+) (limited to 'kernel') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index c3a964d2db..3481d3bedb 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -343,6 +343,28 @@ let type_of_global_in_context env r = let inst = Univ.make_abstract_instance univs in Inductive.type_of_constructor (cstr,inst) specif, univs +(* Build a fresh instance for a given context, its associated substitution and + the instantiated constraints. *) + +let constr_of_global_in_context env r = + let open GlobRef in + match r with + | VarRef id -> mkVar id, Univ.AUContext.empty + | ConstRef c -> + let cb = lookup_constant c env in + let univs = Declareops.constant_polymorphic_context cb in + mkConstU (c, Univ.make_abstract_instance univs), univs + | IndRef ind -> + let (mib,_) = Inductive.lookup_mind_specif env ind in + let univs = Declareops.inductive_polymorphic_context mib in + mkIndU (ind, Univ.make_abstract_instance univs), univs + | ConstructRef cstr -> + let (mib,_) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) + in + let univs = Declareops.inductive_polymorphic_context mib in + mkConstructU (cstr, Univ.make_abstract_instance univs), univs + (************************************************************************) (************************************************************************) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index e83c1b3dc5..1fd070d9d5 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -106,6 +106,14 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t usage. For non-universe-polymorphic constants, it does not matter. *) +(** {6 Building a term from a global reference *) + +(** Map a global reference to a term in its local universe + context. The term should not be used without pushing it's universe + context in the environmnent of usage. For non-universe-polymorphic + constants, it does not matter. *) +val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t + (** {6 Miscellaneous. } *) (** Check that hyps are included in env and fails with error otherwise *) -- cgit v1.2.3