Merge PR #12894: Modify bytecode representation of closures to please OCamls GC (fix #12636).

Reviewed-by: maximedenes
Ack-by: bgregoir
Ack-by: proux01

5 files changed, 145 insertions, 134 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 814cdfe1d8..9118410549 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -33,12 +33,12 @@ void init_arity () {
   arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]=
     arity[ACC6]=arity[ACC7]=arity[PUSH]=arity[PUSHACC0]=arity[PUSHACC1]=
     arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]=
-    arity[PUSHACC6]=arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]=
-    arity[ENVACC3]=arity[ENVACC4]=arity[PUSHENVACC1]=arity[PUSHENVACC2]=
-    arity[PUSHENVACC3]=arity[PUSHENVACC4]=arity[APPLY1]=arity[APPLY2]=
-    arity[APPLY3]=arity[APPLY4]=arity[RESTART]=arity[OFFSETCLOSUREM2]=
-    arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]=
-    arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]=
+    arity[PUSHACC6]=arity[PUSHACC7]=
+    arity[ENVACC0]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]=
+    arity[PUSHENVACC0]=arity[PUSHENVACC1]=arity[PUSHENVACC2]=arity[PUSHENVACC3]=
+    arity[APPLY1]=arity[APPLY2]=arity[APPLY3]=arity[APPLY4]=arity[RESTART]=
+    arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE1]=
+    arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE1]=
     arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]=
     arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
     arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 15cc451ea8..1b6da7dd6f 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -193,6 +193,8 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 #endif
 #endif
 
+#define Is_accu(v) (Is_block(v) && Tag_val(v) == Closure_tag && Code_val(v) == accumulate)
+
 #define CheckPrimArgs(cond, apply_lbl) do{         \
     if (cond) pc++;                                \
     else{                                          \
@@ -383,37 +385,49 @@ value coq_interprete
       }
       /* Access in heap-allocated environment */
 
+      Instruct(ENVACC0){
+        print_instr("ENVACC0");
+        accu = Field(coq_env, 2);
+        Next;
+      }
       Instruct(ENVACC1){
         print_instr("ENVACC1");
-        accu = Field(coq_env, 1); Next;
+        accu = Field(coq_env, 3);
+        Next;
       }
       Instruct(ENVACC2){
         print_instr("ENVACC2");
-        accu = Field(coq_env, 2); Next;
+        accu = Field(coq_env, 4);
+        Next;
       }
       Instruct(ENVACC3){
         print_instr("ENVACC3");
-        accu = Field(coq_env, 3); Next;
+        accu = Field(coq_env, 5);
+        Next;
       }
-      Instruct(ENVACC4){
-        print_instr("ENVACC4");
-        accu = Field(coq_env, 4); Next;
+      Instruct(PUSHENVACC0){
+        print_instr("PUSHENVACC0");
+        *--sp = accu;
+        accu = Field(coq_env, 2);
+        Next;
       }
       Instruct(PUSHENVACC1){
         print_instr("PUSHENVACC1");
-        *--sp = accu; accu = Field(coq_env, 1); Next;
+        *--sp = accu;
+        accu = Field(coq_env, 3);
+        Next;
       }
       Instruct(PUSHENVACC2){
         print_instr("PUSHENVACC2");
-        *--sp = accu; accu = Field(coq_env, 2); Next;
+        *--sp = accu;
+        accu = Field(coq_env, 4);
+        Next;
       }
       Instruct(PUSHENVACC3){
         print_instr("PUSHENVACC3");
-        *--sp = accu; accu = Field(coq_env, 3); Next;
-      }
-      Instruct(PUSHENVACC4){
-        print_instr("PUSHENVACC4");
-        *--sp = accu; accu = Field(coq_env, 4); Next;
+        *--sp = accu;
+        accu = Field(coq_env, 5);
+        Next;
       }
       Instruct(PUSHENVACC){
         print_instr("PUSHENVACC");
@@ -423,7 +437,7 @@ value coq_interprete
       Instruct(ENVACC){
         print_instr("ENVACC");
         print_int(*pc);
-        accu = Field(coq_env, *pc++);
+        accu = Field(coq_env, 2 + *pc++);
         Next;
       }
       /* Function application */
@@ -598,7 +612,6 @@ value coq_interprete
         sp[0] = arg1;
         sp[1] = arg2;
         pc = Code_val(accu);
-        print_lint(accu);
         coq_env = accu;
         coq_extra_args += 1;
         goto check_stack;
@@ -643,13 +656,13 @@ value coq_interprete
       }
 
       Instruct(RESTART) {
-        int num_args = Wosize_val(coq_env) - 2;
+        int num_args = Wosize_val(coq_env) - 3;
         int i;
         print_instr("RESTART");
         CHECK_STACK(num_args);
         sp -= num_args;
-        for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2);
-        coq_env = Field(coq_env, 1);
+        for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 3);
+        coq_env = Field(coq_env, 2);
         coq_extra_args += num_args;
         Next;
       }
