| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
possible, which is the "natural" way to orient an equation. At least
it matters for matching subterms against patterns, so that it is the
pattern variables which are substituted if ever the subterm has itself
existential variables, as in:
Goal exists x, S x = x.
eexists.
destruct (S _).
|
|
arbitrary direction as if it were an "evar = evar" problem.
|
|
Incidentally, this allows to make earlier the collapse of CUMUL to
CONV when force is true.
|
|
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.
|
|
subsumed by the call to project_evar_on_evar.
|
|
scope" error message).
|
|
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.
|
|
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.
|
|
|
|
|
|
instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.
|
|
of metas/evars
|
|
to match on a primitive projection application c.(p) using "?f _", binding f
to (fun x => x.(p)) with the correct typing.
|
|
|
|
from MathClasses).
|
|
invariant that the evar arguments to that function always have to be undefined.
|
|
the computed direction argument. In case pbty is conv, no refreshing is done
as the evar body must be convertible with the given term, however refreshing
of template application evar arguments can still happen.
(Re)-Closing bug #2966.
|
|
there is not the same as in Evd.define.
- Fixed bugs #3330 and #3331.
|
|
for helping fixing this).
Now the issue is handled solely through refreshing of the terms assigned
to evars during unification.
If ?X = list ?Y, then Y's type is refreshed so that it doesn't mention
a template universe and in turn, ?X won't. Same goes when typechecking
(nil ?X, nil ?Y), the pair constructor levels will be set higher than fresh
universes for the lists carriers. This also handles user-defined functions
on template polymorphic inductives, which was fragile before.
Pretyping and Evd are now uncluttered from template-specific code.
|
|
|
|
it was failing with Not_found before previous commit). This "fixes"
the loop by expanding local defs in "imitate" rather than keeping them
explicit. The example is otherwise too large for me to be able to
understand where does the loop come from.
|
|
fix the type of the term which has to be in the signature of the evar
to declare); some problems remain though (see next commit).
|
|
eagerly solve l <= k constraints as k := l when k is a fresh variable coming
from a template type. This has the effect of fixing the variable at the first
instantiation of the parameters of template polymorphic inductive and avoiding
to generate useless <= constraints that need to be minimized afterwards.
|
|
|
