aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2013-11-19Optimization: in case of empty substitution, merging is trivial.Pierre-Marie Pédrot
2013-11-16Slightly faster version of merging substitutions in TacticMatching.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17094 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-14Changes the semantics of Ltac's non-lazy pattern matching in presence of ↵aspiwack
multiple successes. The semantics was a bit strange: an immediate failure of a branch would cause the pattern matching to backtrack, and failure after the match could cause the selected tactic to backtrack. However, the pattern matching process won't backtrack after it has selected a tactic with at least one success. To avoid changing the semantics of pattern matching with single-success tactics, I made it so that it is impossible to backtrack into a pattern matching once done. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17090 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-14Implementation of Ltac's match and match goal fully based on IStream.aspiwack
The implementation was partly based on IStream and partly on a control flow with exception. The latter does not mix well with the monadic tactics. I've moved the algorithmic part of pattern-matching to a new file (tactics/tacticMatching.ml), in order to de-entangle the pattern-matching procedure from the interpretation. This shaves off 300 lines of code from Tacinterp, which is still over 2000 lines of code. It is a first step towards refactoring tacinterp. To be fair, part of what disapeared are lines which sent messages to the debugger. I was not too concerned with them because I understand people found the debugger much too fine-grain on Ltac's pattern matching. But conversely, there may be too few debugging hooks now. This is worth looking into. In TacticMatching itself, I used a monadic style to express the pattern-matching procedure concisely. I implemented the monad in a fairly brute-force way, using the existing primitive of IStream. It may be worth experimenting with specialized primitive. I am less worried about the monadic style than about the number of allocation of list cells that the primitives entail. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17089 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-14Remove some dead code in tacinterp.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17087 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-12Do not print tactic notation names at each interpretation step.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17082 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-10Centralizing the Ltac-defining functions in Tacenv.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17080 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
Instead of putting the body directly in the AST, we register it in a table. This time it should work properly. Tactic notation are given kernel names to ensure the unicity of their contents. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17079 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-09Revert the previous commit. It broke Coq compilation.ppedrot
Tactics notation interpretation was messed up because of the use of identical keys for different notations. All my tentative fixes were unsuccessful, so better blankly revert the commit for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17078 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-09Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
Instead of putting the body directly in the AST, we register it in a table. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17077 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-08Porting Tactics.assumption to the new engine.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17073 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was ↵aspiwack
solved. This made "autorewrite using tac" fail. Spotted in CoLoR and Demos. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17059 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Fix ltac's progress tactical: requires progress in each goal.aspiwack
Proofview.tclPROGRESS considers that a tactic that changes the list of goal progresses, under this semantics, "progress auto" succeeds if its applied to two goals and solves the first one but not the second one. This would break backwards compatibility. Spotted in Fermat4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17058 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Fix the tactical ; [ … ] : the "incorrect number of goal" error was not ↵aspiwack
caught by ltac tacticals. The errors were not translated into ltac errors (and at some occurence errors were raised in OCaml rather than inside the tactic monad). Spotted in ProjectiveGeometry and Goedel. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17057 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Fix change: nf_evar prior to tactic interpretation.aspiwack
Noticed in PTSATR. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17056 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Allowing proofs starting with a non-empty evarmap.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17055 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fixing CAMLP4 compilation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17039 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fix set: nf_evar prior to tactic interpretation.aspiwack
Noticed in CoRN git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17038 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Plug back infoH.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17037 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Plugs back external tactics.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17036 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fix the log of debug auto.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17035 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Update comments.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17033 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Doc: solve the bad interaction between Declare Implicit Tactic and refine.aspiwack
An implicit tactic was declared and made refine fail (trying to solve the open goals of the refined term resulted in an error). There was no way to remove the implicit tactic (it isn't managed by an option so isn't removed by Reset Initial). I added the option under the name Clear Implicit Tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17032 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02The repeat tactic now honors failure levels in ltac.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17030 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fix destruct: nf_evar prior to tactic interpretation.aspiwack
Noticed in CoRN git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17028 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Tacticals.New.tclWITHHOLES: clean up.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17027 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Refine now does iota reduction in addition to beta.aspiwack
Restores more compatibility with the earlier implementation of refine. Needed in ssreflect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17023 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Refine: Tactics.New.refine does beta-reduction.aspiwack
Previously I had wrapped Tactics.New.refine with extra beta-reduction in extratactics.ml4, that is, only for Ltac. Ocaml plugins saw the version without reduction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17019 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds a tactic give_up.aspiwack
Gives up on the focused goals. Shows an unsafe status. Unlike the admit tactic, the proof cannot be closed until the users goes back and solves these goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17018 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02A tactic shelve_unifiable.aspiwack
Puts on the shelf every goals under focus on which other goals under focus depend. Useful when we want to solve these goals by unification (as in a first order proof search procedure, for instance). Also meant to be able to recover approximately the semantics of the old refine with the new implementation (use refine t; shelve_unifiable). TODO: bug dans l'example de shelve_unifiable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17017 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Made multiple-goal tactic work after all: .aspiwack
Internalization was done relative to a goal. It doesn't make sense in the case of all:. When we make a tactic with all: the environment for internalization is taken to be the global environment. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17016 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Make multiple-goal tactics possible after a tclTHEN.aspiwack
Tacinterp used to interprete every tactics inside a goal, making multiple-goal tactics act on a single goal anyway. Uses a simple heuristic to decide when a goal is not needed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17015 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds a shelve tactic.aspiwack
The shelve tactic puts all the focused goals out of sight. They can be later recalled by the Unshelve command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17013 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds an experimental exactly_once tactical.aspiwack
exactly_once t, will have a success if t has exactly once success. There are a few caveats: - The underlying effects of t may happen in an unpredictable order (hence it may be wise to use it only with "pure" tactics) - The second success of a tactic is conditional on the exception thrown. In Ltac it doesn't show, but in the underlying code, the tactical also expects the exception you want to use to produce the second success. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17009 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Made Proofview.Goal.hyps a named_context.aspiwack
There was really no point in having it be a named_context val. The tactics are not going to access the vm cache. Only vm_compute will. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17007 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Refine does beta-reductions.aspiwack
To avoid the unpleasantness of having beta-redex in terms after an application of refine, refine is followed by lazy beta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17006 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds a tactical once.aspiwack
[once t] does just as [t] but has exactly one success it [t] has at least one success. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17004 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Corrects the semantics of the "+" tactical.aspiwack
- Treats goals independently - Honors failure levels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17003 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Less use of the list-based interface for goal-bound tactics.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17002 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Tachmach.New is now in Proofview.Goal.enter style.aspiwack
As a result the use of the glist-style interface for manipulating goals has almost been removed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17001 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02More Proofview.Goal.enter.aspiwack
Proofview.Goal.enter is meant to eventually replace the Goal.sensitive monad. This commit changes the type of Proofview.Goal.enter from taking a four argument function (environment, evar_map, hyps, concl) from a one argument function of abstract type Proofview.Goal.t. It will be both more extensible and more akin to old-style tactics. This commit also changes the type of Proofview.Goal.{concl,hyps,env} from monadic operations to projection from a Proofview.Goal.t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17000 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Added the tactical "tac1 + tac2".aspiwack
It works pretty much like "tac1 || tac2" except that it has as successes all the successes of tac1 followed by all the successes of tac2 (whereas the latter has either the successes of tac1 (if there is at least one) or those of tac2 (otherwise)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16998 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Try to remove intermediate allocations when dealing with goal-specific tactics.aspiwack
Introduces a primitive Goal.enter which allows to access the common information needed by goal-specific tactics, avoids a number of monadic binds, and some unnecessary allocations of lists. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16991 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Various rewriting, mostly for speed purposes.aspiwack
- A variant of tclEVARS directly in the language of the monad - A variant of tclDISPATCHGEN (tclINDEPENDENT) hopefully faster in the case there is only one tactic to copy - A better written tclDISPATCHGEN (which may make thing actually a little slower) - A special case in tclDISPATCHGEN and tclINDEPENDENT for the case when they are 0 or 1 goals (adaptation of a patch sent by Pierre-Marie Pédrot) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16990 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fix behaviour of the refine tactic with respect to evars in types.aspiwack
It used not to propagate discovered constraints on the evars of the conclusion of the goal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16987 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Makes the Ltac debugger usable again.aspiwack
This is just a port of the existing design. Basing the tactics on an IO monad may allow to simplify things a bit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16985 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Replaced monads.ml by an essentially equivalent proofview_gen.ml generated ↵aspiwack
by extraction. The goal was to use Coq's partial evaluation capabilities to do manually some inlining that Ocaml couldn't do. It may be critical as we are defining higher order combinators in term of others and no inlining means a lot of unnecessary, short-lived closures built. With this modification we get back some (but not all) of the loss of performance introduced by threading the monadic type all over the place. I still have an estimated 15% longer compilation time for Coq. Makes use of Set Extraction Conservative Types and Set Extraction File Comment to maintain the relationship between the functions and their types. Uses an intermediate layer Proofview_monad between Proofview_gen and Proofview in order to use a hand-written mli to catch potential errors in the generated file (it uses Extract Constant a lot). A bug in the extraction of signatures forces to remove the generated proofview_gen.mli which does not have the correct types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16981 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).aspiwack
They were a hack to avoid looking where exceptions were raised and not caught. Hopefully I produce a cleaner stack now, catching errors when it is needed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16980 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Clean up a warning.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16978 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02The tactic [admit] exits with the "unsafe" status.aspiwack
It is highlighted in yellow in Coqide. The unsafe status is tracked throughout the execution of tactics such that nested calls to admit are caught. Many function (mainly those building constr with tactics such as typeclass related stuff, and Function, and a few other like eauto's use of Hint Extern) drop the unsafe status. This is unfortunate, but a lot of refactoring would be in order. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16977 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 01:43:02 +0000