aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-02Documentation for the backtracking features.aspiwack
This required some reorganisation of the documentation of existing tacticals. I hope the result is consistent. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17029 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-02Fix congruence: normalise hypotheses with respect to evars.aspiwack
Detected in CompCert. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17026 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Add primitives in Goal.V82 to access the goal in nf_evar'd form.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17025 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02push_rel_context: do not rename section variables.aspiwack
Renaming section variables is incorrect. And interacts badly with Hints and Canonical Structures in sections. (bug noticed in ssreflect) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17024 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-02Fix compilation of pattern matching wrt variables: alias.aspiwack
Aliases (as clause) are a bit tricky. In Goal True, refine match 0 with | S n as p => _ | _ => I end Must produce the goal n:nat, p := S n : nat |- True However, in the deep branches: refine match 0 with | S (S n as p) => _ | _ => I end The alias is used to give a name to the variable of the first S : p:nat, n:nat |- True Before this patch, the goal would be p:nat, n:nat, p:=p : nat |- True Alias was used both to name the variable of the first S and to alias it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17022 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Restore Zsqrt compat now that refine works fine with match.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17021 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fix the compilation of pattern matching wrt to variables.aspiwack
Compilation of pattern-matching used to systematically introduce a dummy alias x:=x in the typing environment for each variable x in the patterns (except for purely variable patterns which correctly alias the term being matched). This interfered badly with the new refine implementation. To correct this I changed the "all variables" case of pattern-matching compilation to check whether the term currently being matched is a term introduced by the user or a subterm which is necessarily a variable. In the latter case, no alias is introduced. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17020 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-02Corrects a bug on Proofview.Goal.enter whereby sigmas were captured and used ↵aspiwack
at the wrong time. The bug was masked by the fact that Tacinterp uses many superfluous Proofview.Goal.enter, it so happens that the tactic Proofview.Goal.enter (fun _ -> Proofview.Goal.enter fun gl -> t)) had the correct semantics! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17014 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-02bootstrap/Monad.v: implements the writer monad in continuation passing style.aspiwack
Benefits: fewer pair constructed/destructed especially in split. Potential costs: plus and zero now have closures with 11 arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17012 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02bootstrap/Monad.v: implements the environment monad in continuation passing ↵aspiwack
style. Benefits: the underlying monads are not referenced in the "current" primitive. Potential costs: some extracted functions now have 9 arguments, Ocaml may not be good at handling these. The split primitive, which is called often, now builds one extra closure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17011 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Factors the lifting of environment and writer monads in bootstrap/Monad.vaspiwack
Takes a few extra lines but is probably more robust to future changes. Doesn't change the extracted code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17010 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-02Normalise goals with respect to evars in the new tactics.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17008 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-02A dedicated view type for Proofview_gen.split.aspiwack
It doesn't seem to affect performances. But the generated code is slightly cleaner. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17005 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-02A better version of Goal.advance.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16999 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-02Typos in a comment.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16997 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02bootstrap/Monads.v: A more efficient split.aspiwack
Exchanges a IO.bind for a Logic.bind. The latter is better inlined. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16996 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02State monad implemented in CPS.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16995 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02A more principled split.aspiwack
Instead of interleaving the reifications and reflection steps, split is defined as a series of reification followed by a series of reflection. The immediate consequence is that split is hoisted out of the Logic interface, and defined in a single block at the end of the file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16994 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Set an extraction flag for inling let-s in Monad.v.aspiwack
Reduces the size of split significantly. In particular it now uses only 2 matches instead of 4. Patch by Pierre-Marie Pédrot and Pierre Letouzey. Signed-off-by: Arnaud Spiwack <arnaud@spiwack.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16993 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02More optimisations of partial applications.aspiwack
This time in Goal. Patch by Pierre-Marie Pédrot. Signed-off-by: Arnaud Spiwack <arnaud@spiwack.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16992 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-02Optimisation of partial applications in the tactic monad.aspiwack
Explanations here: https://ocaml.janestreet.com/?q=node/30 Patch by Pierre-Marie Pédrot, with modifications from Arnaud Spiwack. Signed-off-by: Arnaud Spiwack <arnaud@spiwack.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16989 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fixes parsing of all: followed by a typechecking/evaluation command.aspiwack
Exceptions raised during parsing are caught by the parser and result in weird parsing behaviour. Instead I added a special case in vernac_expr which always raises an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16988 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-02Small syntax fix to be compatible with Ocaml 3.11.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16986 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-02Document "all:" and "Set Default Goal Selector".aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16984 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02New option Default Goal Selector.aspiwack
Set Default Goal Selector "all" prefixes all tactics with "all:" if no selector is specified (it is overridden by 1: for instance). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16983 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds a new goal selector "all:".aspiwack
all:tac applies tac to all the focused subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16982 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 20:37:06 +0000