aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof.ml
Commit message (Collapse)AuthorAge
* Small reorganisation in proof.ml.Gravatar Arnaud Spiwack2014-07-25
|
* Fail gracefully when focusing on non-existing goals with user commands.Gravatar Arnaud Spiwack2014-07-25
| | | Fixes bug #3457
* Proof_global.start_dependent_proof: properly threads the sigma through the ↵Gravatar Arnaud Spiwack2014-07-23
| | | | | telescope. Allows for a more refined notion of dependently generated initial goals.
* Transfering the initial goals from the proofview to the proof object.Gravatar Pierre-Marie Pédrot2014-04-07
| | | | They were just passed along in the tactics.
* Fixing backtrace registering of various tactic-related try-with blocks.Gravatar Pierre-Marie Pédrot2013-12-11
|
* Allow proofs to start with dependent goals.Gravatar Arnaud Spiwack2013-12-04
| | | I use a telescope to represent to goals, and let proofview.ml generate the appropriate existential variables.
* Allowing proofs starting with a non-empty evarmap.Gravatar ppedrot2013-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17055 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update comments.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds a tactic give_up.Gravatar aspiwack2013-11-02
| | | | | | 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
* Adds a shelve tactic.Gravatar aspiwack2013-11-02
| | | | | | 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
* The tactic [admit] exits with the "unsafe" status.Gravatar aspiwack2013-11-02
| | | | | | | | | | | | | 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
* Getting rid of Goal.here, and all the related exceptions and combinators.Gravatar aspiwack2013-11-02
| | | | | | It was a bad idea. The new API based on lists seems more sensible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16969 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
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
* get rid of closures in global/proof stateGravatar gareuselesinge2013-08-08
| | | | | | | | In some cases, an 'a -> 'b field is changed into an ('a -> b') option field so that one can forget the closures and marshal the resulting state git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16683 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
* another Errors.push in a exception reraiseGravatar letouzey2013-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16307 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16288 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monomorphization (proof)Gravatar ppedrot2012-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16002 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the unused "intel" field in Proof.proof_stateGravatar letouzey2012-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15846 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 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
* Change how the number of open goals is printed.Gravatar aspiwack2012-07-04
| | | | | | | | | | If you are focused on 3 subgoals, and unfocusing would reveal 2 extra subgoals, and unfocusing again would reveal 4 extra subgoals, then coqtop will tell you: 3 focused subgoals (unfocused: 2-4) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15508 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a command "Unfocused" which returns an error when the proof isGravatar aspiwack2012-03-30
| | | | | | not fully unfocused (in the style of the Guarded command). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15104 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arranged for the desirable behaviour that bullets do not see beyond braces.Gravatar aspiwack2012-03-20
| | | | | | | | | | | i.e.: after a brace is open, one can use the bullets again without clashing with bullets outside the brace. In particular, one can nest bullets with arbitrary depth (by interleaving them with occasional braces). Also fixed a typo introduced in my previous commit which caused bullets and braces to behave just like regular focuses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15073 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
* Corrects the erroneous error message when trying to unfocus a fullyGravatar aspiwack2012-03-01
| | | | | | unfocused proof (part of bug #2671). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15011 85f007b7-540e-0410-9357-904b9bb8a0f7
* Additional comment on Focus Conditions.Gravatar aspiwack2012-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14975 85f007b7-540e-0410-9357-904b9bb8a0f7
* A "Grab Existential Variables" to transform the unresolved evars at the end ↵Gravatar aspiwack2012-02-07
| | | | | | of a proof into goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14973 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in comments.Gravatar aspiwack2012-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proof using ...Gravatar gareuselesinge2011-12-12
| | | | | | | | | | | | | New vernacular "Proof using idlist" to declare the variables to be discharged at the end of the current proof. The system checks that the set of declared variables is a superset of the set of actually used variables. It can be combined in a single line with "Proof with": Proof with .. using .. Proof using .. with .. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
* In emacs mode, prints a list of the dependent existential variables introducedGravatar aspiwack2011-11-23
| | | | | | | | during the proof together with information whether they were (partially) instantiated and if it's the case the list of existential variables that were used to that effect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14721 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using ↵Gravatar aspiwack2011-09-12
| | | | | | the uid returned by Goal.uid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14467 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes mini-bug: Qed would succeed even on focused proofs.Gravatar aspiwack2011-08-12
| | | | | | It allowed proofs of the Shape [{ solve. Qed.] which is inelegant at best. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14409 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bullets so that they would play well with { }.Gravatar aspiwack2011-07-06
| | | | | | | | | | | | | | | | | | We can now have script like assert P. { destruct n. - solve_case1. - solve_case2. } solve_goal However there is an undesirable interaction with Focus (which we might, anyway, consider deprecated in favour of {}). Indeed, for compatibility with v8.3, Unfocus is called implicitely after each proof command if there is no focused goal. And the new behaviour of bullets is to allow arbitrary unfocusing command "pass trough" them. As a result, a script like Focus. split - solves_first_goal will result in a fully unfocused proof. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14262 85f007b7-540e-0410-9357-904b9bb8a0f7
* The modules in proofs now use the Errors module to explain their exceptions ↵Gravatar aspiwack2011-05-13
| | | | | | to the toplevel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14120 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug causing inconsistent states during proof editting.Gravatar aspiwack2011-04-29
| | | | | | | | | Some toplevel commands (for instance the experimental bullets) are composed of several atomic commands, the failure of one must imply the failure of the whole toplevel command. This commit introduces a system of transaction to that effect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14087 85f007b7-540e-0410-9357-904b9bb8a0f7
* Started to fix the declarative proof mode (C-zar).Gravatar aspiwack2011-02-10
| | | | | | | Everything seems to work fine in CoqIDE (except escape/return and the daimon which are not entirely ported). However, there is some problem causing proof general to fail when using goto or evaluate buffer (evaluate next phrase works fine though), as well as coqc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13817 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
* Typo in comment of proof.mlGravatar herbelin2010-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13037 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
| | | | | | | | | | | | | evar_map into a map for defined evars and a map for undefined evars. Even before Spiwack's new proof engine, some Evd.fold were very costly, e.g. in check_evars or progress_evar_map. With the new proof engine, undefined evars traversals are apparently even more common (at least, it improves significantly the complexity of some calls to omega in JordanCurveTheorem - a new factor 5-7 after the factor 5-6 obtained by removal of evar_merge in clenv_fchain in commit 13007, arriving to figures comparable to the 8.3 ones). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13011 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
* Enlevé les trucs commités au mauvais endroitGravatar aspiwack2007-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10252 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques structures de donnée plus les modules principaux (et Gravatar aspiwack2007-10-23
parfaitement en cours) de la nouvelle machinerie de preuves. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10251 85f007b7-540e-0410-9357-904b9bb8a0f7