| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
unification fails due to that, during a conversion step.
|
| |
|
|
|
|
| |
pattern_of_constr in an evar_map, as they can appear in the context
of said named metas, which is used by change. Not sure what to do in
the PEvar case, which never matches anyway according to Constr_matching.matches.
|
| |
|
|
| |
cases, in some cases.
|
| |
|
|
| |
when called from w_unify, so we protect it.
|
| |
|
|
| |
index lookup.
|
| | |
|
| |
|
|
| |
as revealed by #2141).
|
| |
|
|
| |
It was an integer overflow! All sorts of memories.
|
| |
|
|
|
|
|
|
|
| |
is reduced as if without let-in, when applied to arguments.
This allows e.g. to have a head-betazeta-reduced goal in the following example.
Inductive Foo : let X := Set in X := I : Foo.
Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *)
|
| |
|
|
| |
clause in the presence of let-ins in the arity of inductive type).
|
| |
|
|
| |
inductive types with let-in in arity.
|
| |
|
|
|
| |
Workers send back incomplete system states (only the proof part).
Such part must include the meta/evar counter.
|
| |
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
| |
progress.
Also compare goals up to evar instantiation (otherwise no progress would be observed when only unification occurs, unless some [nf_evar] is done). Performance look unchanged so far.
Some code from [Evd] which was used only in [tclPROGRESS] have been moved out (and [progress_evar_map] was now dead, so I killed it).
Fixes bugs (one reported directly on coqdev, and #3412).
|
| |
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
This was broken by the attempt to use the same algorithm for rewriting
closed subterms than for rewriting subterms with evars: the algorithm
to find subterms (w_unify_to_subterm) did not go through evars. But
what to do when looking say, for a pattern "S ?n" in a goal "S ?x[a:=S ?y]"?
Should we unify ?x[a:=S ?y] with ?n or consider ?x as rigid and look
in the instance? If we adopt the first approach, then, what to do when
looking for "S ?n" in a goal "?x[a:=S ?y]"? Failing? Looking in the
instance? Is it normal that an evar behaves as a rigid constant when
it cannot be unified with the pattern?
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
to display by default (see bc8a5357889 - 17 Oct 2014):
- not printing instances for let-in anymore even when expanded (since
they are canonical up to conversion)
- still printing x:=x in [x:=x;x':=x] when x is directly an instance
of another var, but not in [x:=x;x':=S x]
This can be discussed, but if ever this is to be changed, it should
not be printed in [x:=x;x:=?n] with ?n implicitly depending on x
(otherwise said, variables which are not displayed in instances of
internal evars should not contribute to the decision of writing
x:=x in the instance).
|
| |
|
|
| |
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.
|
| | |
|
| |
|
|
| |
goal in Instance. Also remove some dead code.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
unifications ?X ~= ?Y foo not catched by solve_evar_evar.
|
| |
|
|
| |
from Matthieu).
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
printing functions touched in the kernel).
|
| |
|
|
|
|
| |
match predicates for vm_compute and compile polymorphic definitions
to constant code. Add univscompute test-suite file testing VM
computations in presence of polymorphic universes.
|
| |
|
|
|
| |
One remaining issue: aliased constants raise an anomaly when some unsubstituted
universe variables remain. VM may suffer from the same problem.
|
| |
|
|
|
|
|
|
|
|
| |
definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.
|
| |
|
|
|
|
| |
constr for primitive records (not used anywhere else than printing).
Problem reported by P. LeFanu Lumsdaine on HoTT/HoTT.
Also add some minor fixes in detyping and pretty printing related to universes.
|
| | |
|
| |
|
|
|
|
|
| |
incompatibilities wrt 8.4.", as it creates other problems (in Ergo and
Compcert).
This reverts commit bf388dfec041ab0fa74ae5d484600f6fcf515e4f.
|
| |
|
|
| |
8.4.
|
| | |
|
| |
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
| |
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.
|
Matthieu Sozeau
Hugo Herbelin
Enrico Tassi
Arnaud Spiwack
Guillaume Melquiond
Pierre-Marie Pédrot
Matthieu Sozeau
Pierre Boutillier
Maxime Dénès