Merge PR #8687: Mini reorganization type of global constr of global

2 files changed, 66 insertions, 5 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 164a47dd9a..3481d3bedb 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -319,6 +319,52 @@ 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
+
+(* 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 57acdfe4b5..1fd070d9d5 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,25 @@ 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 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 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 *)
 val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit