Make callback opcodes more generic.

This does not make the code any slower, since

  Is_coq_array(accu) && Is_uint63(sp[0])

and

  !Is_accu(accu) && !Is_accu(sp[0])

take the exact same number of tests to pass in the concrete case.

In the accumulator case, it takes one more test to fail, but we do not
care about the performances then.

5 files changed, 48 insertions, 47 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 1ffb323748..1ba6a8c8fe 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -73,9 +73,10 @@ void init_arity () {
     arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1;
   /* instruction with two operands */
   arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
-  arity[ISARRAY_CAML_CALL1]=arity[ISINT_CAML_CALL2]=
-  arity[ISARRAY_INT_CAML_CALL2]=arity[ISARRAY_INT_CAML_CALL3]=
-  arity[PROJ]=2;
+    arity[CHECKCAMLCALL1]=arity[CHECKCAMLCALL2_1]=
+    arity[CHECKCAMLCALL2]=arity[CHECKCAMLCALL3_1]=
+    arity[PROJ]=
+    2;
   /* instruction with four operands */
   arity[MAKESWITCHBLOCK]=4;
   /* instruction with arbitrary operands */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 72f6e12b0f..672ee60c6d 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1754,11 +1754,11 @@ value coq_interprete
         Next;
       }
 
-
-      Instruct(ISINT_CAML_CALL2) {
+      Instruct(CHECKCAMLCALL2_1) {
+        // arity-2 callback, the last argument can be an accumulator
         value arg;
-        print_instr("ISINT_CAML_CALL2");
-        if (Is_uint63(accu)) {
+        print_instr("CHECKCAMLCALL2_1");
+        if (!Is_accu(accu)) {
           pc++;
           print_int(*pc);
           arg = sp[0];
@@ -1771,47 +1771,50 @@ value coq_interprete
         Next;
       }
 
-      Instruct(ISARRAY_CAML_CALL1) {
-        print_instr("ISARRAY_CAML_CALL1");
-              if (Is_coq_array(accu)) {
-                pc++;
-                Setup_for_caml_call;
-                print_int(*pc);
-                accu = caml_callback(Field(coq_global_data, *pc),accu);
-                Restore_after_caml_call;
-                pc++;
-              }
-              else pc += *pc;
-              Next;
+      Instruct(CHECKCAMLCALL1) {
+        // arity-1 callback, no argument can be an accumulator
+        print_instr("CHECKCAMLCALL1");
+        if (!Is_accu(accu)) {
+          pc++;
+          Setup_for_caml_call;
+          print_int(*pc);
+          accu = caml_callback(Field(coq_global_data, *pc), accu);
+          Restore_after_caml_call;
+          pc++;
+        }
+        else pc += *pc;
+        Next;
       }
 
-      Instruct(ISARRAY_INT_CAML_CALL2) {
+      Instruct(CHECKCAMLCALL2) {
+        // arity-2 callback, no argument can be an accumulator
         value arg;
-        print_instr("ISARRAY_INT_CAML_CALL2");
-          if (Is_coq_array(accu) && Is_uint63(sp[0])) {
-            pc++;
-            arg = sp[0];
-            Setup_for_caml_call;
-            print_int(*pc);
-            accu = caml_callback2(Field(coq_global_data, *pc), accu, arg);
-            Restore_after_caml_call;
-            sp += 1;
-            pc++;
-          } else pc += *pc;
-          Next;
+        print_instr("CHECKCAMLCALL2");
+        if (!Is_accu(accu) && !Is_accu(sp[0])) {
+          pc++;
+          arg = sp[0];
+          Setup_for_caml_call;
+          print_int(*pc);
+          accu = caml_callback2(Field(coq_global_data, *pc), accu, arg);
+          Restore_after_caml_call;
+          sp += 1;
+          pc++;
+        } else pc += *pc;
+        Next;
       }
 
-      Instruct(ISARRAY_INT_CAML_CALL3) {
+      Instruct(CHECKCAMLCALL3_1) {
+        // arity-3 callback, the last argument can be an accumulator
         value arg1;
         value arg2;
-        print_instr("ISARRAY_INT_CAML_CALL3");
-        if (Is_coq_array(accu) && Is_uint63(sp[0])) {
+        print_instr("CHECKCAMLCALL3_1");
+        if (!Is_accu(accu) && !Is_accu(sp[0])) {
           pc++;
           arg1 = sp[0];
           arg2 = sp[1];
           Setup_for_caml_call;
           print_int(*pc);
-          accu = caml_callback3(Field(coq_global_data, *pc),accu, arg1, arg2);
+          accu = caml_callback3(Field(coq_global_data, *pc), accu, arg1, arg2);
           Restore_after_caml_call;
           sp += 2;
           pc++;
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index f07018711b..0cdef34050 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -30,9 +30,6 @@
 #define Is_double(v) (Tag_val(v) == Double_tag)
 #define Is_tailrec_switch(v) (Field(v,1) == Val_true)
 
-/* coq array */
-#define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1))
-
 /* coq values for primitive operations */
 #define coq_tag_C1 2
 #define coq_tag_C0 1
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index c8c8f61d59..63abb50cc2 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -147,10 +147,10 @@ let opcodes =
     "CHECKLDSHIFTEXP";
     "CHECKNEXTUPFLOAT";
     "CHECKNEXTDOWNFLOAT";
-    "ISINT_CAML_CALL2";
-    "ISARRAY_CAML_CALL1";
-    "ISARRAY_INT_CAML_CALL2";
-    "ISARRAY_INT_CAML_CALL3";
+    "CHECKCAMLCALL2_1";
+    "CHECKCAMLCALL1";
+    "CHECKCAMLCALL2";
+    "CHECKCAMLCALL3_1";
     "STOP"
   |]
 
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index 0bd3375169..592bdf775f 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -251,11 +251,11 @@ let check_prim_op = function
   | Float64ldshiftexp -> opCHECKLDSHIFTEXP
   | Float64next_up    -> opCHECKNEXTUPFLOAT
   | Float64next_down  -> opCHECKNEXTDOWNFLOAT
-  | Arraymake -> opISINT_CAML_CALL2
-  | Arrayget -> opISARRAY_INT_CAML_CALL2
-  | Arrayset -> opISARRAY_INT_CAML_CALL3
+  | Arraymake -> opCHECKCAMLCALL2_1
+  | Arrayget -> opCHECKCAMLCALL2
+  | Arrayset -> opCHECKCAMLCALL3_1
   | Arraydefault | Arraycopy | Arraylength ->
-      opISARRAY_CAML_CALL1
+      opCHECKCAMLCALL1
 
 let emit_instr env = function
   | Klabel lbl -> define_label env lbl