| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
Ultimately setoid rewrite should be written in the monad to fix it properly.
|
| |
|
|
| |
actually calling the VM at Qed time.
|
| | |
|
| | |
|
| |
|
|
|
| |
Had to put some hook in the handler of Proofview.NoSuchgoals.
Documentation updated. CHANGE updated.
|
| |
|
|
| |
Updated doc, but not tests-suite yet.
|
| |
|
|
|
|
|
|
| |
After commit b46944e the system got way slower, hence the optimization
is relevant also for non polymorphic constants. Putting it back now,
but we shall find something in between: an optimization that does
not clash with async proofs but that gives some performance improvement
over no optimization at all.
|
| |
|
|
|
|
|
| |
As discussed on coqdev, clear is not perfect, Hints for trivial
using cleared section vars are still used.
But it is better than nothing I guess.
|
| | |
|
| |
|
|
|
|
|
|
| |
Given that the proof state contains a callback (a terminator)
that is not sent (dropped by the ephemeron mechanism at marshall
time) de-referencing the ephemeron during this function makes it
impossible to call it in a worker. Now the worker can call the
function and replace the terminator with a good one.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When one generates a .vi file only the type is stocked.
When one completes a .vi the proof term is stocked but the
corresponding type is not changed:
- if one minimizes the constraints of the body, the minimization
could find that 2 univs are equal and substitute one for the
other in the body, but it should also apply the subst to the type
orelse coqchk could fail
- also, a "retroactive" change of a type (making it stricter)
invalidates what was type checked afterwards, so this operation
clashes with the vi2vo compilation chain
Hence we enable this optimization only for universe polymorphic
constants that:
- are the ones that truly requires such optimization
- are never processed asynchronously, so the scenario above does
not apply
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
Fixes the idtac "string" not appearing in proofgeneral because
printined *before* the goal.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
| |
You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
|
| |
|
|
|
|
| |
propagate it. This allows C-zar to continue to work.
Don't know if it is the best way to do it.
|
| |
|
|
|
|
|
|
|
|
| |
The occur check is done even if the flag [unsafe] is set to true. The rational is that a tactic cannot control where it takes pieces of terms from (and hence will not generally make terms which pass the occur-check), and it would be painful to ask every tactic which takes a term as an argument to do an occur check before [refine].
I reused the same error than used by unification. It gives a pretty nice error message. An alternative would be to have a dedicated error with pretty much the same error message. I'm not sure which is best, so I went for the simplest one.
The same check is done in the compatibility layer.
Fixes a reported bug which I cannot locate for some reason.
|
| |
|
| |
Generally, tactics build type-correct terms. A safe refine is hence a waste of time (somtimes a significant one). The safe option is kept for specific purposes such as debugging, or some weird interaction with the pretyper and universes which still seemed to hold last time I checked (used by the user-level refine tactic).
|
| |
|
| |
Just hoisted a definition out of a loop. Not that this part of the code is time critical at all. I just feel it's cleaner.
|
| |
|
| |
Instead of filtering over the goals we have just creating and running through the evar_map, fetching the evar_info (that we've just created), and marking it as unresolvable, the goals are just created unresolvable. Which is probably what I should have done from the beginning, but it had escaped my notice during my code-cleaning session.
|
| |
|
| |
I can't say I condone having unsafe primitives which are not used anywhere. But if they are to be there, let's make sure they don't duplicate code.
|
| |
|
|
|
| |
The function initializing proofviews were marking all evars as non-resolvables
for the proofview, while only goal evars ought to be.
|
| | |
|
| |
|
|
|
| |
When an evar was instantiated it failed to disapear from the shelf. It had the consequence of stopping Qed from happening.
Fixes test-suite/success/apply.v
|
| |
|
| |
Closes #3801.
|
| |
|
|
| |
at least when f is an evaluable reference.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
reference" and "simpl pattern" in the code (maybe we should have
merged them instead, but I finally decided to enforce their
difference, even if some compatibility is to be preversed - the idea
is that at some time "simpl reference" would only call a weak-head
simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n)
rather than S(S(n)) which could be useful for better using induction
hypotheses.
In the process we also implement the following:
- 'simpl "+"' is accepted to reduce all applicative subterms whose
head symbol is written "+" (in the toplevel scope); idem for
vm_compute and native_compute
- 'simpl reference' works even if reference has maximally inserted
implicit arguments (this solves the "simpl fst" incompatibility)
- compatibility of ltac expressions referring to vm_compute and
native_compute with functor application should now work (i.e.
vm_compute and native_compute are now taken into account in
tacsubst.ml)
- for compatibility, "simpl eq" (assuming no maximal implicit args in
eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed.
By the way, is "mul" on nat defined optimally? "3*n" simplifies to
"n+(n+(n+0))". Are there some advantages of this compared to have it
simplified to "n+n+n" (i.e. to "(n+n)+n").
|
| |
|
|
|
|
|
|
| |
- 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?
|
| |
|
|
|
|
|
|
|
| |
Observing that systematic eager evar unification makes unification
works better, for instance in setoid rewrite (ATBR, SemiRing.v), we
add a new flag use_evars_eagerly_in_conv_on_closed_terms which is put
to true only in Rewrite.rewrite_core_unif_flags (empirically, this
makes the "rewrite" from rewrite.ml working again on examples which
were previously treated by use_metas_eagerly_in_conv_on_closed_terms).
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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).
|
| |
|
|
| |
Hence dispatches are printed as dispatches rather than sequences.
|
| |
|
|
| |
Called with [Info n tac], runs [tac] and prints its info trace unfolding [n] level of tactic names ([0] for no unfolding at all).
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The main change is that selection of subterm is made similar whether
the given term is fully applied or not.
- The selection of subterm now works as follows depending on whether
the "at" is given, of whether the subterm is fully applied or not,
and whether there are incompatible subterms matching the pattern. In
particular, we have:
"at" given
| subterm fully applied
| | incompatible subterms
| | |
Y Y - it works like in 8.4
Y N - this was broken in 8.4 ("at" was ineffective and it was finding
all subterms syntactically equal to the first one which matches)
N Y Y it now finds all subterms like the first one which matches
while in 8.4 it used to fail (I hope it is not a too risky in-draft
for a semantics we would regret...) (e.g. "destruct (S _)" on
goal "S x = S y + S x" now selects the two occurrences of "S x"
while it was failing before)
N Y N it works like in 8.4
N N - it works like in 8.4, selecting all subterms like the
first one which matches
- Note that the "historical" semantics, when looking for a subterm, to
select all subterms that syntactically match the first subterm to
match the pattern (looking from left to right) is now internally called
"like first".
- Selection of subterms can now find the type by pattern-matching (useful e.g.
for "induction (nat_rect _ _ _ _)")
- A version of Unification.w_unify w/o any conversion is used for
finding the subterm: it could be easily replaced by an other
matching algorithm.
In particular, "destruct H" now works on a goal such as "H:True -> x<=y |- P y".
Secondary change is in the interpretation of terms with existential
variables:
- When several arguments are given, interpretation is delayed at the
time of execution
- Because we aim at eventually accepting "edestruct c" with unresolved
holes in c, we need the sigma obtained from c to be an extension of
the sigma of the tactics, while before, we just type-checked c
independently of the sigma of the tactic
- Finishing the resolution of evars (using type classes, candidates,
pending conversion problems) is made slightly cleaner: it now takes
three states: a term is evaluated in state sigma, leading to state
sigma' >= sigma, with evars finally solved in state sigma'' >=
sigma'; we solve evars in the diff of sigma' and sigma and report
the solution in sigma''
- We however renounce to give now a success semantics to "edestruct c"
when "c" has unresolved holes, waiting instead for a decision on
what to do in the case of a similar eapply (see mail to coqdev).
An auxiliary change is that an "in" clause can be attached to each component
of a "destruct t, u, v", etc.
Incidentally, make_abstraction does not do evar resolution itself any longer.
|
| | |
|
| |
|
|
|
|
| |
an updated evar_map, as pattern is working up to universe equalities
that must be kept. Straightforward adaptation of the code depending on
this.
|
| |
|
| |
Otherwise I risked catching errors from the argument functions when I wanted to catch size mismatch to add information to errors.
|
Pierre-Marie Pédrot
Maxime Dénès
Hugo Herbelin
Pierre Courtieu
Enrico Tassi
Arnaud Spiwack
Pierre Boutillier
Matthieu Sozeau