| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
| |
The context matching function was dropping the surrounding context in
let-ins.
|
| |
|
|
|
|
| |
for which there corresponding tag are greater than max_variant_tag.
The code is a merge with the patch proposed by Bruno on
github barras/coq
commit/504c753d7bb104ff4453fa0ede21c870ae2bb00c
|
| |
|
|
|
|
|
| |
change the representation of inductive constructor
when there is too many non constant constructors in the inductive type
Conflicts:
kernel/cbytegen.ml
|
| |
|
|
|
|
|
|
|
|
|
|
| |
presence of let-ins and recursively non-uniform parameters).
The bug was in the List.chop of Inductiveops.get_arity which was wrong
in the presence of let-ins and recursively non-uniform parameters.
The bug #3491 showed up because, in addition to have let-ins, it was
wrongly detected as having recursively non-uniform parameters.
Also added some comments in declarations.mli.
|
| |
|
|
|
|
|
| |
bug #4133)
Note that, if someone was purposely modifying the user name of a type in
order to disable a coercion, it no longer works. Hopefully, no one did.
|
| | |
|
| | |
|
| |
|
|
| |
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.
|
Pierre-Marie Pédrot
Benjamin Gregoire
Hugo Herbelin
Guillaume Melquiond
Matthieu Sozeau
Enrico Tassi
Arnaud Spiwack
Matthieu Sozeau
Pierre Boutillier
Maxime Dénès