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, 36 insertions, 0 deletions

diff --git a/kernel/parray.mli b/kernel/parray.mli
new file mode 100644
index 0000000000..0276278bd0
--- /dev/null
+++ b/kernel/parray.mli
@@ -0,0 +1,36 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val max_length : Uint63.t
+
+type 'a t
+val length  : 'a t -> Uint63.t
+val length_int : 'a t -> int
+val get     : 'a t -> Uint63.t -> 'a
+val set     : 'a t -> Uint63.t -> 'a -> 'a t
+val default : 'a t -> 'a
+val make    : Uint63.t -> 'a -> 'a t
+val init    : Uint63.t -> (int -> 'a) -> 'a -> 'a t
+val copy    : 'a t -> 'a t
+val reroot  : 'a t -> 'a t
+
+val map : ('a -> 'b) -> 'a t -> 'b t
+
+val to_array : 'a t -> 'a array * 'a (* default *)
+
+val of_array : 'a array -> 'a (* default *) -> 'a t
+
+val unsafe_of_array : 'a array -> 'a -> 'a t
+(* [unsafe_of_array] injects a mutable array into a persistent one, but does
+   not perform a copy. This means that if the persistent array is mutated, the
+   original one will be too. *)
+
+val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
+val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a