| Age | Commit message (Collapse) | Author |
|---|
|
This tactical is inspired by discussions on the Coq-club list. For now
it is still undocumented, and there is room left for design issues.
|
|
Side effects are now an opaque data type, called private_constant, you can
only obtain from safe_typing. When add_constant is called on a
definition_entry that contains private constants, they are either
- inlined in the main proof term but not re-checked
- declared globally without re-checking them
As a safety measure, the opaque data type contains a pointer to the
revstruct (an internal field of safe_env that changes every time a new
constant is added), and such pointer is compared with the current value
store in safe_env when the private_constant is inlined. Only when the
comparison is successful the private_constant is not re-checked. Otherwise
else it is. In short, we accept into the kernel private constant only
when they arrive in the very same order and on top of the very same env
they arrived when we fist checked them.
Note: private_constants produced by workers never pass the safety
measure (the revstruct pointer is an Ephemeron). Sending back the
entire revstruct is possible but: 1. we lack a way to quickly compare
two revstructs, 2. it can be large.
|
|
|
|
|
|
Had to put some hook in the handler of Proofview.NoSuchgoals.
Documentation updated. CHANGE updated.
|
|
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
|
|
for typeclasses.
This was not the case for goals created at the end of the tactic by salvaging the [future_goals] from the evar map. It would cause typeclass resolution to try and solve these goals (if they have a class type) at each subsequent tactic.
Fixes #3841.
|
|
propagate it. This allows C-zar to continue to work.
Don't know if it is the best way to do it.
|
|
|
|
- drops all Defined entries from the evar map (applying the subst to the
initial evar and the undefined evars types).
- call Gc.compact
Now the question is: where should these two commands be documented?
|
|
|
|
The name is chosen in accordance to Ltac's syntax. In particular [refine] prints as Ltac's refine, which is not entirely correct (Ltac's refine does some βι-reduction after refinement). Maybe it would be better to give make it clear that it is a different refine. Still in refine, the constr is printed without taking into account the new evars, which, apart from potentially getting the order of the goals wrong, prints new evars as ?x instead of ?[x]. A printer for terms with new evars will be necessary.
In the case of [V82.tactic], the name is just <unknown> because there is no way to retrieve any information. It won't appear in the first level of info in Ltac, however, if the user would require a deeper trace, he may see internal tactics (Tactics defined with TACTIC EXTEND also have weird, unparsable, internal names).
|
|
Called with [Info n tac], runs [tac] and prints its info trace unfolding [n] level of tactic names ([0] for no unfolding at all).
|
|
|
|
of a break.
|
|
|
|
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.
|
|
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.
|
|
It is, after all, a generic function about lists.
|
|
|
|
|
|
The Unsafe module is for unsafe tactics which cannot be done without anytime soon. Whereas V82 indicates a function which we want to get rid of and that shouldn't be used in a new function.
|
|
|
|
|
|
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.
|
|
Uses the new architecture which allows to keep track of all new evars. The [future_goals] are flushed at the end of the tactics, the [principal_future_goal] is ignored.
|
|
|
|
|
|
Now, usual function from Evarutil are used to define evars instead of the variants from Proofview.Refine.
The [update] primitive which tried to patch the difference between pretyping functions and the refine primitive is now replaced by the identity function.
|
|
another one.
|
|
Refine.
|
|
Not very optimized though (if we apply convert_hyp on any hyp, a new
evar will be generated for every different hyp...).
|
|
|
|
Most of the code from Goal.Refine and related was moved to the one
file that was using it, wiz. tactics.ml. Some additional care should
be taken to clean up even more the remaining code.
|
|
|
|
Goals have to be refreshed when observed, because the evarmap may have
changed between the moment where the goal was generated and the moment the
goal is used.
|
|
All goals were normalised up front, rather than normalised after the tactic acting on previous goal had the chance to solve some evars, which then appeared non-instantiated to tactics which do not work up to evar map (most of them).
|
|
for tclEVARS which might solve existing goals.
|
|
|
|
|
|
|
|
|
|
1. Proofview.Goal.enter into Proofview.Goal.nf_enter.
2. Proofview.Goal.raw_enter into Proofview.Goal.enter.
3. Proofview.Goal.goals -> Proofview.Goals.nf_goals
4. Proofview.Goal.raw_goals -> Proofview.Goals.goals
5. Ftactic.goals -> Ftactic.nf_goals
6. Ftactic.raw_goals -> Ftactic.goals
This is more uniform with the other functions of Coq.
|
|
This time it should work at least as well as the previous version. The error
messages were adapted a little. There is still a buggy behaviour when clearing
lets in section, but this is mostly a problem of section handling. The v8.4
version of clearbody did exhibit the same behaviour anyway.
|
|
In order not to be too costly, there is an [unsafe] flag to be set if the
tactic does not have to check that the partial proof term is well-typed (to
be used with caution though).
This patch breaks one [fix]-based example in the refine test-suite, but a huge
development like CompCert still goes through.
|
|
Hopefully, this may fix some nasty bugs lying around.
|
|
This reverts commit 664b3cba1e8d326382ca981aa49fdf00edd429e6.
Conflicts:
proofs/proofview.ml
|
|
|
|
|
|
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
|
