aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Collapse)AuthorAge
* 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
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On the compilation of Coq, we can see an increase of ~20% compile time on my completely non-scientific tests. Hopefully this can be fixed. There are a lot of low hanging fruits, but this is an iso-functionality commit. With a few exceptions which were not necessary for the compilation of the theories: - The declarative mode is not yet ported - The timeout tactical is currently deactivated because it needs some subtle I/O. The framework is ready to handle it, but I haven't done it yet. - For much the same reason, the ltac debugger is unplugged. It will be more difficult, but will eventually be back. A few comments: I occasionnally used a coercion from [unit Proofview.tactic] to the old [Prooftype.tactic]. It should work smoothely, but loses any backtracking information: the coerced tactics has at most one success. - It is used in autorewrite (it shouldn't be a problem there). Autorewrite's code is fairly old and tricky - It is used in eauto, mostly for "Hint Extern". It may be an issue as time goes as we might want to have various success in a "Hint Extern". But it would require a heavy port of eauto.ml4 - It is used in typeclass eauto, but with a little help from Matthieu, it should be easy to port the whole thing to the new tactic engine, actually simplifying the code. - It is used in fourier. I believe it to be inocuous. - It is used in firstorder and congruence. I think it's ok. Their code is somewhat intricate and I'm not sure they would be easy to actually port. - It is used heavily in Function. And honestly, I have no idea whether it can do harm or not. Updates: (11 June 2013) Pierre-Marie Pédrot contributed the rebase over his new stream based architecture for Ltac matching (r16533), which avoid painfully and expensively working around the exception-throwing control flow of the previous API. (11 October 2013) Rebasing over recent commits (somewhere in r16721-r16730) rendered a major bug in my implementation of Tacticals.New.tclREPEAT_MAIN apparent. It caused Field_theory.v to loop. The bug made rewrite !lemma, rewrite ?lemma and autorewrite incorrect (tclREPEAT_MAIN was essentially tclREPEAT, causing rewrites to be tried in the side-conditions of conditional rewrites as well). The new implementation makes Coq faster, but it is pretty much impossible to tell if it is significant at all. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16967 85f007b7-540e-0410-9357-904b9bb8a0f7
* Future: better doc + restore ~pure optimizationGravatar gareuselesinge2013-10-31
| | | | | | | | | | | This optimization was undone because the kernel type checking was not a pure functions (it was accessing the conv_oracle state imperatively). Now that the conv_oracle state is part of env, the optimization can be restored. This was the cause of the increase in memory consumption, since it was forcing to keep a copy of the system state for every proof, even the ones that are not delayed/delegated to slaves. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16963 85f007b7-540e-0410-9357-904b9bb8a0f7
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
| | | | | | But for vm, the kernel should be functional now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not generate useless argument arrays in whd_* functions.Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16954 85f007b7-540e-0410-9357-904b9bb8a0f7
* Useless array to list conversions in proof/logic.ml.Gravatar ppedrot2013-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16941 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstracting evar filter away. The API is not perfect, but better than nothing.Gravatar ppedrot2013-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16939 85f007b7-540e-0410-9357-904b9bb8a0f7
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
| | | | | | | | | | | To reduce the amount of syntactic noise, we now provide a few inner modules Int.List, Id.List, String.List, Sorts.List which contain some monomorphic (or semi-monomorphic) functions such as mem, assoc, ... NB: for Int.List.mem and co we reuse List.memq and so on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
* cList: a few alternative to hashtbl-based uniquize, distinct, subsetGravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
* proof modes: use ephemerons to represent them in proof stateGravatar gareuselesinge2013-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16895 85f007b7-540e-0410-9357-904b9bb8a0f7
* declaration_hooks use EphemeronGravatar gareuselesinge2013-10-18
| | | | | | | | Ideally, any component of the global state that is a function or any other unmarshallable data should be stocked as an ephemeron to make the state always marshallable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16893 85f007b7-540e-0410-9357-904b9bb8a0f7
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
| | | | | | | | | | | | | | | | A future always carries a fix_exn with it: a function that enriches an exception with the state in which the error occurs and also a safe state close to it where one could backtrack. A future can be in two states: Ongoing or Finished. The latter state is obtained by Future.join and after that the future can be safely marshalled. An Ongoing future can be marshalled, but its value is lost. This makes it possible to send the environment to a slave process without pre-processing it to drop all unfinished proofs (they are dropped automatically in some sense). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing dubious use of evarmap manipulating functions in printingGravatar ppedrot2013-10-05
| | | | | | related code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16851 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
* Removing useless evar-related stuff.Gravatar ppedrot2013-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16803 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 22:43:24 +0000