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>

1 files changed, 37 insertions, 0 deletions

diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 78a9b2ea13..08c5bd7126 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -134,6 +134,7 @@ type kind_of_value =
   | Vconst of int
   | Vint64 of int64
   | Vfloat64 of float
+  | Varray of t Parray.t
   | Vblock of block
 
 val kind_of_value : t -> kind_of_value
@@ -332,3 +333,39 @@ val no_check_next_up : t -> t
 
 val no_check_next_down : t -> t
 [@@ocaml.inline always]
+
+(** Support for arrays *)
+
+val parray_of_array : t array -> t -> t
+val is_parray : t -> bool
+
+val arraymake : t -> t -> t -> t -> t (* accu A n def *)
+val arrayget : t -> t -> t -> t -> t (* accu A t n *)
+val arraydefault : t -> t -> t (* accu A t *)
+val arrayset : t -> t -> t -> t -> t -> t (* accu A t n v *)
+val arraycopy : t -> t -> t -> t (* accu A t *)
+val arrayreroot : t -> t -> t -> t (* accu A t *)
+val arraylength : t -> t -> t -> t (* accu A t *)
+val arrayinit : t -> t -> t -> t (* accu A n f def *)
+val arraymap : t -> t -> t (* accu A B f t *)
+
+val no_check_arraymake : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_arrayget : t -> t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_arraydefault : t -> t
+[@@ocaml.inline always]
+
+val no_check_arrayset : t -> t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_arraycopy : t -> t
+[@@ocaml.inline always]
+
+val no_check_arrayreroot : t -> t
+[@@ocaml.inline always]
+
+val no_check_arraylength : t -> t
+[@@ocaml.inline always]