diff options
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 48 |
1 files changed, 38 insertions, 10 deletions
diff --git a/library/global.ml b/library/global.ml index a8121d15f..c56bc9e77 100644 --- a/library/global.ml +++ b/library/global.ml @@ -70,9 +70,12 @@ let globalize_with_summary fs f = let i2l = Label.of_id -let push_named_assum a = globalize (Safe_typing.push_named_assum a) -let push_named_def d = globalize (Safe_typing.push_named_def d) +let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) +let push_named_def d = globalize0 (Safe_typing.push_named_def d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) +let push_context_set c = globalize0 (Safe_typing.push_context_set c) +let push_context c = globalize0 (Safe_typing.push_context c) + let set_engagement c = globalize0 (Safe_typing.set_engagement c) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) @@ -101,6 +104,7 @@ let named_context_val () = named_context_val (env()) let lookup_named id = lookup_named id (env()) let lookup_constant kn = lookup_constant kn (env()) let lookup_inductive ind = Inductive.lookup_mind_specif (env()) ind +let lookup_pinductive (ind,_) = Inductive.lookup_mind_specif (env()) ind let lookup_mind kn = lookup_mind kn (env()) let lookup_module mp = lookup_module mp (env()) @@ -139,19 +143,43 @@ let env_of_context hyps = open Globnames -let type_of_reference env = function +(** Build a fresh instance for a given context, its associated substitution and + the instantiated constraints. *) + +let type_of_global_unsafe r = + let env = env() in + match r with | VarRef id -> Environ.named_type id env - | ConstRef c -> Typeops.type_of_constant env c + | ConstRef c -> + let cb = Environ.lookup_constant c env in cb.Declarations.const_type + | IndRef ind -> + let (mib, oib) = Inductive.lookup_mind_specif env ind in + oib.Declarations.mind_arity.Declarations.mind_user_arity + | ConstructRef cstr -> + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + let inst = Univ.UContext.instance mib.Declarations.mind_universes in + Inductive.type_of_constructor (cstr,inst) specif + + +let is_polymorphic r = + let env = env() in + match r with + | VarRef id -> false + | ConstRef c -> + let cb = Environ.lookup_constant c env in cb.Declarations.const_polymorphic | IndRef ind -> - let specif = Inductive.lookup_mind_specif env ind in - Inductive.type_of_inductive env specif + let (mib, oib) = Inductive.lookup_mind_specif env ind in + mib.Declarations.mind_polymorphic | ConstructRef cstr -> - let specif = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Inductive.type_of_constructor cstr specif + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + mib.Declarations.mind_polymorphic -let type_of_global t = type_of_reference (env ()) t +let current_dirpath () = + Safe_typing.current_dirpath (safe_env ()) +let with_global f = + let (a, ctx) = f (env ()) (current_dirpath ()) in + push_context_set ctx; a (* spiwack: register/unregister functions for retroknowledge *) let register field value by_clause = |