diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-12 14:49:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 15:14:45 +0200 |
| commit | 71563ebb86a83bc7cdfc17f58493f59428d764b0 (patch) | |
| tree | 247d33d8021ede65e34ac6d2de3d4224f0c80e90 /library | |
| parent | 1014de55656c2698500089d940a12f7e4b26a0de (diff) | |
Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 19 | ||||
| -rw-r--r-- | library/global.mli | 7 |
2 files changed, 26 insertions, 0 deletions
diff --git a/library/global.ml b/library/global.ml index 3a74f535d..5fff26566 100644 --- a/library/global.ml +++ b/library/global.ml @@ -191,6 +191,25 @@ let type_of_global_unsafe r = let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in Inductive.type_of_constructor (cstr,inst) specif +let constr_of_global_in_context env r = + let open Constr in + match r with + | VarRef id -> mkVar id, Univ.AUContext.empty + | ConstRef c -> + let cb = Environ.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, oib as specif) = 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,oib as specif) = + 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 + let type_of_global_in_context env r = match r with | VarRef id -> Environ.named_type id env, Univ.AUContext.empty diff --git a/library/global.mli b/library/global.mli index d6d2f1f85..0f1cec44a 100644 --- a/library/global.mli +++ b/library/global.mli @@ -122,6 +122,13 @@ val is_polymorphic : Globnames.global_reference -> bool val is_template_polymorphic : Globnames.global_reference -> bool val is_type_in_type : Globnames.global_reference -> bool +val constr_of_global_in_context : Environ.env -> + Globnames.global_reference -> Constr.types * Univ.AUContext.t +(** Returns the type of the constant in its local 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. *) + val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.types * Univ.AUContext.t (** Returns the type of the constant in its local universe |