From 0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 3 Feb 2020 18:19:42 +0100 Subject: 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 Co-authored-by: Gaëtan Gilbert --- kernel/nativevalues.mli | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) (limited to 'kernel/nativevalues.mli') 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] -- cgit v1.2.3