Modify bytecode representation of closures to please OCaml's GC (fix #12636).

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.

1 files changed, 4 insertions, 6 deletions

diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index 2d74cca44c..f052e03cde 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -38,15 +38,15 @@ let opcodes =
     "PUSHACC7";
     "PUSHACC";
     "POP";
+    "ENVACC0";
     "ENVACC1";
     "ENVACC2";
     "ENVACC3";
-    "ENVACC4";
     "ENVACC";
+    "PUSHENVACC0";
     "PUSHENVACC1";
     "PUSHENVACC2";
     "PUSHENVACC3";
-    "PUSHENVACC4";
     "PUSHENVACC";
     "PUSH_RETADDR";
     "APPLY";
@@ -65,13 +65,11 @@ let opcodes =
     "CLOSURE";
     "CLOSUREREC";
     "CLOSURECOFIX";
-    "OFFSETCLOSUREM2";
     "OFFSETCLOSURE0";
-    "OFFSETCLOSURE2";
+    "OFFSETCLOSURE1";
     "OFFSETCLOSURE";
-    "PUSHOFFSETCLOSUREM2";
     "PUSHOFFSETCLOSURE0";
-    "PUSHOFFSETCLOSURE2";
+    "PUSHOFFSETCLOSURE1";
     "PUSHOFFSETCLOSURE";
     "GETGLOBAL";
     "PUSHGETGLOBAL";