aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.ml4
Commit message (Collapse)AuthorAge
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a flag to control the use of typing when instantiating appliedGravatar herbelin2011-12-17
| | | | | | | meta in the tactic unification algorithm ("auto" becomes much slower if it takes into account the type of metas). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14813 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introducing a notion of evar candidates to be used when an evar isGravatar herbelin2011-12-16
| | | | | | | | | | | | known in advance to be instantiable by only a finite number of terms. When an evar with candidates remain unsolved after unification, the first candidate is taken as a heuristic. This is used in particular to reduce the number of pending conversion problems when trying to infer the return clause of a pattern-matching problem. As an example, this repairs test 2615.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14797 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a DEPRECATED flag in declaration of options. For now only two options ↵Gravatar ppedrot2011-11-24
| | | | | | are declared as such, but I suspect Coq to contain some more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix parsing of :>> and backtrack correctly on the cache of hints for local ↵Gravatar msozeau2011-11-18
| | | | | | contexts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14688 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
| | | | | | | | | | | | | | This adds two experimental features to the typeclass implementation: - Path cuts: a way to specify through regular expressions on instance names search pathes that should be avoided (e.g. [proper_flip proper_flip]). Regular expression matching is implemented through naïve derivatives. - Forward hints for subclasses: e.g. [Equivalence -> Reflexive] is no longer applied backwards, but introducing a specific [Equivalence] in the environment register a [Reflexive] hint as well. Currently not backwards-compatible, the next patch will allow to specify direction of subclasses hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14671 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix implementation of Hint Immediate used by typeclasses eautoGravatar msozeau2011-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14398 85f007b7-540e-0410-9357-904b9bb8a0f7
* Class_tactics: generic equality on named_context_val replaced by ↵Gravatar puech2011-07-29
| | | | | | eq_named_context_val git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14340 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalizing flag use_evars_pattern_unification into a flagGravatar herbelin2011-06-18
| | | | | | | | | | use_pattern_unification common for evars and metas. As a compensation, add a flag use_meta_bound_pattern_unification to restore the old mechanism of pattern unification for metas applied to rels only (this is used e.g. by auto). Not sure yet, what could be the most appropriate set of flags. Added documentation of the flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14221 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a flag to restrict conversion in tactic unification on theGravatar herbelin2011-06-13
| | | | | | | | | strict subterms of the initial unification problem (inspired from ssreflect rewriting strategy). Not activated however (a few applications of setoid rewrite use this possibility on closed terms in the stdlib, e.g. "flip le p (min n m)" identified with "le (min n m) p"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14198 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a new flag for freezing evars in tactic unification. Used thisGravatar herbelin2011-06-12
| | | | | | | | | | | | | | | | flag to forbid rewriting tactics to instantiate an evar of the goal while looking for subterms (this is not clear that we always want that for rewrite but we certainly want it for autorewrite; see comments by Charguéraud on coqdev Oct 2010). In a few cases in the theories, a pre-existing evar of an hyp used for rewriting is instantiated by the rewriting step. Let's accept this at the current time. We have to make progress towards documenting and stabilizing the strategy for matching/unifying subterms in rewrite/induction/set... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14190 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved allow_K to a unification flagGravatar herbelin2011-06-10
| | | | | | | | - seized the opportunity to align unification flags for functional induction to the ones of induction - also tried to add delta in the elim_flags used in tactics.ml - also tried to unify the rewrite flags in concl or in hyp (removed allow_K in hyps) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14186 85f007b7-540e-0410-9357-904b9bb8a0f7
* Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR)Gravatar letouzey2011-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14135 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge branch 'subclasses' into coq-trunkGravatar msozeau2011-05-05
| | | | | | | | | Stop using hnf_constr in unify_type, which might unfold constants that are marked opaque for unification. Conflicts: pretyping/unification.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14092 85f007b7-540e-0410-9357-904b9bb8a0f7
* Don't force progress on instance applications, there is always progress when ↵Gravatar msozeau2011-04-20
| | | | | | refining dependent instances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14031 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a flag to control betaiota reduction during unification to maintain ↵Gravatar msozeau2011-04-18
| | | | | | backward compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Put dependent subgoals first so as to allow backtracking on them, might ↵Gravatar msozeau2011-04-13
| | | | | | change resolution time quite a bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13997 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Make typeclass transparency information directly availableGravatar msozeau2011-04-13
| | | | | | | - Fix pretyping to consider remaining unif problems with the right transparency information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13996 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Remove create_evar_defsGravatar msozeau2011-04-13
| | | | | | - Be careful with consider_remaining_unif_problems: it might instantiate an evar, including the current goal! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13995 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Improve unification (beta-reduction, and same heuristic as evarconv for ↵Gravatar msozeau2011-04-13
| | | | | | reducing matches). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13993 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Do not make constants with an assigned type polymorphic (wrong unfoldings).Gravatar msozeau2011-04-13
| | | | | | - Add Set Typeclasses Debug/Depth n options for typeclasses eauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13989 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
| | | | | | | | | | | | | | | | conversion when checking types of instanciations while having restricted delta reduction for unification itself. This makes auto/eauto... backward compatible. - Change semantics of [Instance foo : C a.] to _not_ search for an instance of [C a] automatically and potentially slow down interaction, except for trivial classes with no fields. Use [C a := _.] or [C a := {}] to search for an instance of the class or for every field. - Correct treatment of transparency information for classes declared in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Better error messages taking unif. constraints into account.Gravatar msozeau2011-03-11
| | | | | | | - Normalize evars in typeclasses eauto also before [intro]. - Disallow use of nf_evars variants that drop unif. constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13904 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot a use of evars_reset_evd in nf_evars, add an optional argument asGravatar msozeau2011-03-10
| | | | | | | in the 8.3 patch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13903 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Allow to set a particular transparent_state for the local hintGravatar msozeau2011-03-04
| | | | | | | | database - Fix [specialize] to properly resolve typeclass constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13868 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
| | | | | | | | | | conversion. - Fix trans_fconv* to use evars correctly. - Normalize the goal with respect to evars before rewriting in [rewrite], allowing to see instanciations from other subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
* Try to clarify a bit Class_tactics (comments, refactoring,...)Gravatar letouzey2011-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13832 85f007b7-540e-0410-9357-904b9bb8a0f7
* An generic imperative union-find, used for deps of evars in Class_tacticsGravatar letouzey2011-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13831 85f007b7-540e-0410-9357-904b9bb8a0f7
* Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)Gravatar letouzey2011-02-03
| | | | | | | | | | After r13717, we concentrate on undefined evars. But doing so too naively was breaking Class_tactics.split_evars, since defined evars may point to undefined ones. We should not ignore them, but rather traverse them, which is now done by functions Evarutil.undefined_evars_of_* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13809 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add [Typeclasses Debug] option that respects backtracking, solveGravatar msozeau2011-01-11
| | | | | | | | regression in typeclass resolution not generating the proper subgoals (may break some contribs). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13787 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evar-related speed-up and clarifications in Class_tactics and RewriteGravatar letouzey2010-12-15
| | | | | | | | | | | Some functions are restricted to consider only undefined evars, and some Evd.fold are replaced by Evd.fold_undefined. I'm less sure about the modifications in rewrite.ml4, but in pratice they seem to work well on the stdlib. I was planning to say assert false for Not_found in Rewrite.evd_of_existentials but some file of the stdlib doesn't like that (to be checked). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13717 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc improvements about evar_mapGravatar letouzey2010-12-15
| | | | | | | | | | | | - A Evd.defined_evars to keep only this part of the evar_map - One Evd.fold less in Typeclasses.mark_unresolvables - We check that only undefined evar_map could be set unresolvable - A duplicated function in himsg.ml TODO: some calls to Evd.fold(_undefined) would be faster if written as Map.map or Map.mapi. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13716 85f007b7-540e-0410-9357-904b9bb8a0f7
* Class_tactics: avoid an Evd.fold taking ages in contrib ProjectiveGeometryGravatar letouzey2010-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13709 85f007b7-540e-0410-9357-904b9bb8a0f7
* Two [Evd.fold] turned into [Evd.fold_undefined].Gravatar aspiwack2010-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13491 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesGravatar glondu2010-09-30
| | | | | | | | | | | | | | Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first component is kept, the second one can be obtained with Tacinterp.eval_tactic. Rationale: these declare parsing rules, and eval_tactic is a semantic action, and therefore should be done in the rule body instead. Moreover, having the glob_tactic_expr and its evaluation captured by these rules was quite confusing IMHO. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13480 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
| | | | | | | | | | In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
| | | | | | | governed in the latter case by a flag since (useful e.g. for setoid rewriting which otherwise loops as it is implemented). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13443 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
* Tentative fix for typeclass resolution raising Evd.define exceptions.Gravatar msozeau2010-06-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13087 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid computing tactic printing tree (std_ppcmds) when printing not needed inGravatar herbelin2010-06-03
| | | | | | eauto and class_tactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13066 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
| | | | | | | | | | | | | | | | | | | | | | | The choice between camlp4/5 is done during configure with flags -usecamlp5 (default for the moment) vs. -usecamlp4. Currently, to have a full camlp4 compatibility, you need to change all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI" into "`EOI" in grammar entries. I've a sed script that does that (actually the converse), but I prefer to re-think it and check a few things before branching this sed into the build mechanism. lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5 and try to propose a common interface (cf LexerSig / GrammarSig). A few incompatible quotations have been turned into underlying code manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END parsable by both camlp4 and 5. See in particular the fate of <:str_item< declare ... end >> Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc). This forces to use camlp5 > 5.01. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove compile-command pragmas for emacsGravatar letouzey2010-05-19
| | | | | | | | | | | | | | | | | | | These declarations (e.g. make -C .. bin/coqtop.byte) are quite annoying when debugging stuff over the whole archive: all of a sudden, M-x recompile isn't doing what you intended just because you've visited some specific files. Instead: - Feel free to rather add intermediate targets in the Makefile if they aren't there yet. - For avoiding typing the -C with many .. after, you can have a look at my recursively-descending make: http://www.pps.jussieu.fr/~letouzey/download/make.sh which is to be renamed make and placed in a bin dir with more priority than /usr/bin. Beware! I've already add a few bad surprises with this hack, but it's really convenient nonetheless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13014 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
* 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
* Util: remove list_split_at which is a clone of list_chopGravatar letouzey2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12939 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix splitting evars tactics and stop dropping evar constraints whenGravatar msozeau2010-03-15
| | | | | | | | | building a new goal evar defs. Allow customization of the reduction function applied to subtac obligations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12867 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix [Existing Class] impl and add documentation. Fix computation of theGravatar msozeau2010-02-10
| | | | | | | dependency order of obligations that was not backwards-compatible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12719 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
| | | | | | | of cleanup in tactics/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12705 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quick fix for references to section variables unbound in the currentGravatar msozeau2010-01-26
| | | | | | | environment during unification. Should be checked earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12692 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 13:02:09 +0000