| Age | Commit message (Collapse) | Author |
|---|
|
Disclaimer: I have no idea what I am doing.
|
|
When encountering a "simpl nomatch" constant, the reduction machinery tries
to unfold it. If the subsequent partial reduction does not produce any
match construct, it keeps going from the reduced term. Unfortunately, the
reduced term has been refolded in the meantime, which means that some of
the previous reduction steps have been canceled, thus causing an infinite
loop. This patch delays the refolding till the very end, so that reduction
always progresses.
Disclaimer: I have no idea what I am doing here. The patch compiles the
standard library and the test suite properly, so hopefully they contain
enough tests to exercise the reduction machinery.
|
|
As noticed by Cyprien Mangin, projected terms cannot directly be used as
head values. Indeed, they might be applications (e.g. constructors as in
the bug report) whose arguments would thus be missing from the evaluation
stack when doing any iota-reduction step.
The only case where it would make sense is when the evaluation stack is
empty, as an optimization. Indeed, in that case, the arguments are put on
the stack, and then immediately put back inside the term.
|
|
build a default case if the pattern is irrefutable. It did not matter
in practice because we did not check for unused clauses in this case.
|
|
while eta-expanding a notation) + a more serious variant of it
(alpha-conversion incorrect wrt eta-expansion).
|
|
It was not accounting for the universe constraints generated by
applications of the coercion.
|
|
The regression was introduced by efa1c32a4d178, which replaced
unification by conversion when looking for more occurrences of a
subterm. The conversion function called was not the right one, as it
was not inferring constraints.
|
|
Due to a change in pretyping, using cast annotations as typing
constraints, the canonical structure problems given to the unification
could contain non-evar-normalized terms, hence we force
evar normalization where necessary to ensure the same CS solutions
can be found. Here the dependency test is fooled by an erasable
dependency, and the following resolution needs a independent codomain
for pop b to be well-scoped.
|
|
|
|
E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive
records with eta for which conversion is incomplete.
- Eta-conversion only applies to BiFinite inductives
- Finiteness information is now checked by the kernel (the constructor types
must be strictly non recursive for BiFinite declarations).
|
|
Try first to find a keyed subterm without conversion/betaiota on open
terms (that is the usual strategy of rewrite), if this fails, try with full
conversion, incuding betaiota. This makes the test-suite pass again,
retaining efficiency in the most common cases.
|
|
projections in unification.ml
|
|
The current solution may not be totally ideal though. We generate names for
anonymous evars on the fly at printing time, based on the Evar_kind data they
are wearing. This means in particular that the printed name of an anonymous
evar may change in the future because some unrelate evar has been solved or
introduced.
|
|
|
|
|
|
This patch was proposed by JH in bug report #4547.
|
|
The performance enhancement introduced by a895b2c0 for non-polymorphic hints
was actually causing a huge regression in the polymorphic case (and was marked
as such). We fix this by only substituting the metas from the evarmap instead
of the whole evarmap.
|
|
|
|
(let x := t in u) a that should be reduced. Maybe a different
decomposition/reduction primitive should be used instead.
|
|
|
|
evars were created making in turn that evars formerly recognized as
pending were not anymore in the list of pending evars). This also
fixes the reopening of #3848.
See comments on #4484 for details.
|
|
constant and arguments _separately_.
|
|
[rewrite] was calling find_suterm using the wrong unification flags, not
allowing full delta in unification of terms with the right keys as desired.
|
|
The rewrite tactic was causing an evar leak because of the use of the
Evd.remove primitive. This function did not modify the future goals of
the evarmap to remove the considered evar and thus maintained dangling
evars in there, causing the anomaly.
|
|
|
|
same evar.
|
|
projections (off by default).
|
|
Prop levels.
As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.
|
|
This was not a typo (was correctly taking the family type of the type).
|
|
|
|
parameters of an inductive type.
|
|
|
|
Was exploitable in 8.3, 8.4 and 8.5beta1. A priori not exploitable in
8.5beta2 and 8.5beta3 from a Coq file because typing done while
compiling "match" would serve as a protection. However exploitable by
calling the kernel directly, e.g. from a plugin (but a plugin can
anyway do what it wants by bypassing kernel type abstraction).
Fixing similar error in pretyping.
|
|
constr, and the associated signature, not needed anymore.
Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
|
|
The clenv_fchain function was needlessly merging universes coming from
two evarmaps even though one was an extension of the other. A flag was
added so that the tactic just retrieves the newer universes.
|
|
unification (not necessarily preserved due to the fo approximation rule).
|
|
only one disjoint component of the typeclasses instances to resolve.
|
|
their type annotation.
|
|
|
|
whd_evar in refresh_universes.
|
|
|
|
When refreshing a type variable, always use a rigid universe to force the most
general universe constraint, as in 8.4.
|
|
|
|
make them rigid to disallow minimization.
|
|
universes are declared correctly in the enclosing proofs evar_map's.
|
|
Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
|
|
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.
|
|
Universe instances for constructors were not always correct, for instance in:
[cons _ list (nil _)] with a polymorphic [list] type, [nil] was receiving an
empty instance.
|
|
- Universes are now represented in the VM by a structured constant containing the
global levels. This constant is applied to local level variables if any.
- When reading back a universe, we perform the union of these levels and return
a [Vsort].
- Fixed a bug: structured constants could contain local universe variables in
constructor arguments, which has to be prevented.
Was showing up for instance when evaluating [cons _ list (nil _)] with
a polymorphic [list] type.
- Fixed a bug: polymorphic inductive types can have an empty stack.
Was showing up when evaluating [bool] with a polymorphic [bool] type.
- Made a few cosmetic changes.
Patch written with Benjamin Grégoire.
|
|
Was showing up when comparing e.g. prod Type Type with prod Type Type (!) with
a polymorphic prod.
|
