aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
authorMatthieu Sozeau2012-10-10 15:35:36 -0400
committerMatthieu Sozeau2014-05-06 09:58:53 +0200
commita4043608f704f026de7eb5167a109ca48e00c221 (patch)
tree938b6b8cb8d6d5dbaf7be3c62abcc8fdfcd45fc2 /plugins/funind
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 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml38
-rw-r--r--plugins/funind/functional_principles_types.ml70
-rw-r--r--plugins/funind/g_indfun.ml413
-rw-r--r--plugins/funind/glob_term_to_relation.ml76
-rw-r--r--plugins/funind/glob_termops.ml9
-rw-r--r--plugins/funind/indfun.ml41
-rw-r--r--plugins/funind/indfun_common.ml13
-rw-r--r--plugins/funind/indfun_common.mli2
-rw-r--r--plugins/funind/invfun.ml69
-rw-r--r--plugins/funind/merge.ml14
-rw-r--r--plugins/funind/recdef.ml101
-rw-r--r--plugins/funind/recdef.mli6
12 files changed, 248 insertions, 204 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f06d8fa53f..a3af23dcda 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -124,11 +124,13 @@ let finish_proof dynamic_infos g =
let refine c =
- Tacmach.refine_no_check c
+ Tacmach.refine c
let thin l =
Tacmach.thin_no_check l
+let eq_constr u v = eq_constr_nounivs u v
+
let is_trivial_eq t =
let res = try
begin
@@ -205,7 +207,7 @@ let prove_trivial_eq h_id context (constructor,type_of_term,term) =
let find_rectype env c =
- let (t, l) = decompose_app (Reduction.whd_betaiotazeta c) in
+ let (t, l) = decompose_app (Reduction.whd_betaiotazeta env c) in
match kind_of_term t with
| Ind ind -> (t, l)
| Construct _ -> (t,l)
@@ -233,7 +235,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
failwith "NoChange";
end
in
- let eq_constr = Reductionops.is_conv env sigma in
+ let eq_constr = Evarconv.e_conv env (ref sigma) in
if not (noccurn 1 end_of_type)
then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *)
if not (isApp t) then nochange "not an equality";
@@ -325,7 +327,8 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
let all_ids = pf_ids_of_hyps g in
let new_ids,_ = list_chop ctxt_size all_ids in
let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in
- refine to_refine g
+ let evm, _ = pf_apply Typing.e_type_of g to_refine in
+ tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g
)
in
let simpl_eq_tac =
@@ -633,8 +636,11 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
( (* we instanciate the hyp if possible *)
fun g ->
let prov_hid = pf_get_new_id hid g in
+ let c = mkApp(mkVar hid,args) in
+ let evm, _ = pf_apply Typing.e_type_of g c in
tclTHENLIST[
- Proofview.V82.of_tactic (pose_proof (Name prov_hid) (mkApp(mkVar hid,args)));
+ Refiner.tclEVARS evm;
+ Proofview.V82.of_tactic (pose_proof (Name prov_hid) c);
thin [hid];
rename_hyp [prov_hid,hid]
] g
@@ -757,6 +763,7 @@ let build_proof
begin
match kind_of_term f with
| App _ -> assert false (* we have collected all the app in decompose_app *)
+ | Proj _ -> assert false (*FIXME*)
| Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ ->
let new_infos =
{ dyn_infos with
@@ -764,7 +771,7 @@ let build_proof
}
in
build_proof_args do_finalize new_infos g
- | Const c when not (List.mem_f Constant.equal c fnames) ->
+ | Const (c,_) when not (List.mem_f Constant.equal c fnames) ->
let new_infos =
{ dyn_infos with
info = (f,args)
@@ -809,6 +816,7 @@ let build_proof
| Fix _ | CoFix _ ->
error ( "Anonymous local (co)fixpoints are not handled yet")
+ | Proj _ -> error "Prod"
| Prod _ -> error "Prod"
| LetIn _ ->
let new_infos =
@@ -938,7 +946,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
(* observe (str "nb_args := " ++ str (string_of_int nb_args)); *)
(* observe (str "nb_params := " ++ str (string_of_int nb_params)); *)
(* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
- let f_def = Global.lookup_constant (destConst f) in
+ let f_def = Global.lookup_constant (fst (destConst f)) in
let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
let f_body = Option.get (body_of_constant f_def)
in
@@ -956,10 +964,10 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
(* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *)
let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args)
- (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in
+ ((*FIXME*)f_def.const_type) in
let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in
- let f_id = Label.to_id (con_label (destConst f)) in
+ let f_id = Label.to_id (con_label (fst (destConst f))) in
let prove_replacement =
tclTHENSEQ
[
@@ -978,8 +986,8 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
Ensures by: obvious
i*)
(mk_equation_id f_id)
- (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
- lemma_type
+ (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
+ (lemma_type, (*FIXME*) Univ.ContextSet.empty)
(fun _ _ -> ());
ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
Lemmas.save_proof (Vernacexpr.Proved(false,None))
@@ -990,10 +998,10 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
let equation_lemma =
try
- let finfos = find_Function_infos (destConst f) in
+ let finfos = find_Function_infos (fst (destConst f)) (*FIXME*) in
mkConst (Option.get finfos.equation_lemma)
with (Not_found | Option.IsNone as e) ->
- let f_id = Label.to_id (con_label (destConst f)) in
+ let f_id = Label.to_id (con_label (fst (destConst f))) in
(*i The next call to mk_equation_id is valid since we will construct the lemma
Ensures by: obvious
i*)
@@ -1002,7 +1010,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
let _ =
match e with
| Option.IsNone ->
- let finfos = find_Function_infos (destConst f) in
+ let finfos = find_Function_infos (fst (destConst f)) in
update_Function
{finfos with
equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
@@ -1306,7 +1314,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
in
let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
tclTHENSEQ
- [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef fname)];
+ [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))];
let do_prove =
build_proof
interactive_proof
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d6f21fb86b..2adc825056 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -106,14 +106,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
let is_dom c =
match kind_of_term c with
- | Ind((u,_)) -> MutInd.equal u rel_as_kn
- | Construct((u,_),_) -> MutInd.equal u rel_as_kn
+ | Ind((u,_),_) -> MutInd.equal u rel_as_kn
+ | Construct(((u,_),_),_) -> MutInd.equal u rel_as_kn
| _ -> false
in
let get_fun_num c =
match kind_of_term c with
- | Ind(_,num) -> num
- | Construct((_,num),_) -> num
+ | Ind((_,num),_) -> num
+ | Construct(((_,num),_),_) -> num
| _ -> assert false
in
let dummy_var = mkVar (Id.of_string "________") in
@@ -251,8 +251,10 @@ let change_property_sort toSort princ princName =
let princ_info = compute_elim_sig princ in
let change_sort_in_predicate (x,v,t) =
(x,None,
- let args,_ = decompose_prod t in
- compose_prod args (mkSort toSort)
+ let args,ty = decompose_prod t in
+ let s = destSort ty in
+ Global.add_constraints (Univ.enforce_leq (univ_of_sort toSort) (univ_of_sort s) Univ.Constraint.empty);
+ compose_prod args (mkSort toSort)
)
in
let princName_as_constr = Constrintern.global_reference princName in
@@ -292,8 +294,8 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
begin
Lemmas.start_proof
new_princ_name
- (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
- new_principle_type
+ (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
+ (new_principle_type, (*FIXME*) Univ.ContextSet.empty)
hook
;
(* let _tim1 = System.get_time () in *)
@@ -315,7 +317,7 @@ let generate_functional_principle
try
let f = funs.(i) in
- let type_sort = Termops.new_sort_in_family InType in
+ let type_sort = Universes.new_sort_in_family InType in
let new_sorts =
match sorts with
| None -> Array.make (Array.length funs) (type_sort)
@@ -334,18 +336,23 @@ let generate_functional_principle
then
(* let id_of_f = Label.to_id (con_label f) in *)
let register_with_sort fam_sort =
- let s = Termops.new_sort_in_family fam_sort in
+ let s = Universes.new_sort_in_family fam_sort in
let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
let value = change_property_sort s new_principle_type new_princ_name in
(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
- let ce = {
- const_entry_body = Future.from_val (value,Declareops.no_seff);
- const_entry_secctx = None;
- const_entry_type = None;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- } in
+ let ce =
+ { const_entry_body =
+ Future.from_val (value,Declareops.no_seff);
+ const_entry_secctx = None;
+ const_entry_type = None;
+ const_entry_polymorphic = false;
+ const_entry_universes = Univ.UContext.empty (*FIXME*);
+ const_entry_proj = None;
+ const_entry_opaque = false;
+ const_entry_feedback = None;
+ const_entry_inline_code = false
+ }
+ in
ignore(
Declare.declare_constant
name
@@ -488,19 +495,20 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
List.map
(fun (idx) ->
let ind = first_fun_kn,idx in
- ind,true,prop_sort
+ (ind,Univ.Instance.empty)(*FIXME*),true,prop_sort
)
funs_indexes
in
+ let sigma, schemes =
+ Indrec.build_mutual_induction_scheme env sigma ind_list
+ in
let l_schemes =
- List.map
- (Typing.type_of env sigma)
- (Indrec.build_mutual_induction_scheme env sigma ind_list)
+ List.map (Typing.type_of env sigma) schemes
in
let i = ref (-1) in
let sorts =
List.rev_map (fun (_,x) ->
- Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
+ Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
)
fas
in
@@ -649,10 +657,10 @@ let build_case_scheme fa =
(* Constrintern.global_reference id *)
(* in *)
let funs = (fun (_,f,_) ->
- try Globnames.constr_of_global (Nametab.global f)
+ try Universes.constr_of_global (Nametab.global f)
with Not_found ->
Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
- let first_fun = destConst funs in
+ let first_fun,u = destConst funs in
let funs_mp,funs_dp,_ = Names.repr_con first_fun in
let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in
@@ -664,16 +672,18 @@ let build_case_scheme fa =
let prop_sort = InProp in
let funs_indexes =
let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
- List.assoc_f Constant.equal (destConst funs) this_block_funs_indexes
+ List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes
in
let ind_fun =
let ind = first_fun_kn,funs_indexes in
- ind,prop_sort
+ (ind,Univ.Instance.empty)(*FIXME*),prop_sort
in
- let scheme_type = (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun) in
+ let sigma, scheme =
+ (fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun in
+ let scheme_type = (Typing.type_of env sigma ) scheme in
let sorts =
(fun (_,_,x) ->
- Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
+ Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
)
fa
in
@@ -690,6 +700,6 @@ let build_case_scheme fa =
(Some princ_name)
this_block_funs
0
- (prove_princ_for_struct false 0 [|destConst funs|])
+ (prove_princ_for_struct false 0 [|fst (destConst funs)|])
in
()
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 2dd78d8908..3802aa3659 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -307,8 +307,11 @@ let rec hdMatchSub inu (test: constr -> bool) : fapp_info list =
max_rel = max_rel; onlyvars = List.for_all isVar args }
::subres
+let make_eq () =
+(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
+
let mkEq typ c1 c2 =
- mkApp (Coqlib.build_coq_eq(),[| typ; c1; c2|])
+ mkApp (make_eq(),[| typ; c1; c2|])
let poseq_unsafe idunsafe cstr gl =
@@ -463,10 +466,10 @@ VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF
[ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")"
"with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] ->
[
- let f1 = Constrintern.interp_constr Evd.empty (Global.env())
- (CRef (Libnames.Ident (Loc.ghost,id1))) in
- let f2 = Constrintern.interp_constr Evd.empty (Global.env())
- (CRef (Libnames.Ident (Loc.ghost,id2))) in
+ let f1,ctx = Constrintern.interp_constr Evd.empty (Global.env())
+ (CRef (Libnames.Ident (Loc.ghost,id1),None)) in
+ let f2,ctx' = Constrintern.interp_constr Evd.empty (Global.env())
+ (CRef (Libnames.Ident (Loc.ghost,id2),None)) in
let f1type = Typing.type_of (Global.env()) Evd.empty f1 in
let f2type = Typing.type_of (Global.env()) Evd.empty f2 in
let ar1 = List.length (fst (decompose_prod f1type)) in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index dd02dfe8d1..4544f736ca 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -333,8 +333,8 @@ let raw_push_named (na,raw_value,raw_typ) env =
match na with
| Anonymous -> env
| Name id ->
- let value = Option.map (Pretyping.understand Evd.empty env) raw_value in
- let typ = Pretyping.understand Evd.empty env ~expected_type:Pretyping.IsType raw_typ in
+ let value = Option.map (fun x-> fst (Pretyping.understand Evd.empty env x)) raw_value in
+ let typ,ctx = Pretyping.understand Evd.empty env ~expected_type:Pretyping.IsType raw_typ in
Environ.push_named (id,value,typ) env
@@ -350,7 +350,7 @@ let add_pat_variables pat typ env : Environ.env =
with Not_found -> assert false
in
let constructors = Inductiveops.get_constructors env indf in
- let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c cs.Inductiveops.cs_cstr) (Array.to_list constructors) in
+ let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in
let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
in
@@ -397,7 +397,7 @@ let rec pattern_to_term_and_type env typ = function
with Not_found -> assert false
in
let constructors = Inductiveops.get_constructors env indf in
- let constructor = List.find (fun cs -> eq_constructor cs.Inductiveops.cs_cstr constr) (Array.to_list constructors) in
+ let constructor = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in
let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
let _,cstl = Inductiveops.dest_ind_family indf in
let csta = Array.of_list cstl in
@@ -486,7 +486,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
a pseudo value "v1 ... vn".
The "value" of this branch is then simply [res]
*)
- let rt_as_constr = Pretyping.understand Evd.empty env rt in
+ let rt_as_constr,ctx = Pretyping.understand Evd.empty env rt in
let rt_typ = Typing.type_of env Evd.empty rt_as_constr in
let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in
let res = fresh_id args_res.to_avoid "_res" in
@@ -559,6 +559,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
*)
build_entry_lc env funnames avoid (mkGApp(b,args))
| GRec _ -> error "Not handled GRec"
+ | GProj _ -> error "Not handled GProj"
| GProd _ -> error "Cannot apply a type"
end (* end of the application treatement *)
@@ -594,7 +595,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
and combine the two result
*)
let v_res = build_entry_lc env funnames avoid v in
- let v_as_constr = Pretyping.understand Evd.empty env v in
+ let v_as_constr,ctx = Pretyping.understand Evd.empty env v in
let v_type = Typing.type_of env Evd.empty v_as_constr in
let new_env =
match n with
@@ -610,7 +611,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
let make_discr = make_discr_match brl in
build_entry_lc_from_case env funnames make_discr el brl avoid
| GIf(_,b,(na,e_option),lhs,rhs) ->
- let b_as_constr = Pretyping.understand Evd.empty env b in
+ let b_as_constr,ctx = Pretyping.understand Evd.empty env b in
let b_typ = Typing.type_of env Evd.empty b_as_constr in
let (ind,_) =
try Inductiveops.find_inductive env Evd.empty b_typ
@@ -619,7 +620,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
Printer.pr_glob_constr b ++ str " in " ++
Printer.pr_glob_constr rt ++ str ". try again with a cast")
in
- let case_pats = build_constructors_of_type ind [] in
+ let case_pats = build_constructors_of_type (fst ind) [] in
assert (Int.equal (Array.length case_pats) 2);
let brl =
List.map_i
@@ -642,7 +643,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
)
nal
in
- let b_as_constr = Pretyping.understand Evd.empty env b in
+ let b_as_constr,ctx = Pretyping.understand Evd.empty env b in
let b_typ = Typing.type_of env Evd.empty b_as_constr in
let (ind,_) =
try Inductiveops.find_inductive env Evd.empty b_typ
@@ -651,7 +652,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
Printer.pr_glob_constr b ++ str " in " ++
Printer.pr_glob_constr rt ++ str ". try again with a cast")
in
- let case_pats = build_constructors_of_type ind nal_as_glob_constr in
+ let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
assert (Int.equal (Array.length case_pats) 1);
let br =
(Loc.ghost,[],[case_pats.(0)],e)
@@ -661,6 +662,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
end
| GRec _ -> error "Not handled GRec"
+ | GProj _ -> error "Not handled GProj"
| GCast(_,b,_) ->
build_entry_lc env funnames avoid b
and build_entry_lc_from_case env funname make_discr
@@ -689,7 +691,7 @@ and build_entry_lc_from_case env funname make_discr
in
let types =
List.map (fun (case_arg,_) ->
- let case_arg_as_constr = Pretyping.understand Evd.empty env case_arg in
+ let case_arg_as_constr,ctx = Pretyping.understand Evd.empty env case_arg in
Typing.type_of env Evd.empty case_arg_as_constr
) el
in
@@ -844,7 +846,7 @@ let is_res id =
let same_raw_term rt1 rt2 =
match rt1,rt2 with
- | GRef(_,r1), GRef (_,r2) -> Globnames.eq_gr r1 r2
+ | GRef(_,r1,_), GRef (_,r2,_) -> Globnames.eq_gr r1 r2
| GHole _, GHole _ -> true
| _ -> false
let decompose_raw_eq lhs rhs =
@@ -894,7 +896,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let new_t =
mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt])
in
- let t' = Pretyping.understand Evd.empty env new_t in
+ let t',ctx = Pretyping.understand Evd.empty env new_t in
let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -907,14 +909,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| _ -> (* the first args is the name of the function! *)
assert false
end
- | GApp(loc1,GRef(loc2,eq_as_ref),[ty;GVar(loc3,id);rt])
+ | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;GVar(loc3,id);rt])
when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
->
begin
try
observe (str "computing new type for eq : " ++ pr_glob_constr rt);
let t' =
- try Pretyping.understand Evd.empty env t
+ try fst (Pretyping.understand Evd.empty env t)(*FIXME*)
with e when Errors.noncritical e -> raise Continue
in
let is_in_b = is_free_in id b in
@@ -936,17 +938,17 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
in
mkGProd(n,t,new_b),id_to_exclude
with Continue ->
- let jmeq = Globnames.IndRef (destInd (jmeq ())) in
- let ty' = Pretyping.understand Evd.empty env ty in
+ let jmeq = Globnames.IndRef (fst (destInd (jmeq ()))) in
+ let ty',ctx = Pretyping.understand Evd.empty env ty in
let ind,args' = Inductive.find_inductive env ty' in
- let mib,_ = Global.lookup_inductive ind in
+ let mib,_ = Global.lookup_inductive (fst ind) in
let nparam = mib.Declarations.mind_nparams in
let params,arg' =
((Util.List.chop nparam args'))
in
let rt_typ =
GApp(Loc.ghost,
- GRef (Loc.ghost,Globnames.IndRef ind),
+ GRef (Loc.ghost,Globnames.IndRef (fst ind),None),
(List.map
(fun p -> Detyping.detype false []
(Termops.names_of_rel_context env)
@@ -956,10 +958,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
(mkGHole ()))))
in
let eq' =
- GApp(loc1,GRef(loc2,jmeq),[ty;GVar(loc3,id);rt_typ;rt])
+ GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt])
in
observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
- let eq'_as_constr = Pretyping.understand Evd.empty env eq' in
+ let eq'_as_constr,ctx = Pretyping.understand Evd.empty env eq' in
observe (str " computing new type for jmeq : done") ;
let new_args =
match kind_of_term eq'_as_constr with
@@ -1007,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
if is_in_b then b else replace_var_by_term id rt b
in
let new_env =
- let t' = Pretyping.understand Evd.empty env eq' in
+ let t',ctx = Pretyping.understand Evd.empty env eq' in
Environ.push_rel (n,None,t') env
in
let new_b,id_to_exclude =
@@ -1024,7 +1026,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
mkGProd(n,t,new_b),id_to_exclude
else new_b, Id.Set.add id id_to_exclude
*)
- | GApp(loc1,GRef(loc2,eq_as_ref),[ty;rt1;rt2])
+ | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;rt1;rt2])
when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
->
begin
@@ -1045,7 +1047,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
else raise Continue
with Continue ->
observe (str "computing new type for prod : " ++ pr_glob_constr rt);
- let t' = Pretyping.understand Evd.empty env t in
+ let t',ctx = Pretyping.understand Evd.empty env t in
let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1061,7 +1063,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
end
| _ ->
observe (str "computing new type for prod : " ++ pr_glob_constr rt);
- let t' = Pretyping.understand Evd.empty env t in
+ let t',ctx = Pretyping.understand Evd.empty env t in
let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1080,7 +1082,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let not_free_in_t id = not (is_free_in id t) in
let new_crossed_types = t :: crossed_types in
observe (str "computing new type for lambda : " ++ pr_glob_constr rt);
- let t' = Pretyping.understand Evd.empty env t in
+ let t',ctx = Pretyping.understand Evd.empty env t in
match n with
| Name id ->
let new_env = Environ.push_rel (n,None,t') env in
@@ -1102,7 +1104,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| GLetIn(_,n,t,b) ->
begin
let not_free_in_t id = not (is_free_in id t) in
- let t' = Pretyping.understand Evd.empty env t in
+ let t',ctx = Pretyping.understand Evd.empty env t in
let type_t' = Typing.type_of env Evd.empty t' in
let new_env = Environ.push_rel (n,Some t',type_t') env in
let new_b,id_to_exclude =
@@ -1127,7 +1129,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
args (crossed_types)
depth t
in
- let t' = Pretyping.understand Evd.empty env new_t in
+ let t',ctx = Pretyping.understand Evd.empty env new_t in
let new_env = Environ.push_rel (na,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1179,7 +1181,7 @@ let rec compute_cst_params relnames params = function
discriminitation ones *)
| GSort _ -> params
| GHole _ -> params
- | GIf _ | GRec _ | GCast _ ->
+ | GIf _ | GRec _ | GCast _ | GProj _->
raise (UserError("compute_cst_params", str "Not handled case"))
and compute_cst_params_from_app acc (params,rtl) =
match params,rtl with
@@ -1267,12 +1269,12 @@ let do_build_inductive
(fun (n,t,is_defined) acc ->
if is_defined
then
- Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t,
+ Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
acc)
else
Constrexpr.CProdN
(Loc.ghost,
- [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t],
+ [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
acc
)
)
@@ -1285,7 +1287,8 @@ let do_build_inductive
*)
let rel_arities = Array.mapi rel_arity funsargs in
Util.Array.fold_left2 (fun env rel_name rel_ar ->
- Environ.push_named (rel_name,None, Constrintern.interp_constr Evd.empty env rel_ar) env) env relnames rel_arities
+ Environ.push_named (rel_name,None,
+ fst (with_full_print (Constrintern.interp_constr Evd.empty env) rel_ar)) env) env relnames rel_arities
in
(* and of the real constructors*)
let constr i res =
@@ -1333,12 +1336,12 @@ let do_build_inductive
(fun (n,t,is_defined) acc ->
if is_defined
then
- Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t,
+ Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
acc)
else
Constrexpr.CProdN
(Loc.ghost,
- [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t],
+ [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
acc
)
)
@@ -1366,8 +1369,7 @@ let do_build_inductive
Array.map (List.map
(fun (id,t) ->
false,((Loc.ghost,id),
- Flags.with_option
- Flags.raw_print
+ with_full_print
(Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) t)
)
))
@@ -1403,7 +1405,7 @@ let do_build_inductive
(* in *)
let _time2 = System.get_time () in
try
- with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds)) true
+ with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false)) true
with
| UserError(s,msg) as e ->
let _time3 = System.get_time () in
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 6a7f326e6c..5efaf7954e 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -10,7 +10,7 @@ open Misctypes
Some basic functions to rebuild glob_constr
In each of them the location is Loc.ghost
*)
-let mkGRef ref = GRef(Loc.ghost,ref)
+let mkGRef ref = GRef(Loc.ghost,ref,None)
let mkGVar id = GVar(Loc.ghost,id)
let mkGApp(rt,rtl) = GApp(Loc.ghost,rt,rtl)
let mkGLambda(n,t,b) = GLambda(Loc.ghost,n,Explicit,t,b)
@@ -180,6 +180,7 @@ let change_vars =
| GRec _ -> error "Local (co)fixes are not supported"
| GSort _ -> rt
| GHole _ -> rt
+ | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GCast(loc,b,c) ->
GCast(loc,change_vars mapping b,
Miscops.map_cast_type (change_vars mapping) c)
@@ -357,6 +358,7 @@ let rec alpha_rt excluded rt =
alpha_rt excluded rhs
)
| GRec _ -> error "Not handled GRec"
+ | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GSort _ -> rt
| GHole _ -> rt
| GCast (loc,b,c) ->
@@ -407,6 +409,7 @@ let is_free_in id =
| GIf(_,cond,_,br1,br2) ->
is_free_in cond || is_free_in br1 || is_free_in br2
| GRec _ -> raise (UserError("",str "Not handled GRec"))
+ | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GSort _ -> false
| GHole _ -> false
| GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
@@ -503,6 +506,7 @@ let replace_var_by_term x_id term =
replace_var_by_pattern rhs
)
| GRec _ -> raise (UserError("",str "Not handled GRec"))
+ | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GSort _ -> rt
| GHole _ -> rt
| GCast(loc,b,c) ->
@@ -598,6 +602,7 @@ let ids_of_glob_constr c =
| GCases (loc,sty,rtntypopt,tml,brchl) ->
List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl)
| GRec _ -> failwith "Fix inside a constructor branch"
+ | GProj _ -> error "Native projections are not supported" (** FIXME *)
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> []
in
(* build the set *)
@@ -656,6 +661,7 @@ let zeta_normalize =
zeta_normalize_term rhs
)
| GRec _ -> raise (UserError("",str "Not handled GRec"))
+ | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GSort _ -> rt
| GHole _ -> rt
| GCast(loc,b,c) ->
@@ -698,6 +704,7 @@ let expand_as =
GIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
expand_as map br1, expand_as map br2)
| GRec _ -> error "Not handled GRec"
+ | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GCast(loc,b,c) ->
GCast(loc,expand_as map b,
Miscops.map_cast_type (expand_as map) c)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 661e5e4869..d98f824e84 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -38,7 +38,7 @@ let functional_induction with_clean c princl pat =
| None -> (* No principle is given let's find the good one *)
begin
match kind_of_term f with
- | Const c' ->
+ | Const (c',u) ->
let princ_option =
let finfo = (* we first try to find out a graph on f *)
try find_Function_infos c'
@@ -148,7 +148,7 @@ let build_newrecursive
List.fold_left
(fun (env,impls) ((_,recname),bl,arityc,_) ->
let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
- let arity = Constrintern.interp_type sigma env0 arityc in
+ let arity,ctx = Constrintern.interp_type sigma env0 arityc in
let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
(Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls))
(env0,Constrintern.empty_internalization_env) lnameargsardef in
@@ -182,6 +182,7 @@ let is_rec names =
| GVar(_,id) -> check_id id names
| GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false
| GCast(_,b,_) -> lookup names b
+ | GProj _ -> error "GProj not handled"
| GRec _ -> error "GRec not handled"
| GIf(_,b,_,lhs,rhs) ->
(lookup names b) || (lookup names lhs) || (lookup names rhs)
@@ -222,7 +223,7 @@ let derive_inversion fix_names =
try
(* we first transform the fix_names identifier into their corresponding constant *)
let fix_names_as_constant =
- List.map (fun id -> destConst (Constrintern.global_reference id)) fix_names
+ List.map (fun id -> fst (destConst (Constrintern.global_reference id))) fix_names
in
(*
Then we check that the graphs have been defined
@@ -239,7 +240,7 @@ let derive_inversion fix_names =
Ensures by : register_built
i*)
(List.map
- (fun id -> destInd (Constrintern.global_reference (mk_rel_id id)))
+ (fun id -> fst (destInd (Constrintern.global_reference (mk_rel_id id))))
fix_names
)
with e when Errors.noncritical e ->
@@ -326,9 +327,8 @@ let generate_principle on_error
let _ =
List.map_i
(fun i x ->
- let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in
- let princ_type = Typeops.type_of_constant (Global.env()) princ
- in
+ let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in
+ let princ_type = Global.type_of_global_unsafe princ in
Functional_principles_types.generate_functional_principle
interactive_proof
princ_type
@@ -351,10 +351,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
match fixpoint_exprl with
| [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in
- Command.do_definition fname (Decl_kinds.Global,Decl_kinds.Definition)
+ Command.do_definition fname (Decl_kinds.Global,(*FIXME*)false,Decl_kinds.Definition)
bl None body (Some ret_type) (fun _ _ -> ())
| _ ->
- Command.do_fixpoint Global fixpoint_exprl
+ Command.do_fixpoint Global false(*FIXME*) fixpoint_exprl
let generate_correction_proof_wf f_ref tcc_lemma_ref
is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
@@ -385,7 +385,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
let f_app_args =
Constrexpr.CAppExpl
(Loc.ghost,
- (None,(Ident (Loc.ghost,fname))) ,
+ (None,(Ident (Loc.ghost,fname)),None) ,
(List.map
(function
| _,Anonymous -> assert false
@@ -399,7 +399,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
[(f_app_args,None);(body,None)])
in
let eq = Constrexpr_ops.prod_constr_expr unbounded_eq args in
- let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type
+ let hook (f_ref,_) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type
nb_args relation =
try
pre_hook
@@ -536,7 +536,7 @@ let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ
let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
- let ((_,_,typel),_) = Command.interp_fixpoint fixl ntns in
+ let ((_,_,typel),_,_) = Command.interp_fixpoint fixl ntns in
let constr_expr_typel =
with_full_print (List.map (Constrextern.extern_constr false (Global.env ()))) typel in
let fixpoint_exprl_with_new_bl =
@@ -631,10 +631,10 @@ let do_generate_principle on_error register_built interactive_proof
let rec add_args id new_args b =
match b with
- | CRef r ->
+ | CRef (r,_) ->
begin match r with
| Libnames.Ident(loc,fname) when Id.equal fname id ->
- CAppExpl(Loc.ghost,(None,r),new_args)
+ CAppExpl(Loc.ghost,(None,r,None),new_args)
| _ -> b
end
| CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo")
@@ -648,12 +648,12 @@ let rec add_args id new_args b =
add_args id new_args b1)
| CLetIn(loc,na,b1,b2) ->
CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
- | CAppExpl(loc,(pf,r),exprl) ->
+ | CAppExpl(loc,(pf,r,us),exprl) ->
begin
match r with
| Libnames.Ident(loc,fname) when Id.equal fname id ->
- CAppExpl(loc,(pf,r),new_args@(List.map (add_args id new_args) exprl))
- | _ -> CAppExpl(loc,(pf,r),List.map (add_args id new_args) exprl)
+ CAppExpl(loc,(pf,r,us),new_args@(List.map (add_args id new_args) exprl))
+ | _ -> CAppExpl(loc,(pf,r,us),List.map (add_args id new_args) exprl)
end
| CApp(loc,(pf,b),bl) ->
CApp(loc,(pf,add_args id new_args b),
@@ -767,11 +767,10 @@ let make_graph (f_ref:global_reference) =
| Some body ->
let env = Global.env () in
let extern_body,extern_type =
- with_full_print
- (fun () ->
+ with_full_print (fun () ->
(Constrextern.extern_constr false env body,
Constrextern.extern_type false env
- (Typeops.type_of_constant_type env c_body.const_type)
+ ((*FIXNE*) c_body.const_type)
)
)
()
@@ -792,7 +791,7 @@ let make_graph (f_ref:global_reference) =
| Constrexpr.LocalRawAssum (nal,_,_) ->
List.map
(fun (loc,n) ->
- CRef(Libnames.Ident(loc, Nameops.out_name n)))
+ CRef(Libnames.Ident(loc, Nameops.out_name n),None))
nal
)
nal_tas
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 5c37dcec34..8cccb0bedf 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -114,7 +114,7 @@ let const_of_id id =
let def_of_const t =
match (Term.kind_of_term t) with
Term.Const sp ->
- (try (match Declareops.body_of_constant (Global.lookup_constant sp) with
+ (try (match Environ.constant_opt_value_in (Global.env()) sp with
| Some c -> c
| _ -> assert false)
with Not_found -> assert false)
@@ -146,7 +146,7 @@ let get_locality = function
| Local -> true
| Global -> false
-let save with_clean id const (locality,kind) hook =
+let save with_clean id const (locality,_,kind) hook =
let l,r = match locality with
| Discharge when Lib.sections_are_opened () ->
let k = Kindops.logical_kind_of_goal_kind kind in
@@ -177,7 +177,8 @@ let get_proof_clean do_reduce =
let with_full_print f a =
let old_implicit_args = Impargs.is_implicit_args ()
and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
- and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
+ and old_contextual_implicit_args = Impargs.is_contextual_implicit_args ()
+ in
let old_rawprint = !Flags.raw_print in
Flags.raw_print := true;
Impargs.make_implicit_args false;
@@ -259,8 +260,8 @@ let cache_Function (_,finfos) =
let load_Function _ = cache_Function
let subst_Function (subst,finfos) =
- let do_subst_con c = fst (Mod_subst.subst_con subst c)
- and do_subst_ind (kn,i) = (Mod_subst.subst_ind subst kn,i)
+ let do_subst_con c = Mod_subst.subst_constant subst c
+ and do_subst_ind i = Mod_subst.subst_ind subst i
in
let function_constant' = do_subst_con finfos.function_constant in
let graph_ind' = do_subst_ind finfos.graph_ind in
@@ -336,7 +337,7 @@ let pr_info f_info =
str "function_constant_type := " ++
(try
Printer.pr_lconstr
- (Global.type_of_global (ConstRef f_info.function_constant))
+ (Global.type_of_global_unsafe (ConstRef f_info.function_constant))
with e when Errors.noncritical e -> mt ()) ++ fnl () ++
str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 0e8b22deba..6e8b79a6be 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -58,7 +58,7 @@ val get_proof_clean : bool ->
-(* [with_full_print f a] applies [f] to [a] in full printing environment
+(* [with_full_print f a] applies [f] to [a] in full printing environment.
This function preserves the print settings
*)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 7c8f5714e6..897c8765bf 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -112,7 +112,9 @@ let id_to_constr id =
let generate_type g_to_f f graph i =
(*i we deduce the number of arguments of the function and its returned type from the graph i*)
- let graph_arity = Inductive.type_of_inductive (Global.env()) (Global.lookup_inductive (destInd graph)) in
+ let gr,u = destInd graph in
+ let graph_arity = Inductive.type_of_inductive (Global.env())
+ (Global.lookup_inductive gr, u) in
let ctxt,_ = decompose_prod_assum graph_arity in
let fun_ctxt,res_type =
match ctxt with
@@ -138,8 +140,11 @@ let generate_type g_to_f f graph i =
the hypothesis [res = fv] can then be computed
We will need to lift it by one in order to use it as a conclusion
i*)
+ let make_eq () =
+(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
+ in
let res_eq_f_of_args =
- mkApp(Coqlib.build_coq_eq (),[|lift 2 res_type;mkRel 1;mkRel 2|])
+ mkApp(make_eq (),[|lift 2 res_type;mkRel 1;mkRel 2|])
in
(*i
The hypothesis [graph\ x_1\ldots x_n\ res] can then be computed
@@ -166,7 +171,7 @@ let generate_type g_to_f f graph i =
WARNING: while convertible, [type_of body] and [type] can be non equal
*)
let find_induction_principle f =
- let f_as_constant = match kind_of_term f with
+ let f_as_constant,u = match kind_of_term f with
| Const c' -> c'
| _ -> error "Must be used with a function"
in
@@ -205,6 +210,11 @@ let rec generate_fresh_id x avoid i =
let id = Namegen.next_ident_away_in_goal x avoid in
id::(generate_fresh_id x (id::avoid) (pred i))
+let make_eq () =
+(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
+let make_eq_refl () =
+(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq_refl ())
+
(* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ]
is the tactic used to prove correctness lemma.
@@ -237,7 +247,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
\[fun (x_1:t_1)\ldots(x_n:t_n)=> fun fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\]
*)
(* we the get the definition of the graphs block *)
- let graph_ind = destInd graphs_constr.(i) in
+ let graph_ind,u = destInd graphs_constr.(i) in
let kn = fst graph_ind in
let mib,_ = Global.lookup_inductive graph_ind in
(* and the principle to use in this lemma in $\zeta$ normal form *)
@@ -267,8 +277,8 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
branches
in
(* before building the full intro pattern for the principle *)
- let eq_ind = Coqlib.build_coq_eq () in
- let eq_construct = mkConstruct((destInd eq_ind),1) in
+ let eq_ind = make_eq () in
+ let eq_construct = mkConstructUi (destInd eq_ind, 1) in
(* The next to referencies will be used to find out which constructor to apply in each branch *)
let ind_number = ref 0
and min_constr_number = ref 0 in
@@ -731,7 +741,7 @@ let rec intros_with_rewrite g =
observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
and intros_with_rewrite_aux : tactic =
fun g ->
- let eq_ind = Coqlib.build_coq_eq () in
+ let eq_ind = make_eq () in
match kind_of_term (pf_concl g) with
| Prod(_,t,t') ->
begin
@@ -830,7 +840,7 @@ let rec reflexivity_with_destruct_cases g =
| _ -> Proofview.V82.of_tactic reflexivity
with e when Errors.noncritical e -> Proofview.V82.of_tactic reflexivity
in
- let eq_ind = Coqlib.build_coq_eq () in
+ let eq_ind = make_eq () in
let discr_inject =
Tacticals.onAllHypsAndConcl (
fun sc g ->
@@ -936,7 +946,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
let rewrite_tac j ids : tactic =
let graph_def = graphs.(j) in
let infos =
- try find_Function_infos (destConst funcs.(j))
+ try find_Function_infos (fst (destConst funcs.(j)))
with Not_found -> error "No graph found"
in
if infos.is_general
@@ -962,7 +972,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
thin ids
]
else
- unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (destConst f))]
+ unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))]
in
(* The proof of each branche itself *)
let ind_number = ref 0 in
@@ -1026,7 +1036,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
let lemmas_types_infos =
Util.Array.map2_i
(fun i f_constr graph ->
- let const_of_f = destConst f_constr in
+ let const_of_f,u = destConst f_constr in
let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
generate_type false const_of_f graph i
in
@@ -1065,22 +1075,22 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
i*)
let lem_id = mk_correct_id f_id in
Lemmas.start_proof lem_id
- (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
- (fst lemmas_types_infos.(i))
+ (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
+ (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty)
(fun _ _ -> ());
ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
(proving_tac i))));
do_save ();
let finfo = find_Function_infos f_as_constant in
- let lem_cst = destConst (Constrintern.global_reference lem_id) in
+ let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in
update_Function {finfo with correctness_lemma = Some lem_cst}
)
funs;
let lemmas_types_infos =
Util.Array.map2_i
(fun i f_constr graph ->
- let const_of_f = destConst f_constr in
+ let const_of_f = fst (destConst f_constr) in
let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
generate_type true const_of_f graph i
in
@@ -1092,19 +1102,21 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
funs_constr
graphs_constr
in
- let kn,_ as graph_ind = destInd graphs_constr.(0) in
+ let kn,_ as graph_ind = fst (destInd graphs_constr.(0)) in
let mib,mip = Global.lookup_inductive graph_ind in
- let schemes =
- Array.of_list
+ let sigma, scheme =
(Indrec.build_mutual_induction_scheme (Global.env ()) Evd.empty
(Array.to_list
(Array.mapi
- (fun i _ -> (kn,i),true,InType)
+ (fun i _ -> ((kn,i),Univ.Instance.empty)(*FIXME*),true,InType)
mib.Declarations.mind_packets
)
)
)
in
+ let schemes =
+ Array.of_list scheme
+ in
let proving_tac =
prove_fun_complete funs_constr mib.Declarations.mind_packets schemes lemmas_types_infos
in
@@ -1116,15 +1128,12 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
i*)
let lem_id = mk_complete_id f_id in
Lemmas.start_proof lem_id
- (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
- (fst lemmas_types_infos.(i))
+ (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
+ (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty)
(fun _ _ -> ());
- ignore (Pfedit.by
- (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
- (proving_tac i))));
do_save ();
let finfo = find_Function_infos f_as_constant in
- let lem_cst = destConst (Constrintern.global_reference lem_id) in
+ let lem_cst,u = destConst (Constrintern.global_reference lem_id) in
update_Function {finfo with completeness_lemma = Some lem_cst}
)
funs)
@@ -1142,7 +1151,7 @@ let revert_graph kn post_tac hid g =
let typ = pf_type_of g (mkVar hid) in
match kind_of_term typ with
| App(i,args) when isInd i ->
- let ((kn',num) as ind') = destInd i in
+ let ((kn',num) as ind'),u = destInd i in
if MutInd.equal kn kn'
then (* We have generated a graph hypothesis so that we must change it if we can *)
let info =
@@ -1192,7 +1201,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in
let type_of_h = pf_type_of g (mkVar hid) in
match kind_of_term type_of_h with
- | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) ->
+ | App(eq,args) when eq_constr eq (make_eq ()) ->
let pre_tac,f_args,res =
match kind_of_term args.(1),kind_of_term args.(2) with
| App(f,f_args),_ when eq_constr f fconst ->
@@ -1244,12 +1253,12 @@ let invfun qhyp f g =
(fun hid -> Proofview.V82.tactic begin fun g ->
let hyp_typ = pf_type_of g (mkVar hid) in
match kind_of_term hyp_typ with
- | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) ->
+ | App(eq,args) when eq_constr eq (make_eq ()) ->
begin
let f1,_ = decompose_app args.(1) in
try
if not (isConst f1) then failwith "";
- let finfos = find_Function_infos (destConst f1) in
+ let finfos = find_Function_infos (fst (destConst f1)) in
let f_correct = mkConst(Option.get finfos.correctness_lemma)
and kn = fst finfos.graph_ind
in
@@ -1258,7 +1267,7 @@ let invfun qhyp f g =
try
let f2,_ = decompose_app args.(2) in
if not (isConst f2) then failwith "";
- let finfos = find_Function_infos (destConst f2) in
+ let finfos = find_Function_infos (fst (destConst f2)) in
let f_correct = mkConst(Option.get finfos.correctness_lemma)
and kn = fst finfos.graph_ind
in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ac54e44cc7..d0497f6f6c 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -70,7 +70,7 @@ let isVarf f x =
in global environment. *)
let ident_global_exist id =
try
- let ans = CRef (Libnames.Ident (Loc.ghost,id)) in
+ let ans = CRef (Libnames.Ident (Loc.ghost,id), None) in
let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
true
with e when Errors.noncritical e -> false
@@ -134,16 +134,12 @@ let prNamedRLDecl s lc =
let showind (id:Id.t) =
let cstrid = Constrintern.global_reference id in
let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
- let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
+ let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in
List.iter (fun (nm, optcstr, tp) ->
print_string (string_of_name nm^":");
prconstr tp; print_string "\n")
ib1.mind_arity_ctxt;
- (match ib1.mind_arity with
- | Monomorphic x ->
- Printf.printf "arity :"; prconstr x.mind_user_arity
- | Polymorphic x ->
- Printf.printf "arity : universe?");
+ Printf.printf "arity :"; prconstr ib1.mind_arity.mind_user_arity;
Array.iteri
(fun i x -> Printf.printf"type constr %d :" i ; prconstr x)
ib1.mind_user_lc
@@ -888,7 +884,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
(* Declare inductive *)
let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
- let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in
+ let mie,impls = Command.interp_mutual_inductive indl [] false (*FIXMEnon-poly *) true (* means: not coinductive *) in
(* Declare the mutual inductive block with its associated schemes *)
ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls)
@@ -961,7 +957,7 @@ let funify_branches relinfo nfuns branch =
| _ -> assert false in
let is_dom c =
match kind_of_term c with
- | Ind((u,_)) | Construct((u,_),_) -> MutInd.equal u mut_induct
+ | Ind(((u,_),_)) | Construct(((u,_),_),_) -> MutInd.equal u mut_induct
| _ -> false in
let _dom_i c =
assert (is_dom c);
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 6148860730..96bf4c9216 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -52,29 +52,21 @@ let find_reference sl s =
let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
locate (make_qualid dp (Id.of_string s))
-let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) =
- fun f_id kind value ->
- let ce = {const_entry_body = Future.from_val
- (value, Declareops.no_seff);
- const_entry_secctx = None;
- const_entry_type = None;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- } in
- ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
+let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value =
+ let ce = definition_entry ~univs:ctx value (*FIXME *) in
+ ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
let defined () = Lemmas.save_proof (Vernacexpr.Proved (false,None))
let def_of_const t =
match (kind_of_term t) with
Const sp ->
- (try (match body_of_constant (Global.lookup_constant sp) with
+ (try (match constant_opt_value_in (Global.env ()) sp with
| Some c -> c
| _ -> raise Not_found)
with Not_found ->
anomaly (str "Cannot find definition of constant " ++
- (Id.print (Label.to_id (con_label sp))))
+ (Id.print (Label.to_id (con_label (fst sp)))))
)
|_ -> assert false
@@ -83,6 +75,7 @@ let type_of_const t =
Const sp -> Typeops.type_of_constant (Global.env()) sp
|_ -> assert false
+let constr_of_global = Universes.constr_of_global
let constant sl s = constr_of_global (find_reference sl s)
@@ -188,7 +181,7 @@ let (value_f:constr list -> global_reference -> constr) =
let glob_body =
GCases
(d0,RegularStyle,None,
- [GApp(d0, GRef(d0,fterm), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l),
+ [GApp(d0, GRef(d0,fterm,None), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l),
(Anonymous,None)],
[d0, [v_id], [PatCstr(d0,(destIndRef
(delayed_force coq_sig_ref),1),
@@ -197,7 +190,7 @@ let (value_f:constr list -> global_reference -> constr) =
Anonymous)],
GVar(d0,v_id)])
in
- let body = understand Evd.empty env glob_body in
+ let body = fst (understand Evd.empty env glob_body)(*FIXME*) in
it_mkLambda_or_LetIn body context
let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) =
@@ -302,6 +295,7 @@ let check_not_nested forbidden e =
| Lambda(_,t,b) -> check_not_nested t;check_not_nested b
| LetIn(_,v,t,b) -> check_not_nested t;check_not_nested b;check_not_nested v
| App(f,l) -> check_not_nested f;Array.iter check_not_nested l
+ | Proj (p,c) -> check_not_nested c
| Const _ -> ()
| Ind _ -> ()
| Construct _ -> ()
@@ -412,6 +406,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
match kind_of_term expr_info.info with
| CoFix _ | Fix _ -> error "Function cannot treat local fixpoint or cofixpoint"
+ | Proj _ -> error "Function cannot treat projections"
| LetIn(na,b,t,e) ->
begin
let new_continuation_tac =
@@ -640,7 +635,16 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
in
continuation_tac {info with info = new_e; forbidden_ids = new_forbidden}
+let pf_type c tac gl =
+ let evars, ty = Typing.e_type_of (pf_env gl) (project gl) c in
+ tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
+let pf_typel l tac =
+ let rec aux tys l =
+ match l with
+ | [] -> tac (List.rev tys)
+ | hd :: tl -> pf_type hd (fun ty -> aux (ty::tys) tl)
+ in aux [] l
(* This is like the previous one except that it also rewrite on all
hypotheses except the ones given in the first argument. All the
@@ -660,12 +664,13 @@ let mkDestructEq :
let type_of_expr = pf_type_of g expr in
let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
to_revert_constr in
+ pf_typel new_hyps (fun _ ->
tclTHENLIST
[Simple.generalize new_hyps;
(fun g2 ->
change_in_concl None
(pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2);
- Proofview.V82.of_tactic (simplest_case expr)], to_revert
+ Proofview.V82.of_tactic (simplest_case expr)]), to_revert
let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
@@ -1167,7 +1172,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
let get_current_subgoals_types () =
let p = Proof_global.give_me_the_proof () in
let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in
- List.map (Goal.V82.abstract_type sigma) sgs
+ sigma, List.map (Goal.V82.abstract_type sigma) sgs
let build_and_l l =
let and_constr = Coqlib.build_coq_and () in
@@ -1225,12 +1230,12 @@ let clear_goals =
let build_new_goal_type () =
- let sub_gls_types = get_current_subgoals_types () in
- (* Pp.msgnl (str "sub_gls_types1 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
+ let sigma, sub_gls_types = get_current_subgoals_types () in
+ (* Pp.msgnl (str "sub_gls_types1 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
let sub_gls_types = clear_goals sub_gls_types in
(* Pp.msgnl (str "sub_gls_types2 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
let res = build_and_l sub_gls_types in
- res
+ sigma, res
let is_opaque_constant c =
let cb = Global.lookup_constant c in
@@ -1239,7 +1244,7 @@ let is_opaque_constant c =
| Declarations.Undef _ -> true
| Declarations.Def _ -> false
-let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) =
+let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) =
(* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
let current_proof_name = get_current_proof_name () in
let name = match goal_name with
@@ -1265,7 +1270,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
let lid = ref [] in
let h_num = ref (-1) in
Proof_global.discard_all ();
- build_proof
+ build_proof (Univ.ContextSet.empty)
( fun gls ->
let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
tclTHENSEQ
@@ -1312,8 +1317,8 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
in
Lemmas.start_proof
na
- (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma)
- gls_type
+ (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
+ (gls_type, ctx)
hook;
if Indfun_common.is_strict_tcc ()
then
@@ -1330,7 +1335,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
(fun c ->
tclTHENSEQ
[Proofview.V82.of_tactic intros;
- Simple.apply (interp_constr Evd.empty (Global.env()) c);
+ Simple.apply (fst (interp_constr Evd.empty (Global.env()) c)) (*FIXME*);
tclCOMPLETE (Proofview.V82.of_tactic Auto.default_auto)
]
)
@@ -1354,22 +1359,24 @@ let com_terminate
relation
rec_arg_num
thm_name using_lemmas
- nb_args
+ nb_args ctx
hook =
- let start_proof (tac_start:tactic) (tac_end:tactic) =
+ let ctx = Univ.ContextSet.of_context ctx in
+ let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
let (evmap, env) = Lemmas.get_current_context() in
Lemmas.start_proof thm_name
- (Global, Proof Lemma) ~sign:(Environ.named_context_val env)
- (compute_terminate_type nb_args fonctional_ref) hook;
+ (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
+ (compute_terminate_type nb_args fonctional_ref, ctx) hook;
ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start)));
ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
input_type relation rec_arg_num ))))
in
- start_proof tclIDTAC tclIDTAC;
+ start_proof ctx tclIDTAC tclIDTAC;
try
- let new_goal_type = build_new_goal_type () in
- open_new_goal start_proof using_lemmas tcc_lemma_ref
+ let sigma, new_goal_type = build_new_goal_type () in
+ open_new_goal start_proof (Evd.get_universe_context_set sigma)
+ using_lemmas tcc_lemma_ref
(Some tcc_lemma_name)
(new_goal_type);
with Failure "empty list of subgoals!" ->
@@ -1384,7 +1391,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
(cont_tactic:Id.t list -> tactic) g =
let ids = pf_ids_of_hyps g in
let terminate_constr = constr_of_global term_f in
- let nargs = nb_prod (type_of_const terminate_constr) in
+ let nargs = nb_prod (fst (type_of_const terminate_constr)) (*FIXME*) in
let x = n_x_id ids nargs in
tclTHENLIST [
h_intros x;
@@ -1406,8 +1413,8 @@ let (com_eqn : int -> Id.t ->
let (evmap, env) = Lemmas.get_current_context() in
let f_constr = constr_of_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
- (Lemmas.start_proof eq_name (Global, Proof Lemma)
- ~sign:(Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
+ (Lemmas.start_proof eq_name (Global, false, Proof Lemma)
+ ~sign:(Environ.named_context_val env) (equation_lemma_type, (*FIXME*)Univ.ContextSet.empty) (fun _ _ -> ());
ignore (by
(Proofview.V82.tactic (start_equation f_ref terminate_ref
(fun x ->
@@ -1445,13 +1452,15 @@ let (com_eqn : int -> Id.t ->
let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
generate_induction_principle using_lemmas : unit =
- let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
- let env = push_named (function_name,None,function_type) (Global.env()) in
+ let env = Global.env() in
+ let evd = ref (Evd.from_env env) in
+ let function_type = interp_type_evars evd env type_of_f in
+ let env = push_named (function_name,None,function_type) env in
(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
- let equation_lemma_type =
- nf_betaiotazeta
- (interp_constr Evd.empty env ~impls:rec_impls eq)
- in
+ let ty = interp_type_evars evd env ~impls:rec_impls eq in
+ let evm, nf = Evarutil.nf_evars_and_universes !evd in
+ let equation_lemma_type = nf_betaiotazeta (nf ty) in
+ let function_type = nf function_type in
(* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
let res_vars,eq' = decompose_prod equation_lemma_type in
let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in
@@ -1471,13 +1480,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let equation_id = add_suffix function_name "_equation" in
let functional_id = add_suffix function_name "_F" in
let term_id = add_suffix function_name "_terminate" in
- let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) res in
+ let ctx = Evd.universe_context evm in
+ let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res in
let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in
let relation =
- interp_constr
+ fst (*FIXME*)(interp_constr
Evd.empty
env_with_pre_rec_args
- r
+ r)
in
let tcc_lemma_name = add_suffix function_name "_tcc" in
let tcc_lemma_constr = ref None in
@@ -1524,6 +1534,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
term_id
using_lemmas
(List.length res_vars)
- hook)
+ ctx hook)
()
-
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 2ef6852036..f60eedbe6e 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -12,9 +12,9 @@ bool ->
Constrintern.internalization_env ->
Constrexpr.constr_expr ->
Constrexpr.constr_expr ->
- int -> Constrexpr.constr_expr -> (Names.constant ->
+ int -> Constrexpr.constr_expr -> (Term.pconstant ->
Term.constr option ref ->
- Names.constant ->
- Names.constant -> int -> Term.types -> int -> Term.constr -> 'a) -> Constrexpr.constr_expr list -> unit
+ Term.pconstant ->
+ Term.pconstant -> int -> Term.types -> int -> Term.constr -> 'a) -> Constrexpr.constr_expr list -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:24:36 +0000