aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorMatthieu Sozeau2012-10-10 15:35:36 -0400
committerMatthieu Sozeau2014-05-06 09:58:53 +0200
commita4043608f704f026de7eb5167a109ca48e00c221 (patch)
tree938b6b8cb8d6d5dbaf7be3c62abcc8fdfcd45fc2 /toplevel
parenta2a249211c2ac1e18eff0d4f28e5afc98c137f97 (diff)
This commit adds full universe polymorphism and fast projections to Coq.
Add [Polymorphic] and [Monomorphic] local flag for definitions as well as [Set Universe Polymorphism] global flag to make all following definitions polymorphic. Mainly syntax for now. First part of the big changes to the kernel: - Const, Ind, Construct now come with a universe level instance - It is used for type inference in the kernel, which now also takes a graph as input: actually a set of local universe variables and their constraints. Type inference just checks that the constraints are enough to satisfy its own rules. - Remove polymorphic_arity and _knowing_parameters everywhere: we don't need full applications for polymorphism to apply anymore, as we generate fresh variables at each constant/inductive/constructor application. However knowing_parameters variants might be reinstated later for optimization. - New structures exported in univ.mli: - universe_list for universe level instances - universe_context(_set) for the local universe constraints, also recording which variables will be local and hence generalized after inference if defining a polymorphic ind/constant. - this patch makes coq stop compiling at indtypes.ml Adapt kernel, library, pretyping, tactics and toplevel to universe polymorphism. Various degrees of integration, places where I was not sure what to do or just postponed bigger reorganizations of the code are marked with FIXMEs. Main changes: - Kernel now checks constraints and does not infer them anymore. - The inference functions produce a context of constraints that were checked during inference, useful to do double-checking of the univ. poly. code but might be removed later. - Constant, Inductive entries now have a universe context (local variables and constraints) associated to them. - Printing, debugging functions for the new structures are also implemented. - Now stopping at Logic.v - Lots of new code in kernel/univ.ml that should be reviewed. - kernel/indtypes probably does not do what's right when inferring inductive type constraints. - Adapted evd to use the new universe context structure. - Did not deal with unification/evar_conv. - Add externalisation code for universe level instances. - Support for polymorphism in pretyping/command and proofs/proofview etc. Needed wrapping of [fresh_.._instance] through the evar_map, which contains the local state of universes during type-checking. - Correct the inductive scheme generation to support polymorphism as well. - Have to review kernel code for correctness, and especially rework the computation of universe constraints for inductives. Stops somewhat later in Logic.v - Fix naming of local/toplevel universes to be correctly done at typechecking time: local variables have no dirpath. - Add code to do substitution of universes in modules, not finished yet. - Move fresh_* functions out of kernel, it won't ever build a universe level again! - Adapt a lot of new_Type to use the correct dirpath and declare the new types in the evar_map so we keep track of them. - A bit of code factorization (evd_comb moved, pretype_global). - Refactor more code - Adapt plugins code (sometimes wrong, marked with FIXME) - Fix cases generating unneeded universe (not sure it's ok though) - Fix scheme generation for good, might have opportunity to cleanup the terms later. Init compiles now (which means rewrite, inversion, elim etc.. work as well). - Unsolved issue of pretyping to lower sorts properly (to Prop for example). This has to do with the (Retyping.get_type_of) giving algebraic universes that would appear on the right of constraints. This makes checking for dangling universes at the end of pretyping fail, hence the check in kernel/univ was removed. It should come back when we have a fix for this. - Correctly (?) compute the levels of inductive types. Removed old code pertaining to universe polymorphism. Note that we generate constraint variables for the conclusion of inductive types invariably. - Shrink constraints before going to the kernel, combine substitution of the smaller universe set with normalization of evars (maybe not done everywhere, only ordinary inductives, definitions and proofs) - More API reworks overall. tclPUSHCONTEXT can be used to add fresh universes to the proof goal (used in a few places to get the right instance. - Quick fix for auto that won't work in the long run. It should always have been restricted to take constant references as input, without any loss of generality over constrs. Fix some plugins and insertion of non-polymorphic constants in a module. Now stops in relation classes. Cleanup and move code from kernel to library and from pretyping to library too. Now there is a unique universe counter declared in library/universes.ml along with all the functions to generate new universes and get fresh constant/inductive terms. - Various function renamings - One important change in kernel/univ.ml: now [sup] can be applied to Prop. - Adapt records/classes to universe polymorphism - Now stops in EqDepFacts due to imprecise universe polymorphism. Forgot to git add those files. interp_constr returns the universe context The context is then pushed through the environment (or proof goal sigma). - Fix insertion of constants/inductives in env, pushing constraints to the global env for non-polymorphic ones. - Add Prop as a universe level to do proper type inference with sorts. It is allowed to take [sup] of [Prop] now. - New nf_evar based on new Evd.map(_undefined) - In proofs/logic.ml: conv_leq_goal might create some constraints that are now recorded. - Adapt Program code to universes. Merge with latest trunk + fixes -Use new constr_of_global from universes - fix eqschemes to use polymorphic universes - begin fixing cctac but f_equal still fails - fix [simpl] and rest of tacred - all the eq_constr with mkConst foo should be fixed as well, only partially done - Fix term hashing function to recognize equal terms up to universe instances. - Fix congruence closure to equate terms that differ only in universe instances, these will be resolved by constraints. Add a set of undefined universe variables to unification. Universe variables can now be declared rigid or flexible (unifiable). Flexible variables are resolved at the end of typechecking by instantiating them to their glb, adding upper bound constraints associated to them. Also: - Add polymorphic flag for inductives. - Fix cooking partially - Fix kernel/univ.ml to do normalization of universe expressions at the end of substitution. Correct classes/structures universe inference - Required a bit of extension in Univ to handle Max properly (sup u (u+1)) was returning (max(u,u+1)) for example. - Try a version where substitution of universe expressions for universe levels is allowed at the end of unification. By an invariant this should only instantiate with max() types that are morally "on the right" only. This is controlled using a rigidity attribute of universe variables, also allowing to properly do unification w.r.t. universes during typechecking/inference. - Currently fails in Vectors/Fin.v because case compilation generates "flexible" universes that actually appear in the term... Fix unification of universe variables. - Fix choice of canonical universe in presence of universe constraints, and do so by relying on a trichotomy for universe variables: rigid (won't be substituted), flexible (might be if not substituted by an algebraic) and flexible_alg (always substituted). - Fix romega code and a few more plugins, most of the standard library goes through now. - Had to define some inductives as Polymorphic explicitly to make proofs go through, more to come, and definitions should be polymorphic too, otherwise inconsistencies appear quickly (two uses of the same polymorphic ind through monomorphic functions (like nth on lists of Props and nats) will fix the monomorphic function's universe with eq constraints that are incompatible). - Correct universe polymorphism handling for fixpoint/cofixpoint definitions. - Fix romega to use the right universes for list constructors. - Fix internalization/externalization to deal properly with the implicit parsing of params. - Fix fourier tactic w.r.t. GRefs - Fix substitution saturation of universes. - Fix number syntax plugin. - Fix setoid_ring to take its coefficients in a Set rather than a Type, avoiding a large number of useless universe constraints. - Fix minor checker decl - Fix btauto w.r.t. GRef - Fix proofview to normalize universes in the original types as well. - Fix definitions of projections to not take two universes at the same level, but at different levels instead, avoiding unnecessary constraints that could lower the level of one component depending on the use of the other component. Fix simpl fst, snd to use @fst @snd as they have maximal implicits now. - More simpl snd, fst fixes. - Try to make the nth theory of lists polymorphic. Check with Enrico if this change is ok. Case appearing in RingMicromega's call to congruence l417, through a call to refine -> the_conv_x_leq. Compile everything. - "Fix" checker by deactivating code related to polymorphism, should be updated. - Make most of List.v polymorphic to help with following definitions. - When starting a lemma, normalize w.r.t. universes, so that the types get a fixed universe, not refinable later. - In record, don't assign a fully flexible universe variable to the record type if it is a definitional typeclass, as translate_constant doesn't expect an algebraic universe in the type of a constant. It certainly should though. - Fix micromega code. Fix after rebase. Update printing functions to print the polymorphic status of definitions and their universe context. Refine printing of universe contexts - Fix printer for universe constraints - Rework normalization of constraints to separate the Union-Find result from computation of lubs/glbs. Keep universe contexts of inductives/constants in entries for correct substitution inside modules. Abstract interface to get an instantiation of an inductive with its universe substitution in the kernel (no substitution if the inductive is not polymorphic, even if mind_universes is non-empty). Make fst and snd polymorphic, fix instances in RelationPairs to use different universes for the two elements of a pair. - Fix bug in nf_constraints: was removing Set <= constraints, but should remove Prop <= constraints only. - Make proj1_sig, projT1... polymorphic to avoid weird universe unifications, giving rise to universe inconsistenties. Adapt auto hints to polymorphic references. Really produce polymorphic hints... second try - Remove algebraic universes that can't appear in the goal when taking the type of a lemma to start. Proper handling of universe contexts in clenv and auto so that polymorphic hints are really refreshed at each application. Fix erroneous shadowing of sigma variable. - Make apparent the universe context used in pretyping, including information about flexibility of universe variables. - Fix induction to generate a fresh constant instance with flexible universe variables. Add function to do conversion w.r.t. an evar map and its local universes. - Fix define_evar_as_sort to not forget constraints coming from the refinement. - Do not nf_constraints while we don't have the whole term at hand to substitute in. - Move substitution of full universes to Universes - Normalize universes inside an evar_map when doing nf_evar_map_universes. - Normalize universes at each call to interp_ltac (potentially expensive) Do not normalize all evars at each call to interp_gen in tactics: rather incrementally normalize the terms at hand, supposing the normalization of universes will concern only those appearing in it (dangerous but much more efficient). Do not needlessly generate new universes constraints for projections of records. Correct polymorphic discharge of section variables. Fix autorewrite w.r.t. universes: polymorphic rewrite hints get fresh universe instances at each application. Fix r2l rewrite scheme to support universe polymorphism Fix a bug in l2r_forward scheme and fix congruence scheme to handle polymorphism correctly. Second try at fixing autorewrite, cannot do without pushing the constraints and the set of fresh universe variables into the proof context. - tclPUSHCONTEXT allow to set the ctx universe variables as flexible or rigid - Fix bug in elimschemes, not taking the right sigma Wrong sigma used in leibniz_rewrite Avoid recomputation of bounds for equal universes in normalization of constraints, only the canonical one need to be computed. Make coercions work with universe polymorphic projections. Fix eronneous bound in universes constraint solving. Make kernel reduction and term comparison strictly aware of universe instances, with variants for relaxed comparison that output constraints. Otherwise some constraints that should appear during pretyping don't and we generate unnecessary constraints/universe variables. Have to adapt a few tactics to this new behavior by making them universe aware. - Fix elimschemes to minimize universe variables - Fix coercions to not forget the universe constraints generated by an application - Change universe substitutions to maps instead of assoc lists. - Fix absurd tactic to handle univs properly - Make length and app polymorphic in List, unification sets their levels otherwise. Move to modules for namespace management instead of long names in universe code. More putting things into modules. Change evar_map structure to support an incremental substitution of universes (populated from Eq constraints), allowing safe and fast inference of precise levels, without computing lubs. - Add many printers and reorganize code - Extend nf_evar to normalize universe variables according to the substitution. - Fix ChoiceFacts.v in Logic, no universe inconsistencies anymore. But Diaconescu still has one (something fixes a universe to Set). - Adapt omega, functional induction to the changes. Fix congruence, eq_constr implem, discharge of polymorphic inductives. Fix merge in auto. The [-parameters-matter] option (formerly relevant_equality). Add -parameters-matter to coqc Do compute the param levels at elaboration time if parameters_matter. - Fix generalize tactic - add ppuniverse_subst - Start fixing normalize_universe_context w.r.t. normalize_univ_variables. - Fix HUGE bug in Ltac interpretation not folding the sigma correctly if interpreting a tactic application to multiple arguments. - Fix bug in union of universe substitution. - rename parameters-matter to indices-matter - Fix computation of levels from indices not parameters. - Fixing parsing so that [Polymorphic] can be applied to gallina extensions. - When elaborating definitions, make the universes from the type rigid when checking the term: they should stay abstracted. - Fix typeclasses eauto's handling of universes for exact hints. Rework all the code for infering the levels of inductives and checking their allowed eliminations sorts. This is based on the computation of a natural level for an inductive type I. The natural level [nat] of [I : args -> sort := c1 : A1 -> I t1 .. cn : An -> I tn] is computed by taking the max of the levels of the args (if indices matter) and the levels of the constructor arguments. The declared level [decl] of I is [sort], which might be Prop, Set or some Type u (u fresh or not). If [decl >= nat && not (decl = Prop && n >= 2)], the level of the inductive is [decl], otherwise, _smashing_ occured. If [decl] is impredicative (Prop or Set when Set is impredicative), we accept the declared level, otherwise it's an error. To compute the allowed elimination sorts, we have the following situations: - No smashing occured: all sorts are allowed. (Recall props that are not smashed are Empty/Unitary props) - Some smashing occured: - if [decl] is Type, we allow all eliminations (above or below [decl], not sure why this is justified in general). - if [decl] is Set, we used smashing for impredicativity, so only small sorts are allowed (Prop, Set). - if [decl] is Prop, only logical sorts are allowed: I has either large universes inside it or more than 1 constructor. This does not treat the case where only a Set appeared in I which was previously accepted it seems. All the standard library works with these changes. Still have to cleanup kernel/indtypes.ml. It is a good time to have a whiskey with OJ. Thanks to Peter Lumsdaine for bug reporting: - fix externalisation of universe instances (still appearing when no Printing Universes) - add [convert] and [convert_leq] tactics that keep track of evars and universe constraints. - use them in [exact_check]. Fix odd behavior in inductive type declarations allowing to silently lower a Type i parameter to Set for squashing a naturally Type i inductive to Set. Reinstate the LargeNonPropInductiveNotInType exception. Fix the is_small function not dealing properly with aliases of Prop/Set in Type. Add check_leq in Evd and use it to decide if we're trying to squash an inductive naturally in some Type to Set. - Fix handling of universe polymorphism in typeclasses Class/Instance declarations. - Don't allow lowering a rigid Type universe to Set silently. - Move Ring/Field back to Type. It was silently putting R in Set due to the definition of ring_morph. - Rework inference of universe levels for inductive definitions. - Make fold_left/right polymorphic on both levels A and B (the list's type). They don't have to be at the same level. Handle selective Polymorphic/Monomorphic flag right for records. Remove leftover command Fix after update with latest trunk. Backport patches on HoTT/coq to rebased version of universe polymorphism. - Fix autorewrite wrong handling of universe-polymorphic rewrite rules. Fixes part of issue #7. - Fix the [eq_constr_univs] and add an [leq_constr_univs] to avoid eager equation of universe levels that could just be inequal. Use it during kernel conversion. Fixes issue #6. - Fix a bug in unification that was failing too early if a choice in unification of universes raised an inconsistency. - While normalizing universes, remove Prop in the le part of Max expressions. - Stop rigidifying the universes on the right hand side of a : in definitions. - Now Hints can be declared polymorphic or not. In the first case they must be "refreshed" (undefined universes are renamed) at each application. - Have to refresh the set of universe variables associated to a hint when it can be used multiple times in a single proof to avoid fixing a level... A better & less expensive solution should exist. - Do not include the levels of let-ins as part of records levels. - Fix a NotConvertible uncaught exception to raise a more informative error message. - Better substitution of algebraics in algebraics (for universe variables that can be algebraics). - Fix issue #2, Context was not properly normalizing the universe context. - Fix issue with typeclasses that were not catching UniverseInconsistencies raised by unification, resulting in early failure of proof-search. - Let the result type of definitional classes be an algebraic. - Adapt coercions to universe polymorphic flag (Identity Coercion etc..) - Move away a dangerous call in autoinstance that added constraints for every polymorphic definitions once in the environment for no use. Forgot one part of the last patch on coercions. - Adapt auto/eauto to polymorphic hints as well. - Factor out the function to refresh a clenv w.r.t. undefined universes. Use leq_univ_poly in evarconv to avoid fixing universes. Disallow polymorphic hints based on a constr as it is not possible to infer their universe context. Only global references can be made polymorphic. Fixes issue #8. Fix SearchAbout bug (issue #10). Fix program w.r.t. universes: the universe context of a definition changes according to the successive refinements due to typechecking obligations. This requires the Proof modules to return the generated universe substitution when finishing a proof, and this information is passed in the closing hook. The interface is not very clean, will certainly change in the future. - Better treatment of polymorphic hints in auto: terms can be polymorphic now, we refresh their context as well. - Needs a little change in test-pattern that seems breaks multiary uses of destruct in NZDiv.v, l495. FIX to do. Fix [make_pattern_test] to keep the universe information around and still allow tactics to take multiple patterns at once. - Fix printing of universe instances that should not be factorized blindly - Fix handling of the universe context in program definitions by allowing the hook at the end of an interactive proof to give back the refined universe context, before it is transformed in the kernel. - Fix a bug in evarconv where solve_evar_evar was not checking types of instances, resulting in a loss of constraints in unification of universes and a growing number of useless parametric universes. - Move from universe_level_subst to universe_subst everywhere. - Changed representation of universes for a canonical one - Adapt the code so that universe variables might be substituted by arbitrary universes (including algebraics). Not used yet except for polymorphic universe variables instances. - Adapt code to new constraint structure. - Fix setoid rewrite handling of evars that was forgetting the initial universe substitution ! - Fix code that was just testing conversion instead of keeping the resulting universe constraints around in the proof engine. - Make a version of reduction/fconv that deals with the more general set of universe constraints. - [auto using] should use polymorphic versions of the constants. - When starting a proof, don't forget about the algebraic universes in the universe context. Rationalize substitution and normalization functions for universes. Also change back the structure of universes to avoid considering levels n+k as pure levels: they are universe expressions like max. Everything is factored out in the Universes and Univ modules now and the normalization functions can be efficient in the sense that they can cache the normalized universes incrementally. - Adapt normalize_context code to new normalization/substitution functions. - Set more things to be polymorphic, e.g. in Ring or SetoidList for the rest of the code to work properly while the constraint generation code is not adapted. And temporarily extend the universe constraint code in univ to solve max(is) = max(js) by first-order unification (these constraints should actually be implied not enforced). - Fix romega plugin to use the right universes for polymorphic lists. - Fix auto not refreshing the poly hints correctly. - Proper postponing of universe constraints during unification, avoid making arbitrary choices. - Fix nf_evars_and* to keep the substitution around for later normalizations. - Do add simplified universe constraints coming from unification during typechecking. - Fix solve_by_tac in obligations to handle universes right, and the corresponding substitution function. Test global universe equality early during simplication of constraints. Better hashconsing, but still not good on universe lists. - Add postponing of "lub" constraints that should not be checked early, they are implied by the others. - Fix constructor tactic to use a fresh constructor instance avoiding fixing universes. - Use [eq_constr_universes] instead of [eq_constr_univs] everywhere, this is the comparison function that doesn't care about the universe instances. - Almost all the library compiles in this new setting, but some more tactics need to be adapted. - Reinstate hconsing. - Keep Prop <= u constraints that can be used to set the level of a universe metavariable. Add better hashconsing and unionfind in normalisation of constraints. Fix a few problems in choose_canonical, normalization and substitution functions. Fix after merge Fixes after rebase with latest Coq trunk, everything compiles again, albeit slowly in some cases. - Fix module substitution and comparison of table keys in conversion using the wrong order (should always be UserOrd now) - Cleanup in universes, removing commented code. - Fix normalization of universe context which was assigning global levels to local ones. Should always be the other way! - Fix universe implementation to implement sorted cons of universes preserving order. Makes Univ.sup correct again, keeping universe in normalized form. - In evarconv.ml, allow again a Fix to appear as head of a weak-head normal form (due to partially applied fixpoints). - Catch anomalies of conversion as errors in reductionops.ml, sad but necessary as eta-expansion might build ill-typed stacks like FProd, [shift;app Rel 1], as it expands not only if the other side is rigid. - Fix module substitution bug in auto.ml - Fix case compilation: impossible cases compilation was generating useless universe levels. Use an IDProp constant instead of the polymorphic identity to not influence the level of the original type when building the case construct for the return type. - Simplify normalization of universe constraints. - Compute constructor levels of records correctly. Fall back to levels for universe instances, avoiding issues of unification. Add more to the test-suite for universe polymorphism. Fix after rebase with trunk Fix substitution of universes inside fields/params of records to be made after all normalization is done and the level of the record has been computed. Proper sharing of lower bounds with fixed universes. Conflicts: library/universes.ml library/universes.mli Constraints were not enforced in compilation of cases Fix after rebase with trunk - Canonical projections up to universes - Fix computation of class/record universe levels to allow squashing to Prop/Set in impredicative set mode. - Fix descend_in_conjunctions to properly instantiate projections with universes - Avoid Context-bound variables taking extra universes in their associated universe context. - Fix evar_define using the wrong direction when refreshing a universe under cumulativity - Do not instantiate a local universe with some lower bound to a global one just because they have the same local glb (they might not have the same one globally). - Was loosing some global constraints during normalization (brought again by the kernel), fixed now. - Proper [abstract] with polymorphic lemmas (polymorphic if the current proof is). - Fix silly bug in autorewrite: any hint after the first one was always monomorphic. - Fix fourier after rebase - Refresh universes when checking types of metas in unification (avoid (sup (sup univ))). - Speedup a script in FSetPositive.v Rework definitions in RelationClasses and Morphisms to share universe levels as much as possible. This factorizes many useless x <= RelationClasses.foo constraints in code that uses setoid rewriting. Slight incompatible change in the implicits for Reflexivity and Irreflexivity as well. - Share even more universes in Morphisms using a let. - Use splay_prod instead of splay_prod_assum which doesn't reduce let's to find a relation in setoid_rewrite - Fix [Declare Instance] not properly dealing with let's in typeclass contexts. Fixes in inductiveops, evarutil. Patch by Yves Bertot to allow naming universes in inductive definitions. Fixes in tacinterp not propagating evars correctly. Fix for issue #27: lowering a Type to Prop is allowed during inference (resulting in a Type (* Set *)) but kernel reduction was wrongly refusing the equation [Type (*Set*) = Set]. Fix in interface of canonical structures: an instantiated polymorphic projection is not needed to lookup a structure, just the projection name is enough (reported by C. Cohen). Move from universe inference to universe checking in the kernel. All tactics have to be adapted so that they carry around their generated constraints (living in their sigma), which is mostly straightforward. The more important changes are when refering to Coq constants, the tactics code is adapted so that primitive eq, pairing and sigma types might be polymorphic. Fix another few places in tacinterp and evarconv/evarsolve where the sigma was not folded correctly. - Fix discharge adding spurious global constraints on polymorphic universe variables appearing in assumptions. - Fixes in inductiveops not taking into account universe polymorphic inductives. WIP on checked universe polymorphism, it is clearly incompatible with the previous usage of polymorphic inductives + non-polymorphic definitions on them as universe levels now appear in the inductive type, and add equality constraints between universes that were otherwise just in a cumulativity relation (not sure that was actually correct). Refined version of unification of universe instances for first-order unification, prefering unfolding to arbitrary identification of universes. Moved kernel to universe checking only. Adapt the code to properly infer constraints during typechecking and refinement (tactics) and only check constraints when adding constants/inductives to the environment. Exception made of module subtyping that needs inference of constraints... The kernel conversion (fconv) has two modes: checking only and inference, the later being used by modules only. Evarconv/unification make use of a different strategy for conversion of constants that prefer unfolding to blind unification of rigid universes. Likewise, conversion checking backtracks on different universe instances (modulo the constraints). - adapt congruence/funind/ring plugins to this new mode, forcing them to declare their constraints. - To avoid big performance penalty with reification, make ring/field non-polymorphic (non-linear explosion in run time to be investigated further). - pattern and change tactics need special treatment: as they are not _reduction_ but conversion functions, their operation requires to update an evar_map with new universe constraints. - Fix vm_compute to work better with universes. If the normal form is made only of constructors then the readback is correct. However a deeper change will be needed to treat substitution of universe instances when unfolding constants. Remove libtypes.ml Fix after merge. Fix after rebase with trunk. **** Add projections to the kernel, as optimized implementations of constants. - New constructor Proj expects a projection constant applied to its principal inductive argument. - Reduction machines shortcut the expansion to a case and directly project the right argument. - No need to keep parameters as part of the projection's arguments as they are inferable from the type of the principal argument. - ML code now compiles, debugging needed. Start debugging the implementation of projections. Externalisation should keep the information about projections. Internalization, pattern-matching, unification and reduction of projections. Fix some code that used to have _ for parameters that are no longer present in projections. Fixes in unification, reduction, term indexing, auto hints based on projections, add debug printers. Fix byte-compilation of projections, unification, congruence with projections. Adapt .v files using "@proj _ _ record" syntax, should come back on this later. Fix coercion insertion code to properly deal with projection coercions. Fix [simpl proj]... TODO [unfold proj], proj is not considered evaluable. - Fix whnf of projections, now respecting opacity information. - Fix conversion of projections to try first-order first and then incrementally unfold them. - Fix computation of implicit args for projections, simply dropping the information for parameters. - Fix a few scripts that relied on projections carrying their parameters (few at's, rewrites). - Fix unify_with_subterm to properly match under projections. - Fix bug in cooking of projections. - Add pattern PProj for projections. - A very strange bug appeared in BigZ.v, making coqtop segfault on the export of BigN... tofix Fixes after rebase with trunk. Everything compiles now, with efficient projections. Fixes after rebase with trunk (esp. reductionops). Remove warnings, backport patch from old univs+projs branch. Proper expansion of projections during unification. They are considered as maybe flexible keys in evarconv/unification. We try firstorder unification and otherwise expand them as necessary, completely mimicking the original behavior, when they were constants. Fix head_constr_bound interface, the arguments are never needed (they're outside their environment actually). [simpl] and [red]/[intro] should behave just like before now. Fix evarconv that was giving up on proj x = ?e problems too early. - Port patch by Maxime Denes implementing fast projections in the native conversion. - Backport patch to add eta-expansion for records. Do not raise an exception but simply fails if trying to do eta on an inductive that is not a record. Fix projections detyping/matching and unification.ml not always recovering on first-order universe inequalities. Correct eta-expansion for records, and change strategy for conversion with projections to favor reduction over first-order unification a little more. Fix a bug in Ltac pattern matching on projections. Fix evars_reset_evd to not recheck existing constraints in case it is just an update (performance improvement for typeclass resolution). - Respect Global/Transparent oracle during unification. Opaque means _never_ unfolded there. - Add empty universes as well as the initial universes (having Prop < Set). - Better display of universe inconsistencies. - Add Beta Ziliani's patch to go fast avoiding imitation when possible. - Allow instantiation by lower bound even if there are universes above - (tentative) In refinement, avoid incremental refinement of terms containing no holes and do it in one step (much faster on big terms). Turned on only if not a checked command. Remove dead code in univ/universes.ml and cleanup setup of hashconsing, for a small speed and memory footprint improvement. - Fix bug in unification using cumulativity when conversion should have been used. - Fix unification of evars having type Type, no longer forcing them to be equal (potentially more constraints): algorithm is now complete w.r.t. cumulativity. - In clenvtac, use refine_nocheck as we are guaranteed to get well-typed terms from unification now, including sufficient universe constraints. Small general speedup. - Fix inference of universe levels of inductive types to avoid smashing inadvertently from Set to Prop. - Fix computation of discharged hypotheses forgetting the arity in inductives. - Fix wrong order in printing of universe inconsistency explanation - Allow coercions between two polymorphic instances of the same inductive/constant. - Do evar normalization and saturation by classes before trying to use program coercion during pretyping. - In unification, force equalities of universes when unifying the same rigid head constants. - Fix omission of projections in constr_leq - Fix [admit] tactic's handling of normalized universes. Fix typing of projections not properly normalizing w.r.t. evars, resulting in anomaly sometimes. Adapt rewrite to work with computational relations (in Type), while maintaining backward compatibility with Propositional rewriting. Introduce a [diff] function on evar maps and universe contexts to properly deal with clause environments. Local hints in auto now store just the extension of the evar map they rely on, so merging them becomes efficient. This fixes an important performance issue in auto and typeclass resolution in presence of a large number of universe constraints. Change FSetPositive and MSetPositive to put their [elt] and [t] universes in Type to avoid restricting global universes to [Set]. This is due to [flip]s polymorphic type being fixed in monomorphic instances of Morphisms.v, and rewriting hence forcing unification of levels that could be left unrelated. - Try a fast_typeops implementation of kernel type inference that allocates less by not rebuilding the term, shows a little performance improvement, and less allocation. - Build universe inconsistency explanations lazily, avoiding huge blowup (x5) in check_constraints/merge_constraints in time and space (these are stressed in universe polymorphic mode). - Hashcons universe instances. Add interface file for fast_typeops Use monomorphic comparisons, little optimizations of hashconsing and comparison in univ.ml. Fix huge slowdown due to building huge error messages. Lazy is not enough to tame this completely. Fix last performance issue, due to abstracts building huge terms abstracting on parts of the section context. Was due to wrong handling of Let... Qed.s in abstract. Performance is a tiny bit better than the trunk now. First step at compatibility layer for projections. Compatibility mode for projections. c.(p), p c use primitive projs, while @p refers to an expansion [λ params c, c.(p)]. Recovers almost entire source compatibility with trunk scripts, except when mixing @p and p and doing syntactic matching (they're unifiable though). Add a [Set Primitive Projections] flag to set/unset the use of primitive projections, selectively for each record. Adapt code to handle both the legacy encoding and the primitive projections. Library is almost source-to-source compatible, except for syntactic operations relying on the presence of parameters. In primitive projections mode, @p refers to an expansion [λ params r. p.(r)]. More information in CHANGES (to be reformated/moved to reference manual). Backport changes from HoTT/coq: - Fix anomaly on uncatched NotASort in retyping. - Better recognition of evars that are subject to typeclass resolution. Fixes bug reported by J. Gross on coq-club. - Print universe polymorphism information for parameters as well. Fix interface for unsatisfiable constraints error, now a type error. Try making ring polymorphic again, with a big slowdown, to be investigated. Fix evar/universe leak in setoid rewrite. - Add profiling flag - Move setoid_ring back to non-polymorphic mode to compare perfs with trunk - Change unification to allow using infer_conv more often (big perf culprit), but semantics of backtracking on unification of constants is not properly implemented there. - Fix is_empty/union_evar_universe_context forgetting about some assignments. - Performance is now very close to the trunk from june, with projections deactivated.
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml144
-rw-r--r--toplevel/auto_ind_decl.mli9
-rw-r--r--toplevel/cerrors.ml16
-rw-r--r--toplevel/class.ml68
-rw-r--r--toplevel/class.mli21
-rw-r--r--toplevel/classes.ml107
-rw-r--r--toplevel/classes.mli5
-rw-r--r--toplevel/command.ml331
-rw-r--r--toplevel/command.mli42
-rw-r--r--toplevel/coqtop.ml1
-rw-r--r--toplevel/discharge.ml17
-rw-r--r--toplevel/discharge.mli2
-rw-r--r--toplevel/himsg.ml32
-rw-r--r--toplevel/ind_tables.ml40
-rw-r--r--toplevel/ind_tables.mli7
-rw-r--r--toplevel/indschemes.ml44
-rw-r--r--toplevel/metasyntax.ml4
-rw-r--r--toplevel/obligations.ml184
-rw-r--r--toplevel/obligations.mli4
-rw-r--r--toplevel/record.ml203
-rw-r--r--toplevel/record.mli7
-rw-r--r--toplevel/search.ml7
-rw-r--r--toplevel/usage.ml1
-rw-r--r--toplevel/vernacentries.ml162
-rw-r--r--toplevel/whelp.ml412
25 files changed, 941 insertions, 529 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 04d0f3de4b..1a1a4dfe7d 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -25,6 +25,8 @@ open Ind_tables
open Misctypes
open Proofview.Notations
+let out_punivs = Univ.out_punivs
+
(**********************************************************************)
(* Generic synthesis of boolean equality *)
@@ -55,6 +57,8 @@ exception NonSingletonProp of inductive
let dl = Loc.ghost
+let constr_of_global g = lazy (Universes.constr_of_global g)
+
(* Some pre declaration of constant we are going to use *)
let bb = constr_of_global Coqlib.glob_bool
@@ -93,7 +97,7 @@ let destruct_on c =
None (None,None) None
(* reconstruct the inductive with the correct deBruijn indexes *)
-let mkFullInd ind n =
+let mkFullInd (ind,u) n =
let mib = Global.lookup_mind (fst ind) in
let nparams = mib.mind_nparams in
let nparrec = mib.mind_nparams_rec in
@@ -101,12 +105,12 @@ let mkFullInd ind n =
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
if nparrec > 0
- then mkApp (mkInd ind,
+ then mkApp (mkIndU (ind,u),
Array.of_list(extended_rel_list (nparrec+n) lnamesparrec))
- else mkInd ind
+ else mkIndU (ind,u)
let check_bool_is_defined () =
- try let _ = Global.type_of_global Coqlib.glob_bool in ()
+ try let _ = Global.type_of_global_unsafe Coqlib.glob_bool in ()
with e when Errors.noncritical e -> raise (UndefinedCst "bool")
let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
@@ -142,7 +146,7 @@ let build_beq_scheme kn =
let eqs_typ = List.map (fun aa ->
let a = lift !lift_cnt aa in
incr lift_cnt;
- myArrow a (myArrow a bb)
+ myArrow a (myArrow a (Lazy.force bb))
) ext_rel_list in
let eq_input = List.fold_left2
@@ -159,11 +163,12 @@ let build_beq_scheme kn =
t a) eq_input lnamesparrec
in
let make_one_eq cur =
- let ind = kn,cur in
+ let u = Univ.Instance.empty in
+ let ind = (kn,cur),u (* FIXME *) in
(* current inductive we are working on *)
- let cur_packet = mib.mind_packets.(snd ind) in
+ let cur_packet = mib.mind_packets.(snd (fst ind)) in
(* Inductive toto : [rettyp] := *)
- let rettyp = Inductive.type_of_inductive env (mib,cur_packet) in
+ let rettyp = Inductive.type_of_inductive env ((mib,cur_packet),u) in
(* split rettyp in a list without the non rec params and the last ->
e.g. Inductive vec (A:Set) : nat -> Set := ... will do [nat] *)
let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in
@@ -182,7 +187,7 @@ let build_beq_scheme kn =
| Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Declareops.no_seff
| Cast (x,_,_) -> aux (applist (x,a))
| App _ -> assert false
- | Ind (kn',i as ind') ->
+ | Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Declareops.no_seff
else begin
try
@@ -200,16 +205,17 @@ let build_beq_scheme kn =
(Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in
if Int.equal (Array.length args) 0 then eq, eff
else mkApp (eq, args), eff
- with Not_found -> raise(EqNotFound (ind',ind))
+ with Not_found -> raise(EqNotFound (ind', fst ind))
end
| Sort _ -> raise InductiveWithSort
| Prod _ -> raise InductiveWithProduct
| Lambda _-> raise (EqUnknown "Lambda")
| LetIn _ -> raise (EqUnknown "LetIn")
| Const kn ->
- (match Environ.constant_opt_value env kn with
- | None -> raise (ParameterWithoutEquality kn)
+ (match Environ.constant_opt_value_in env kn with
+ | None -> raise (ParameterWithoutEquality (fst kn))
| Some c -> aux (applist (c,a)))
+ | Proj _ -> raise (EqUnknown "Proj")
| Construct _ -> raise (EqUnknown "Construct")
| Case _ -> raise (EqUnknown "Case")
| CoFix _ -> raise (EqUnknown "CoFix")
@@ -224,28 +230,28 @@ let build_beq_scheme kn =
List.fold_left (fun a b -> mkLambda(Anonymous,b,a))
(mkLambda (Anonymous,
mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1),
- bb))
+ (Lazy.force bb)))
(List.rev rettyp_l) in
(* make_one_eq *)
(* do the [| C1 ... => match Y with ... end
...
Cn => match Y with ... end |] part *)
- let ci = make_case_info env ind MatchStyle in
+ let ci = make_case_info env (fst ind) MatchStyle in
let constrs n = get_constructors env (make_ind_family (ind,
extended_rel_list (n+nb_ind-1) mib.mind_params_ctxt)) in
let constrsi = constrs (3+nparrec) in
let n = Array.length constrsi in
- let ar = Array.make n ff in
- let eff = ref Declareops.no_seff in
+ let ar = Array.make n (Lazy.force ff) in
+ let eff = ref Declareops.no_seff in
for i=0 to n-1 do
let nb_cstr_args = List.length constrsi.(i).cs_args in
- let ar2 = Array.make n ff in
+ let ar2 = Array.make n (Lazy.force ff) in
let constrsj = constrs (3+nparrec+nb_cstr_args) in
for j=0 to n-1 do
if Int.equal i j then
ar2.(j) <- let cc = (match nb_cstr_args with
- | 0 -> tt
- | _ -> let eqs = Array.make nb_cstr_args tt in
+ | 0 -> Lazy.force tt
+ | _ -> let eqs = Array.make nb_cstr_args (Lazy.force tt) in
for ndx = 0 to nb_cstr_args-1 do
let _,_,cc = List.nth constrsi.(i).cs_args ndx in
let eqA, eff' = compute_A_equality rel_list
@@ -270,7 +276,7 @@ let build_beq_scheme kn =
(constrsj.(j).cs_args)
)
else ar2.(j) <- (List.fold_left (fun a (p,q,r) ->
- mkLambda (p,r,a)) ff (constrsj.(j).cs_args) )
+ mkLambda (p,r,a)) (Lazy.force ff) (constrsj.(j).cs_args) )
done;
ar.(i) <- (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a))
@@ -287,21 +293,23 @@ let build_beq_scheme kn =
types = Array.make nb_ind mkSet and
cores = Array.make nb_ind mkSet in
let eff = ref Declareops.no_seff in
+ let u = Univ.Instance.empty in
for i=0 to (nb_ind-1) do
names.(i) <- Name (Id.of_string (rec_name i));
- types.(i) <- mkArrow (mkFullInd (kn,i) 0)
- (mkArrow (mkFullInd (kn,i) 1) bb);
+ types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0)
+ (mkArrow (mkFullInd ((kn,i),u) 1) (Lazy.force bb));
let c, eff' = make_one_eq i in
cores.(i) <- c;
eff := Declareops.union_side_effects eff' !eff
done;
- Array.init nb_ind (fun i ->
+ (Array.init nb_ind (fun i ->
let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in
- if not (Sorts.List.mem InSet kelim) then
- raise (NonSingletonProp (kn,i));
- let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in
- create_input fix),
- !eff
+ if not (Sorts.List.mem InSet kelim) then
+ raise (NonSingletonProp (kn,i));
+ let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in
+ create_input fix),
+ Evd.empty_evar_universe_context (* FIXME *)),
+ !eff
let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme
@@ -343,8 +351,8 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
(* if this happen then the args have to be already declared as a
Parameter*)
(
- let mp,dir,lbl = repr_con (destConst v) in
- mkConst (make_con mp dir (Label.make (
+ let mp,dir,lbl = repr_con (fst (destConst v)) in
+ mkConst (make_con mp dir (mk_label (
if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
else ((Label.to_string lbl)^"_lb")
)))
@@ -355,7 +363,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
let u,v = destruct_ind type_of_pq
in let lb_type_of_p =
try
- let c, eff = find_scheme lb_scheme_key u in
+ let c, eff = find_scheme lb_scheme_key (out_punivs u) (*FIXME*) in
Proofview.tclUNIT (mkConst c, eff)
with Not_found ->
(* spiwack: the format of this error message should probably
@@ -383,7 +391,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
end
(* used in the bool -> leib side *)
-let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
+let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let avoid = Array.of_list aavoid in
let do_arg v offset =
try
@@ -400,8 +408,8 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
(* if this happen then the args have to be already declared as a
Parameter*)
(
- let mp,dir,lbl = repr_con (destConst v) in
- mkConst (make_con mp dir (Label.make (
+ let mp,dir,lbl = repr_con (fst (destConst v)) in
+ mkConst (make_con mp dir (mk_label (
if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
else ((Label.to_string lbl)^"_bl")
)))
@@ -417,13 +425,13 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
else (
let u,v = try destruct_ind tt1
(* trick so that the good sequence is returned*)
- with e when Errors.noncritical e -> ind,[||]
- in if eq_ind u ind
+ with e when Errors.noncritical e -> indu,[||]
+ in if eq_ind (fst u) ind
then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ]
else (
let bl_t1, eff =
try
- let c, eff = find_scheme bl_scheme_key u in
+ let c, eff = find_scheme bl_scheme_key (out_punivs u) (*FIXME*) in
mkConst c, eff
with Not_found ->
(* spiwack: the format of this error message should probably
@@ -462,15 +470,15 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
begin try Proofview.tclUNIT (destApp rgt)
with DestKO -> Proofview.tclZERO (UserError ("" , str"replace failed."))
end >>= fun (ind2,ca2) ->
- begin try Proofview.tclUNIT (destInd ind1)
+ begin try Proofview.tclUNIT (out_punivs (destInd ind1))
with DestKO ->
- begin try Proofview.tclUNIT (fst (destConstruct ind1))
+ begin try Proofview.tclUNIT (fst (fst (destConstruct ind1)))
with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one."))
end
end >>= fun (sp1,i1) ->
- begin try Proofview.tclUNIT (destInd ind2)
+ begin try Proofview.tclUNIT (out_punivs (destInd ind2))
with DestKO ->
- begin try Proofview.tclUNIT (fst (destConstruct ind2))
+ begin try Proofview.tclUNIT (fst (fst (destConstruct ind2)))
with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one."))
end
end >>= fun (sp2,i2) ->
@@ -517,15 +525,15 @@ let compute_bl_goal ind lnamesparrec nparrec =
mkNamedProd x (mkVar s) (
mkNamedProd y (mkVar s) (
mkArrow
- ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
- ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
+ ( mkApp(Lazy.force eq,[|(Lazy.force bb);mkApp(mkVar seq,[|mkVar x;mkVar y|]);(Lazy.force tt)|]))
+ ( mkApp(Lazy.force eq,[|mkVar s;mkVar x;mkVar y|]))
))
) list_id in
let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b ->
mkNamedProd sbl b a
) c (List.rev list_id) (List.rev bl_typ) in
let eqs_typ = List.map (fun (s,_,_,_) ->
- mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb))
+ mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,(Lazy.force bb)))
) list_id in
let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
mkNamedProd seq b a
@@ -536,12 +544,13 @@ let compute_bl_goal ind lnamesparrec nparrec =
in
let n = Id.of_string "x" and
m = Id.of_string "y" in
+ let u = Univ.Instance.empty in
create_input (
- mkNamedProd n (mkFullInd ind nparrec) (
- mkNamedProd m (mkFullInd ind (nparrec+1)) (
+ mkNamedProd n (mkFullInd (ind,u) nparrec) (
+ mkNamedProd m (mkFullInd (ind,u) (nparrec+1)) (
mkArrow
- (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
- (mkApp(eq,[|mkFullInd ind (nparrec+3);mkVar n;mkVar m|]))
+ (mkApp(Lazy.force eq,[|(Lazy.force bb);mkApp(eqI,[|mkVar n;mkVar m|]);(Lazy.force tt)|]))
+ (mkApp(Lazy.force eq,[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|]))
))), eff
let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec =
@@ -600,7 +609,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
match (kind_of_term gl) with
| App (c,ca) -> (
match (kind_of_term c) with
- | Ind indeq ->
+ | Ind (indeq, u) ->
if eq_gr (IndRef indeq) Coqlib.glob_eq
then
Tacticals.New.tclTHEN
@@ -629,12 +638,14 @@ let make_bl_scheme mind =
let ind = (mind,0) in
let nparams = mib.mind_nparams in
let nparrec = mib.mind_nparams_rec in
- let lnonparrec,lnamesparrec =
+ let lnonparrec,lnamesparrec = (* TODO subst *)
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
- [|fst (Pfedit.build_by_tactic (Global.env()) bl_goal
- (compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec))|],
- eff
+ let ctx = Univ.ContextSet.empty (*FIXME univs *) in
+ let (ans, _, _) = Pfedit.build_by_tactic (Global.env()) (bl_goal, ctx)
+ (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec)
+ in
+ ([|ans|], Evd.empty_evar_universe_context), eff
let bl_scheme_kind = declare_mutual_scheme_object "_dec_bl" make_bl_scheme
@@ -645,6 +656,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
let compute_lb_goal ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
+ let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
let eqI, eff = eqI ind lnamesparrec in
let create_input c =
let x = Id.of_string "x" and
@@ -672,11 +684,12 @@ let compute_lb_goal ind lnamesparrec nparrec =
in
let n = Id.of_string "x" and
m = Id.of_string "y" in
+ let u = Univ.Instance.empty in
create_input (
- mkNamedProd n (mkFullInd ind nparrec) (
- mkNamedProd m (mkFullInd ind (nparrec+1)) (
+ mkNamedProd n (mkFullInd (ind,u) nparrec) (
+ mkNamedProd m (mkFullInd (ind,u) (nparrec+1)) (
mkArrow
- (mkApp(eq,[|mkFullInd ind (nparrec+2);mkVar n;mkVar m|]))
+ (mkApp(eq,[|mkFullInd (ind,u) (nparrec+2);mkVar n;mkVar m|]))
(mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
))), eff
@@ -750,9 +763,10 @@ let make_lb_scheme mind =
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
- [|fst (Pfedit.build_by_tactic (Global.env()) lb_goal
- (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec))|],
- eff
+ let (ans, _, _) = Pfedit.build_by_tactic (Global.env()) (lb_goal,Univ.ContextSet.empty)
+ (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
+ in
+ ([|ans|], Evd.empty_evar_universe_context (* FIXME *)), eff
let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme
@@ -768,6 +782,7 @@ let check_not_is_defined () =
(* {n=m}+{n<>m} part *)
let compute_dec_goal ind lnamesparrec nparrec =
check_not_is_defined ();
+ let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
let list_id = list_id lnamesparrec in
let create_input c =
let x = Id.of_string "x" and
@@ -818,6 +833,8 @@ let compute_dec_goal ind lnamesparrec nparrec =
)
let compute_dec_tact ind lnamesparrec nparrec =
+ let eq = Lazy.force eq and tt = Lazy.force tt
+ and ff = Lazy.force ff and bb = Lazy.force bb in
let list_id = list_id lnamesparrec in
let eqI, eff = eqI ind lnamesparrec in
let avoid = ref [] in
@@ -915,11 +932,14 @@ let make_eq_decidability mind =
let ind = (mind,0) in
let nparams = mib.mind_nparams in
let nparrec = mib.mind_nparams_rec in
+ let u = Univ.Instance.empty in
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
- [|fst (Pfedit.build_by_tactic (Global.env())
- (compute_dec_goal ind lnamesparrec nparrec)
- (compute_dec_tact ind lnamesparrec nparrec))|], Declareops.no_seff
+ let (ans, _, _) = Pfedit.build_by_tactic (Global.env())
+ (compute_dec_goal (ind,u) lnamesparrec nparrec, Univ.ContextSet.empty)
+ (compute_dec_tact ind lnamesparrec nparrec)
+ in
+ ([|ans|], Evd.empty_evar_universe_context (* FIXME *)), Declareops.no_seff
let eq_dec_scheme_kind =
declare_mutual_scheme_object "_eq_dec" make_eq_decidability
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index 6509a7d3b8..21362c973d 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -26,17 +26,16 @@ exception ParameterWithoutEquality of constant
exception NonSingletonProp of inductive
val beq_scheme_kind : mutual scheme_kind
-val build_beq_scheme : mutual_inductive -> constr array * Declareops.side_effects
+val build_beq_scheme : mutual_scheme_object_function
(** {6 Build equivalence between boolean equality and Leibniz equality } *)
val lb_scheme_kind : mutual scheme_kind
-val make_lb_scheme : mutual_inductive -> constr array * Declareops.side_effects
-
+val make_lb_scheme : mutual_scheme_object_function
val bl_scheme_kind : mutual scheme_kind
-val make_bl_scheme : mutual_inductive -> constr array * Declareops.side_effects
+val make_bl_scheme : mutual_scheme_object_function
(** {6 Build decidability of equality } *)
val eq_dec_scheme_kind : mutual scheme_kind
-val make_eq_decidability : mutual_inductive -> constr array * Declareops.side_effects
+val make_eq_decidability : mutual_scheme_object_function
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 0186b08ac7..f5cc2015b8 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -58,22 +58,10 @@ let wrap_vernac_error exn strm =
Exninfo.copy exn e
let process_vernac_interp_error exn = match exn with
- | Univ.UniverseInconsistency (o,u,v,p) ->
- let pr_rel r =
- match r with
- Univ.Eq -> str"=" | Univ.Lt -> str"<" | Univ.Le -> str"<=" in
- let reason = match p with
- [] -> mt()
- | _::_ ->
- str " because" ++ spc() ++ Univ.pr_uni v ++
- prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ Univ.pr_uni v)
- p ++
- (if Univ.Universe.equal (snd (List.last p)) u then mt() else
- (spc() ++ str "= " ++ Univ.pr_uni u)) in
+ | Univ.UniverseInconsistency i ->
let msg =
if !Constrextern.print_universes then
- spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++
- pr_rel o ++ spc() ++ Univ.pr_uni v ++ reason ++ str")"
+ str "." ++ spc() ++ Univ.explain_universe_inconsistency i
else
mt() in
wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
diff --git a/toplevel/class.ml b/toplevel/class.ml
index a9cb6ca5ef..d54efb6328 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -66,7 +66,7 @@ let explain_coercion_error g = function
(* Verifications pour l'ajout d'une classe *)
let check_reference_arity ref =
- if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global ref)) then
+ if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global_unsafe ref)) then
raise (CoercionError (NotAClass ref))
let check_arity = function
@@ -118,19 +118,19 @@ l'indice de la classe source dans la liste lp
let get_source lp source =
match source with
| None ->
- let (cl1,lv1) =
+ let (cl1,u1,lv1) =
match lp with
| [] -> raise Not_found
| t1::_ -> find_class_type Evd.empty t1
in
- (cl1,lv1,1)
+ (cl1,u1,lv1,1)
| Some cl ->
let rec aux = function
| [] -> raise Not_found
| t1::lt ->
try
- let cl1,lv1 = find_class_type Evd.empty t1 in
- if cl_typ_eq cl cl1 then cl1,lv1,(List.length lt+1)
+ let cl1,u1,lv1 = find_class_type Evd.empty t1 in
+ if cl_typ_eq cl cl1 then cl1,u1,lv1,(List.length lt+1)
else raise Not_found
with Not_found -> aux lt
in aux (List.rev lp)
@@ -139,7 +139,7 @@ let get_target t ind =
if (ind > 1) then
CL_FUN
else
- fst (find_class_type Evd.empty t)
+ pi1 (find_class_type Evd.empty t)
let prods_of t =
let rec aux acc d = match kind_of_term d with
@@ -177,12 +177,12 @@ let error_not_transparent source =
errorlabstrm "build_id_coercion"
(pr_class source ++ str " must be a transparent constant.")
-let build_id_coercion idf_opt source =
+let build_id_coercion idf_opt source poly =
let env = Global.env () in
- let vs = match source with
- | CL_CONST sp -> mkConst sp
+ let vs, ctx = match source with
+ | CL_CONST sp -> Universes.fresh_global_instance env (ConstRef sp)
| _ -> error_not_transparent source in
- let c = match constant_opt_value env (destConst vs) with
+ let c = match constant_opt_value_in env (destConst vs) with
| Some c -> c
| None -> error_not_transparent source in
let lams,t = decompose_lam_assum c in
@@ -211,7 +211,7 @@ let build_id_coercion idf_opt source =
match idf_opt with
| Some idf -> idf
| None ->
- let cl,_ = find_class_type Evd.empty t in
+ let cl,u,_ = find_class_type Evd.empty t in
Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
(ident_key_of_class cl))
in
@@ -221,6 +221,9 @@ let build_id_coercion idf_opt source =
(mkCast (val_f, DEFAULTcast, typ_f),Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = Some typ_f;
+ const_entry_proj = None;
+ const_entry_polymorphic = poly;
+ const_entry_universes = Univ.ContextSet.to_context ctx;
const_entry_opaque = false;
const_entry_inline_code = true;
const_entry_feedback = None;
@@ -244,14 +247,14 @@ booleen "coercion identite'?"
lorque source est None alors target est None aussi.
*)
-let add_new_coercion_core coef stre source target isid =
+let add_new_coercion_core coef stre poly source target isid =
check_source source;
- let t = Global.type_of_global coef in
+ let t = Global.type_of_global_unsafe coef in
if coercion_exists coef then raise (CoercionError AlreadyExists);
let tg,lp = prods_of t in
let llp = List.length lp in
if Int.equal llp 0 then raise (CoercionError NotAFunction);
- let (cls,lvs,ind) =
+ let (cls,us,lvs,ind) =
try
get_source lp source
with Not_found ->
@@ -275,44 +278,45 @@ let add_new_coercion_core coef stre source target isid =
in
declare_coercion coef ~local ~isid ~src:cls ~target:clt ~params:(List.length lvs)
-let try_add_new_coercion_core ref ~local c d e =
- try add_new_coercion_core ref (loc_of_bool local) c d e
+
+let try_add_new_coercion_core ref ~local c d e f =
+ try add_new_coercion_core ref (loc_of_bool local) c d e f
with CoercionError e ->
errorlabstrm "try_add_new_coercion_core"
(explain_coercion_error ref e ++ str ".")
-let try_add_new_coercion ref ~local =
- try_add_new_coercion_core ref ~local None None false
+let try_add_new_coercion ref ~local poly =
+ try_add_new_coercion_core ref ~local poly None None false
-let try_add_new_coercion_subclass cl ~local =
- let coe_ref = build_id_coercion None cl in
- try_add_new_coercion_core coe_ref ~local (Some cl) None true
+let try_add_new_coercion_subclass cl ~local poly =
+ let coe_ref = build_id_coercion None cl poly in
+ try_add_new_coercion_core coe_ref ~local poly (Some cl) None true
-let try_add_new_coercion_with_target ref ~local ~source ~target =
- try_add_new_coercion_core ref ~local (Some source) (Some target) false
+let try_add_new_coercion_with_target ref ~local poly ~source ~target =
+ try_add_new_coercion_core ref ~local poly (Some source) (Some target) false
-let try_add_new_identity_coercion id ~local ~source ~target =
- let ref = build_id_coercion (Some id) source in
- try_add_new_coercion_core ref ~local (Some source) (Some target) true
+let try_add_new_identity_coercion id ~local poly ~source ~target =
+ let ref = build_id_coercion (Some id) source poly in
+ try_add_new_coercion_core ref ~local poly (Some source) (Some target) true
-let try_add_new_coercion_with_source ref ~local ~source =
- try_add_new_coercion_core ref ~local (Some source) None false
+let try_add_new_coercion_with_source ref ~local poly ~source =
+ try_add_new_coercion_core ref ~local poly (Some source) None false
-let add_coercion_hook local ref =
+let add_coercion_hook poly local ref =
let stre = match local with
| Local -> true
| Global -> false
| Discharge -> assert false
in
- let () = try_add_new_coercion ref stre in
+ let () = try_add_new_coercion ref stre poly in
let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
Flags.if_verbose msg_info msg
-let add_subclass_hook local ref =
+let add_subclass_hook poly local ref =
let stre = match local with
| Local -> true
| Global -> false
| Discharge -> assert false
in
let cl = class_of_global ref in
- try_add_new_coercion_subclass cl stre
+ try_add_new_coercion_subclass cl stre poly
diff --git a/toplevel/class.mli b/toplevel/class.mli
index 8bb3eb7ce8..d472bd984a 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -14,32 +14,35 @@ open Globnames
(** [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion
from [src] to [tg] *)
-val try_add_new_coercion_with_target : global_reference -> local:bool ->
+val try_add_new_coercion_with_target : global_reference -> local:bool ->
+ Decl_kinds.polymorphic ->
source:cl_typ -> target:cl_typ -> unit
(** [try_add_new_coercion ref s] declares [ref], assumed to be of type
[(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *)
-val try_add_new_coercion : global_reference -> local:bool -> unit
+val try_add_new_coercion : global_reference -> local:bool ->
+ Decl_kinds.polymorphic -> unit
(** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a
transparent constant which unfolds to some class [tg]; it declares
an identity coercion from [cst] to [tg], named something like
["Id_cst_tg"] *)
-val try_add_new_coercion_subclass : cl_typ -> local:bool -> unit
+val try_add_new_coercion_subclass : cl_typ -> local:bool ->
+ Decl_kinds.polymorphic -> unit
(** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion
from [src] to [tg] where the target is inferred from the type of [ref] *)
-val try_add_new_coercion_with_source : global_reference -> local:bool ->
- source:cl_typ -> unit
+val try_add_new_coercion_with_source : global_reference -> local:bool ->
+ Decl_kinds.polymorphic -> source:cl_typ -> unit
(** [try_add_new_identity_coercion id s src tg] enriches the
environment with a new definition of name [id] declared as an
identity coercion from [src] to [tg] *)
-val try_add_new_identity_coercion : Id.t -> local:bool ->
- source:cl_typ -> target:cl_typ -> unit
+val try_add_new_identity_coercion : Id.t -> local:bool ->
+ Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit
-val add_coercion_hook : unit Tacexpr.declaration_hook
+val add_coercion_hook : Decl_kinds.polymorphic -> unit Tacexpr.declaration_hook
-val add_subclass_hook : unit Tacexpr.declaration_hook
+val add_subclass_hook : Decl_kinds.polymorphic -> unit Tacexpr.declaration_hook
val class_of_global : global_reference -> cl_typ
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 2e17f646bd..cf47abf445 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -33,11 +33,14 @@ let set_typeclass_transparency c local b =
let _ =
Hook.set Typeclasses.add_instance_hint_hook
- (fun inst path local pri ->
+ (fun inst path local pri poly ->
+ let inst' = match inst with IsConstr c -> Auto.IsConstr (c, Univ.ContextSet.empty)
+ | IsGlobal gr -> Auto.IsGlobRef gr
+ in
Flags.silently (fun () ->
Auto.add_hints local [typeclasses_db]
(Auto.HintsResolveEntry
- [pri, false, Auto.PathHints path, inst])) ());
+ [pri, poly, false, Auto.PathHints path, inst'])) ());
Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
Hook.set Typeclasses.classes_transparent_state_hook
(fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db))
@@ -52,10 +55,11 @@ let declare_class g =
(** TODO: add subinstances *)
let existing_instance glob g pri =
let c = global g in
- let instance = Typing.type_of (Global.env ()) Evd.empty (constr_of_global c) in
+ let instance = Typing.type_of (Global.env ()) Evd.empty (Universes.constr_of_global c) in
let _, r = decompose_prod_assum instance in
match class_of_constr r with
- | Some (_, (tc, _)) -> add_instance (new_instance tc pri glob c)
+ | Some (_, ((tc,u), _)) -> add_instance (new_instance tc pri glob
+ (*FIXME*) (Flags.use_polymorphic_flag ()) c)
| None -> user_err_loc (loc_of_reference g, "declare_instance",
Pp.str "Constant does not build instances of a declared type class.")
@@ -95,27 +99,22 @@ let instance_hook k pri global imps ?hook cst =
Typeclasses.declare_instance pri (not global) cst;
(match hook with Some h -> h cst | None -> ())
-let declare_instance_constant k pri global imps ?hook id term termtype =
+let declare_instance_constant k pri global imps ?hook id poly uctx term termtype =
let kind = IsDefinition Instance in
- let entry = {
- const_entry_body = Future.from_val term;
- const_entry_secctx = None;
- const_entry_type = Some termtype;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- } in
+ let entry =
+ Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
+ in
let cdecl = (DefinitionEntry entry, kind) in
let kn = Declare.declare_constant id cdecl in
Declare.definition_message id;
instance_hook k pri global imps ?hook (ConstRef kn);
id
-let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
+let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) props
?(generalize=true)
?(tac:unit Proofview.tactic option) ?hook pri =
let env = Global.env() in
- let evars = ref Evd.empty in
+ let evars = ref (Evd.from_env env) in
let tclass, ids =
match bk with
| Implicit ->
@@ -129,15 +128,19 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
cl
| Explicit -> cl, Id.Set.empty
in
- let tclass = if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass) else tclass in
- let k, cty, ctx', ctx, len, imps, subst =
+ let tclass =
+ if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass)
+ else tclass
+ in
+ let k, u, cty, ctx', ctx, len, imps, subst =
let impls, ((env', ctx), imps) = interp_context_evars evars env ctx in
let c', imps' = interp_type_evars_impls ~impls evars env' tclass in
let len = List.length ctx in
let imps = imps @ Impargs.lift_implicits len imps' in
let ctx', c = decompose_prod_assum c' in
let ctx'' = ctx' @ ctx in
- let cl, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in
+ let k, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in
+ let cl, u = Typeclasses.typeclass_univ_instance k in
let _, args =
List.fold_right (fun (na, b, t) (args, args') ->
match b with
@@ -145,7 +148,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
| Some b -> (args, substl args' b :: args'))
(snd cl.cl_context) (args, [])
in
- cl, c', ctx', ctx, len, imps, args
+ cl, u, c', ctx', ctx, len, imps, args
in
let id =
match snd instid with
@@ -161,19 +164,23 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
let env' = push_rel_context ctx env in
evars := Evarutil.nf_evar_map !evars;
evars := resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env !evars;
- let sigma = !evars in
- let subst = List.map (Evarutil.nf_evar sigma) subst in
+ let subst = List.map (Evarutil.nf_evar !evars) subst in
if abstract then
begin
- let _, ty_constr = instance_constructor k (List.rev subst) in
+ let subst = List.fold_left2
+ (fun subst' s (_, b, _) -> if Option.is_empty b then s :: subst' else subst')
+ [] subst (snd k.cl_context)
+ in
+ let (_, ty_constr) = instance_constructor (k,u) subst in
let termtype =
let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
- Evarutil.nf_evar !evars t
+ fst (Evarutil.e_nf_evars_and_universes evars) t
in
Evarutil.check_evars env Evd.empty !evars termtype;
+ let ctx = Evd.universe_context !evars in
let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
(Entries.ParameterEntry
- (None,termtype,None), Decl_kinds.IsAssumption Decl_kinds.Logical)
+ (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
in instance_hook k None global imps ?hook (ConstRef cst); id
end
else (
@@ -203,11 +210,11 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
let props, rest =
List.fold_left
(fun (props, rest) (id,b,_) ->
- if Option.is_empty b then
- try
- let is_id (id', _) = match id, get_id id' with
- | Name id, (_, id') -> Id.equal id id'
- | Anonymous, _ -> false
+ if Option.is_empty b then
+ try
+ let is_id (id', _) = match id, get_id id' with
+ | Name id, (_, id') -> Id.equal id id'
+ | Anonymous, _ -> false
in
let (loc_mid, c) =
List.find is_id rest
@@ -242,7 +249,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
(fun subst' s (_, b, _) -> if Option.is_empty b then s :: subst' else subst')
[] subst (k.cl_props @ snd k.cl_context)
in
- let app, ty_constr = instance_constructor k subst in
+ let (app, ty_constr) = instance_constructor (k,u) subst in
let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
Some term, termtype
@@ -259,17 +266,19 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false
env !evars
in
- let termtype = Evarutil.nf_evar !evars termtype in
+ let _ = evars := Evarutil.nf_evar_map_undefined !evars in
+ let evm, nf = Evarutil.nf_evar_map_universes !evars in
+ let termtype = nf termtype in
let _ = (* Check that the type is free of evars now. *)
- Evarutil.check_evars env Evd.empty !evars termtype
+ Evarutil.check_evars env Evd.empty evm termtype
in
- let term = Option.map (Evarutil.nf_evar !evars) term in
- let evm = Evarutil.nf_evar_map_undefined !evars in
+ let term = Option.map nf term in
if not (Evd.has_undefined evm) && not (Option.is_empty term) then
+ let ctx = Evd.universe_context evm in
declare_instance_constant k pri global imps ?hook id
- (Option.get term,Declareops.no_seff) termtype
+ poly ctx (Option.get term) termtype
else begin
- let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+ let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
if Flags.is_program_mode () then
let hook vis gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
@@ -280,17 +289,18 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
match term with
| Some t ->
let obls, _, constr, typ =
- Obligations.eterm_obligations env id !evars 0 t termtype
+ Obligations.eterm_obligations env id evm 0 t termtype
in obls, Some constr, typ
| None -> [||], None, termtype
in
+ let ctx = Evd.get_universe_context_set evm in
ignore (Obligations.add_definition id ?term:constr
- typ ~kind:(Global,Instance) ~hook obls);
+ typ ctx ~kind:(Global,poly,Instance) ~hook obls);
id
else
(Flags.silently
(fun () ->
- Lemmas.start_proof id kind termtype
+ Lemmas.start_proof id kind (termtype, Evd.get_universe_context_set evm)
(fun _ -> instance_hook k pri global imps ?hook);
(* spiwack: I don't know what to do with the status here. *)
if not (Option.is_empty term) then
@@ -315,7 +325,8 @@ let context l =
let env = Global.env() in
let evars = ref Evd.empty in
let _, ((env', fullctx), impls) = interp_context_evars evars env l in
- let fullctx = Evarutil.nf_rel_context_evar !evars fullctx in
+ let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in
+ let fullctx = Context.map_rel_context subst fullctx in
let ce t = Evarutil.check_evars env Evd.empty !evars t in
let () = List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx in
let ctx =
@@ -323,13 +334,17 @@ let context l =
with e when Errors.noncritical e ->
error "Anonymous variables not allowed in contexts."
in
- let fn status (id, _, t) =
+ let uctx = Evd.get_universe_context_set !evars in
+ let fn status (id, b, t) =
+ let uctx = Universes.shrink_universe_context uctx (Universes.universes_of_constr t) in
if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
- let decl = (ParameterEntry (None,t,None), IsAssumption Logical) in
+ let uctx = Univ.ContextSet.to_context uctx in
+ let decl = (ParameterEntry (None,false,(t,uctx),None), IsAssumption Logical) in
let cst = Declare.declare_constant ~internal:Declare.KernelSilent id decl in
match class_of_constr t with
- | Some (rels, (tc, args) as _cl) ->
- add_instance (Typeclasses.new_instance tc None false (ConstRef cst));
+ | Some (rels, ((tc,_), args) as _cl) ->
+ add_instance (Typeclasses.new_instance tc None false (*FIXME*)
+ (Flags.use_polymorphic_flag ()) (ConstRef cst));
status
(* declare_subclasses (ConstRef cst) cl *)
| None -> status
@@ -339,9 +354,9 @@ let context l =
| _ -> false
in
let impl = List.exists test impls in
- let decl = (Discharge, Definitional) in
+ let decl = (Discharge, (Flags.use_polymorphic_flag ()), Definitional) in
let nstatus =
- snd (Command.declare_assumption false decl t [] impl
+ snd (Command.declare_assumption false decl (t, uctx) [] impl
Vernacexpr.NoInline (Loc.ghost, id))
in
status && nstatus
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index de62ff369e..4dd62ba9fc 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -36,13 +36,16 @@ val declare_instance_constant :
Impargs.manual_explicitation list -> (** implicits *)
?hook:(Globnames.global_reference -> unit) ->
Id.t -> (** name *)
- Entries.proof_output -> (** body *)
+ bool -> (* polymorphic *)
+ Univ.universe_context -> (* Universes *)
+ Constr.t -> (** body *)
Term.types -> (** type *)
Names.Id.t
val new_instance :
?abstract:bool -> (** Not abstract by default. *)
?global:bool -> (** Not global by default. *)
+ Decl_kinds.polymorphic ->
local_binder list ->
typeclass_constraint ->
constr_expr option ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f41acaba27..d2111f0fb2 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -56,8 +56,8 @@ let rec complete_conclusion a cs = function
user_err_loc (loc,"",
strbrk"Cannot infer the non constant arguments of the conclusion of "
++ pr_id cs ++ str ".");
- let args = List.map (fun id -> CRef(Ident(loc,id))) params in
- CAppExpl (loc,(None,Ident(loc,name)),List.rev args)
+ let args = List.map (fun id -> CRef(Ident(loc,id),None)) params in
+ CAppExpl (loc,(None,Ident(loc,name),None),List.rev args)
| c -> c
(* Commands of the interface *)
@@ -74,29 +74,34 @@ let red_constant_entry n ce = function
under_binders env
(fst (reduction_of_red_expr env red)) n body,eff) }
-let interp_definition bl red_option c ctypopt =
+let interp_definition bl p red_option c ctypopt =
let env = Global.env() in
- let evdref = ref Evd.empty in
+ let evdref = ref (Evd.from_env env) in
let impls, ((env_bl, ctx), imps1) = interp_context_evars evdref env bl in
let nb_args = List.length ctx in
let imps,ce =
match ctypopt with
None ->
+ let subst = evd_comb0 Evd.nf_univ_variables evdref in
+ let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in
+ let env_bl = push_rel_context ctx env in
let c, imps2 = interp_constr_evars_impls ~impls evdref env_bl c in
- let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
- imps1@(Impargs.lift_implicits nb_args imps2),
- { const_entry_body = Future.from_val (body,Declareops.no_seff);
- const_entry_secctx = None;
- const_entry_type = None;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- }
+ let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
+ let body = nf (it_mkLambda_or_LetIn c ctx) in
+ let vars = Universes.universes_of_constr body in
+ let ctx = Universes.restrict_universe_context
+ (Evd.get_universe_context_set !evdref) vars in
+ imps1@(Impargs.lift_implicits nb_args imps2),
+ definition_entry ~univs:(Univ.ContextSet.to_context ctx) ~poly:p body
| Some ctyp ->
let ty, impsty = interp_type_evars_impls ~impls evdref env_bl ctyp in
+ let subst = evd_comb0 Evd.nf_univ_variables evdref in
+ let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in
+ let env_bl = push_rel_context ctx env in
let c, imps2 = interp_casted_constr_evars_impls ~impls evdref env_bl c ty in
- let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
- let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in
+ let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
+ let body = nf (it_mkLambda_or_LetIn c ctx) in
+ let typ = nf (it_mkProd_or_LetIn ty ctx) in
let beq b1 b2 = if b1 then b2 else not b2 in
let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in
(* Check that all implicit arguments inferable from the term
@@ -108,14 +113,13 @@ let interp_definition bl red_option c ctypopt =
then msg_warning
(strbrk "Implicit arguments declaration relies on type." ++ spc () ++
strbrk "The term declares more implicits than the type here.");
+ let vars = Univ.LSet.union (Universes.universes_of_constr body)
+ (Universes.universes_of_constr typ) in
+ let ctx = Universes.restrict_universe_context
+ (Evd.get_universe_context_set !evdref) vars in
imps1@(Impargs.lift_implicits nb_args impsty),
- { const_entry_body = Future.from_val(body,Declareops.no_seff);
- const_entry_secctx = None;
- const_entry_type = Some typ;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- }
+ definition_entry ~types:typ ~poly:p
+ ~univs:(Univ.ContextSet.to_context ctx) body
in
red_constant_entry (rel_context_length ctx) ce red_option, !evdref, imps
@@ -144,7 +148,7 @@ let declare_definition_hook = ref ignore
let set_declare_definition_hook = (:=) declare_definition_hook
let get_declare_definition_hook () = !declare_definition_hook
-let declare_definition ident (local,k) ce imps hook =
+let declare_definition ident (local, p, k) ce imps hook =
let () = !declare_definition_hook ce in
let r = match local with
| Discharge when Lib.sections_are_opened () ->
@@ -164,7 +168,7 @@ let declare_definition ident (local,k) ce imps hook =
let _ = Obligations.declare_definition_ref := declare_definition
let do_definition ident k bl red_option c ctypopt hook =
- let (ce, evd, imps as def) = interp_definition bl red_option c ctypopt in
+ let (ce, evd, imps as def) = interp_definition bl (pi2 k) red_option c ctypopt in
if Flags.is_program_mode () then
let env = Global.env () in
let c,sideff = Future.force ce.const_entry_body in
@@ -177,16 +181,17 @@ let do_definition ident k bl red_option c ctypopt hook =
let obls, _, c, cty =
Obligations.eterm_obligations env ident evd 0 c typ
in
- ignore(Obligations.add_definition ident ~term:c cty ~implicits:imps ~kind:k ~hook obls)
+ let ctx = Evd.get_universe_context_set evd in
+ ignore(Obligations.add_definition ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
else let ce = check_definition def in
ignore(declare_definition ident k ce imps
(fun l r -> hook l r;r))
(* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
-let declare_assumption is_coe (local, kind) c imps impl nl (_,ident) = match local with
+let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = match local with
| Discharge when Lib.sections_are_opened () ->
- let decl = (Lib.cwd(), SectionLocalAssum (c,impl), IsAssumption kind) in
+ let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
let _ = declare_variable ident decl in
let () = assumption_message ident in
let () =
@@ -196,8 +201,9 @@ let declare_assumption is_coe (local, kind) c imps impl nl (_,ident) = match loc
in
let r = VarRef ident in
let () = Typeclasses.declare_instance None true r in
- let () = if is_coe then Class.try_add_new_coercion r ~local:true in
+ let () = if is_coe then Class.try_add_new_coercion r ~local:true false in
(r,true)
+
| Global | Local | Discharge ->
let local = get_locality ident local in
let inl = match nl with
@@ -205,18 +211,25 @@ let declare_assumption is_coe (local, kind) c imps impl nl (_,ident) = match loc
| DefaultInline -> Some (Flags.get_inline_level())
| InlineAt i -> Some i
in
- let decl = (ParameterEntry (None,c,inl), IsAssumption kind) in
+ let ctx = Univ.ContextSet.to_context ctx in
+ let decl = (ParameterEntry (None,p,(c,ctx),inl), IsAssumption kind) in
let kn = declare_constant ident ~local decl in
let gr = ConstRef kn in
let () = maybe_declare_manual_implicits false gr imps in
let () = assumption_message ident in
let () = Typeclasses.declare_instance None false gr in
- let () = if is_coe then Class.try_add_new_coercion gr local in
+ let () = if is_coe then Class.try_add_new_coercion gr local p in
(gr,Lib.is_modtype_strict ())
+let declare_assumptions_hook = ref ignore
+let set_declare_assumptions_hook = (:=) declare_assumptions_hook
+
let interp_assumption evdref env bl c =
let c = prod_constr_expr c bl in
- interp_type_evars_impls evdref env c
+ let ty, impls = interp_type_evars_impls evdref env c in
+ let evd, nf = nf_evars_and_universes !evdref in
+ let ctx = Evd.get_universe_context_set evd in
+ ((nf ty, ctx), impls)
let declare_assumptions idl is_coe k c imps impl_is_on nl =
let refs, status =
@@ -229,16 +242,16 @@ let do_assumptions kind nl l =
let env = Global.env () in
let evdref = ref Evd.empty in
let _,l = List.fold_map (fun env (is_coe,(idl,c)) ->
- let t,imps = interp_assumption evdref env [] c in
+ let (t,ctx),imps = interp_assumption evdref env [] c in
let env =
push_named_context (List.map (fun (_,id) -> (id,None,t)) idl) env in
- (env,((is_coe,idl),t,imps))) env l in
+ (env,((is_coe,idl),t,(ctx,imps)))) env l in
let evd = solve_remaining_evars all_and_fail_flags env Evd.empty !evdref in
let l = List.map (on_pi2 (nf_evar evd)) l in
- snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,imps) ->
+ snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) ->
let t = replace_vars subst t in
- let (refs,status') = declare_assumptions idl is_coe kind t imps false nl in
- let subst' = List.map2 (fun (_,id) c -> (id,constr_of_global c)) idl refs in
+ let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) imps false nl in
+ let subst' = List.map2 (fun (_,id) c -> (id,Universes.constr_of_global c)) idl refs in
(subst'@subst, status' && status)) ([],true) l)
(* 3a| Elimination schemes for mutual inductive definitions *)
@@ -290,6 +303,23 @@ let prepare_param = function
| (na,None,t) -> out_name na, LocalAssum t
| (na,Some b,_) -> out_name na, LocalDef b
+
+let make_conclusion_flexible evdref ty =
+ if isArity ty then
+ let _, concl = destArity ty in
+ match concl with
+ | Type u ->
+ (match Univ.universe_level u with
+ | Some u -> evdref := Evd.make_flexible_variable !evdref true u
+ | None -> ())
+ | _ -> ()
+ else ()
+
+let is_impredicative env u =
+ u = Prop Null ||
+ (engagement env = Some Declarations.ImpredicativeSet && u = Prop Pos)
+
+(** Make the arity conclusion flexible to avoid generating an upper bound universe now. *)
let interp_ind_arity evdref env ind =
interp_type_evars_impls evdref env ind.ind_arity
@@ -301,10 +331,88 @@ let interp_cstrs evdref env impls mldata arity ind =
let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls) ctyps') in
(cnames, ctyps'', cimpls)
-let interp_mutual_inductive (paramsl,indl) notations finite =
+let sign_level env evd sign =
+ fst (List.fold_right
+ (fun (_,_,t as d) (lev,env) ->
+ let s = destSort (Reduction.whd_betadeltaiota env
+ (nf_evar evd (Retyping.get_type_of env evd t)))
+ in
+ let u = univ_of_sort s in
+ (Univ.sup u lev, push_rel d env))
+ sign (Univ.type0m_univ,env))
+
+let sup_list = List.fold_left Univ.sup Univ.type0m_univ
+
+let extract_level env evd tys =
+ let sorts = List.map (fun ty ->
+ let ctx, concl = Reduction.dest_prod_assum env ty in
+ sign_level env evd ctx) tys
+ in sup_list sorts
+
+let inductive_levels env evdref arities inds =
+ let destarities = List.map (Reduction.dest_arity env) arities in
+ let levels = List.map (fun (ctx,a) ->
+ if a = Prop Null then None
+ else Some (univ_of_sort a)) destarities
+ in
+ let cstrs_levels, min_levels, sizes =
+ CList.split3
+ (List.map2 (fun (_,tys,_) (ctx,du) ->
+ let len = List.length tys in
+ let clev = extract_level env !evdref tys in
+ let minlev =
+ if len > 1 && not (is_impredicative env du) then
+ Univ.type0_univ
+ else Univ.type0m_univ
+ in
+ (clev, minlev, len)) inds destarities)
+ in
+ (* Take the transitive closure of the system of constructors *)
+ (* level constraints and remove the recursive dependencies *)
+ let levels' = Univ.solve_constraints_system (Array.of_list levels)
+ (Array.of_list cstrs_levels) (Array.of_list min_levels)
+ in
+ let evd =
+ CList.fold_left3 (fun evd cu (ctx,du) len ->
+ if is_impredicative env du then
+ (** Any product is allowed here. *)
+ evd
+ else (** If in a predicative sort, or asked to infer the type,
+ we take the max of:
+ - indices (if in indices-matter mode)
+ - constructors
+ - Type(1) if there is more than 1 constructor
+ *)
+ let evd =
+ (** Indices contribute. *)
+ if Indtypes.is_indices_matter () then (
+ let ilev = sign_level env !evdref ctx in
+ Evd.set_leq_sort evd (Type ilev) du)
+ else evd
+ in
+ (** Constructors contribute. *)
+ let evd =
+ if Sorts.is_set du then
+ if not (Evd.check_leq evd cu Univ.type0_univ) then
+ raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType)
+ else evd
+ else Evd.set_leq_sort evd (Type cu) du
+ in
+ let evd =
+ if len >= 2 && Univ.is_type0m_univ cu then
+ (** "Polymorphic" type constraint and more than one constructor,
+ should not land in Prop. Add constraint only if it would
+ land in Prop directly (no informative arguments as well). *)
+ Evd.set_leq_sort evd (Prop Pos) du
+ else evd
+ in evd)
+ !evdref (Array.to_list levels') destarities sizes
+ in evdref := evd; arities
+
+let interp_mutual_inductive (paramsl,indl) notations poly finite =
check_all_names_different indl;
let env0 = Global.env() in
- let evdref = ref Evd.empty in
+ let evdref = ref Evd.(from_env env0) in
let _, ((env_params, ctx_params), userimpls) =
interp_context_evars evdref env0 paramsl
in
@@ -316,12 +424,14 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
(* Interpret the arities *)
let arities = List.map (interp_ind_arity evdref env_params) indl in
+
let fullarities = List.map (fun (c, _) -> it_mkProd_or_LetIn c ctx_params) arities in
let env_ar = push_types env0 indnames fullarities in
let env_ar_params = push_rel_context ctx_params env_ar in
(* Compute interpretation metadatas *)
- let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (rel_context_nhyps ctx_params) impls) arities in
+ let indimpls = List.map (fun (_, impls) -> userimpls @
+ lift_implicits (rel_context_nhyps ctx_params) impls) arities in
let arities = List.map fst arities in
let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
@@ -336,9 +446,24 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
(* Try further to solve evars, and instantiate them *)
let sigma = solve_remaining_evars all_and_fail_flags env_params Evd.empty !evdref in
- let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
- let ctx_params = Context.map_rel_context (nf_evar sigma) ctx_params in
- let arities = List.map (nf_evar sigma) arities in
+ evdref := sigma;
+ (* Compute renewed arities *)
+ let nf,_ = e_nf_evars_and_universes evdref in
+ let arities = List.map nf arities in
+ let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
+ let _ = List.iter (fun ty -> make_conclusion_flexible evdref ty) arities in
+ let arities = inductive_levels env_ar_params evdref arities constructors in
+ let nf',_ = e_nf_evars_and_universes evdref in
+ let nf x = nf' (nf x) in
+ let arities = List.map nf' arities in
+ let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
+ let ctx_params = map_rel_context nf ctx_params in
+ let evd = !evdref in
+ List.iter (check_evars env_params Evd.empty evd) arities;
+ iter_rel_context (check_evars env0 Evd.empty evd) ctx_params;
+ List.iter (fun (_,ctyps,_) ->
+ List.iter (check_evars env_ar_params Evd.empty evd) ctyps)
+ constructors;
(* Build the inductive entries *)
let entries = List.map3 (fun ind arity (cnames,ctypes,cimpls) -> {
@@ -357,7 +482,9 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
{ mind_entry_params = List.map prepare_param ctx_params;
mind_entry_record = false;
mind_entry_finite = finite;
- mind_entry_inds = entries },
+ mind_entry_inds = entries;
+ mind_entry_polymorphic = poly;
+ mind_entry_universes = Evd.universe_context evd },
impls
(* Very syntactical equality *)
@@ -412,16 +539,19 @@ type one_inductive_impls =
Impargs.manual_explicitation list (* for inds *)*
Impargs.manual_explicitation list list (* for constrs *)
-let do_mutual_inductive indl finite =
+type one_inductive_expr =
+ lident * local_binder list * constr_expr option * constructor_expr list
+
+let do_mutual_inductive indl poly finite =
let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in
(* Interpret the types *)
- let mie,impls = interp_mutual_inductive indl ntns finite in
+ let mie,impls = interp_mutual_inductive indl ntns poly finite in
(* Declare the mutual inductive block with its associated schemes *)
ignore (declare_mutual_inductive_with_eliminations UserVerbose mie impls);
(* Declare the possible notations of inductive types *)
List.iter Metasyntax.add_notation_interpretation ntns;
(* Declare the coercions *)
- List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false) coes
+ List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes
(* 3c| Fixpoints and co-fixpoints *)
@@ -525,11 +655,14 @@ let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
-let declare_fix kind f def t imps =
+let declare_fix (_,poly,_ as kind) ctx f def t imps =
let ce = {
const_entry_body = Future.from_val def;
const_entry_secctx = None;
const_entry_type = Some t;
+ const_entry_polymorphic = poly;
+ const_entry_universes = ctx;
+ const_entry_proj = None;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None;
@@ -576,7 +709,7 @@ let fix_sub_ref = make_ref fixsub_module "Fix_sub"
let measure_on_R_ref = make_ref fixsub_module "MR"
let well_founded = init_constant ["Init"; "Wf"] "well_founded"
let mkSubset name typ prop =
- mkApp ((delayed_force build_sigma).typ,
+ mkApp (Universes.constr_of_global (delayed_force build_sigma).typ,
[| typ; mkLambda (name, typ, prop) |])
let sigT = Lazy.lazy_from_fun build_sigma_type
@@ -591,15 +724,19 @@ let rec telescope = function
List.fold_left
(fun (ty, tys, (k, constr)) (n, b, t) ->
let pred = mkLambda (n, t, ty) in
- let sigty = mkApp ((Lazy.force sigT).typ, [|t; pred|]) in
- let intro = mkApp ((Lazy.force sigT).intro, [|lift k t; lift k pred; mkRel k; constr|]) in
+ let ty = Universes.constr_of_global (Lazy.force sigT).typ in
+ let intro = Universes.constr_of_global (Lazy.force sigT).intro in
+ let sigty = mkApp (ty, [|t; pred|]) in
+ let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in
(sigty, pred :: tys, (succ k, intro)))
(t, [], (2, mkRel 1)) tl
in
let (last, subst) = List.fold_right2
(fun pred (n, b, t) (prev, subst) ->
- let proj1 = applistc (Lazy.force sigT).proj1 [t; pred; prev] in
- let proj2 = applistc (Lazy.force sigT).proj2 [t; pred; prev] in
+ let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in
+ let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in
+ let proj1 = applistc p1 [t; pred; prev] in
+ let proj2 = applistc p2 [t; pred; prev] in
(lift 1 proj2, (n, Some proj1, t) :: subst))
(List.rev tys) tl (mkRel 1, [])
in ty, ((n, Some last, t) :: subst), constr
@@ -648,7 +785,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
it_mkLambda_or_LetIn measure letbinders,
it_mkLambda_or_LetIn measure binders
in
- let comb = constr_of_global (delayed_force measure_on_R_ref) in
+ let comb = Universes.constr_of_global (delayed_force measure_on_R_ref) in
let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
let wf_rel_fun x y =
mkApp (rel, [| subst1 x measure_body;
@@ -663,7 +800,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
in
let intern_bl = wfarg 1 :: [arg] in
let _intern_env = push_rel_context intern_bl env in
- let proj = (delayed_force build_sigma).Coqlib.proj1 in
+ let proj = (*FIXME*)Universes.constr_of_global (delayed_force build_sigma).Coqlib.proj1 in
let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
let projection = (* in wfarg :: arg :: before *)
mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
@@ -676,7 +813,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in
let curry_fun =
let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
- let arg = mkApp ((delayed_force build_sigma).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
+ let intro = (*FIXME*)Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro in
+ let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
let rcurry = mkApp (rel, [| measure; lift len measure |]) in
let lam = (Name (Id.of_string "recproof"), None, rcurry) in
@@ -701,7 +839,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
let prop = mkLambda (Name argname, argtyp, top_arity_let) in
let def =
- mkApp (constr_of_global (delayed_force fix_sub_ref),
+ mkApp (Universes.constr_of_global (delayed_force fix_sub_ref),
[| argtyp ; wf_rel ;
Evarutil.e_new_evar evdref env
~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
@@ -715,16 +853,20 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
if List.length binders_rel > 1 then
let name = add_suffix recname "_func" in
let hook l gr =
- let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in
+ let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in
let ty = it_mkProd_or_LetIn top_arity binders_rel in
let ce =
{ const_entry_body = Future.from_val (Evarutil.nf_evar !evdref body,Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = Some ty;
- const_entry_opaque = false;
- const_entry_inline_code = false;
+ (* FIXME *)
+ const_entry_proj = None;
+ const_entry_polymorphic = false;
+ const_entry_universes = Evd.universe_context !evdref;
const_entry_feedback = None;
- } in
+ const_entry_opaque = false;
+ const_entry_inline_code = false}
+ in
(** FIXME: include locality *)
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
@@ -746,9 +888,9 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
let evars, _, evars_def, evars_typ =
Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp
in
- ignore(Obligations.add_definition
- recname ~term:evars_def evars_typ evars ~hook)
-
+ let ctx = Evd.get_universe_context_set !evdref in
+ ignore(Obligations.add_definition recname ~term:evars_def
+ evars_typ ctx evars ~hook)
let interp_recursive isfix fixl notations =
let env = Global.env() in
@@ -794,8 +936,9 @@ let interp_recursive isfix fixl notations =
(* Instantiate evars and check all are resolved *)
let evd = consider_remaining_unif_problems env_rec !evdref in
- let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in
- let fixtypes = List.map (nf_evar evd) fixtypes in
+ let evd, nf = nf_evars_and_universes evd in
+ let fixdefs = List.map (Option.map nf) fixdefs in
+ let fixtypes = List.map nf fixtypes in
let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in
(* Build the fix declaration block *)
@@ -811,25 +954,25 @@ let check_recursive isfix env evd (fixnames,fixdefs,_) =
let interp_fixpoint l ntns =
let (env,_,evd),fix,info = interp_recursive true l ntns in
check_recursive true env evd fix;
- fix,info
+ (fix,Evd.get_universe_context_set evd,info)
let interp_cofixpoint l ntns =
let (env,_,evd),fix,info = interp_recursive false l ntns in
check_recursive false env evd fix;
- fix,info
+ fix,Evd.get_universe_context_set evd,info
-let declare_fixpoint local ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
+let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns =
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
- List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
+ List.map3 (fun id t (len,imps,_) -> (id,((t,ctx),(len,imps)))) fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
fixdefs) in
let init_tac =
Option.map (List.map Proofview.V82.tactic) init_tac
in
- Lemmas.start_proof_with_initialization (Global,DefinitionBody Fixpoint)
+ Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
(Some(false,indexes,init_tac)) thms None (fun _ _ -> ())
else begin
(* We shortcut the proof process *)
@@ -841,25 +984,27 @@ let declare_fixpoint local ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
let fixdecls =
List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
let fixdecls = List.map (fun c -> c, Declareops.no_seff) fixdecls in
- ignore (List.map4 (declare_fix (local, Fixpoint)) fixnames fixdecls fixtypes fiximps);
+ let ctx = Univ.ContextSet.to_context ctx in
+ ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx)
+ fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
fixpoint_message (Some indexes) fixnames;
end;
(* Declare notations *)
List.iter Metasyntax.add_notation_interpretation ntns
-let declare_cofixpoint local ((fixnames,fixdefs,fixtypes),fiximps) ntns =
+let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns =
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
- List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
+ List.map3 (fun id t (len,imps,_) -> (id,((t,ctx),(len,imps)))) fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
fixdefs) in
let init_tac =
Option.map (List.map Proofview.V82.tactic) init_tac
in
- Lemmas.start_proof_with_initialization (Global,DefinitionBody CoFixpoint)
+ Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
(Some(true,[],init_tac)) thms None (fun _ _ -> ())
else begin
(* We shortcut the proof process *)
@@ -868,7 +1013,9 @@ let declare_cofixpoint local ((fixnames,fixdefs,fixtypes),fiximps) ntns =
let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
let fixdecls = List.map (fun c-> c,Declareops.no_seff) fixdecls in
let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
- ignore (List.map4 (declare_fix (local, CoFixpoint)) fixnames fixdecls fixtypes fiximps);
+ let ctx = Univ.ContextSet.to_context ctx in
+ ignore (List.map4 (declare_fix (local, poly, CoFixpoint) ctx)
+ fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
cofixpoint_message fixnames
end;
@@ -898,7 +1045,12 @@ let out_def = function
| Some def -> def
| None -> error "Program Fixpoint needs defined bodies."
-let do_program_recursive local fixkind fixl ntns =
+let collect_evars_of_term evd c ty =
+ let evars = Evar.Set.union (evars_of_term c) (evars_of_term ty) in
+ Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
+ evars Evd.empty
+
+let do_program_recursive local p fixkind fixl ntns =
let isfix = fixkind != Obligations.IsCoFixpoint in
let (env, rec_sign, evd), fix, info =
interp_recursive isfix fixl ntns
@@ -934,13 +1086,14 @@ let do_program_recursive local fixkind fixl ntns =
Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in
List.iteri (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl
end in
+ let ctx = Evd.get_universe_context_set evd in
let kind = match fixkind with
- | Obligations.IsFixpoint _ -> (local, Fixpoint)
- | Obligations.IsCoFixpoint -> (local, CoFixpoint)
+ | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
+ | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
in
- Obligations.add_mutual_definitions defs ~kind ntns fixkind
+ Obligations.add_mutual_definitions defs ~kind ctx ntns fixkind
-let do_program_fixpoint local l =
+let do_program_fixpoint local poly l =
let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
match g, l with
| [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
@@ -954,30 +1107,30 @@ let do_program_fixpoint local l =
| [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
build_wellfounded (id, n, bl, typ, out_def def)
- (Option.default (CRef lt_ref) r) m ntn
+ (Option.default (CRef (lt_ref,None)) r) m ntn
| _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g ->
let fixl,ntns = extract_fixpoint_components true l in
let fixkind = Obligations.IsFixpoint g in
- do_program_recursive local fixkind fixl ntns
+ do_program_recursive local poly fixkind fixl ntns
| _, _ ->
errorlabstrm "do_program_fixpoint"
(str "Well-founded fixpoints not allowed in mutually recursive blocks")
-let do_fixpoint local l =
- if Flags.is_program_mode () then do_program_fixpoint local l
+let do_fixpoint local poly l =
+ if Flags.is_program_mode () then do_program_fixpoint local poly l
else
let fixl, ntns = extract_fixpoint_components true l in
let fix = interp_fixpoint fixl ntns in
let possible_indexes =
- List.map compute_possible_guardness_evidences (snd fix) in
- declare_fixpoint local fix possible_indexes ntns
+ List.map compute_possible_guardness_evidences (pi3 fix) in
+ declare_fixpoint local poly fix possible_indexes ntns
-let do_cofixpoint local l =
+let do_cofixpoint local poly l =
let fixl,ntns = extract_cofixpoint_components l in
if Flags.is_program_mode () then
- do_program_recursive local Obligations.IsCoFixpoint fixl ntns
+ do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns
else
let cofix = interp_cofixpoint fixl ntns in
- declare_cofixpoint local cofix ntns
+ declare_cofixpoint local poly cofix ntns
diff --git a/toplevel/command.mli b/toplevel/command.mli
index d2ebdc5611..b2ba23ef2d 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -29,7 +29,7 @@ val get_declare_definition_hook : unit -> (definition_entry -> unit)
(** {6 Definitions/Let} *)
val interp_definition :
- local_binder list -> red_expr option -> constr_expr ->
+ local_binder list -> polymorphic -> red_expr option -> constr_expr ->
constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
val declare_definition : Id.t -> definition_kind ->
@@ -42,16 +42,25 @@ val do_definition : Id.t -> definition_kind ->
(** {6 Parameters/Assumptions} *)
+(* val interp_assumption : env -> evar_map ref -> *)
+(* local_binder list -> constr_expr -> *)
+(* types Univ.in_universe_context_set * Impargs.manual_implicits *)
+
(** returns [false] if the assumption is neither local to a section,
nor in a module type and meant to be instantiated. *)
-val declare_assumption : coercion_flag -> assumption_kind -> types ->
+val declare_assumption : coercion_flag -> assumption_kind ->
+ types Univ.in_universe_context_set ->
Impargs.manual_implicits ->
bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located ->
global_reference * bool
-val do_assumptions : locality * assumption_object_kind ->
+val do_assumptions : locality * polymorphic * assumption_object_kind ->
Vernacexpr.inline -> simple_binder with_coercion list -> bool
+(* val declare_assumptions : variable Loc.located list -> *)
+(* coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> *)
+(* Impargs.manual_implicits -> bool -> Vernacexpr.inline -> bool *)
+
(** {6 Inductive and coinductive types} *)
(** Extracting the semantical components out of the raw syntax of mutual
@@ -77,7 +86,7 @@ type one_inductive_impls =
Impargs.manual_implicits list (** for constrs *)
val interp_mutual_inductive :
- structured_inductive_expr -> decl_notation list -> bool ->
+ structured_inductive_expr -> decl_notation list -> polymorphic -> bool(*finite*) ->
mutual_inductive_entry * one_inductive_impls list
(** Registering a mutual inductive definition together with its
@@ -90,7 +99,7 @@ val declare_mutual_inductive_with_eliminations :
(** Entry points for the vernacular commands Inductive and CoInductive *)
val do_mutual_inductive :
- (one_inductive_expr * decl_notation list) list -> bool -> unit
+ (one_inductive_expr * decl_notation list) list -> polymorphic -> bool -> unit
(** {6 Fixpoints and cofixpoints} *)
@@ -120,33 +129,38 @@ type recursive_preentry =
val interp_fixpoint :
structured_fixpoint_expr list -> decl_notation list ->
- recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list
+ recursive_preentry * Univ.universe_context_set *
+ (Name.t list * Impargs.manual_implicits * int option) list
val interp_cofixpoint :
structured_fixpoint_expr list -> decl_notation list ->
- recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list
+ recursive_preentry * Univ.universe_context_set *
+ (Name.t list * Impargs.manual_implicits * int option) list
(** Registering fixpoints and cofixpoints in the environment *)
val declare_fixpoint :
- locality -> recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list ->
+ locality -> polymorphic ->
+ recursive_preentry * Univ.universe_context_set *
+ (Name.t list * Impargs.manual_implicits * int option) list ->
lemma_possible_guards -> decl_notation list -> unit
-val declare_cofixpoint :
- locality -> recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list ->
- decl_notation list -> unit
+val declare_cofixpoint : locality -> polymorphic ->
+ recursive_preentry * Univ.universe_context_set *
+ (Name.t list * Impargs.manual_implicits * int option) list ->
+ decl_notation list -> unit
(** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
val do_fixpoint :
- locality -> (fixpoint_expr * decl_notation list) list -> unit
+ locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
val do_cofixpoint :
- locality -> (cofixpoint_expr * decl_notation list) list -> unit
+ locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
(** Utils *)
val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
-val declare_fix : definition_kind -> Id.t ->
+val declare_fix : definition_kind -> Univ.universe_context -> Id.t ->
Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 51dc8d5bbd..d772171e59 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -382,6 +382,7 @@ let parse_args arglist =
Serialize.document Xml_printer.to_string_fmt; exit 0
|"-ideslave" -> Flags.ide_slave := true
|"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet
+ |"-indices-matter" -> Indtypes.enforce_indices_matter ()
|"-just-parsing" -> Vernac.just_parsing := true
|"-lazy-load-proofs" -> Flags.load_proofs := Flags.Lazy
|"-m"|"--memory" -> memory_stat := true
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index b9ffbaea55..55475a3785 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -69,14 +69,9 @@ let abstract_inductive hyps nparams inds =
in (params',ind'')
let refresh_polymorphic_type_of_inductive (_,mip) =
- match mip.mind_arity with
- | Monomorphic s ->
- s.mind_user_arity
- | Polymorphic ar ->
- let ctx = List.rev mip.mind_arity_ctxt in
- mkArity (List.rev ctx,Termops.new_Type_sort())
+ mip.mind_arity.mind_user_arity
-let process_inductive sechyps modlist mib =
+let process_inductive (sechyps,abs_ctx) modlist mib =
let nparams = mib.mind_nparams in
let inds =
Array.map_to_list
@@ -90,7 +85,11 @@ let process_inductive sechyps modlist mib =
mib.mind_packets in
let sechyps' = map_named_context (expmod_constr modlist) sechyps in
let (params',inds') = abstract_inductive sechyps' nparams inds in
- { mind_entry_record = mib.mind_record;
+ let univs = Univ.UContext.union abs_ctx mib.mind_universes in
+ { mind_entry_record = mib.mind_record <> None;
mind_entry_finite = mib.mind_finite;
mind_entry_params = params';
- mind_entry_inds = inds' }
+ mind_entry_inds = inds';
+ mind_entry_polymorphic = mib.mind_polymorphic;
+ mind_entry_universes = univs
+ }
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index 6cef31c8a8..c074a1cc88 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -12,4 +12,4 @@ open Entries
open Opaqueproof
val process_inductive :
- named_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+ named_context Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index fd74f9c06d..9d6e9756dd 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -65,7 +65,7 @@ let contract3' env a b c = function
contract3 env a b c, ConversionFailed (env',t1,t2)
| NotSameArgSize | NotSameHead | NoCanonicalStructure
| MetaOccurInBody _ | InstanceNotSameType _
- | UnifUnivInconsistency as x -> contract3 env a b c, x
+ | UnifUnivInconsistency _ as x -> contract3 env a b c, x
(** Printers *)
@@ -143,9 +143,15 @@ let rec pr_disjunction pr = function
| a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l
| [] -> assert false
+let pr_puniverses f env (c,u) =
+ f env c ++
+ (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then
+ str"(*" ++ Univ.Instance.pr u ++ str"*)"
+ else mt())
+
let explain_elim_arity env ind sorts c pj okinds =
let env = make_all_name_different env in
- let pi = pr_inductive env ind in
+ let pi = pr_inductive env (fst ind) in
let pc = pr_lconstr_env env c in
let msg = match okinds with
| Some(kp,ki,explanation) ->
@@ -200,14 +206,14 @@ let explain_number_branches env sigma cj expn =
str "expects " ++ int expn ++ str " branches."
let explain_ill_formed_branch env sigma c ci actty expty =
- let simp t = Reduction.nf_betaiota (Evarutil.nf_evar sigma t) in
+ let simp t = Reduction.nf_betaiota env (Evarutil.nf_evar sigma t) in
let c = Evarutil.nf_evar sigma c in
let env = make_all_name_different env in
let pc = pr_lconstr_env env c in
let pa, pe = pr_explicit env (simp actty) (simp expty) in
strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++
spc () ++ strbrk "the branch for constructor" ++ spc () ++
- quote (pr_constructor env ci) ++
+ quote (pr_puniverses pr_constructor env ci) ++
spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++
str "which should be" ++ brk(1,1) ++ pe ++ str "."
@@ -260,8 +266,12 @@ let explain_unification_error env sigma p1 p2 = function
quote (pr_existential_key evk) ++ str ":" ++ spc () ++
str "cannot unify" ++ t ++ spc () ++ str "and" ++ spc () ++
u ++ str ")"
- | UnifUnivInconsistency ->
- spc () ++ str "(Universe inconsistency)"
+ | UnifUnivInconsistency p ->
+ if !Constrextern.print_universes then
+ spc () ++ str "(Universe inconsistency: " ++
+ Univ.explain_universe_inconsistency p ++ str")"
+ else
+ spc () ++ str "(Universe inconsistency)"
let explain_actual_type env sigma j t reason =
let env = make_all_name_different env in
@@ -513,7 +523,7 @@ let explain_var_not_found env id =
spc () ++ str "was not found" ++
spc () ++ str "in the current" ++ spc () ++ str "environment" ++ str "."
-let explain_wrong_case_info env ind ci =
+let explain_wrong_case_info env (ind,u) ci =
let pi = pr_inductive (Global.env()) ind in
if eq_ind ci.ci_ind ind then
str "Pattern-matching expression on an object of inductive type" ++
@@ -584,6 +594,10 @@ let explain_non_linear_unification env m t =
strbrk " which would require to abstract twice on " ++
pr_lconstr_env env t ++ str "."
+let explain_unsatisfied_constraints env cst =
+ strbrk "Unsatisfied constraints: " ++ Univ.pr_constraints cst ++
+ spc () ++ str "(maybe a bugged tactic)."
+
let explain_type_error env sigma err =
let env = make_all_name_different env in
match err with
@@ -619,6 +633,8 @@ let explain_type_error env sigma err =
explain_ill_typed_rec_body env sigma i lna vdefj vargs
| WrongCaseInfo (ind,ci) ->
explain_wrong_case_info env ind ci
+ | UnsatisfiedConstraints cst ->
+ explain_unsatisfied_constraints env cst
let explain_pretype_error env sigma err =
let env = Evarutil.env_nf_betaiotaevar sigma env in
@@ -998,7 +1014,7 @@ let error_not_allowed_case_analysis isrec kind i =
str (if isrec then "Induction" else "Case analysis") ++
strbrk " on sort " ++ pr_sort kind ++
strbrk " is not allowed for inductive definition " ++
- pr_inductive (Global.env()) i ++ str "."
+ pr_inductive (Global.env()) (fst i) ++ str "."
let error_not_mutual_in_scheme ind ind' =
if eq_ind ind ind' then
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index f5ee027f13..2a408e03d1 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -27,13 +27,18 @@ open Decl_kinds
(**********************************************************************)
(* Registering schemes in the environment *)
-type mutual_scheme_object_function = mutual_inductive -> constr array * Declareops.side_effects
-type individual_scheme_object_function = inductive -> constr * Declareops.side_effects
+
+type mutual_scheme_object_function =
+ mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
+type individual_scheme_object_function =
+ inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
type 'a scheme_kind = string
let scheme_map = Summary.ref Indmap.empty ~name:"Schemes"
+let pr_scheme_kind = Pp.str
+
let cache_one_scheme kind (ind,const) =
let map = try Indmap.find ind !scheme_map with Not_found -> String.Map.empty in
scheme_map := Indmap.add ind (String.Map.add kind const map) !scheme_map
@@ -41,9 +46,9 @@ let cache_one_scheme kind (ind,const) =
let cache_scheme (_,(kind,l)) =
Array.iter (cache_one_scheme kind) l
-let subst_one_scheme subst ((mind,i),const) =
+let subst_one_scheme subst (ind,const) =
(* Remark: const is a def: the result of substitution is a constant *)
- ((subst_ind subst mind,i),fst (subst_con subst const))
+ (subst_ind subst ind,subst_constant subst const)
let subst_scheme (subst,(kind,l)) =
(kind,Array.map (subst_one_scheme subst) l)
@@ -67,8 +72,8 @@ type individual
type mutual
type scheme_object_function =
- | MutualSchemeFunction of (mutual_inductive -> constr array * Declareops.side_effects)
- | IndividualSchemeFunction of (inductive -> constr * Declareops.side_effects)
+ | MutualSchemeFunction of mutual_scheme_object_function
+ | IndividualSchemeFunction of individual_scheme_object_function
let scheme_object_table =
(Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t)
@@ -111,31 +116,37 @@ let compute_name internal id =
| KernelSilent ->
Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
-let define internal id c =
+let define internal id c p univs =
let fd = declare_constant ~internal in
let id = compute_name internal id in
+ let ctx = Evd.normalize_evar_universe_context univs in
+ let c = Vars.subst_univs_fn_constr
+ (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in
let entry = {
const_entry_body = Future.from_val (c,Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = None;
+ const_entry_proj = None;
+ const_entry_polymorphic = p;
+ const_entry_universes = Evd.evar_context_universe_context ctx;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None;
} in
let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
let () = match internal with
- | KernelSilent -> ()
- | _-> definition_message id
+ | KernelSilent -> ()
+ | _-> definition_message id
in
kn
let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =
- let c, eff = f ind in
+ let (c, ctx), eff = f ind in
let mib = Global.lookup_mind mind in
let id = match idopt with
| Some id -> id
| None -> add_suffix mib.mind_packets.(i).mind_typename suff in
- let const = define internal id c in
+ let const = define internal id c mib.mind_polymorphic ctx in
declare_scheme kind [|ind,const|];
const, Declareops.cons_side_effects
(Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff
@@ -147,12 +158,14 @@ let define_individual_scheme kind internal names (mind,i as ind) =
define_individual_scheme_base kind s f internal names ind
let define_mutual_scheme_base kind suff f internal names mind =
- let cl, eff = f mind in
+ let (cl, ctx), eff = f mind in
let mib = Global.lookup_mind mind in
let ids = Array.init (Array.length mib.mind_packets) (fun i ->
try Int.List.assoc i names
with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
- let consts = Array.map2 (define internal) ids cl in
+
+ let consts = Array.map2 (fun id cl ->
+ define internal id cl mib.mind_polymorphic ctx) ids cl in
let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
declare_scheme kind schemes;
consts,
@@ -185,4 +198,3 @@ let find_scheme kind (mind,i as ind) =
let check_scheme kind ind =
try let _ = find_scheme_on_env_too kind ind in true
with Not_found -> false
-
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index d57f1556d7..7f84843a9c 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -19,9 +19,9 @@ type individual
type 'a scheme_kind
type mutual_scheme_object_function =
- mutual_inductive -> constr array * Declareops.side_effects
+ mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
type individual_scheme_object_function =
- inductive -> constr * Declareops.side_effects
+ inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
(** Main functions to register a scheme builder *)
@@ -49,3 +49,6 @@ val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** inter
val find_scheme : 'a scheme_kind -> inductive -> constant * Declareops.side_effects
val check_scheme : 'a scheme_kind -> inductive -> bool
+
+
+val pr_scheme_kind : 'a scheme_kind -> Pp.std_ppcmds
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 2cc98feea4..c139f19108 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -113,13 +113,16 @@ let _ =
(* Util *)
-let define id internal c t =
+let define id internal ctx c t =
let f = declare_constant ~internal in
let kn = f id
(DefinitionEntry
{ const_entry_body = c;
const_entry_secctx = None;
const_entry_type = t;
+ const_entry_proj = None;
+ const_entry_polymorphic = true;
+ const_entry_universes = Evd.universe_context ctx; (* FIXME *)
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None;
@@ -292,6 +295,7 @@ let declare_sym_scheme ind =
(* Scheme command *)
+let smart_global_inductive y = smart_global_inductive y
let rec split_scheme l =
let env = Global.env() in
match l with
@@ -311,7 +315,7 @@ requested
let names inds recs isdep y z =
let ind = smart_global_inductive y in
let sort_of_ind = inductive_sort_family (snd (lookup_mind_specif env ind)) in
- let z' = family_of_sort (interp_sort z) in
+ let z' = interp_elimination_sort z in
let suffix = (
match sort_of_ind with
| InProp ->
@@ -345,19 +349,20 @@ requested
let do_mutual_induction_scheme lnamedepindsort =
let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
- and sigma = Evd.empty
and env0 = Global.env() in
- let lrecspec =
- List.map
- (fun (_,dep,ind,sort) -> (ind,dep,interp_elimination_sort sort))
- lnamedepindsort
+ let sigma, lrecspec =
+ List.fold_left
+ (fun (evd, l) (_,dep,ind,sort) ->
+ let evd, indu = Evd.fresh_inductive_instance env0 evd ind in
+ (evd, (indu,dep,interp_elimination_sort sort) :: l))
+ (Evd.from_env env0,[]) lnamedepindsort
in
- let listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
+ let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
let declare decl fi lrecref =
- let decltype = Retyping.get_type_of env0 Evd.empty decl in
- let decltype = refresh_universes decltype in
+ let decltype = Retyping.get_type_of env0 sigma decl in
+ (* let decltype = refresh_universes decltype in *)
let proof_output = Future.from_val (decl,Declareops.no_seff) in
- let cst = define fi UserVerbose proof_output (Some decltype) in
+ let cst = define fi UserVerbose sigma proof_output (Some decltype) in
ConstRef cst :: lrecref
in
let _ = List.fold_right2 declare listdecl lrecnames [] in
@@ -407,7 +412,9 @@ let fold_left' f = function
| hd :: tl -> List.fold_left f hd tl
let build_combined_scheme env schemes =
- let defs = List.map (fun cst -> (cst, Typeops.type_of_constant env cst)) schemes in
+ let defs = List.map (fun cst -> (* FIXME *)
+ let evd, c = Evd.fresh_constant_instance env Evd.empty cst in
+ (c, Typeops.type_of_constant_in env c)) schemes in
(* let nschemes = List.length schemes in *)
let find_inductive ty =
let (ctx, arity) = decompose_prod ty in
@@ -415,7 +422,7 @@ let build_combined_scheme env schemes =
match kind_of_term last with
| App (ind, args) ->
let ind = destInd ind in
- let (_,spec) = Inductive.lookup_mind_specif env ind in
+ let (_,spec) = Inductive.lookup_mind_specif env (fst ind) in
ctx, ind, spec.mind_nrealargs
| _ -> ctx, destInd last, 0
in
@@ -426,8 +433,8 @@ let build_combined_scheme env schemes =
let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in
let relargs = rel_vect 0 prods in
let concls = List.rev_map
- (fun (cst, t) ->
- mkApp(mkConst cst, relargs),
+ (fun (cst, t) -> (* FIXME *)
+ mkApp(mkConstU cst, relargs),
snd (decompose_prod_n prods t)) defs in
let concl_bod, concl_typ =
fold_left'
@@ -451,10 +458,9 @@ let do_combined_scheme name schemes =
with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared."))
schemes
in
- let env = Global.env () in
- let body,typ = build_combined_scheme env csts in
+ let body,typ = build_combined_scheme (Global.env ()) csts in
let proof_output = Future.from_val (body,Declareops.no_seff) in
- ignore (define (snd name) UserVerbose proof_output (Some typ));
+ ignore (define (snd name) UserVerbose Evd.empty proof_output (Some typ));
fixpoint_message None [snd name]
(**********************************************************************)
@@ -464,7 +470,7 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
let declare_default_schemes kn =
let mib = Global.lookup_mind kn in
let n = Array.length mib.mind_packets in
- if !elim_flag && (not mib.mind_record || !record_elim_flag) then
+ if !elim_flag && (mib.mind_record = None || !record_elim_flag) then
declare_induction_schemes kn;
if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
if is_eq_flag() then try_declare_beq_scheme kn;
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 761f9c214b..3b86cf72f8 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1269,7 +1269,7 @@ let add_notation local c ((loc,df),modifiers) sc =
(* Infix notations *)
-let inject_var x = CRef (Ident (Loc.ghost, Id.of_string x))
+let inject_var x = CRef (Ident (Loc.ghost, Id.of_string x),None)
let add_infix local ((loc,inf),modifiers) pr sc =
check_infix_modifiers modifiers;
@@ -1323,7 +1323,7 @@ let add_class_scope scope cl =
(* Check if abbreviation to a name and avoid early insertion of
maximal implicit arguments *)
let try_interp_name_alias = function
- | [], CRef ref -> intern_reference ref
+ | [], CRef (ref,_) -> intern_reference ref
| _ -> raise Not_found
let add_syntactic_definition ident (vars,c) local onlyparse =
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index d772af3c18..d937c400a7 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -21,7 +21,7 @@ open Pp
open Errors
open Util
-let declare_fix_ref = ref (fun _ _ _ _ _ -> assert false)
+let declare_fix_ref = ref (fun _ _ _ _ _ _ -> assert false)
let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
let trace s =
@@ -298,11 +298,15 @@ type obligation_info =
(Names.Id.t * Term.types * Evar_kinds.t Loc.located *
Evar_kinds.obligation_definition_status * Int.Set.t * unit Proofview.tactic option) array
+type 'a obligation_body =
+ | DefinedObl of 'a
+ | TermObl of constr
+
type obligation =
{ obl_name : Id.t;
obl_type : types;
obl_location : Evar_kinds.t Loc.located;
- obl_body : constr option;
+ obl_body : constant obligation_body option;
obl_status : Evar_kinds.obligation_definition_status;
obl_deps : Int.Set.t;
obl_tac : unit Proofview.tactic option;
@@ -320,6 +324,8 @@ type program_info = {
prg_name: Id.t;
prg_body: constr;
prg_type: constr;
+ prg_ctx: Univ.universe_context_set;
+ prg_subst : Universes.universe_opt_subst;
prg_obligations: obligations;
prg_deps : Id.t list;
prg_fixkind : fixpoint_kind option ;
@@ -383,27 +389,43 @@ let _ =
let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
-let get_obligation_body expand obl =
- let c = Option.get obl.obl_body in
+let get_body subst obl =
+ match obl.obl_body with
+ | None -> assert false
+ | Some (DefinedObl c) ->
+ let _, ctx = Environ.constant_type_in_ctx (Global.env ()) c in
+ let pc = subst_univs_fn_puniverses (Univ.level_subst_of subst) (c, Univ.UContext.instance ctx) in
+ DefinedObl pc
+ | Some (TermObl c) ->
+ TermObl (subst_univs_fn_constr subst c)
+
+let get_obligation_body expand subst obl =
+ let c = get_body subst obl in
+ let c' =
if expand && obl.obl_status == Evar_kinds.Expand then
- match kind_of_term c with
- | Const c -> constant_value (Global.env ()) c
- | _ -> c
- else c
-
-let obl_substitution expand obls deps =
+ (match c with
+ | DefinedObl pc -> constant_value_in (Global.env ()) pc
+ | TermObl c -> c)
+ else (match c with
+ | DefinedObl pc -> mkConstU pc
+ | TermObl c -> c)
+ in c'
+
+let obl_substitution expand subst obls deps =
Int.Set.fold
(fun x acc ->
let xobl = obls.(x) in
let oblb =
- try get_obligation_body expand xobl
+ try get_obligation_body expand subst xobl
with e when Errors.noncritical e -> assert false
in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
deps []
-let subst_deps expand obls deps t =
- let subst = obl_substitution expand obls deps in
- Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) subst) t
+let subst_deps expand subst obls deps t =
+ let subst = Universes.make_opt_subst subst in
+ let osubst = obl_substitution expand subst obls deps in
+ Vars.subst_univs_fn_constr subst
+ (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
let rec prod_app t n =
match kind_of_term (strip_outer_cast t) with
@@ -431,17 +453,18 @@ let replace_appvars subst =
in map_constr aux
let subst_prog expand obls ints prg =
- let subst = obl_substitution expand obls ints in
+ let usubst = Universes.make_opt_subst prg.prg_subst in
+ let subst = obl_substitution expand usubst obls ints in
if get_hide_obligations () then
(replace_appvars subst prg.prg_body,
- replace_appvars subst (Termops.refresh_universes prg.prg_type))
+ replace_appvars subst ((* Termops.refresh_universes *) prg.prg_type))
else
let subst' = List.map (fun (n, (_, b)) -> n, b) subst in
(Vars.replace_vars subst' prg.prg_body,
- Vars.replace_vars subst' (Termops.refresh_universes prg.prg_type))
+ Vars.replace_vars subst' ((* Termops.refresh_universes *) prg.prg_type))
-let subst_deps_obl obls obl =
- let t' = subst_deps true obls obl.obl_deps obl.obl_type in
+let subst_deps_obl subst obls obl =
+ let t' = subst_deps true subst obls obl.obl_deps obl.obl_type in
{ obl with obl_type = t' }
module ProgMap = Map.Make(Id)
@@ -509,6 +532,9 @@ let declare_definition prg =
{ const_entry_body = Future.from_val (body,Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = Some typ;
+ const_entry_proj = None;
+ const_entry_polymorphic = pi2 prg.prg_kind;
+ const_entry_universes = Univ.ContextSet.to_context prg.prg_ctx;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None;
@@ -556,10 +582,9 @@ let declare_mutual_definition l =
let fixkind = Option.get first.prg_fixkind in
let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
+ let (local,poly,kind) = first.prg_kind in
let fixnames = first.prg_deps in
- let kind =
- fst first.prg_kind,
- if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in
+ let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in
let indexes, fixdecls =
match fixkind with
| IsFixpoint wfl ->
@@ -578,13 +603,15 @@ let declare_mutual_definition l =
mkCoFix (i,fixdecls),Declareops.no_seff) 0 l
in
(* Declare the recursive definitions *)
- let kns = List.map4 (!declare_fix_ref kind) fixnames fixdecls fixtypes fiximps in
+ let ctx = Univ.ContextSet.to_context first.prg_ctx in
+ let kns = List.map4 (!declare_fix_ref (local, poly, kind) ctx)
+ fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
List.iter Metasyntax.add_notation_interpretation first.prg_notations;
Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
let gr = List.hd kns in
let kn = match gr with ConstRef kn -> kn | _ -> assert false in
- first.prg_hook (fst first.prg_kind) gr;
+ first.prg_hook local gr;
List.iter progmap_remove l; kn
let shrink_body c =
@@ -597,20 +624,25 @@ let shrink_body c =
(b, 1, []) ctx
in List.map (fun (c,t) -> (c,None,t)) ctx, b', Array.of_list args
-let declare_obligation prg obl body =
+let declare_obligation prg obl body uctx =
let body = prg.prg_reduce body in
let ty = prg.prg_reduce obl.obl_type in
match obl.obl_status with
- | Evar_kinds.Expand -> { obl with obl_body = Some body }
+ | Evar_kinds.Expand -> { obl with obl_body = Some (TermObl body) }
| Evar_kinds.Define opaque ->
let opaque = if get_proofs_transparency () then false else opaque in
+ let poly = pi2 prg.prg_kind in
let ctx, body, args =
- if get_shrink_obligations () then shrink_body body else [], body, [||]
+ if get_shrink_obligations () && not poly then
+ shrink_body body else [], body, [||]
in
let ce =
{ const_entry_body = Future.from_val(body,Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = if List.is_empty ctx then Some ty else None;
+ const_entry_proj = None;
+ const_entry_polymorphic = poly;
+ const_entry_universes = uctx;
const_entry_opaque = opaque;
const_entry_inline_code = false;
const_entry_feedback = None;
@@ -623,9 +655,13 @@ let declare_obligation prg obl body =
Auto.add_hints false [Id.to_string prg.prg_name]
(Auto.HintsUnfoldEntry [EvalConstRef constant]);
definition_message obl.obl_name;
- { obl with obl_body = Some (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx) }
+ { obl with obl_body =
+ if poly then
+ Some (DefinedObl constant)
+ else
+ Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
-let init_prog_info n b t deps fixkind notations obls impls k reduce hook =
+let init_prog_info n b t ctx deps fixkind notations obls impls kind reduce hook =
let obls', b =
match b with
| None ->
@@ -645,9 +681,10 @@ let init_prog_info n b t deps fixkind notations obls impls k reduce hook =
obls, b
in
{ prg_name = n ; prg_body = b; prg_type = reduce t;
+ prg_ctx = ctx; prg_subst = Univ.LMap.empty;
prg_obligations = (obls', Array.length obls');
prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
- prg_implicits = impls; prg_kind = k; prg_reduce = reduce;
+ prg_implicits = impls; prg_kind = kind; prg_reduce = reduce;
prg_hook = hook; }
let get_prog name =
@@ -734,14 +771,14 @@ let dependencies obls n =
obls;
!res
-let goal_kind = Decl_kinds.Local, Decl_kinds.DefinitionBody Decl_kinds.Definition
+let goal_kind poly = Decl_kinds.Local, poly, Decl_kinds.DefinitionBody Decl_kinds.Definition
-let goal_proof_kind = Decl_kinds.Local, Decl_kinds.Proof Decl_kinds.Lemma
+let goal_proof_kind poly = Decl_kinds.Local, poly, Decl_kinds.Proof Decl_kinds.Lemma
-let kind_of_opacity o =
+let kind_of_obligation poly o =
match o with
- | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind
- | _ -> goal_proof_kind
+ | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind poly
+ | _ -> goal_proof_kind poly
let not_transp_msg =
str "Obligation should be transparent but was declared opaque." ++ spc () ++
@@ -755,17 +792,37 @@ let rec string_of_list sep f = function
| x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl
(* Solve an obligation using tactics, return the corresponding proof term *)
-let solve_by_tac evi t =
+
+let solve_by_tac evi t poly subst ctx =
let id = Id.of_string "H" in
+ let concl = Universes.subst_opt_univs_constr subst evi.evar_concl in
(* spiwack: the status is dropped *)
- let (entry,_) = Pfedit.build_constant_by_tactic
- id ~goal_kind evi.evar_hyps evi.evar_concl (Tacticals.New.tclCOMPLETE t) in
+ let (entry,_,subst) = Pfedit.build_constant_by_tactic
+ id ~goal_kind:(goal_kind poly) evi.evar_hyps (concl, ctx) (Tacticals.New.tclCOMPLETE t) in
let env = Global.env () in
let entry = Term_typing.handle_side_effects env entry in
let body, eff = Future.force entry.Entries.const_entry_body in
assert(Declareops.side_effects_is_empty eff);
Inductiveops.control_only_guard (Global.env ()) body;
- body
+ body, subst, entry.Entries.const_entry_universes
+
+ (* try *)
+ (* let substref = ref (Univ.LMap.empty, Univ.UContext.empty) in *)
+ (* Pfedit.start_proof id (goal_kind poly) evi.evar_hyps *)
+ (* (Universes.subst_opt_univs_constr subst evi.evar_concl, ctx) *)
+ (* (fun subst-> substref:=subst; fun _ _ -> ()); *)
+ (* Pfedit.by (tclCOMPLETE t); *)
+ (* let _,(const,_,_,_) = Pfedit.cook_proof ignore in *)
+ (* Pfedit.delete_current_proof (); *)
+ (* Inductiveops.control_only_guard (Global.env ()) *)
+ (* const.Entries.const_entry_body; *)
+ (* let subst, ctx = !substref in *)
+ (* subst_univs_fn_constr (Universes.make_opt_subst subst) const.Entries.const_entry_body, *)
+ (* subst, const.Entries.const_entry_universes *)
+ (* with reraise -> *)
+ (* let reraise = Errors.push reraise in *)
+ (* Pfedit.delete_current_proof(); *)
+ (* raise reraise *)
let rec solve_obligation prg num tac =
let user_num = succ num in
@@ -776,9 +833,12 @@ let rec solve_obligation prg num tac =
else
match deps_remaining obls obl.obl_deps with
| [] ->
- let obl = subst_deps_obl obls obl in
- Lemmas.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
- (fun strength gr ->
+ let ctx = prg.prg_ctx in
+ let obl = subst_deps_obl prg.prg_subst obls obl in
+ let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
+ Lemmas.start_proof obl.obl_name kind
+ (Universes.subst_opt_univs_constr prg.prg_subst obl.obl_type, ctx)
+ (fun strength gr ->
let cst = match gr with ConstRef cst -> cst | _ -> assert false in
let obl =
let transparent = evaluable_constant cst (Global.env ()) in
@@ -786,10 +846,10 @@ let rec solve_obligation prg num tac =
match obl.obl_status with
| Evar_kinds.Expand ->
if not transparent then error_not_transp ()
- else constant_value (Global.env ()) cst
+ else DefinedObl cst
| Evar_kinds.Define opaque ->
if not opaque && not transparent then error_not_transp ()
- else Globnames.constr_of_global gr
+ else DefinedObl cst
in
if transparent then
Auto.add_hints true [Id.to_string prg.prg_name]
@@ -798,8 +858,15 @@ let rec solve_obligation prg num tac =
in
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
- let res =
- try update_obls prg obls (pred rem)
+(* let ctx = Univ.ContextSet.of_context ctx in *)
+ let subst = Univ.LMap.empty (** FIXME *) in
+ let res =
+ try update_obls
+ {prg with prg_body = Universes.subst_opt_univs_constr subst prg.prg_body;
+ prg_type = Universes.subst_opt_univs_constr subst prg.prg_type;
+ prg_ctx = ctx;
+ prg_subst = Univ.LMap.union prg.prg_subst subst}
+ obls (pred rem)
with e when Errors.noncritical e ->
pperror (Errors.print (Cerrors.process_vernac_interp_error e))
in
@@ -835,7 +902,7 @@ and solve_obligation_by_tac prg obls i tac =
| None ->
try
if List.is_empty (deps_remaining obls obl.obl_deps) then
- let obl = subst_deps_obl obls obl in
+ let obl = subst_deps_obl prg.prg_subst obls obl in
let tac =
match tac with
| Some t -> t
@@ -844,8 +911,11 @@ and solve_obligation_by_tac prg obls i tac =
| Some t -> t
| None -> snd (get_default_tactic ())
in
- let t = solve_by_tac (evar_of_obligation obl) tac in
- obls.(i) <- declare_obligation prg obl t;
+ let t, subst, ctx =
+ solve_by_tac (evar_of_obligation obl) tac
+ (pi2 prg.prg_kind) prg.prg_subst prg.prg_ctx
+ in
+ obls.(i) <- declare_obligation {prg with prg_subst = subst} obl t ctx;
true
else false
with e when Errors.noncritical e ->
@@ -929,10 +999,10 @@ let show_term n =
Printer.pr_constr_env (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
++ Printer.pr_constr_env (Global.env ()) prg.prg_body)
-let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
+let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
let info = str (Id.to_string n) ++ str " has type-checked" in
- let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
+ let prg = init_prog_info n term t ctx [] None [] obls implicits kind reduce hook in
let obls,_ = prg.prg_obligations in
if Int.equal (Array.length obls) 0 then (
Flags.if_verbose msg_info (info ++ str ".");
@@ -947,12 +1017,12 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
| _ -> res)
-let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce)
+let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
?(hook=fun _ _ -> ()) notations fixkind =
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
List.iter
(fun (n, b, t, imps, obls) ->
- let prg = init_prog_info n (Some b) t deps (Some fixkind)
+ let prg = init_prog_info n (Some b) t ctx deps (Some fixkind)
notations obls imps kind reduce hook
in progmap_add n prg) l;
let _defined =
@@ -975,13 +1045,13 @@ let admit_prog prg =
(fun i x ->
match x.obl_body with
| None ->
- let x = subst_deps_obl obls x in
- (** ppedrot: seems legit to have admitted obligations as local *)
+ let x = subst_deps_obl prg.prg_subst obls x in
+ let ctx = Univ.ContextSet.to_context prg.prg_ctx in
let kn = Declare.declare_constant x.obl_name ~local:true
- (ParameterEntry (None, x.obl_type,None), IsAssumption Conjectural)
+ (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural)
in
assumption_message x.obl_name;
- obls.(i) <- { x with obl_body = Some (mkConst kn) }
+ obls.(i) <- { x with obl_body = Some (DefinedObl kn) }
| Some _ -> ())
obls;
ignore(update_obls prg obls 0)
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 746b4ed14d..f03e6c4468 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -17,7 +17,7 @@ open Decl_kinds
open Tacexpr
(** Forward declaration. *)
-val declare_fix_ref : (definition_kind -> Id.t ->
+val declare_fix_ref : (definition_kind -> Univ.universe_context -> Id.t ->
Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref
val declare_definition_ref :
@@ -64,6 +64,7 @@ val set_proofs_transparency : bool -> unit (* true = All transparent, false = Op
val get_proofs_transparency : unit -> bool
val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types ->
+ Univ.universe_context_set ->
?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
?kind:Decl_kinds.definition_kind ->
?tactic:unit Proofview.tactic ->
@@ -80,6 +81,7 @@ type fixpoint_kind =
val add_mutual_definitions :
(Names.Id.t * Term.constr * Term.types *
(Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
+ Univ.universe_context_set ->
?tactic:unit Proofview.tactic ->
?kind:Decl_kinds.definition_kind ->
?reduce:(Term.constr -> Term.constr) ->
diff --git a/toplevel/record.ml b/toplevel/record.ml
index dc38d25194..7411a6377b 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -13,6 +13,7 @@ open Names
open Globnames
open Nameops
open Term
+open Context
open Vars
open Environ
open Declarations
@@ -23,9 +24,21 @@ open Decl_kinds
open Type_errors
open Constrexpr
open Constrexpr_ops
+open Goptions
(********** definition d'un record (structure) **************)
+(** Flag governing use of primitive projections. Disabled by default. *)
+let primitive_flag = ref false
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "use of primitive projections";
+ optkey = ["Primitive";"Projections"];
+ optread = (fun () -> !primitive_flag) ;
+ optwrite = (fun b -> primitive_flag := b) }
+
let interp_fields_evars evars env impls_env nots l =
List.fold_left2
(fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
@@ -41,15 +54,25 @@ let interp_fields_evars evars env impls_env nots l =
(push_rel d env, impl :: uimpls, d::params, impls))
(env, [], [], impls_env) nots l
+let compute_constructor_level evars env l =
+ List.fold_right (fun (n,b,t as d) (env, univ) ->
+ let univ =
+ if b = None then
+ let s = Retyping.get_sort_of env evars t in
+ Univ.sup (univ_of_sort s) univ
+ else univ
+ in (push_rel d env, univ))
+ l (env, Univ.type0m_univ)
+
let binder_of_decl = function
| Vernacexpr.AssumExpr(n,t) -> (n,None,t)
| Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None, None))
let binders_of_decls = List.map binder_of_decl
-let typecheck_params_and_fields id t ps nots fs =
+let typecheck_params_and_fields def id t ps nots fs =
let env0 = Global.env () in
- let evars = ref Evd.empty in
+ let evars = ref (Evd.from_env ~ctx:(Univ.ContextSet.empty) env0) in
let _ =
let error bk (loc, name) =
match bk, name with
@@ -62,15 +85,48 @@ let typecheck_params_and_fields id t ps nots fs =
| LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps
in
let impls_env, ((env1,newps), imps) = interp_context_evars evars env0 ps in
- let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (Termops.new_Type ()) t) newps in
+ let t' = match t with
+ | Some t ->
+ let env = push_rel_context newps env0 in
+ let s = interp_type_evars evars env ~impls:empty_internalization_env t in
+ let sred = Reductionops.whd_betadeltaiota env !evars s in
+ (match kind_of_term sred with
+ | Sort s' ->
+ (match Evd.is_sort_variable !evars s' with
+ | Some (l, _) -> evars := Evd.make_flexible_variable !evars true (* (not def) *) l; sred
+ | None -> s)
+ | _ -> user_err_loc (constr_loc t,"", str"Sort expected."))
+ | None ->
+ let uvarkind = if (* not def *) true then Evd.univ_flexible_alg else Evd.univ_flexible in
+ mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars)
+ in
+ let fullarity = it_mkProd_or_LetIn t' newps in
let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
let env2,impls,newfs,data =
interp_fields_evars evars env_ar impls_env nots (binders_of_decls fs)
in
- let sigma = Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar Evd.empty !evars in
- let newps = Evarutil.nf_rel_context_evar sigma newps in
- let newfs = Evarutil.nf_rel_context_evar sigma newfs in
- imps, newps, impls, newfs
+ let sigma =
+ Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar Evd.empty !evars in
+ let evars, nf = Evarutil.nf_evars_and_universes sigma in
+ let arity = nf t' in
+ let evars =
+ let _, univ = compute_constructor_level evars env_ar newfs in
+ let aritysort = destSort arity in
+ if Sorts.is_prop aritysort ||
+ (Sorts.is_set aritysort && engagement env0 = Some ImpredicativeSet) then
+ evars
+ else Evd.set_leq_sort evars (Type univ) aritysort
+ (* try Evarconv.the_conv_x_leq env_ar ty arity evars *)
+ (* with Reduction.NotConvertible -> *)
+ (* Pretype_errors.error_cannot_unify env_ar evars (ty, arity) *)
+ in
+ let evars, nf = Evarutil.nf_evars_and_universes evars in
+ let newps = map_rel_context nf newps in
+ let newfs = map_rel_context nf newfs in
+ let ce t = Evarutil.check_evars env0 Evd.empty evars t in
+ List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps);
+ List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs);
+ Evd.universe_context evars, nf arity, imps, newps, impls, newfs
let degenerate_decl (na,b,t) =
let id = match na with
@@ -147,21 +203,25 @@ let subst_projection fid l c =
raise (NotDefinable (MissingProj (fid,List.rev !bad_projs)));
c''
-let instantiate_possibly_recursive_type indsp paramdecls fields =
+let instantiate_possibly_recursive_type indu paramdecls fields =
let subst = List.map_i (fun i _ -> mkRel i) 1 paramdecls in
- Termops.substl_rel_context (subst@[mkInd indsp]) fields
+ Termops.substl_rel_context (subst@[mkIndU indu]) fields
(* We build projections *)
let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
let paramdecls = mib.mind_params_ctxt in
- let r = mkInd indsp in
+ let poly = mib.mind_polymorphic and ctx = mib.mind_universes in
+ let u = Inductive.inductive_instance mib in
+ let indu = indsp, u in
+ let r = mkIndU (indsp,u) in
let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in
let paramargs = Termops.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
let x = match name with Some n -> Name n | None -> Namegen.named_hd (Global.env()) r Anonymous in
- let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
+ let fields = instantiate_possibly_recursive_type indu paramdecls fields in
let lifted_fields = Termops.lift_rel_context 1 fields in
+ let nfields = List.length fields in
let (_,kinds,sp_projs,_) =
List.fold_left3
(fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) impls ->
@@ -181,18 +241,29 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
let p = mkLambda (x, lift 1 rp, ccl') in
let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
let ci = Inductiveops.make_case_info env indsp LetStyle in
- mkCase (ci, p, mkRel 1, [|branch|]) in
+ mkCase (ci, p, mkRel 1, [|branch|])
+ in
let proj =
it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
let projtyp =
it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
let kn =
try
+ let projinfo =
+ (fst indsp, mib.mind_nparams, nfields - nfi, ccl)
+ in
+ let projinfo =
+ if !primitive_flag && optci = None then Some projinfo
+ else None
+ in
let cie = {
const_entry_body =
Future.from_val (proj,Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = Some projtyp;
+ const_entry_polymorphic = poly;
+ const_entry_universes = ctx;
+ const_entry_proj = projinfo;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None;
@@ -204,15 +275,18 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
with Type_errors.TypeError (ctx,te) ->
raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
let refi = ConstRef kn in
- let constr_fi = mkConst kn in
Impargs.maybe_declare_manual_implicits false refi impls;
if coe then begin
let cl = Class.class_of_global (IndRef indsp) in
- Class.try_add_new_coercion_with_source refi ~local:false ~source:cl
+ Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl
end;
- let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
- let constr_fip = applist (constr_fi,proj_args) in
- (Some kn::sp_projs, Projection constr_fip::subst)
+ let constr_fip =
+ if !primitive_flag then mkProj (kn,mkRel 1)
+ else
+ let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
+ applist (mkConstU (kn,u),proj_args)
+ in
+ (Some kn::sp_projs, Projection constr_fip::subst)
with NotDefinable why ->
warning_or_error coe indsp why;
(None::sp_projs,NoProjection fi::subst) in
@@ -238,7 +312,7 @@ let structure_signature ctx =
open Typeclasses
-let declare_structure finite infer id idbuild paramimpls params arity fieldimpls fields
+let declare_structure finite infer poly ctx id idbuild paramimpls params arity fieldimpls fields
?(kind=StructureComponent) ?name is_coe coers sign =
let nparams = List.length params and nfields = List.length fields in
let args = Termops.extended_rel_list nfields params in
@@ -256,20 +330,23 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
begin match finite with
| BiFinite ->
if Termops.dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then
- error "Records declared with the keyword Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command."
+ error ("Records declared with the keyword Record or Structure cannot be recursive." ^
+ "You can, however, define recursive records using the Inductive or CoInductive command.")
| _ -> ()
end;
let mie =
{ mind_entry_params = List.map degenerate_decl params;
mind_entry_record = true;
mind_entry_finite = finite != CoFinite;
- mind_entry_inds = [mie_ind] } in
+ mind_entry_inds = [mie_ind];
+ mind_entry_polymorphic = poly;
+ mind_entry_universes = ctx } in
let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose mie [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let cstr = (rsp,1) in
let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
let build = ConstructRef cstr in
- let () = if is_coe then Class.try_add_new_coercion build ~local:false in
+ let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
rsp
@@ -282,43 +359,34 @@ let implicits_of_context ctx =
in ExplByPos (i, explname), (true, true, true))
1 (List.rev (Anonymous :: (List.map pi1 ctx)))
-let declare_class finite def infer id idbuild paramimpls params arity fieldimpls fields
+let declare_class finite def infer poly ctx id idbuild paramimpls params arity fieldimpls fields
?(kind=StructureComponent) ?name is_coe coers priorities sign =
let fieldimpls =
- (* Make the class and all params implicits in the projections *)
- let ctx_impls = implicits_of_context params in
- let len = succ (List.length params) in
- List.map (fun x -> ctx_impls @ Impargs.lift_implicits len x) fieldimpls
+ (* Make the class implicit in the projections, and the params if applicable. *)
+ (* if def then *)
+ let len = List.length params in
+ let impls = implicits_of_context params in
+ List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls
+ (* else List.map (fun x -> (ExplByPos (1, None), (true, true, true)) :: *)
+ (* Impargs.lift_implicits 1 x) fieldimpls *)
in
let impl, projs =
match fields with
| [(Name proj_name, _, field)] when def ->
let class_body = it_mkLambda_or_LetIn field params in
- let class_type = Option.map (fun ar -> it_mkProd_or_LetIn ar params) arity in
- let class_entry =
- { const_entry_body =
- Future.from_val (class_body,Declareops.no_seff);
- const_entry_secctx = None;
- const_entry_type = class_type;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- } in
+ let _class_type = it_mkProd_or_LetIn arity params in
+ let class_entry =
+ Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in
let cst = Declare.declare_constant (snd id)
(DefinitionEntry class_entry, IsDefinition Definition)
in
- let inst_type = appvectc (mkConst cst) (Termops.rel_vect 0 (List.length params)) in
- let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in
- let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
- let proj_entry =
- { const_entry_body =
- Future.from_val (proj_body,Declareops.no_seff);
- const_entry_secctx = None;
- const_entry_type = Some proj_type;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- } in
+ let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in
+ let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in
+ let proj_type =
+ it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in
+ let proj_body =
+ it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
+ let proj_entry = Declare.definition_entry ~types:proj_type ~poly ~univs:ctx proj_body in
let proj_cst = Declare.declare_constant proj_name
(DefinitionEntry proj_entry, IsDefinition Definition)
in
@@ -326,16 +394,20 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
Impargs.declare_manual_implicits false cref [paramimpls];
Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
Classes.set_typeclass_transparency (EvalConstRef cst) false false;
- let sub = match List.hd coers with Some b -> Some ((if b then Backward else Forward), List.hd priorities) | None -> None in
+ let sub = match List.hd coers with
+ | Some b -> Some ((if b then Backward else Forward), List.hd priorities)
+ | None -> None
+ in
cref, [Name proj_name, sub, Some proj_cst]
| _ ->
let idarg = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
- let ind = declare_structure BiFinite infer (snd id) idbuild paramimpls
- params (Option.default (Termops.new_Type ()) arity) fieldimpls fields
+ let ind = declare_structure BiFinite infer poly ctx (snd id) idbuild paramimpls
+ params arity fieldimpls fields
~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
in
let coers = List.map2 (fun coe pri ->
- Option.map (fun b -> if b then Backward, pri else Forward, pri) coe)
+ Option.map (fun b ->
+ if b then Backward, pri else Forward, pri) coe)
coers priorities
in
IndRef ind, (List.map3 (fun (id, _, _) b y -> (id, b, y))
@@ -344,7 +416,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
let ctx_context =
List.map (fun (na, b, t) ->
match Typeclasses.class_of_constr t with
- | Some (_, (cl, _)) -> Some (cl.cl_impl, true) (*List.exists (fun (_, n) -> n = na) supnames)*)
+ | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true) (*FIXME: ignore universes?*)
| None -> None)
params, params
in
@@ -359,19 +431,12 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
(* k.cl_projs coers priorities; *)
add_class k; impl
-let interp_and_check_sort sort =
- Option.map (fun sort ->
- let env = Global.env() and sigma = Evd.empty in
- let s = interp_constr sigma env sort in
- if isSort (Reductionops.whd_betadeltaiota env sigma s) then s
- else user_err_loc (constr_loc sort,"", str"Sort expected.")) sort
-
open Vernacexpr
(* [fs] corresponds to fields and [ps] to parameters; [coers] is a
list telling if the corresponding fields must me declared as coercions
or subinstances *)
-let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
+let definition_structure (kind,poly,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
let cfs,notations = List.split cfs in
let cfs,priorities = List.split cfs in
let coers,fs = List.split cfs in
@@ -386,20 +451,20 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
error "Priorities only allowed for type class substructures";
(* Now, younger decl in params and fields is on top *)
- let sc = interp_and_check_sort s in
- let implpars, params, implfs, fields =
+ let ctx, arity, implpars, params, implfs, fields =
States.with_state_protection (fun () ->
- typecheck_params_and_fields idstruc sc ps notations fs) () in
+ typecheck_params_and_fields (kind = Class true) idstruc s ps notations fs) () in
let sign = structure_signature (fields@params) in
match kind with
| Class def ->
- let gr = declare_class finite def infer (loc,idstruc) idbuild
- implpars params sc implfs fields is_coe coers priorities sign in
+ let gr = declare_class finite def infer poly ctx (loc,idstruc) idbuild
+ implpars params arity implfs fields is_coe coers priorities sign in
gr
| _ ->
- let arity = Option.default (Termops.new_Type ()) sc in
let implfs = List.map
- (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
- let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs
+ (fun impls -> implpars @ Impargs.lift_implicits
+ (succ (List.length params)) impls) implfs in
+ let ind = declare_structure finite infer poly ctx idstruc
+ idbuild implpars params arity implfs
fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
IndRef ind
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 018366667f..dac8636cb2 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -14,6 +14,8 @@ open Constrexpr
open Impargs
open Globnames
+val primitive_flag : bool ref
+
(** [declare_projections ref name coers params fields] declare projections of
record [ref] (if allowed) using the given [name] as argument, and put them
as coercions accordingly to [coers]; it returns the absolute names of projections *)
@@ -24,7 +26,8 @@ val declare_projections :
(Name.t * bool) list * constant option list
val declare_structure : Decl_kinds.recursivity_kind ->
- bool (**infer?*) -> Id.t -> Id.t ->
+ bool (**infer?*) -> bool (** polymorphic?*) -> Univ.universe_context ->
+ Id.t -> Id.t ->
manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *)
Impargs.manual_explicitation list list -> rel_context -> (** fields *)
?kind:Decl_kinds.definition_object_kind -> ?name:Id.t ->
@@ -34,6 +37,6 @@ val declare_structure : Decl_kinds.recursivity_kind ->
inductive
val definition_structure :
- inductive_kind * Decl_kinds.recursivity_kind * bool(**infer?*)* lident with_coercion * local_binder list *
+ inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * bool(**infer?*)* lident with_coercion * local_binder list *
(local_decl_expr with_instance with_priority with_notation) list *
Id.t * constr_expr option -> global_reference
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 38717850c9..1535ae6174 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -45,7 +45,7 @@ module SearchBlacklist =
let iter_constructors indsp fn env nconstr =
for i = 1 to nconstr do
- let typ = Inductiveops.type_of_constructor env (indsp, i) in
+ let typ, _ = Inductiveops.type_of_constructor_in_ctx env (indsp, i) in
fn (ConstructRef (indsp, i)) env typ
done
@@ -60,14 +60,15 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
with Not_found -> (* we are in a section *) () end
| "CONSTANT" ->
let cst = Global.constant_of_delta_kn kn in
- let typ = Typeops.type_of_constant env cst in
+ let typ, _ = Environ.constant_type_in_ctx env cst in
fn (ConstRef cst) env typ
| "INDUCTIVE" ->
let mind = Global.mind_of_delta_kn kn in
let mib = Global.lookup_mind mind in
let iter_packet i mip =
let ind = (mind, i) in
- let typ = Inductiveops.type_of_inductive env ind in
+ let i = (ind, Univ.UContext.instance mib.mind_universes) in
+ let typ = Inductiveops.type_of_inductive env i in
let () = fn (IndRef ind) env typ in
let len = Array.length mip.mind_user_lc in
iter_constructors ind fn env len
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 73a5095778..9851cfe87c 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -66,6 +66,7 @@ let print_usage_channel co command =
\n -dump-glob f dump globalizations in file f (to be used by coqdoc)\
\n -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\
\n -impredicative-set set sort Set impredicative\
+\n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\
\n -force-load-proofs load opaque proofs in memory initially\
\n -lazy-load-proofs load opaque proofs in memory by necessity (default)\
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d5559f9762..2e9bfedc78 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -252,11 +252,7 @@ let print_namespace ns =
print_list pr_id qn
in
let print_constant k body =
- let t =
- match body.Declarations.const_type with
- | Declarations.PolymorphicArity (ctx,a) -> mkArity (ctx, Term.Type a.Declarations.poly_level)
- | Declarations.NonPolymorphicType t -> t
- in
+ let t = body.Declarations.const_type in
print_kn k ++ str":" ++ spc() ++ Printer.pr_type t
in
let matches mp = match match_modulepath ns mp with
@@ -457,22 +453,22 @@ let start_proof_and_print k l hook =
let no_hook _ _ = ()
-let vernac_definition_hook = function
-| Coercion -> Class.add_coercion_hook
-| CanonicalStructure -> (fun _ -> Recordops.declare_canonical_structure)
-| SubClass -> Class.add_subclass_hook
+let vernac_definition_hook p = function
+| Coercion -> Class.add_coercion_hook p
+| CanonicalStructure -> fun _ -> Recordops.declare_canonical_structure
+| SubClass -> Class.add_subclass_hook p
| _ -> no_hook
-let vernac_definition locality (local,k) (loc,id as lid) def =
+let vernac_definition locality p (local,k) (loc,id as lid) def =
let local = enforce_locality_exp locality local in
- let hook = vernac_definition_hook k in
+ let hook = vernac_definition_hook p k in
let () = match local with
| Discharge -> Dumpglob.dump_definition lid true "var"
| Local | Global -> Dumpglob.dump_definition lid false "def"
in
(match def with
| ProveBody (bl,t) -> (* local binders, typ *)
- start_proof_and_print (local,DefinitionBody Definition)
+ start_proof_and_print (local,p,DefinitionBody Definition)
[Some lid, (bl,t,None)] no_hook
| DefineBody (bl,red_option,c,typ_opt) ->
let red_option = match red_option with
@@ -480,9 +476,9 @@ let vernac_definition locality (local,k) (loc,id as lid) def =
| Some r ->
let (evc,env)= get_current_context () in
Some (snd (interp_redexp env evc r)) in
- do_definition id (local,k) bl red_option c typ_opt hook)
+ do_definition id (local,p,k) bl red_option c typ_opt hook)
-let vernac_start_proof kind l lettop =
+let vernac_start_proof p kind l lettop =
if Dumpglob.dump () then
List.iter (fun (id, _) ->
match id with
@@ -492,7 +488,7 @@ let vernac_start_proof kind l lettop =
if lettop then
errorlabstrm "Vernacentries.StartProof"
(str "Let declarations can only be used in proof editing mode.");
- start_proof_and_print (Global, Proof kind) l no_hook
+ start_proof_and_print (Global, p, Proof kind) l no_hook
let qed_display_script = ref true
@@ -512,10 +508,10 @@ let vernac_exact_proof c =
save_proof (Vernacexpr.Proved(true,None));
if not status then Pp.feedback Interface.AddedAxiom
-let vernac_assumption locality (local, kind) l nl =
+let vernac_assumption locality poly (local, kind) l nl =
let local = enforce_locality_exp locality local in
let global = local == Global in
- let kind = local, kind in
+ let kind = local, poly, kind in
List.iter (fun (is_coe,(idl,c)) ->
if Dumpglob.dump () then
List.iter (fun lid ->
@@ -524,7 +520,7 @@ let vernac_assumption locality (local, kind) l nl =
let status = do_assumptions kind nl l in
if not status then Pp.feedback Interface.AddedAxiom
-let vernac_record k finite infer struc binders sort nameopt cfs =
+let vernac_record k poly finite infer struc binders sort nameopt cfs =
let const = match nameopt with
| None -> add_prefix "Build_" (snd (snd struc))
| Some (_,id as lid) ->
@@ -535,9 +531,9 @@ let vernac_record k finite infer struc binders sort nameopt cfs =
match x with
| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
| _ -> ()) cfs);
- ignore(Record.definition_structure (k,finite,infer,struc,binders,cfs,const,sort))
+ ignore(Record.definition_structure (k,poly,finite,infer,struc,binders,cfs,const,sort))
-let vernac_inductive finite infer indl =
+let vernac_inductive poly finite infer indl =
if Dumpglob.dump () then
List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
match cstrs with
@@ -550,13 +546,13 @@ let vernac_inductive finite infer indl =
match indl with
| [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
vernac_record (match b with Class true -> Class false | _ -> b)
- finite infer id bl c oc fs
+ poly finite infer id bl c oc fs
| [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
let f =
let (coe, ((loc, id), ce)) = l in
let coe' = if coe then Some true else None in
(((coe', AssumExpr ((loc, Name id), ce)), None), [])
- in vernac_record (Class true) finite infer id bl c None [f]
+ in vernac_record (Class true) poly finite infer id bl c None [f]
| [ ( id , bl , c , Class true, _), _ ] ->
Errors.error "Definitional classes must have a single method"
| [ ( id , bl , c , Class false, Constructors _), _ ] ->
@@ -568,19 +564,19 @@ let vernac_inductive finite infer indl =
| _ -> Errors.error "Cannot handle mutually (co)inductive records."
in
let indl = List.map unpack indl in
- do_mutual_inductive indl (finite != CoFinite)
+ do_mutual_inductive indl poly (finite != CoFinite)
-let vernac_fixpoint locality local l =
+let vernac_fixpoint locality poly local l =
let local = enforce_locality_exp locality local in
if Dumpglob.dump () then
List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
- do_fixpoint local l
+ do_fixpoint local poly l
-let vernac_cofixpoint locality local l =
+let vernac_cofixpoint locality poly local l =
let local = enforce_locality_exp locality local in
if Dumpglob.dump () then
List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
- do_cofixpoint local l
+ do_cofixpoint local poly l
let vernac_scheme l =
if Dumpglob.dump () then
@@ -766,27 +762,26 @@ let vernac_require import qidl =
let vernac_canonical r =
Recordops.declare_canonical_structure (smart_global r)
-let vernac_coercion locality local ref qids qidt =
+let vernac_coercion locality poly local ref qids qidt =
let local = enforce_locality locality local in
let target = cl_of_qualid qidt in
let source = cl_of_qualid qids in
let ref' = smart_global ref in
- Class.try_add_new_coercion_with_target ref' ~local ~source ~target;
+ Class.try_add_new_coercion_with_target ref' ~local poly ~source ~target;
if_verbose msg_info (pr_global ref' ++ str " is now a coercion")
-let vernac_identity_coercion locality local id qids qidt =
+let vernac_identity_coercion locality poly local id qids qidt =
let local = enforce_locality locality local in
let target = cl_of_qualid qidt in
let source = cl_of_qualid qids in
- Class.try_add_new_identity_coercion id ~local ~source ~target
+ Class.try_add_new_identity_coercion id ~local poly ~source ~target
(* Type classes *)
-let vernac_instance abst locality sup inst props pri =
+let vernac_instance abst locality poly sup inst props pri =
let global = not (make_section_locality locality) in
Dumpglob.dump_constraint inst false "inst";
- ignore(Classes.new_instance
- ~abstract:abst ~global sup inst props pri)
+ ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri)
let vernac_context l =
if not (Classes.context l) then Pp.feedback Interface.AddedAxiom
@@ -909,9 +904,9 @@ let vernac_remove_hints locality dbs ids =
let local = make_module_locality locality in
Auto.remove_hints local dbs (List.map Smartlocate.global_with_alias ids)
-let vernac_hints locality local lb h =
+let vernac_hints locality poly local lb h =
let local = enforce_module_locality locality local in
- Auto.add_hints local lb (Auto.interp_hints h)
+ Auto.add_hints local lb (Auto.interp_hints poly h)
let vernac_syntactic_definition locality lid x local y =
Dumpglob.dump_definition lid false "syndef";
@@ -938,7 +933,8 @@ let vernac_declare_arguments locality r l nargs flags =
then error "Arguments names must be distinct.";
let sr = smart_global r in
let inf_names =
- Impargs.compute_implicits_names (Global.env()) (Global.type_of_global sr) in
+ let ty = Global.type_of_global_unsafe sr in
+ Impargs.compute_implicits_names (Global.env ()) ty in
let string_of_name = function Anonymous -> "_" | Name id -> Id.to_string id in
let rec check li ld ls = match li, ld, ls with
| [], [], [] -> ()
@@ -1051,7 +1047,7 @@ let default_env () = {
let vernac_reserve bl =
let sb_decl = (fun (idl,c) ->
- let t = Constrintern.interp_type Evd.empty (Global.env()) c in
+ let t,ctx = Constrintern.interp_type Evd.empty (Global.env()) c in
let t = Detyping.detype false [] [] t in
let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
Reserve.declare_reserved_type idl t)
@@ -1218,6 +1214,15 @@ let _ =
declare_bool_option
{ optsync = true;
optdepr = false;
+ optname = "universe polymorphism";
+ optkey = ["Universe"; "Polymorphism"];
+ optread = Flags.is_universe_polymorphism;
+ optwrite = Flags.make_universe_polymorphism }
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
optname = "use of virtual machine inside the kernel";
optkey = ["Virtual";"Machine"];
optread = (fun () -> Vconv.use_vm ());
@@ -1378,7 +1383,10 @@ let get_current_context_of_args = function
let vernac_check_may_eval redexp glopt rc =
let (sigma, env) = get_current_context_of_args glopt in
let sigma', c = interp_open_constr sigma env rc in
- Evarconv.check_problems_are_solved sigma';
+ let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in
+ Evarconv.check_problems_are_solved env sigma';
+ let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
+ let c = nf c in
let j =
try
Evarutil.check_evars env sigma sigma' c;
@@ -1402,8 +1410,9 @@ let vernac_declare_reduction locality s r =
let vernac_global_check c =
let evmap = Evd.empty in
let env = Global.env() in
- let c = interp_constr evmap env c in
+ let c,ctx = interp_constr evmap env c in
let senv = Global.safe_env() in
+ let senv = Safe_typing.add_constraints (snd ctx) senv in
let j = Safe_typing.typing senv c in
msg_notice (print_safe_judgment env j)
@@ -1453,7 +1462,7 @@ let vernac_print = function
dump_global qid; msg_notice (print_impargs qid)
| PrintAssumptions (o,t,r) ->
(* Prints all the axioms and section variables used by a term *)
- let cstr = constr_of_global (smart_global r) in
+ let cstr = printable_constr_of_global (smart_global r) in
let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in
let nassums =
Assumptions.assumptions st ~add_opaque:o ~add_transparent:t cstr in
@@ -1522,7 +1531,7 @@ let vernac_register id r =
error "Register inline: a constant is expected";
let kn = destConst t in
match r with
- | RegisterInline -> Global.register_inline kn
+ | RegisterInline -> Global.register_inline (Univ.out_punivs kn)
(********************)
(* Proof management *)
@@ -1651,7 +1660,7 @@ let vernac_load interp fname =
(* "locality" is the prefix "Local" attribute, while the "local" component
* is the outdated/deprecated "Local" attribute of some vernacular commands
* still parsed as the obsolete_locality grammar entry for retrocompatibility *)
-let interp ?proof locality c =
+let interp ?proof locality poly c =
prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
match c with
(* Done later in this file *)
@@ -1678,14 +1687,14 @@ let interp ?proof locality c =
vernac_notation locality local c infpl sc
(* Gallina *)
- | VernacDefinition (k,lid,d) -> vernac_definition locality k lid d
- | VernacStartTheoremProof (k,l,top) -> vernac_start_proof k l top
+ | VernacDefinition (k,lid,d) -> vernac_definition locality poly k lid d
+ | VernacStartTheoremProof (k,l,top) -> vernac_start_proof poly k l top
| VernacEndProof e -> vernac_end_proof ?proof e
| VernacExactProof c -> vernac_exact_proof c
- | VernacAssumption (stre,nl,l) -> vernac_assumption locality stre l nl
- | VernacInductive (finite,infer,l) -> vernac_inductive finite infer l
- | VernacFixpoint (local, l) -> vernac_fixpoint locality local l
- | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality local l
+ | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
+ | VernacInductive (finite,infer,l) -> vernac_inductive poly finite infer l
+ | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l
+ | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
| VernacScheme l -> vernac_scheme l
| VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
@@ -1706,13 +1715,13 @@ let interp ?proof locality c =
| VernacRequire (export, qidl) -> vernac_require export qidl
| VernacImport (export,qidl) -> vernac_import export qidl
| VernacCanonical qid -> vernac_canonical qid
- | VernacCoercion (local,r,s,t) -> vernac_coercion locality local r s t
+ | VernacCoercion (local,r,s,t) -> vernac_coercion locality poly local r s t
| VernacIdentityCoercion (local,(_,id),s,t) ->
- vernac_identity_coercion locality local id s t
+ vernac_identity_coercion locality poly local id s t
(* Type classes *)
| VernacInstance (abst, sup, inst, props, pri) ->
- vernac_instance abst locality sup inst props pri
+ vernac_instance abst locality poly sup inst props pri
| VernacContext sup -> vernac_context sup
| VernacDeclareInstances (ids, pri) -> vernac_declare_instances locality ids pri
| VernacDeclareClass id -> vernac_declare_class id
@@ -1744,7 +1753,7 @@ let interp ?proof locality c =
| VernacCreateHintDb (dbname,b) -> vernac_create_hintdb locality dbname b
| VernacRemoveHints (dbnames,ids) -> vernac_remove_hints locality dbnames ids
| VernacHints (local,dbnames,hints) ->
- vernac_hints locality local dbnames hints
+ vernac_hints locality poly local dbnames hints
| VernacSyntacticDefinition (id,c,local,b) ->
vernac_syntactic_definition locality id c local b
| VernacDeclareImplicits (qid,l) ->
@@ -1772,7 +1781,7 @@ let interp ?proof locality c =
| VernacNop -> ()
(* Proof management *)
- | VernacGoal t -> vernac_start_proof Theorem [None,([],t,None)] false
+ | VernacGoal t -> vernac_start_proof poly Theorem [None,([],t,None)] false
| VernacAbort id -> anomaly (str "VernacAbort not handled by Stm")
| VernacAbortAll -> anomaly (str "VernacAbortAll not handled by Stm")
| VernacRestart -> anomaly (str "VernacRestart not handled by Stm")
@@ -1801,6 +1810,7 @@ let interp ?proof locality c =
(* Handled elsewhere *)
| VernacProgram _
+ | VernacPolymorphic _
| VernacLocal _ -> assert false
(* Vernaculars that take a locality flag *)
@@ -1827,6 +1837,24 @@ let check_vernac_supports_locality c l =
| VernacExtend _ ) -> ()
| Some _, _ -> Errors.error "This command does not support Locality"
+(* Vernaculars that take a polymorphism flag *)
+let check_vernac_supports_polymorphism c p =
+ match p, c with
+ | None, _ -> ()
+ | Some _, (
+ VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
+ | VernacAssumption _ | VernacInductive _
+ | VernacStartTheoremProof _
+ | VernacCoercion _ | VernacIdentityCoercion _
+ | VernacInstance _ | VernacDeclareInstances _
+ | VernacHints _
+ | VernacExtend _ ) -> ()
+ | Some _, _ -> Errors.error "This command does not support Polymorphism"
+
+let enforce_polymorphism = function
+ | None -> Flags.is_universe_polymorphism ()
+ | Some b -> b
+
(** A global default timeout, controled by option "Set Default Timeout n".
Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
@@ -1883,13 +1911,17 @@ exception HasFailed of string
let interp ?(verbosely=true) ?proof (loc,c) =
let orig_program_mode = Flags.is_program_mode () in
- let rec aux ?locality isprogcmd = function
- | VernacProgram c when not isprogcmd -> aux ?locality true c
+ let rec aux ?locality ?polymorphism isprogcmd = function
+ | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c
| VernacProgram _ -> Errors.error "Program mode specified twice"
- | VernacLocal (b, c) when Option.is_empty locality -> aux ~locality:b isprogcmd c
+ | VernacLocal (b, c) when Option.is_empty locality ->
+ aux ~locality:b ?polymorphism isprogcmd c
+ | VernacPolymorphic (b, c) when polymorphism = None ->
+ aux ?locality ~polymorphism:b isprogcmd c
+ | VernacPolymorphic (b, c) -> Errors.error "Polymorphism specified twice"
| VernacLocal _ -> Errors.error "Locality specified twice"
- | VernacStm (Command c) -> aux ?locality isprogcmd c
- | VernacStm (PGLast c) -> aux ?locality isprogcmd c
+ | VernacStm (Command c) -> aux ?locality ?polymorphism isprogcmd c
+ | VernacStm (PGLast c) -> aux ?locality ?polymorphism isprogcmd c
| VernacStm _ -> assert false (* Done by Stm *)
| VernacFail v ->
begin try
@@ -1899,7 +1931,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
Future.purify
(fun v ->
try
- aux ?locality isprogcmd v;
+ aux ?locality ?polymorphism isprogcmd v;
raise HasNotFailed
with
| HasNotFailed as e -> raise e
@@ -1919,10 +1951,10 @@ let interp ?(verbosely=true) ?proof (loc,c) =
end
| VernacTimeout (n,v) ->
current_timeout := Some n;
- aux ?locality isprogcmd v
+ aux ?locality ?polymorphism isprogcmd v
| VernacTime v ->
let tstart = System.get_time() in
- aux ?locality isprogcmd v;
+ aux ?locality ?polymorphism isprogcmd v;
let tend = System.get_time() in
let msg = if !Flags.time then "" else "Finished transaction in " in
msg_info (str msg ++ System.fmt_time_difference tstart tend)
@@ -1930,11 +1962,13 @@ let interp ?(verbosely=true) ?proof (loc,c) =
| VernacLoad (_,fname) -> vernac_load (aux false) fname
| c ->
check_vernac_supports_locality c locality;
+ check_vernac_supports_polymorphism c polymorphism;
+ let poly = enforce_polymorphism polymorphism in
Obligations.set_program_mode isprogcmd;
let psh = default_set_timeout () in
try
- if verbosely then Flags.verbosely (interp ?proof locality) c
- else Flags.silently (interp ?proof locality) c;
+ if verbosely then Flags.verbosely (interp ?proof locality poly) c
+ else Flags.silently (interp ?proof locality poly) c;
restore_timeout psh;
if orig_program_mode || not !Flags.program_mode || isprogcmd then
Flags.program_mode := orig_program_mode
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 79673df32b..2da4058c88 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -126,9 +126,9 @@ let uri_params f = function
let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp)
let section_parameters = function
- | GRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) ->
+ | GRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_)),_) ->
get_discharged_hyp_names (path_of_global (IndRef(induri,0)))
- | GRef (_,(ConstRef cst as ref)) ->
+ | GRef (_,(ConstRef cst as ref),_) ->
get_discharged_hyp_names (path_of_global ref)
| _ -> []
@@ -141,10 +141,10 @@ let merge vl al =
let rec uri_of_constr c =
match c with
| GVar (_,id) -> url_id id
- | GRef (_,ref) -> uri_of_global ref
+ | GRef (_,ref,_) -> uri_of_global ref
| GHole _ | GEvar _ -> url_string "?"
| GSort (_,s) -> url_string (whelp_of_glob_sort s)
- | _ -> url_paren (fun () -> match c with
+ | GProj _ -> assert false
| GApp (_,f,args) ->
let inst,rest = merge (section_parameters f) args in
uri_of_constr f; url_char ' '; uri_params uri_of_constr inst;
@@ -164,10 +164,10 @@ let rec uri_of_constr c =
uri_of_constr c; url_string ":"; uri_of_constr t
| GRec _ | GIf _ | GLetTuple _ | GCases _ ->
error "Whelp does not support pattern-matching and (co-)fixpoint."
- | GVar _ | GRef _ | GHole _ | GEvar _ | GSort _ | GCast (_,_, CastCoerce) ->
+ | GCast (_,_, CastCoerce) ->
anomaly (Pp.str "Written w/o parenthesis")
| GPatVar _ ->
- anomaly (Pp.str "Found constructors not supported in constr")) ()
+ anomaly (Pp.str "Found constructors not supported in constr")
let make_string f x = Buffer.reset b; f x; Buffer.contents b
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 01:49:05 +0000