aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refiner.mli
Commit message (Collapse)AuthorAge
* [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
|
* [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
|
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | We do up to `Term` which is the main bulk of the changes.
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Removing the tclWEAK_PROGRESS tactical.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | The only remaining use was applied on the unfold tactic, and the behaviours of tclPROGRESS and tclWEAK_PROGRESS coincide whenever only one goal is produced by their argument tactic.
* Removing the tclNOTSAMEGOAL primitive from the API.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | The only use in Equality is reimplemented in the new engine.
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr.
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
|/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
| | | | | | | | | | | | | | | | | | | | Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads.
* More self-contained code for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
|
* Removing unused Refiner.tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
|
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in ↵Gravatar Matthieu Sozeau2014-06-10
| | | | | | | | Universes. Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes. Remove unused functions from univ as well and refactor a little bit. Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
* - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ↵Gravatar Matthieu Sozeau2014-05-08
| | | | | | | | evar_map in tactics, avoiding useless and potentially costly merge's of constraints. - Implement revert and generalize using the new tactics (not bound to syntax though, as they are not backwards-compatible yet).
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
|
* Removing unused functions in Refiner.Gravatar Pierre-Marie Pédrot2014-04-06
|
* Removing the Change_evar refiner rule.Gravatar Pierre-Marie Pédrot2014-03-31
|
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On the compilation of Coq, we can see an increase of ~20% compile time on my completely non-scientific tests. Hopefully this can be fixed. There are a lot of low hanging fruits, but this is an iso-functionality commit. With a few exceptions which were not necessary for the compilation of the theories: - The declarative mode is not yet ported - The timeout tactical is currently deactivated because it needs some subtle I/O. The framework is ready to handle it, but I haven't done it yet. - For much the same reason, the ltac debugger is unplugged. It will be more difficult, but will eventually be back. A few comments: I occasionnally used a coercion from [unit Proofview.tactic] to the old [Prooftype.tactic]. It should work smoothely, but loses any backtracking information: the coerced tactics has at most one success. - It is used in autorewrite (it shouldn't be a problem there). Autorewrite's code is fairly old and tricky - It is used in eauto, mostly for "Hint Extern". It may be an issue as time goes as we might want to have various success in a "Hint Extern". But it would require a heavy port of eauto.ml4 - It is used in typeclass eauto, but with a little help from Matthieu, it should be easy to port the whole thing to the new tactic engine, actually simplifying the code. - It is used in fourier. I believe it to be inocuous. - It is used in firstorder and congruence. I think it's ok. Their code is somewhat intricate and I'm not sure they would be easy to actually port. - It is used heavily in Function. And honestly, I have no idea whether it can do harm or not. Updates: (11 June 2013) Pierre-Marie Pédrot contributed the rebase over his new stream based architecture for Ltac matching (r16533), which avoid painfully and expensively working around the exception-throwing control flow of the previous API. (11 October 2013) Rebasing over recent commits (somewhere in r16721-r16730) rendered a major bug in my implementation of Tacticals.New.tclREPEAT_MAIN apparent. It caused Field_theory.v to loop. The bug made rewrite !lemma, rewrite ?lemma and autorewrite incorrect (tclREPEAT_MAIN was essentially tclREPEAT, causing rewrites to be tried in the side-conditions of conditional rewrites as well). The new implementation makes Coq faster, but it is pretty much impossible to tell if it is significant at all. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16967 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
| | | | | | | | | | | | | | | | | | | state out of one we were threading all the way along. This should be safer, as one cannot forego side effects accidentally by manipulating explicitly the [sigma] container. Still, this patch raised the issue of badly used evar maps. There is an ad-hoc workaround (i.e. a hack) in Rewrite to handle the fact it uses evar maps in an unorthodox way. Likewise, that mean we have to revert all contrib patches that added effect threading... There was also a dubious use of side effects in their toplevel handling, that duplicates them, leading to the need of a rather unsafe List.uniquize afterwards. It should be investigaged. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16850 85f007b7-540e-0410-9357-904b9bb8a0f7
* State Transaction MachineGravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | | | | | | | | | The process_transaction function adds a new edge to the Dag without executing the transaction (when possible). The observe id function runs the transactions necessary to reach to the state id. Transaction being on a merged branch are not executed but stored into a future. The finish function calls observe on the tip of the current branch. Imperative modifications to the environment made by some tactics are now explicitly declared by the tactic and modeled as let-in/beta-redexes at the root of the proof term. An example is the abstract tactic. This is the work described in the Coq Workshop 2012 paper. Coq is compile with thread support from now on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merging Context and Sign.Gravatar ppedrot2013-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove Refiner.abstract_tactic and similarGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15872 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clean-up : removal of Proof_type.tactic_exprGravatar letouzey2012-10-06
| | | | | | | | This instance of gen_tactic_expr was used only to decorate tactics via Refiner.abstract_tactics and alii, but these expressions are now ignored by the new proof-engine (no "info"...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15865 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxGravatar letouzey2012-10-06
| | | | | | | Nested was never constructed, while the notion of abstract_tactic_box is obsolete (cf. Refiner.abstract_tactic). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15862 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a new tactical infoH tac, that displays the names of hypothesis ↵Gravatar courtieu2012-10-01
| | | | | | created by tac, in the 'as' format. Interfaces can use this to insert automatically an 'as' close at the end of the tactic (afterward). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15839 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* info_trivial, info_auto, info_eauto, and debug (trivial|auto)Gravatar letouzey2012-03-30
| | | | | | | | | | | | | | | | | | | | | | | To mitigate the lack of a general "info" tactical, let's introduce some specialized tactics info_trivial, info_auto and info_eauto that display the basic tactics used when solving a goal. We also add tactics "debug trivial" and "debug auto" which display every basic tactics attempted by trivial or auto. Triggering the "info" or "debug" mode for auto, eauto, trivial can also be done now via global options, such as Set Debug Auto or Set Info Eauto. In case both debug and info modes are activated, the debug mode takes precedence. NB: it would be nice to name these tactics "info xxx" instead of "info_xxx", but I don't see how to implement a "info eauto" in eauto.ml4 (hence by TACTIC EXTEND) while keeping a generic "info foo" tactic in g_ltac.ml4 (useful to display a nice message about the unavailability of the general info). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15103 85f007b7-540e-0410-9357-904b9bb8a0f7
* A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsGravatar letouzey2011-03-18
| | | | | | | | | | | | | | Note: even if this new tactical can be quite handy during the development phase, (for instance to bound the time allocated to some search tactics), please be aware of its main drawback: with it, scripts are no longer machine-independant, something that works on a quick machine may fail on a slow one. The converse is even possible if you combine this "timeout" with other tactic combinators. We strongly advise to not leave any "timeout" in the final version of a development. In addition, this feature won't probably work on native win32, since Unix.alarm isn't implemented. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13917 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
| | | | | | Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
| | | | | | | | | | | | | | | | | | | dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a fairly large commit (around 140 files and 7000 lines of code impacted), it will cause some troubles for sure (I've listed the know regressions below, there is bound to be more). At this state of developpement it brings few features to the user, as the old tactics were ported with no change. Changes are on the side of the developer mostly. Here comes a list of the major changes. I will stay brief, but the code is hopefully well documented so that it is reasonably easy to infer the details from it. Feature developer-side: * Primitives for a "real" refine tactic (generating a goal for each evar). * Abstract type of tactics, goals and proofs * Tactics can act on several goals (formally all the focused goals). An interesting consequence of this is that the tactical (. ; [ . | ... ]) can be separated in two tacticals (. ; .) and ( [ . | ... ] ) (although there is a conflict for this particular syntax). We can also imagine a tactic to reorder the goals. * Possibility for a tactic to pass a value to following tactics (a typical example is an intro function which tells the following tactics which name it introduced). * backtracking primitives for tactics (it is now possible to implement a tactical '+' with (a+b);c equivalent to (a;c+b;c) (itself equivalent to (a;c||b;c)). This is a valuable tool to implement tactics like "auto" without nowing of the implementation of tactics. * A notion of proof modes, which allows to dynamically change the parser for tactics. It is controlled at user level with the keywords Set Default Proof Mode (this is the proof mode which is loaded at the start of each proof) and Proof Mode (switches the proof mode of the current proof) to control them. * A new primitive Evd.fold_undefined which operates like an Evd.fold, except it only goes through the evars whose body is Evar_empty. This is a common operation throughout the code, some of the fold-and-test-if-empty occurences have been replaced by fold_undefined. For now, it is only implemented as a fold-and-test, but we expect to have some optimisations coming some day, as there can be a lot of evars in an evar_map with this new implementation (I've observed a couple of thousands), whereas there are rarely more than a dozen undefined ones. Folding being a linear operation, this might result in a significant speed-up. * The declarative mode has been moved into the plugins. This is made possible by the proof mode feature. I tried to document it so that it can serve as a tutorial for a tactic mode plugin. Features user-side: * Unfocus does not go back to the root of the proof if several Focus-s have been performed. It only goes back to the point where it was last focused. * experimental (non-documented) support of keywords BeginSubproof/EndSubproof: BeginSubproof focuses on first goal, one can unfocus only with EndSubproof, and only if the proof is completed for that goal. * experimental (non-documented) support for bullets ('+', '-' and '*') they act as hierarchical BeginSubproof/EndSubproof: First time one uses '+' (for instance) it focuses on first goal, when the subproof is completed, one can use '+' again which unfocuses and focuses on next first goal. Meanwhile, one cas use '*' (for instance) to focus more deeply. Known regressions: * The xml plugin had some functions related to proof trees. As the structure of proof changed significantly, they do not work anymore. * I do not know how to implement info or show script in this new engine. Actually I don't even know what they were suppose to actually mean in earlier versions either. I wager they would require some calm thinking before going back to work. * Declarative mode not entirely working (in particular proofs by induction need to be restored). * A bug in the inversion tactic (observed in some contributions) * A bug in Program (observed in some contributions) * Minor change in the 'old' type of tactics causing some contributions to fail. * Compilation time takes about 10-15% longer for unknown reasons (I suspect it might be linked to the fact that I don't perform any reduction at QED-s, and also to some linear operations on evar_map-s (see Evd.fold_undefined above)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We renounced to distribute evars to constr and bindings and to let tactics do the merge. There are now two disciplines: - the general case is that the holes in tactic arguments are pushed to the general sigma of the goal so that tactics have no such low-level tclEVARS, Evd.merge, or check_evars to do: - what takes tclEVARS and check_evars in charge is now a new tactical of name tclWITHHOLES (this tactical has a flag to support tactics in either the "e"- mode and the non "e"- mode); - the merge of goal evars and holes is now done generically at interpretation time (in tacinterp) and as a side-effect it also anticipates the possibility to refer to evars of the goal in the arguments; - with this approach, we don't need such constr/open_constr or bindings/ebindings variants and we can get rid of all ugly inj_open-style coercions; - some tactics however needs to have the exact subset of holes known; this is the case e.g. of "rewrite !c" which morally reevaluates c at each new rewriting step; this kind of tactics still receive a specific sigma around their arguments and they have to merge evars and call tclWITHHOLES by themselves. Changes so that each specific tactics can take benefit of this generic support remain to be done. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
| | | | | | | | | | unnecessarily computed when the user won't see it (avoids the costly nf_evar_defs in typeclass errors). Add hook support for mutual definitions in Program. Try to solve only the argument typeclasses when calling [refine]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12185 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixing declarative mode in presence of high use of Change_evars nodesGravatar herbelin2009-05-20
| | | | | | | | | | | | | (bug 2092 and decl_mode.v in test suite). - Added a debugging printer for pftreestate. - Fixing American spelling in RefMan-decl.tex. - Optimizing application of tactic validation by removing consistency test in descend. - Fixing printing ambiguity for Hint Rewrite ->/<- in extratactics.ml4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12134 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11980 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
| | | | | | | | | the number of conjunctions to split. - A few cleaning and uniformisation in auto.ml. - Removal of v62 hints already in core. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
| | | | | | | | | | abusivement sur les clauses. Nettoyage au passage de metamap qui était utilisé à la fois pour les substitutions de meta et pour les contextes de typage de meta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11467 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move exception-handling code for catching tactics failure Gravatar msozeau2008-05-01
| | | | | | | | in a separate function in Refiner and use it in eauto to capture the same semantics as auto (which uses tclTRY) when trying tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10879 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
| | | | | | | | | | - New vernac command "Delete" - New vernac command "Undo To" - Added a few hooks used by new contrib/interface - Beta/incomplete version of dependency generation and dumping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merged revisions ↵Gravatar msozeau2007-12-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses ........ r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line Comment grammar error ........ r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines The initial Type Classes patch. This patch introduces type classes and instance definitions a la Haskell. Technically, it uses the implicit arguments mechanism which was extended a bit. The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters. It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). ........ r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line Fix interface ........ r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line Fix more xlate code ........ r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines Update coqdoc for type classes, fix proof state not being displayed on Next Obligation. ........ r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines Bug fixes in Instance decls. ........ r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines Streamline typeclass context implementation, prepare for class binders in proof statements. ........ r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions ........ r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context. ........ r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line Stupid bug ........ r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints ........ r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors ........ r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent. New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental. Other bugs related to naming in typeclasses fixed. ........ r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines Progress on setoids using type classes, recognize setoid equalities in hyps better. Streamline implementation to return more information when resolving setoids (return the results setoid). ........ r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line Syntax change, more like Coq ........ r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax ........ r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines Work on type classes based rewrite tactic. ........ r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets. ........ r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line Forgot to add a file ........ r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts. ........ r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. Add useful tactics to Program.Subsets. ........ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding the tactic "instantiate" (without argument), to force theGravatar glondu2007-12-07
| | | | | | | instantiation of evars in tacticals (cf r9985, r10294). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10356 85f007b7-540e-0410-9357-904b9bb8a0f7