@@ -663,9 +676,10 @@ value coq_interprete
         } else {
           mlsize_t num_args, i;
           num_args = 1 + coq_extra_args; /* arg1 + extra args */
-          Alloc_small(accu, num_args + 2, Closure_tag);
-          Field(accu, 1) = coq_env;
-          for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
+          Alloc_small(accu, num_args + 3, Closure_tag);
+          Field(accu, 1) = Val_int(2);
+          Field(accu, 2) = coq_env;
+          for (i = 0; i < num_args; i++) Field(accu, i + 3) = sp[i];
           Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
           sp += num_args;
           pc = (code_t)(sp[0]);
@@ -680,16 +694,18 @@ value coq_interprete
         int rec_pos = *pc++; /* commence a zero */
         print_instr("GRABREC");
         if (rec_pos <= coq_extra_args && !Is_accu(sp[rec_pos])) {
-          pc++;/* On saute le Restart */
+          pc++; /* Skip the next RESTART, then point coq_env at the free variables. */
+          coq_env = coq_env + (Int_val(Field(coq_env, 1)) - 2) * sizeof(value);
         } else {
           if (coq_extra_args < rec_pos) {
             /* Partial application */
             mlsize_t num_args, i;
             num_args = 1 + coq_extra_args; /* arg1 + extra args */
-            Alloc_small(accu, num_args + 2, Closure_tag);
-            Field(accu, 1) = coq_env;
-            for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
-            Code_val(accu) = pc - 3;
+            Alloc_small(accu, num_args + 3, Closure_tag);
+            Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
+            Field(accu, 1) = Val_int(2);
+            Field(accu, 2) = coq_env;
+            for (i = 0; i < num_args; i++) Field(accu, i + 3) = sp[i];
             sp += num_args;
             pc = (code_t)(sp[0]);
             coq_env = sp[1];
@@ -698,25 +714,26 @@ value coq_interprete
           } else {
             /* The recursif argument is an accumulator */
             mlsize_t num_args, i;
+            value block;
             /* Construction of fixpoint applied to its [rec_pos-1] first arguments */
-            Alloc_small(accu, rec_pos + 2, Closure_tag);
-            Field(accu, 1) = coq_env; // We store the fixpoint in the first field
-            for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; // Storing args
-            Code_val(accu) = pc;
-            sp += rec_pos;
-            *--sp = accu;
-              /* Construction of the atom */
-            Alloc_small(accu, 2, ATOM_FIX_TAG);
-            Field(accu,1) = sp[0];
-            Field(accu,0)  = sp[1];
-            sp++; sp[0] = accu;
-              /* Construction of the accumulator */
+            Alloc_small(accu, rec_pos + 3, Closure_tag);
+            Code_val(accu) = pc; /* Point to the next RESTART instr. */
+            Field(accu, 1) = Val_int(2);
+            Field(accu, 2) = coq_env; // We store the fixpoint in the first field
+            for (i = 0; i < rec_pos; i++) Field(accu, i + 3) = *sp++; // Storing args
+            /* Construction of the atom */
+            Alloc_small(block, 2, ATOM_FIX_TAG);
+            Field(block, 0) = *sp++;
+            Field(block, 1) = accu;
+            accu = block;
+            /* Construction of the accumulator */
             num_args = coq_extra_args - rec_pos;
-            Alloc_small(accu, 2+num_args, Accu_tag);
-            Code_val(accu) = accumulate;
-            Field(accu,1) = sp[0]; sp++;
-            for (i = 0; i < num_args;i++)Field(accu, i + 2) = sp[i];
-            sp += num_args;
+            Alloc_small(block, 3 + num_args, Closure_tag);
+            Code_val(block) = accumulate;
+            Field(block, 1) = Val_int(2);
+            Field(block, 2) = accu;
+            for (i = 0; i < num_args; i++) Field(block, i + 3) = *sp++;
+            accu = block;
             pc = (code_t)(sp[0]);
             coq_env = sp[1];
             coq_extra_args = Long_val(sp[2]);
@@ -732,12 +749,13 @@ value coq_interprete
         print_instr("CLOSURE");
         print_int(nvars);
         if (nvars > 0) *--sp = accu;
-        Alloc_small(accu, 1 + nvars, Closure_tag);
+        Alloc_small(accu, 2 + nvars, Closure_tag);
+        Field(accu, 1) = Val_int(2);
         Code_val(accu) = pc + *pc;
         pc++;
         for (i = 0; i < nvars; i++) {
           print_lint(sp[i]);
-          Field(accu, i + 1) = sp[i];
+          Field(accu, i + 2) = sp[i];
         }
         sp += nvars;
         Next;
@@ -758,24 +776,19 @@ value coq_interprete
         }
         pc += nfuncs;
         *--sp=accu;
-        Alloc_small(accu, nfuncs * 2 + nvars, Closure_tag);
-        Field(accu, nfuncs * 2 + nvars - 1) = *sp++;
-        /* On remplie la partie pour les variables libres */
-        p = &Field(accu, nfuncs * 2 - 1);
-        for (i = 0; i < nvars; i++) {
-          *p++ = *sp++;
-        }
+        Alloc_small(accu, nfuncs * 3 + nvars, Closure_tag);
+        Field(accu, nfuncs * 3 + nvars - 1) = *sp++;
         p = &Field(accu, 0);
-        *p = (value) (pc + pc[0]);
-        p++;
+        *p++ = (value) (pc + pc[0]);
+        *p++ = Val_int(nfuncs * 3 - 1);
         for (i = 1; i < nfuncs; i++) {
-          *p = Make_header(i * 2, Infix_tag, Caml_white);
-          p++;                                /* color irrelevant. */
-          *p = (value) (pc + pc[i]);
-          p++;
+          *p++ = Make_header(i * 3, Infix_tag, Caml_white); /* color irrelevant. */
+          *p++ = (value) (pc + pc[i]);
+          *p++ = Val_int((nfuncs - i) * 3 - 1);
         }
+        for (i = 0; i < nvars; i++) *p++ = *sp++;
         pc += nfuncs;
-        accu = accu + 2 * start * sizeof(value);
+        accu = accu + start * 3 * sizeof(value);
         Next;
       }
 
@@ -797,31 +810,28 @@ value coq_interprete
 
         /* Creation des blocks accumulate */
         for(i=0; i < nfunc; i++) {
-          Alloc_small(accu, 2, Accu_tag);
+          Alloc_small(accu, 3, Closure_tag);
           Code_val(accu) = accumulate;
-          Field(accu,1) = Val_int(1);
+          Field(accu, 1) = Val_int(2);
+          Field(accu, 2) = Val_int(1);
           *--sp=accu;
         }
         /* creation des fonction cofix */
 
         p = sp;
-        size = nfunc + nvars + 2;
+        size = nfunc + nvars + 3;
         for (i=0; i < nfunc; i++) {
-
+          value block;
           Alloc_small(accu, size, Closure_tag);
           Code_val(accu) = pc+pc[i];
-          for (j = 0; j < nfunc; j++) Field(accu, j+1) = p[j];
+          Field(accu, 1) = Val_int(2);
+          for (j = 0; j < nfunc; ++j) Field(accu, j + 2) = p[j];
           Field(accu, size - 1) = p[nfunc];
-          for (j = nfunc+1; j <= nfunc+nvars; j++) Field(accu, j) = p[j];
-          *--sp = accu;
-          /* creation du block contenant le cofix */
-
-          Alloc_small(accu,1, ATOM_COFIX_TAG);
-          Field(accu, 0) = sp[0];
-          *sp = accu;
-          /* mise a jour du block accumulate */
-          caml_modify(&Field(p[i], 1),*sp);
-          sp++;
+          for (j = nfunc + 1; j <= nfunc + nvars; ++j) Field(accu, j + 1) = p[j];
+          Alloc_small(block, 1, ATOM_COFIX_TAG);
+          Field(block, 0) = accu;
+          /* update the accumulate block */
+          caml_modify(&Field(p[i], 2), block);
         }
         pc += nfunc;
         accu = p[start];
@@ -837,15 +847,8 @@ value coq_interprete
       } /* fallthrough */
       Instruct(OFFSETCLOSURE) {
         print_instr("OFFSETCLOSURE");
-        accu = coq_env + *pc++ * sizeof(value); Next;
-      }
-      Instruct(PUSHOFFSETCLOSUREM2) {
-        print_instr("PUSHOFFSETCLOSUREM2");
-        *--sp = accu;
-      } /* fallthrough */
-      Instruct(OFFSETCLOSUREM2) {
-        print_instr("OFFSETCLOSUREM2");
-        accu = coq_env - 2 * sizeof(value); Next;
+        accu = coq_env - *pc++ * 3 * sizeof(value);
+        Next;
       }
       Instruct(PUSHOFFSETCLOSURE0) {
         print_instr("PUSHOFFSETCLOSURE0");
@@ -853,15 +856,17 @@ value coq_interprete
       }/* fallthrough */
       Instruct(OFFSETCLOSURE0) {
         print_instr("OFFSETCLOSURE0");
-        accu = coq_env; Next;
+        accu = coq_env;
+        Next;
       }
