Use the same memory layout as closures for accumulators.

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.

4 files changed, 68 insertions, 66 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index b44ae34582..40ddcbb213 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -712,26 +712,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 + 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[i]; // Storing args
-            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 */
+            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, Accu_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]);
@@ -808,9 +808,10 @@ value coq_interprete
 
         /* Creation des blocks accumulate */
         for(i=0; i < nfunc; i++) {
-          Alloc_small(accu, 2, Accu_tag);
+          Alloc_small(accu, 3, Accu_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 */
@@ -818,22 +819,17 @@ value coq_interprete
         p = sp;
         size = nfunc + nvars + 3;
         for (i=0; i < nfunc; i++) {
-
+          value block;
           Alloc_small(accu, size, Closure_tag);
           Code_val(accu) = pc+pc[i];
           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 + 1) = 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++;
+          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];
@@ -1028,7 +1024,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
             {
@@ -1040,11 +1036,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
@@ -1066,9 +1062,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, Accu_tag);
               Code_val(block) = accumulate;
-              Field(block, 1) = accu;
+              Field(block, 1) = Val_int(2);
+              Field(block, 2) = accu;
               accu = block;
             }
           }
@@ -1142,7 +1139,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
           {
@@ -1156,11 +1153,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;
@@ -1181,6 +1178,7 @@ value coq_interprete
             mlsize_t sz;
             int i, annot;
             code_t typlbl,swlbl;
+            value block;
             print_instr("MAKESWITCHBLOCK");
 
             typlbl = (code_t)pc + *pc;
@@ -1207,24 +1205,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, Accu_tag);
+            Code_val(block) = accumulate;
+            Field(block, 1) = Val_int(2);
+            Field(block, 2) = accu;
+            accu = block;
           }
         }
         Next;
@@ -1235,10 +1235,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, Accu_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]);
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index a19f9b56c1..bde6e14367 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -30,7 +30,6 @@
 
 /* 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)
 
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
index a826cf8193..375b1aface 100644
--- a/kernel/vmbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -74,23 +74,23 @@ open Environ
 (*                      ^                                                 *)
 (* The [ai] blocks are functions that accumulate their arguments:         *)
 (*           ai arg1  argp --->                                           *)
-(*    ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ]   *)
+(*    ai' = [A_t | accumulate | envofs | [Cfx_t | fcofixi] | arg1 | ... | argp ] *)
 (* If such a block is matched against, we have to force evaluation,       *)
 (* function [fcofixi] is then applied to [ai'] [arg1] ... [argp]          *)
 (* (note that [ai'] is a pointer to the closure, passed as argument)      *)
 (* Once evaluation is completed [ai'] is updated with the result:         *)
 (*  ai' <--                                                               *)
-(*   [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ]   *)
+(*   [A_t | accumulate | envofs | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *)
 (* This representation is nice because the application of the cofix is    *)
 (* evaluated only once (it simulates a lazy evaluation)                   *)
 (* Moreover, when cofix don't have arguments, it is possible to create    *)
 (* a cycle, e.g.:                                                         *)
 (*   cofix one := cons 1 one                                              *)
-(*   a1 = [A_t | accumulate | [Cfx_t|fcofix1] ]                           *)
+(*   a1 = [A_t | accumulate | envofs | [Cfx_t|fcofix1] ]                  *)
 (*   fcofix1 = [clos_t | code | envofs | a1]                              *)
 (* The result of evaluating [a1] is [cons_t | 1 | a1].                    *)
 (* When [a1] is updated :                                                 *)
-(*  a1 = [A_t | accumulate | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ]     *)
+(*  a1 = [A_t | accumulate | envofs | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ] *)
 (* The cycle is created ...                                               *)
 (*                                                                        *)
 (* In Cfxe_t accumulators, we need to store [fcofixi] for testing         *)
@@ -394,16 +394,16 @@ let add_grabrec rec_arg arity lbl cont =
 let cont_cofix arity =
     (* accu = res                                                         *)
     (* stk  = ai::args::ra::...                                           *)
-    (* ai   = [At|accumulate|[Cfx_t|fcofix]|args]                         *)
+    (* ai   = [At|accumulate|envofs|[Cfx_t|fcofix]|args]                  *)
   [ Kpush;
     Kpush;        (*                 stk = res::res::ai::args::ra::...    *)
     Kacc 2;
-    Kfield 1;
+    Kfield 2;
     Kfield 0;
     Kmakeblock(2, cofix_evaluated_tag);
     Kpush;        (*  stk = [Cfxe_t|fcofix|res]::res::ai::args::ra::...*)
     Kacc 2;
-    Ksetfield 1;  (*   ai = [At|accumulate|[Cfxe_t|fcofix|res]|args]      *)
+    Ksetfield 2;  (*   ai = [At|accumulate|envofs|[Cfxe_t|fcofix|res]|args] *)
                   (*  stk = res::ai::args::ra::...                        *)
     Kacc 0;       (* accu = res                                           *)
     Kreturn (arity+2) ]
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 177f67210c..98a1b13373 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -231,7 +231,7 @@ type vswitch = {
 (* + vm_env is the type of the machine environments (i.e. a function or   *)
 (*   a fixpoint)                                                          *)
 (*                                                                        *)
-(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ]            *)
+(* + Accumulators : At_[accumulate | envofs=2 | accu | arg1 | ... | argn ] *)
 (*   - representation of [accu] : tag_[....]                              *)
 (*     -- tag <= 3 : encoding atom type (sorts, free vars, etc.)          *)
 (*     -- 10_[accu|proj name] : a projection blocked by an accu           *)
@@ -328,9 +328,9 @@ let uni_lvl_val (v : values) : Univ.Level.t =
 
 let rec whd_accu a stk =
   let stk =
-    if Int.equal (Obj.size a) 2 then stk
+    if Int.equal (Obj.size a) 3 then stk
     else Zapp (Obj.obj a) :: stk in
-  let at = Obj.field a 1 in
+  let at = Obj.field a 2 in
   match Obj.tag at with
   | i when Int.equal i type_atom_tag ->
      begin match stk with
@@ -421,9 +421,10 @@ let whd_val : values -> whd =
 
 let obj_of_atom : atom -> Obj.t =
   fun a ->
-    let res = Obj.new_block accu_tag 2 in
+    let res = Obj.new_block accu_tag 3 in
     set_bytecode_field res 0 accumulate;
-    Obj.set_field res 1 (Obj.repr a);
+    Obj.set_field res 1 (Obj.repr 2);
+    Obj.set_field res 2 (Obj.repr a);
     res
 
 (* obj_of_str_const : structured_constant -> Obj.t *)
@@ -631,9 +632,10 @@ let mk_cofix_body apply_varray k ndef vcf =
     let c = Obj.field (Obj.repr vcfi) 0 in
     Obj.set_field e 0 c;
     let atom = Obj.new_block cofix_tag 1 in
-    let self = Obj.new_block accu_tag 2 in
+    let self = Obj.new_block accu_tag 3 in
     set_bytecode_field self 0 accumulate;
-    Obj.set_field self 1 (Obj.repr atom);
+    Obj.set_field self 1 (Obj.repr 2);
+    Obj.set_field self 2 (Obj.repr atom);
     apply_varray (Obj.obj e) [|Obj.obj self|] in
   Array.init ndef cofix_body