diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 5 | ||||
| -rw-r--r-- | library/global.ml | 24 | ||||
| -rw-r--r-- | library/global.mli | 3 | ||||
| -rw-r--r-- | library/universes.ml | 19 | ||||
| -rw-r--r-- | library/universes.mli | 13 |
5 files changed, 56 insertions, 8 deletions
diff --git a/library/declare.ml b/library/declare.ml index 41f50753f..820e72369 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -253,7 +253,10 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) = let cd = (* We deal with side effects of non-opaque constants *) match cd with | Entries.DefinitionEntry ({ - const_entry_opaque = false; const_entry_body = bo } as de) -> + const_entry_opaque = false; const_entry_body = bo } as de) + | Entries.DefinitionEntry ({ + const_entry_polymorphic = true; const_entry_body = bo } as de) + -> let pt, seff = Future.force bo in if Declareops.side_effects_is_empty seff then cd else begin diff --git a/library/global.ml b/library/global.ml index c56bc9e77..16b07db25 100644 --- a/library/global.ml +++ b/library/global.ml @@ -160,6 +160,30 @@ let type_of_global_unsafe r = let inst = Univ.UContext.instance mib.Declarations.mind_universes in Inductive.type_of_constructor (cstr,inst) specif +let type_of_global_in_context env r = + let open Declarations in + match r with + | VarRef id -> Environ.named_type id env, Univ.UContext.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + let univs = + if cb.const_polymorphic then Future.force cb.const_universes + else Univ.UContext.empty + in cb.Declarations.const_type, univs + | IndRef ind -> + let (mib, oib) = Inductive.lookup_mind_specif env ind in + let univs = + if mib.mind_polymorphic then mib.mind_universes + else Univ.UContext.empty + in oib.Declarations.mind_arity.Declarations.mind_user_arity, univs + | ConstructRef cstr -> + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + let univs = + if mib.mind_polymorphic then mib.mind_universes + else Univ.UContext.empty + in + let inst = Univ.UContext.instance univs in + Inductive.type_of_constructor (cstr,inst) specif, univs let is_polymorphic r = let env = env() in diff --git a/library/global.mli b/library/global.mli index b6825ffa5..410be961b 100644 --- a/library/global.mli +++ b/library/global.mli @@ -108,7 +108,8 @@ val join_safe_environment : unit -> unit val is_polymorphic : Globnames.global_reference -> bool -(* val type_of_global : Globnames.global_reference -> types Univ.in_universe_context_set *) +val type_of_global_in_context : Environ.env -> + Globnames.global_reference -> Constr.types Univ.in_universe_context val type_of_global_unsafe : Globnames.global_reference -> Constr.types (** {6 Retroknowledge } *) diff --git a/library/universes.ml b/library/universes.ml index 79286792d..c7009b400 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -60,7 +60,7 @@ let fresh_instance_from ctx = let fresh_constant_instance env c = let cb = lookup_constant c env in if cb.Declarations.const_polymorphic then - let (inst,_), ctx = fresh_instance_from (Future.join cb.Declarations.const_universes) in + let (inst,_), ctx = fresh_instance_from (Future.force cb.Declarations.const_universes) in ((c, inst), ctx) else ((c,Instance.empty), ContextSet.empty) @@ -94,7 +94,20 @@ let fresh_global_instance env gr = let constr_of_global gr = let c, ctx = fresh_global_instance (Global.env ()) gr in - Global.push_context_set ctx; c + if not (Univ.ContextSet.is_empty ctx) then + if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then + (* Should be an error as we might forget constraints, allow for now + to make firstorder work with "using" clauses *) + c + else raise (Invalid_argument + ("constr_of_global: globalization of polymorphic reference " ^ + Pp.string_of_ppcmds (Nametab.pr_global_env Id.Set.empty gr) ^ + " would forget universes.")) + else c + +let unsafe_constr_of_global gr = + let c, ctx = fresh_global_instance (Global.env ()) gr in + c let constr_of_global_univ (gr,u) = match gr with @@ -132,7 +145,7 @@ let type_of_reference env r = | ConstRef c -> let cb = Environ.lookup_constant c env in if cb.const_polymorphic then - let (inst, subst), ctx = fresh_instance_from (Future.join cb.const_universes) in + let (inst, subst), ctx = fresh_instance_from (Future.force cb.const_universes) in Vars.subst_univs_constr subst cb.const_type, ctx else cb.const_type, ContextSet.empty diff --git a/library/universes.mli b/library/universes.mli index 47876269a..fb662d7a3 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -136,12 +136,19 @@ val normalize_universe_opt_subst : universe_opt_subst ref -> val normalize_universe_subst : universe_subst ref -> (universe -> universe) -(** Create a fresh global in the global environment, shouldn't be done while - building polymorphic values as the constraints are added to the global - environment already. *) +(** Create a fresh global in the global environment, without side effects. + BEWARE: this raises an ANOMALY on polymorphic constants/inductives: + the constraints should be properly added to an evd. + See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for + the proper way to get a fresh copy of a global reference. *) val constr_of_global : Globnames.global_reference -> constr +(** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic + reference by building a "dummy" universe instance that is not recorded + anywhere. The constraints are forgotten as well. DO NOT USE in new code. *) +val unsafe_constr_of_global : Globnames.global_reference -> constr + val type_of_global : Globnames.global_reference -> types in_universe_context_set (** Full universes substitutions into terms *) |