| Age | Commit message (Collapse) | Author |
|---|
|
This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).
|
|
Impacts MapleMode.
|
|
The prefered style is to use continuation passing style when necessary, or simply passing the goal explicitely in the case of interpretation functions which do not evolve the current goal.
|
|
I'm trying to avoid unecessary construction of intermediate lists. Interpretation function don't modify the goals, they just need a goal in their
context.
Some care has to be given to the evar maps, though, as we can extract an outdated evar map from a goal (this is probably an undesirable feature, but significantly simplified the compatibility API).
Also, Proofview.Goal.enter{,l} catch exceptions (and transfer the non-critical ones into errors of the tactics monad). So I had to do just that for every "enter" removed (I probably have been overprotective but it's better that way).
Not as trivial a modification as it should, but it will hopefully go over well. It was much needed anyway.
|
|
|
|
I use a telescope to represent to goals, and let proofview.ml generate the appropriate existential variables.
|
|
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
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17055 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Noticed in CoRN
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17028 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
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
|
|
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
|
|
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
|
|
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
|
|
[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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
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
|
|
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
|
|
- 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
|
|
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
|
|
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
|
|
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
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16976 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16971 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
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
|
|
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
|
|
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
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
All the purely monadic code has been moved to a new module Monads,
where, I'm afraid to confess, I got to use a number of proof transformers
to modularise the definition of tactics. It is still not easy to understand (why
would it with backtracking support?) but at least it's more robust, cleaner,
and more extensible. Plus there is now a Proofview.tclORELSE which will
be used to interprete the Ltac tactical (t1 || t2).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15596 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15577 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
of a proof into goals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14973 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
the uid returned by Goal.uid.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14467 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14406 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- 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
|
|
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
|
