| Age | Commit message (Collapse) | Author |
|---|
|
PArray.set has arity 4, but due to the polymorphic universe, its actual
arity is 5. As a consequence, Kshort_apply cannot be used to invoke it
(or rather its accumulating version).
Using Kapply does not quite work here, because Kpush_retaddr would have to
be invoked before the arguments, that is, before we even know whether the
arguments are accumulators. So, to use Kapply, one would need to push the
return address, push duplicates of the already computed arguments, call
the accumulator, and then pop the original arguments.
This commit follows a simpler approach, but more restrictive, as it is
still limited to arity 4, but this time independently from universes. To
do so, the call is performed in two steps. First, a closure containing the
universes is created. Second, the actual application to the original
arguments is performed, for which Kshort_apply is sufficient.
So, this is inefficient, because a closure is created just so that it can
be immediately fully applied. But since this is the accumulator slow path,
this does not matter.
|
|
Despite their names, APPLY1 to APPLY4 are completely different from
APPLY(n) with n = 1 to 4. Indeed, the latter assumes that the return
address was already pushed on the stack, before the arguments were. On the
other hand, APPLY1 to APPLY4 insert the return address in the middle of
the already pushed arguments.
|
|
|
|
Otherwise, the interpreter sees already unified evars as accumulators
rather than actual constants, thus preventing the computations from
progressing.
This was caused by 6b61b63bb8626827708024cbea1312a703a54124, which removed
evar normalization. The effect went unnoticed because the computed term is
still convertible to the reduced term, except that it is the lazy
machinery that ends up reducing it, rather than the bytecode one.
So, performances became abysmal, seemingly at random.
|
|
MAKEPROD is just MAKEBLOCK2(0), but one word shorter. Since this opcode is
never encountered in the fast path, this optimization is not worth the
extra complexity.
|
|
|
|
|
|
Otherwise, these constructs would be followed by a spurious Kreturn
opcode, when in tail position.
|
|
|
|
|
|
That way, accumulators again can be used directly as execution
environments by the bytecode interpreter. This fixes the issue of the
first argument of accumulators being dropped when strongly normalizing.
|
|
The second field of a closure can no longer be the value of the first free
variable (or another closure of a mutually recursive block) but must be an
offset to the first free variable.
This commit makes the bytecode compiler and interpreter agnostic to the
actual representation of closures. To do so, the execution environment
(variable coq_env) no longer points to the currently executed closure but
to the last one. This has the following consequences:
- OFFSETCLOSURE(n) now always loads the n-th closure of a recursive block
(counted from last to first);
- ENVACC(n) now always loads the value of the n-th free variable.
These two changes make the bytecode compiler simpler, since it no
longer has to track the relative position of closures and free variables.
The last change makes the interpreter a bit slower, since it has to adjust
coq_env when executing GRABREC. Hopefully, cache locality will make the
overhead negligible.
|
|
|
