diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-11-08 11:31:22 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:58 +0200 |
| commit | 1ed00e4f8cded2a2024b66c3f7f4deee6ecd7c83 (patch) | |
| tree | 471afc13a25bfe689d30447a6042c9f62c72f92e /library/global.ml | |
| parent | 62fb849cf9410ddc2d9f355570f4fb859f3044c3 (diff) | |
- Fix bug preventing apply from unfolding Fixpoints.
- Remove Universe Polymorphism flags everywhere.
- Properly infer, discharge template arities and fix substitution inside them
(kernel code to check for correctness).
- Fix tactics that were supposing universe polymorphic constants/inductives to
be parametric on that status. Required to make interp_constr* return the whole evar
universe context now.
- Fix the univ/level/instance hashconsing to respect the fact that marshalling doesn't preserve sharing,
sadly losing most of its benefits.
Short-term solution is to add hashes to these for faster comparison, longer term requires rewriting
all serialization code.
Conflicts:
kernel/univ.ml
tactics/tactics.ml
theories/Logic/EqdepFacts.v
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 36 |
1 files changed, 28 insertions, 8 deletions
diff --git a/library/global.ml b/library/global.ml index 74a2a1c0e..6c088e542 100644 --- a/library/global.ml +++ b/library/global.ml @@ -189,18 +189,38 @@ let type_of_global_in_context env r = let inst = Univ.UContext.instance univs in Inductive.type_of_constructor (cstr,inst) specif, univs +let universes_of_global env r = + let open Declarations in + match r with + | VarRef id -> Univ.UContext.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + Declareops.universes_of_constant cb + | IndRef ind -> + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + mib.mind_universes + | ConstructRef cstr -> + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + mib.mind_universes + +let universes_of_global gr = + universes_of_global (env ()) gr + 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 (mib, oib) = Inductive.lookup_mind_specif env ind in - mib.Declarations.mind_polymorphic - | ConstructRef cstr -> - let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - mib.Declarations.mind_polymorphic + | ConstRef c -> Environ.polymorphic_constant c env + | IndRef ind -> Environ.polymorphic_ind ind env + | ConstructRef cstr -> Environ.polymorphic_ind (inductive_of_constructor cstr) env + +let is_template_polymorphic r = + let env = env() in + match r with + | VarRef id -> false + | ConstRef c -> Environ.template_polymorphic_constant c env + | IndRef ind -> Environ.template_polymorphic_ind ind env + | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env let current_dirpath () = Safe_typing.current_dirpath (safe_env ()) |