aboutsummaryrefslogtreecommitdiff
path: root/bootstrap/Monads.v
AgeCommit message (Collapse)Author
2014-08-04Cleaning of the new implementation of the tactic monad.Arnaud Spiwack
* Add comments in the code (mostly imported from Monad.v) * Inline duplicated module * Clean up some artifacts due to the extracted code. * [NonLogical.new_ref] -> [NonLogical.ref] (I don't even remember why I chose this name originally) * Remove the now superfluous [Proof_errors] module (which was used to define exceptions to be used in the extracted code). * Remove Monad.v
2014-07-15Using the generic timeout function in the boostrapped file.Pierre-Marie Pédrot
2014-04-20Adding a [map] primitive to the tactic monad. Hopefully this should bePierre-Marie Pédrot
slightly more efficient in general.
2014-04-07Transfering the initial goals from the proofview to the proof object.Pierre-Marie Pédrot
They were just passed along in the tactics.
2014-04-06Adding an [modify] function to the tactic monad. It allows to modifyPierre-Marie Pédrot
the current state without having to use both get, bind and set.
2014-02-02Fixing backtrace reporting.Pierre-Marie Pédrot
2014-01-30Fixing backtrace handling here and there.Pierre-Marie Pédrot
2013-11-02Cleanup of comments in bootstrap/Monads.vaspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17031 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-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-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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 17:33:00 +0000