| Age | Commit message (Collapse) | Author |
|---|
|
Evarconv was made precociously dependent on user-declared reduction
behaviors. Only cbn should rely on that.
|
|
This avoids postponing constraints which will surely produce
an occur-check and allow to backtrack on first-order unifications
producing those constraints directly (e.g. to apply eta).
(fixes HoTT/HoTT with 8.5).
|
|
Function default_fail was always part of an ise_try. Its associated
error message was anyway thrown away. It is then irrelevant and could
be made simpler.
|
|
This can happen with the "with" clause (see e.g. #4782), but also with
recursive calls in first-order unification (e.g. "?n a a b = f a" when
a matching between "b" and "a" is tried before expanding f).
|
|
Typically, a problem of the form "?x args = match ?y with ... end" was
a failure even if miller-unification was applicable.
|
|
|
|
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).
|
|
|
|
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
|
of arguments of eta_constructor.
|
|
naming of arguments of eta.
|
|
|
|
|
|
|
|
because of the name of a bound variable lost when unifying under a
binder in evarconv.
|
|
Indeed, the name of a bound variable was lost when unifying under a Prod in
evarconv.
The error message for "Unable to satisfy the following constraints" is
still to be improved though.
|
|
|
|
unification fails due to that, during a conversion step.
|
|
Unifying two let-in's expresions syntactically is a heuristic
(compared to performing the zeta-reduction). This heuristic was
requiring unification of types which is too strong for the heuristic
to work uniformly since the types might only be related modulo
subtyping.
The patch is to remove the unification of types, which allows then to
have the heuristic work uniformly on the bodies. On the other side, I
hope it does not loose (still heuristical) unifications compared to
before (presumably, since instantiating the evars in the body will
induce constraints for solving potential evars in the types of the
let-in bodies, but this would need a proof). Anyway, it is not about
correction, it is about a heuristic, which maybe done too early
actually.
|
|
|
|
typed-based matching: it provokes a stack overflow in contrib
ClassicalRealisability. To be investigated later on.
(See 893a02f643858ba0b0172648e77af9ccb65f03df.)
|
|
3cd718c, to the case of second_order_matching.
|
|
|
|
unification algorithm in consider_remaining_unif_problems. If it
happens to be problematic, one can backtrack to the "optimization"
from 3bd9cb26b which has a restriction on rels/vars.
|
|
following working:
Definition test {A B:Type} {H:A=B} (a:A) : B := rew H in a.
|
|
initial segment of the context of the evar.
|
|
|
|
- In evarconv, check_conv_record properly computes the parameters of
primitive record projections for later unification, adding env and
sigma as arguments.
- In unification, backtrack on pattern-unification and not only
application unification if eta for a record failed.
|
|
|
|
e.g. for MTac.
|
|
evar_define.
Interestingly, the added choose in evarconv.ml allows solve_evar_evar
to be observationally commutative, in the sense of not either fail or
succeed in compiling the stdlib whether problems are given in the
left-to-right or right-to-left order.
|
|
inductive types + deactivate test for equality of sort + deactivate
the check that the constraints Prop/Set <= Type are declared).
|
|
forms in evarconv and unification, as well as fallback to first-order
unification when eta for constructors fail. Update test-suite file
3484 to test for the FO case in evarconv as well.
|
|
folded primitive projections in applicative stacks in rhs as named, hence
prefering to unfold the lhs in these cases.
|
|
|
|
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
|
|
in cases of unification with existentials requiring it.
|
|
2nd-order matching).
We made the filter type-safe (i.e. to ensure that Gamma |- ?n:T is
well-typed when taking the filtered context Gamma) in 2nd order
matching. Maybe this weakens the power of the 2nd order matching
algorithm, so it is not clear that it is the good fix.
Another fix could have been to ensure that taking the closure of
filter does not extend it beyond the original filter (hence keeping
the filter untyped if it was already untyped).
As for the bug #3045, it also revealed that some "destruct c as [[]]"
could be made stronger as decomposing the destruct in two parts
"destruct c as [x]; destruct x" workis while it currently fails if in
one part.
|
|
potentially different types, resulting in ill-typed terms due to eta.
Projection expansion now fails gracefully on retyping errors.
The proper fix to unification, checking that the heads for FO
have unifiable types, is currently too strong, adding unnecessary universe
constraints, so it is disabled for now. It might be quite expensive
too also it's not noticeable on the stdlib.
|
|
|
|
using whd_state_gen to handle unfolding. Add an isProj/destProj
in term. Use the proper environment everywhere in unification.ml.
|
|
their eta-expanded forms which can then unfold back to the unfolded
primitive projection form. This removes all special code that
was necessary to handle primitive projections before, while keeping
compatibility.
Also fix cbn which was not refolding primitive projections correctly
in all cases.
Update some test-suite files accordingly.
|
|
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
|
|
eta-expansion, creating a loop. This is now deactivated. Fixes bugs #3665 and #3667.
|
|
with existing ML code.
|
|
for e_contextually where it is used. Bug #3648 is fixed.
|
|
matching partial applications of primitive projections. Fixes bug #3637.
|
|
|
|
equality of universes, along with a few other functions in evd.
|