-      Instruct(PUSHOFFSETCLOSURE2){
-        print_instr("PUSHOFFSETCLOSURE2");
+      Instruct(PUSHOFFSETCLOSURE1){
+        print_instr("PUSHOFFSETCLOSURE1");
         *--sp = accu; /* fallthrough */
       }
-      Instruct(OFFSETCLOSURE2) {
-        print_instr("OFFSETCLOSURE2");
-        accu = coq_env + 2 * sizeof(value); Next;
+      Instruct(OFFSETCLOSURE1) {
+        print_instr("OFFSETCLOSURE1");
+        accu = coq_env - 3 * sizeof(value);
+        Next;
       }
 
 /* Access to global variables */
@@ -954,6 +959,7 @@ value coq_interprete
         print_int(sizes & 0xFFFFFF);
         if (Is_block(accu)) {
           long index = Tag_val(accu);
+          if (index == Closure_tag) index = 0;
           print_instr("block");
           print_lint(index);
           pc += pc[(sizes & 0xFFFFFF) + index];
@@ -1021,7 +1027,7 @@ value coq_interprete
         print_instr("PROJ");
         if (Is_accu (accu)) {
           *--sp = accu; // Save matched block on stack
-          accu = Field(accu, 1); // Save atom to accu register
+          accu = Field(accu, 2); // Save atom to accu register
           switch (Tag_val(accu)) {
           case ATOM_COFIX_TAG: // We are forcing a cofix
             {
@@ -1033,11 +1039,11 @@ value coq_interprete
               coq_env = Field(accu, 0); // Pointer to suspension
               accu = sp[2]; // Save accumulator to accu register
               sp[2] = Val_long(coq_extra_args); // Push number of args for return
-              nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom)
+              nargs = Wosize_val(accu) - 3; // Number of args = size of accumulator - 2 (accumulator closure) - 1 (atom)
               // Push arguments to stack
               CHECK_STACK(nargs + 1);
               sp -= nargs;
-              for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 2);
+              for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 3);
               *--sp = accu; // Last argument is the pointer to the suspension
               coq_extra_args = nargs;
               pc = Code_val(coq_env); // Trigger evaluation
@@ -1059,9 +1065,10 @@ value coq_interprete
               Field(accu, 0) = Field(coq_global_data, *pc++);
               Field(accu, 1) = *sp++;
               /* Create accumulator */
-              Alloc_small(block, 2, Accu_tag);
+              Alloc_small(block, 3, Closure_tag);
               Code_val(block) = accumulate;
-              Field(block, 1) = accu;
+              Field(block, 1) = Val_int(2);
+              Field(block, 2) = accu;
               accu = block;
             }
           }
@@ -1122,7 +1129,7 @@ value coq_interprete
         mlsize_t i, size;
         print_instr("ACCUMULATE");
         size = Wosize_val(coq_env);
-        Alloc_small(accu, size + coq_extra_args + 1, Accu_tag);
+        Alloc_small(accu, size + coq_extra_args + 1, Closure_tag);
         for(i = 0; i < size; i++) Field(accu, i) = Field(coq_env, i);
         for(i = size; i <= coq_extra_args + size; i++)
           Field(accu, i) = *sp++;
@@ -1135,7 +1142,7 @@ value coq_interprete
       Instruct(MAKESWITCHBLOCK) {
         print_instr("MAKESWITCHBLOCK");
         *--sp = accu; // Save matched block on stack
-        accu = Field(accu,1); // Save atom to accu register
+        accu = Field(accu, 2); // Save atom to accu register
         switch (Tag_val(accu)) {
         case ATOM_COFIX_TAG: // We are forcing a cofix
           {
@@ -1149,11 +1156,11 @@ value coq_interprete
             coq_env = Field(accu,0); // Pointer to suspension
             accu = sp[2]; // Save accumulator to accu register
             sp[2] = Val_long(coq_extra_args); // Push number of args for return
-            nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom)
+            nargs = Wosize_val(accu) - 3; // Number of args = size of accumulator - 2 (accumulator closure) - 1 (atom)
             // Push arguments to stack
             CHECK_STACK(nargs+1);
             sp -= nargs;
-            for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2);
+            for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 3);
             *--sp = accu; // Leftmost argument is the pointer to the suspension
             print_lint(nargs);
             coq_extra_args = nargs;
@@ -1174,6 +1181,7 @@ value coq_interprete
             mlsize_t sz;
             int i, annot;
             code_t typlbl,swlbl;
+            value block;
             print_instr("MAKESWITCHBLOCK");
 
             typlbl = (code_t)pc + *pc;
@@ -1200,24 +1208,26 @@ value coq_interprete
             *--sp = accu;
             Alloc_small(accu, 1, Abstract_tag);
             Code_val(accu) = swlbl;
-            *--sp = accu;
             /* We create the switch zipper */
-            Alloc_small(accu, 5, Default_tag);
-            Field(accu, 0) = sp[1];
-            Field(accu, 1) = sp[0];
-            Field(accu, 2) = sp[3];
-            Field(accu, 3) = sp[2];
-            Field(accu, 4) = coq_env;
+            Alloc_small(block, 5, Default_tag);
+            Field(block, 0) = sp[0];
+            Field(block, 1) = accu;
+            Field(block, 2) = sp[2];
+            Field(block, 3) = sp[1];
+            Field(block, 4) = coq_env;
             sp += 3;
-            sp[0] = accu;
+            accu = block;
             /* We create the atom */
-            Alloc_small(accu, 2, ATOM_SWITCH_TAG);
-            Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0];
-            sp++;sp[0] = accu;
+            Alloc_small(block, 2, ATOM_SWITCH_TAG);
+            Field(block, 0) = *sp++;
+            Field(block, 1) = accu;
+            accu = block;
             /* We create the accumulator */
