Primitive persistent arrays

Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.

Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

3 files changed, 73 insertions, 1 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 306643f758..814cdfe1d8 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -75,6 +75,8 @@ 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;
   /* instruction with four operands */
   arity[MAKESWITCHBLOCK]=4;
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 7588c1ce07..9921208e04 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -22,6 +22,7 @@
 #include <caml/memory.h>
 #include <caml/signals.h>
 #include <caml/version.h>
+#include <caml/callback.h>
 
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
@@ -111,7 +112,8 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 /* GC interface */
 #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; }
 #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; }
-
+#define Setup_for_caml_call { *--sp = coq_env; coq_sp = sp; }
+#define Restore_after_caml_call { sp = coq_sp; coq_env = *sp++; }
 
 /* Register optimization.
    Some compilers underestimate the use of the local variables representing
@@ -1771,6 +1773,71 @@ value coq_interprete
         Next;
       }
 
+
+      Instruct(ISINT_CAML_CALL2) {
+        value arg;
+        print_instr("ISINT_CAML_CALL2");
+        if (Is_uint63(accu)) {
+          pc++;
+          print_int(*pc);
+          arg = sp[0];
+          Setup_for_caml_call;
+          accu = caml_callback2(Field(coq_global_data, *pc), accu, arg);
+          Restore_after_caml_call;
+          sp += 1;
+          pc++;
+        } else pc += *pc;
+        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(ISARRAY_INT_CAML_CALL2) {
+        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;
+      }
+
+      Instruct(ISARRAY_INT_CAML_CALL3) {
+        value arg1;
+        value arg2;
+        print_instr("ISARRAY_INT_CAML_CALL3");
+        if (Is_coq_array(accu) && Is_uint63(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);
+          Restore_after_caml_call;
+          sp += 2;
+          pc++;
+        } else pc += *pc;
+        Next;
+      }
+
 /* Debugging and machine control */
 
       Instruct(STOP){
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index b027673ac7..86ae6295fd 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -33,6 +33,9 @@
 #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)
 
+/* 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