| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
When encountering a "simpl nomatch" constant, the reduction machinery tries
to unfold it. If the subsequent partial reduction does not produce any
match construct, it keeps going from the reduced term. Unfortunately, the
reduced term has been refolded in the meantime, which means that some of
the previous reduction steps have been canceled, thus causing an infinite
loop. This patch delays the refolding till the very end, so that reduction
always progresses.
Disclaimer: I have no idea what I am doing here. The patch compiles the
standard library and the test suite properly, so hopefully they contain
enough tests to exercise the reduction machinery.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
Was exploitable in 8.3, 8.4 and 8.5beta1. A priori not exploitable in
8.5beta2 and 8.5beta3 from a Coq file because typing done while
compiling "match" would serve as a protection. However exploitable by
calling the kernel directly, e.g. from a plugin (but a plugin can
anyway do what it wants by bypassing kernel type abstraction).
Fixing similar error in pretyping.
|
| | |
|
| |
|
|
|
| |
Was showing up when comparing e.g. prod Type Type with prod Type Type (!) with
a polymorphic prod.
|
| |
|
|
|
|
|
|
|
| |
Using the same hack as in the kernel: VM conversion is a reference to
a function, updated when modules using C code are actually linked.
This hack should one day go away, but always linking C code may produce some
other trouble (with the OCaml debugger for instance), so better be safe
for now.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
| | |
|
| |
|
|
|
|
| |
In case we need to backtrack on universe inconsistencies when converting
two (incompatible) instances of the same constant and unfold them.
Bug reported by Amin Timany.
|
| |
|
|
| |
unification fails due to that, during a conversion step.
|
| |
|
|
| |
cases, in some cases.
|
| |
|
|
| |
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. *)
|
| | |
|
| | |
|
| |
|
|
| |
printing functions touched in the kernel).
|
| | |
|
| |
|
|
|
| |
inductive types + deactivate test for equality of sort + deactivate
the check that the constraints Prop/Set <= Type are declared).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As witnessed in the ProjectiveGeometry contrib, some evar normalization were
taking ages because of an exponential behaviour due to a call-by-name
substitution: when normalizing an evar, its arguments were substituted right
away and the resulting term was then normalized, leading to a potential
duplication of normalizations.
Now we normalize evar arguments before substituting them, in a call-by-value
fashion. It makes examples from ProjectiveGeometry compile instanteanously
when they were killing the machine due to excessive memory allocation before
the patch.
Note that there is a tension here: we may be normalizing evar arguments too
eagerly, and try a call-by-need approach instead. To choose which particular
strategy we use, we should do some benchmarks... On stdlib, call-by-value
and call-by-need seem indistinguishable. To be continued?
|
| |
|
|
|
| |
required, i.e. in first-order unification cases where the head of the
other side is a hole or the eta-expanded constant.
|
| | |
|
| |
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
projections and their expansion, allowing unfolding when it fails.
Cleanup code in reductionops.ml
|
| |
|
|
| |
- Decomment code in reductionops forgotten after debugging.
|
| |
|
|
|
|
|
| |
variables.
Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.
|
| |
|
|
| |
Specifications indicating that the record object must be a constructor. Fixes bug #3432.
|
| | |
|
| | |
|
| |
|
|
| |
primitive projections obey the Arguments command.
|
| |
|
|
|
| |
- Monomorphize Cst_stack to 'a = constr.
- Add corresponding debug printer.
|
| |
|
|
|
|
|
|
| |
Universes.
Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes.
Remove unused functions from univ as well and refactor a little bit.
Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
|
| |
|
|
|
|
|
|
|
|
|
| |
allowing fast conversion to be used during unification while respecting the
semantics of unification w.r.t universes.
- Inside kernel, checked_conv is used mainly, it just does checking, while infer_conv
is used for module subtyping.
- Outside, infer_conv is wrapped in Reductionops to register the right constraints
in an evarmap.
- In univ, add a flag to universes to cache the fact that they are >= Set, the
most common constraints, resulting in an 4x speedup in some cases (e.g. HigmanS).
|
| |
|
|
| |
different places
|
| |
|
|
|
|
|
| |
collapsed universes.
- Fix normalization with universe substitutions during refinement being inconsistent
with the one in the kernel.
|
| |
|
|
|
| |
Of course, this is an under approximation of the expected behavior : unfolding
a constant iff a leaf of its underlying split-tree is reached.
|
| |
|
|
| |
(refolding of cbn is smarter)
|
Guillaume Melquiond
Maxime Dénès
Hugo Herbelin
Pierre-Marie Pédrot
Matthieu Sozeau
Enrico Tassi
Pierre Boutillier
Pierre Boutillier
Jason Gross
Matthieu Sozeau