-            Alloc_small(accu, 2, Accu_tag);
-            Code_val(accu) = accumulate;
-            Field(accu,1) = *sp++;
+            Alloc_small(block, 3, Closure_tag);
+            Code_val(block) = accumulate;
+            Field(block, 1) = Val_int(2);
+            Field(block, 2) = accu;
+            accu = block;
           }
         }
         Next;
@@ -1228,10 +1238,11 @@ value coq_interprete
       Instruct(MAKEACCU) {
         int i;
         print_instr("MAKEACCU");
-        Alloc_small(accu, coq_extra_args + 3, Accu_tag);
+        Alloc_small(accu, coq_extra_args + 4, Closure_tag);
         Code_val(accu) = accumulate;
-        Field(accu,1) = Field(coq_atom_tbl, *pc);
-        for(i = 2; i < coq_extra_args + 3; i++) Field(accu, i) = *sp++;
+        Field(accu, 1) = Val_int(2);
+        Field(accu, 2) = Field(coq_atom_tbl, *pc);
+        for (i = 2; i < coq_extra_args + 3; i++) Field(accu, i + 1) = *sp++;
         pc = (code_t)(sp[0]);
         coq_env = sp[1];
         coq_extra_args = Long_val(sp[2]);
@@ -1875,11 +1886,11 @@ value coq_push_val(value v) {
 value coq_push_arguments(value args) {
   int nargs,i;
   value * sp = coq_sp;
-  nargs = Wosize_val(args) - 2;
+  nargs = Wosize_val(args) - 3;
   CHECK_STACK(nargs);
   coq_sp -= nargs;
   print_instr("push_args");print_int(nargs);
-  for(i = 0; i < nargs; i++) coq_sp[i] = Field(args, i+2);
+  for (i = 0; i < nargs; i++) coq_sp[i] = Field(args, i + 3);
   return Val_unit;
 }
 
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 6233675c66..ae5251c252 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -108,7 +108,7 @@ value init_coq_vm(value unit) /* ML */
     init_coq_interpreter();
 
     /* Some predefined pointer code.
-     * It is typically contained in accumulator blocks whose tag is 0 and thus
+     * It is typically contained in accumulator blocks and thus might be
      * scanned by the GC, so make it look like an OCaml block. */
     value accu_block = (value) coq_stat_alloc(2 * sizeof(value));
     Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black);        \
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index bbe91da628..adfd4e8954 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -38,9 +38,9 @@ value coq_closure_arity(value clos) {
   opcode_t * c = Code_val(clos);
   if (Is_instruction(c,RESTART)) {
     c++;
-    if (Is_instruction(c,GRAB)) return Val_int(3 + c[1] - Wosize_val(clos));
+    if (Is_instruction(c,GRAB)) return Val_int(4 + c[1] - Wosize_val(clos));
     else {
-      if (Wosize_val(clos) != 2) caml_failwith("Coq Values : coq_closure_arity");
+      if (Wosize_val(clos) != 3) caml_failwith("Coq Values : coq_closure_arity");
       return Val_int(1);
     }
   }
@@ -50,13 +50,17 @@ value coq_closure_arity(value clos) {
 
 /* Fonction sur les  fix */
 
-value coq_offset(value v) {
+value coq_current_fix(value v) {
   if (Tag_val(v) == Closure_tag) return Val_int(0);
-  else return Val_long(-Wsize_bsize(Infix_offset_val(v)));
+  else return Val_long(Wsize_bsize(Infix_offset_val(v)) / 3);
 }
 
-value coq_offset_closure(value v, value offset){
-  return (value)&Field(v, Int_val(offset));
+value coq_shift_fix(value v, value offset) {
+  return v + Int_val(offset) * 3 * sizeof(value);
+}
+
+value coq_last_fix(value v) {
+  return v + (Int_val(Field(v, 1)) - 2) * sizeof(value);
 }
 
 value coq_set_bytecode_field(value v, value i, value code) {
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index a19f9b56c1..f07018711b 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -17,7 +17,6 @@
 #include <float.h>
 
 #define Default_tag 0
-#define Accu_tag 0
 
 #define ATOM_ID_TAG 0
 #define ATOM_INDUCTIVE_TAG 1
@@ -28,9 +27,6 @@
 #define ATOM_COFIX_TAG 6
 #define ATOM_COFIXEVALUATED_TAG 7
 
-/* Les blocs accumulate */
-#define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag))
-#define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG))
 #define Is_double(v) (Tag_val(v) == Double_tag)
 #define Is_tailrec_switch(v) (Field(v,1) == Val_true)