aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Collapse)AuthorAge
* Useless computation in Goal handle augmentation.Gravatar ppedrot2013-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17083 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not print tactic notation names at each interpretation step.Gravatar ppedrot2013-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17082 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial applications in Goal.Gravatar ppedrot2013-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17074 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rewriting the proof monad mechanism. Now it uses pure OCaml code, withoutGravatar ppedrot2013-11-07
| | | | | | | | | | | | | going through a Coq extraction phase. We use second order quantification through OCaml records, which allows for a very precise use of low-level application. This results in quite a remarkable speedup but there is still room for improvement. This code was written by translating straightforwardly the Coq generated code in a human-readable dialect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17068 85f007b7-540e-0410-9357-904b9bb8a0f7
* Less partial applications in Vars, as well as better memory allocation.Gravatar ppedrot2013-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17065 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reducing allocation in tclDISPATCHGEN, by doing a List.map at the same timeGravatar ppedrot2013-11-05
| | | | | | the argument list is consumed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17062 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was ↵Gravatar aspiwack2013-11-04
| | | | | | | | | | 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
* Fix the tactical ; [ … ] : the "incorrect number of goal" error was not ↵Gravatar aspiwack2013-11-04
| | | | | | | | | | 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
* 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
* A try/with was catching every exception.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17034 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
* Doc: solve the bad interaction between Declare Implicit Tactic and refine.Gravatar aspiwack2013-11-02
| | | | | | 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
* Fix destruct: nf_evar prior to tactic interpretation.Gravatar aspiwack2013-11-02
| | | | | | Noticed in CoRN git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17028 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add primitives in Goal.V82 to access the goal in nf_evar'd form.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17025 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
* A tactic shelve_unifiable.Gravatar aspiwack2013-11-02
| | | | | | | | | | | | | 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
* Corrects a bug on Proofview.Goal.enter whereby sigmas were captured and used ↵Gravatar aspiwack2013-11-02
| | | | | | | | | | 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
* 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
* bootstrap/Monad.v: implements the writer monad in continuation passing style.Gravatar aspiwack2013-11-02
| | | | | | | 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
* bootstrap/Monad.v: implements the environment monad in continuation passing ↵Gravatar aspiwack2013-11-02
| | | | | | | | | 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
* Adds an experimental exactly_once tactical.Gravatar aspiwack2013-11-02
| | | | | | | | | | 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
* Normalise goals with respect to evars in the new tactics.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17008 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made Proofview.Goal.hyps a named_context.Gravatar aspiwack2013-11-02
| | | | | | 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
* A dedicated view type for Proofview_gen.split.Gravatar aspiwack2013-11-02
| | | | | | 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
* Adds a tactical once.Gravatar aspiwack2013-11-02
| | | | | | [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
* Less use of the list-based interface for goal-bound tactics.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17002 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tachmach.New is now in Proofview.Goal.enter style.Gravatar aspiwack2013-11-02
| | | | | | 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
* More Proofview.Goal.enter.Gravatar aspiwack2013-11-02
| | | | | | | | | | 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
* A better version of Goal.advance.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16999 85f007b7-540e-0410-9357-904b9bb8a0f7
* bootstrap/Monads.v: A more efficient split.Gravatar aspiwack2013-11-02
| | | | | | 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
* State monad implemented in CPS.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16995 85f007b7-540e-0410-9357-904b9bb8a0f7
* A more principled split.Gravatar aspiwack2013-11-02
| | | | | | | | 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
* Set an extraction flag for inling let-s in Monad.v.Gravatar aspiwack2013-11-02
| | | | | | | | | | 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
* More optimisations of partial applications.Gravatar aspiwack2013-11-02
| | | | | | | | | | 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
* Try to remove intermediate allocations when dealing with goal-specific tactics.Gravatar aspiwack2013-11-02
| | | | | | 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
* Various rewriting, mostly for speed purposes.Gravatar aspiwack2013-11-02
| | | | | | | | | - 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
* Optimisation of partial applications in the tactic monad.Gravatar aspiwack2013-11-02
| | | | | | | | | | 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
* Makes the Ltac debugger usable again.Gravatar aspiwack2013-11-02
| | | | | | | 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
* New option Default Goal Selector.Gravatar aspiwack2013-11-02
| | | | | | | 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
* Adds a new goal selector "all:".Gravatar aspiwack2013-11-02
| | | | | | 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
* Replaced monads.ml by an essentially equivalent proofview_gen.ml generated ↵Gravatar aspiwack2013-11-02
| | | | | | | | | | | | | | | | | | | | | | | | 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
* Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).Gravatar aspiwack2013-11-02
| | | | | | | | 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
* 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
* Cleanup of comments.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16976 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small change to the IO monad interface: [val ref : 'a -> 'a ref t]Gravatar aspiwack2013-11-02
| | | | | | | | It doesn't matter much, it's simply a matter of aesthetic, so that all functions in the interface of [Monads.IO] are pure ([IO.run] being the only impure function but it's not part of the generic interface). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16974 85f007b7-540e-0410-9357-904b9bb8a0f7
* A whole new implemenation of the refine tactic.Gravatar aspiwack2013-11-02
| | | | | | | | | | | It now uses the same algorithm as pretyping does. This produces pretty weird goal when refining pattern matching terms. Modification of the pattern matching compilation algorithm are pending, hence I will let it be so for now. The file Zsqrt_compat.v has two temporary [Admitted] related to this issue. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16973 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bases tactics on an IO monad.Gravatar aspiwack2013-11-02
| | | | | | | | | It allowed to restore the timeout tactics. It also prepares for the debugging mechanism to be restored. ['a IO.t] is just [unit -> 'a]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16970 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
* Uses Proofview.tclEXTEND more sparingly.Gravatar aspiwack2013-11-02
| | | | | | | It is used where failures can be caughts (tclORELSE, tclTRY, …) rather than at each tclTHEN. Hopefully avoiding making things a bit less slow. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16968 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 08:58:36 +0000