aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview_monad.mli
Commit message (Collapse)AuthorAge
* Moving Proofview_monad to the engine/ folder.Gravatar Pierre-Marie Pédrot2015-02-28
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Info: do not record info trace unless needed.Gravatar Arnaud Spiwack2014-11-01
|
* An API for info traces.Gravatar Arnaud Spiwack2014-11-01
|
* Split [Proofview] into a file where the basic operations on the state are ↵Gravatar Arnaud Spiwack2014-10-22
| | | | | | defined and the file providing the primitives. The datatypes are defined in [Proofview_monad], previous [Proofview_monad] is now called [Logic_monad] since it is more generic since the refactoring.
* Make names in [Proofview_monad] more uniform.Gravatar Arnaud Spiwack2014-10-22
| | | | ret -> return, bind -> (>>=), etc… So that monads expose a [Monad.S] signature. Also Proofview now exposes the [Monad.S] signature directly rather than in a [Monad.S] subdirectory.
* Refactoring proofview: make the definition of the logic monad polymorphic.Gravatar Arnaud Spiwack2014-10-16
| | | | | | Makes the monad more flexible as it will be easier to add new components to the concrete state of the tactic monad. The Proofview module is also organised in a more abstract way with dedicated submodules to access various parts of the state or writer.
* Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Gravatar Pierre-Marie Pédrot2014-09-04
| | | | Hopefully, this may fix some nasty bugs lying around.
* Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."Gravatar Pierre-Marie Pédrot2014-09-04
| | | | | | | This reverts commit 664b3cba1e8d326382ca981aa49fdf00edd429e6. Conflicts: proofs/proofview.ml
* Adding a [make] primitive to the NonLogical monad.Gravatar Pierre-Marie Pédrot2014-08-05
|
* Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].Gravatar Arnaud Spiwack2014-08-05
| | | | | When "entering" in a goal, the environment observed by [tclENV] is changed (in the scope of the goal) to be that of the goal. I'm not entirely sure it is the right semantics. But it allows to write tactics which are agnostic of whether they are run in a goal or not.
* Some comments in the interface of Proofview_monad.Gravatar Arnaud Spiwack2014-08-04
|
* Cleaning of the new implementation of the tactic monad.Gravatar Arnaud Spiwack2014-08-04
| | | | | | | | | * 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
* Adding a tclBREAK primitive to the tactic monad.Gravatar Pierre-Marie Pédrot2014-07-28
|
* Adding a tail-rec tclONCE.Gravatar Pierre-Marie Pédrot2014-07-24
|
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
| | | | This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
* time tacGravatar Hugo Herbelin2014-07-07
|
* Adding a [map] primitive to the tactic monad. Hopefully this should beGravatar Pierre-Marie Pédrot2014-04-20
| | | | slightly more efficient in general.
* 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.
* Adding an [modify] function to the tactic monad. It allows to modifyGravatar Pierre-Marie Pédrot2014-04-06
| | | | the current state without having to use both get, bind and set.
* 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
* 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
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 04:52:39 +0000