| Age | Commit message (Collapse) | Author |
|---|
|
This reverts commit 0b417c12eb10bb29bcee04384b6c0855cb9de73a.
A good fix requires to review a bit the design of unification constraint
postponement, which we do in 8.6. We leave things as they are in 8.5 for
compatibility.
|
|
The fix solves the original bug report but it only turns the Not_found
into a normal error in the alternative example by Guillaume. See
test-suite file for comments on how to eventually improve the
situation and find a solution in Guillaume's example too.
|
|
Do not force all remaining conversions problems to be solved after the
_first_ solution of an evar, but only at the end of assignment of terms
to evars in w_merge. This was hell to track down, thanks for the help of
Maxime. contribs pass and HoTT too.
|
|
Because refreshing Prop is not semantics-preserving,
the new universe is >= Set, so cannot be minimized to Prop
afterwards.
|
|
In congruence, refresh universes including the Set/Prop ones so that
congruence works with cumulativity, not restricting itself to the
inferred types of terms that are manipulated but allowing them to be
used at more general types. This fixes bug #4609.
|
|
|
|
|
|
same evar.
|
|
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.
|
|
Update the evar_source of the solution evar in evar/evar problems to
propagate the information that it does not necessarily have to be solved
in Program mode.
|
|
|
|
|
|
math-classes.
|
|
Rechecking applications built by evarconv's imitation.
|
|
This is a bug in a pretty old code, showing also in 8.3 and 8.4.
|
|
former filter after 48509b61 and 3cd718c, because filtered let-ins
were not any longer preserved).
|
|
when called from w_unify, so we protect it.
|
|
index lookup.
|
|
|
|
ensure_evar_independent into is_constrainable_in (a simpler approach
closest to what existed before cf6a68b45).
|
|
|
|
inefficiency #4076.
In an evar context like this one
x:X, y:=f(x), z:Z(x,y) |- ?x : T(x,y,z)
with unification problem
a:A, b:=f(t(a)) |- ?x[x:=t(a);y:=b;z:=u(a,b)] = v(a,b,c)
we now keep y after filtering, iff the name b occurs effectively in
v(a,b,c), while before, we kept it as soon as its expansion f(t(a))
had free variables in v(a,b,c), which was more often, but useless
since the point in keeping a let-in in the instance is precisely to
reuse the name of the let-in while unifying with a right-hand side
which mentions this name.
|
|
integrating ensure_evar_independent into is_constrainable_in.
|
|
Pushing pending problems had the side-effect of later solving them in
the opposite order as they arrived, resulting on different complexity
(see e.g. #4076). We now take care of pushing them in reverse order so
that they are treated in the same order.
|
|
is_constrainable_in.
|
|
is_constrainable_in to do the job of ensuring that ?p does not belong to the ti while solving ?p[...]:=?n[t1..tn].
|
|
Bindings of the form [let x:T := M] are unfolded into [(M:T)], so that
occur-check is done in [T] as well as in [M] (except when [M] is a
variable, where it is hopefully not necessary).
This is a way to fix #4062 (evars with type depending on themselves).
The fix modifies the alias map (make_alias_map) but it should behave
the same at all places using alias maps other than
has_constrainable_free_vars.
|
|
unifications ?X ~= ?Y foo not catched by solve_evar_evar.
|
|
from Matthieu).
|
|
|
|
incompatibilities wrt 8.4.", as it creates other problems (in Ergo and
Compcert).
This reverts commit bf388dfec041ab0fa74ae5d484600f6fcf515e4f.
|
|
8.4.
|
|
not using the intended test. By fixing the intended test, the need for
a delta-expansion resulting from this commit in PFsection6.v (line
1255) of ssreflect disappears.
|
|
|
|
accidentally mixed up in 9aa416c0c6.
|
|
step, prefer QuestionMark's to other evars, to comply with the
filtering made on VarInstance, GoalEvar and QuestionMark for type
class resolution. Maybe evars to be resolved by type class instances
should eventually be marked with a specific tag.
At least, this solves the current problem with compiling cancel2.v in
LemmaOverloading.
|
|
|
|
in reporting the chain of causes when unification fails.
|
|
pattern-matching predicate.
|
|
In the case of conversion, postponing by preserving the
initial orientation.
Was wrong from its initial version in Jan 2014, but was not visible
because evar-evar subtyping was approximated by evar-evar conversion.
Thanks to Enrico for a very short example highlighting the problem. In
particular, this fixes Ergo.
|
|
test pattern-unification after restriction of the evars so as to
succeed earlier (no observational changes however in the examples at my
disposal).
|
|
?n[...] = ?p[...;x:=?n[...];...]. Indeed, x could be a solution for ?p.
|
|
similar optimization broke at some time some ssreflect code; we now
treat the easy case of a let-in to a rel - a pattern common in
pattern-matching compilation -; later on, we shall want to investigate
whether any let-in found to refer to out of scope rels or vars can be
filtered out).
|
|
|
|
|
|
types: we downcast the evar in the higher type to the lower type.
Then, we have the freedom to choose the order of instantiation
according to the instances of the evars (e.g. choosing the
instantiation for which pattern-unification is possible, if ever it is
possible in only one way - as shown by an example in contribution
Paco).
This still does not preserve compatibility because it happens that
type classes resolution is crucially dependent on the order of
presentation of the ?n=?p problems. Consider e.g. an example taken
from Containers. Both now and before e2fa65fccb9, one has this asymmetry:
Context `{Helt : OrderedType elt}.
Check forall x y r l h, @Equivalence.equiv _ _ _ x y -> In x (Node l x r h).
--> @Equivalence.equiv QArith_base.Q QArith_base.Qeq QArith_base.Q_Setoid x y
Context `{Helt : OrderedType elt}.
Check forall x y r l h, In x (Node l x r h) -> @Equivalence.equiv _ _ _ x y.
--> @Equivalence.equiv elt (@_eq elt Helt) (@OT_Equivalence elt Helt)
Then, embedding this example within a bigger one which relies on the
?n=?n' resolution order, one can get two incompatible resolution of
the same problem.
To be continued...
|
|
types as it was before commit 710bae2a8c81a44.
There is still at least one problem with bug #3392 to solve.
|
