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>

12 files changed, 265 insertions, 1 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 59cc3e5a38..0935617fbf 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -112,7 +112,7 @@ INTERACTIVE := interactive
 UNIT_TESTS := unit-tests
 VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \
   output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \
-  coqdoc ssr primitive/uint63 primitive/float ltac2
+  coqdoc ssr $(wildcard primitive/*) ltac2
 
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk output-coqchk coqwc coq-makefile tools $(UNIT_TESTS)
diff --git a/test-suite/ltac2/constr.v b/test-suite/ltac2/constr.v
index 018596ed95..8c06bff056 100644
--- a/test-suite/ltac2/constr.v
+++ b/test-suite/ltac2/constr.v
@@ -10,3 +10,9 @@ Axiom something : SProp.
 Ltac2 Eval match (kind '(forall x : something, bool)) with
            | Prod a c => a
            | _ => throw Match_failure end.
+
+From Coq Require Import Int63 PArray.
+Open Scope array_scope.
+Ltac2 Eval match (kind '([|true|true|])) with
+  | Array _ _ _ ty => ty
+  | _ => throw Match_failure end.
diff --git a/test-suite/primitive/arrays/copy.v b/test-suite/primitive/arrays/copy.v
new file mode 100644
index 0000000000..bc8e733334
--- /dev/null
+++ b/test-suite/primitive/arrays/copy.v
@@ -0,0 +1,22 @@
+From Coq Require Import Int63 PArray.
+
+Open Scope array_scope.
+
+Definition t : array nat := [| 1; 5; 2 | 4 |].
+Definition t' : array nat := PArray.copy t.
+
+Definition foo1 := (eq_refl : t'.[1] = 5).
+Definition foo2 := (eq_refl 5 <: t'.[1] = 5).
+Definition foo3 := (eq_refl 5 <<: t'.[1] = 5).
+Definition x1 := Eval compute in t'.[1].
+Definition foo4 := (eq_refl : x1 = 5).
+Definition x2 := Eval cbn in t'.[1].
+Definition foo5 := (eq_refl : x2 = 5).
+
+Definition foo6 := (eq_refl : t.[1] = 5).
+Definition foo7 := (eq_refl 5 <: t.[1] = 5).
+Definition foo8 := (eq_refl 5 <<: t.[1] = 5).
+Definition x3 := Eval compute in t.[1].
+Definition foo9 := (eq_refl : x3 = 5).
+Definition x4 := Eval cbn in t.[1].
+Definition foo10 := (eq_refl : x4 = 5).
diff --git a/test-suite/primitive/arrays/default.v b/test-suite/primitive/arrays/default.v
new file mode 100644
index 0000000000..3b89787faf
--- /dev/null
+++ b/test-suite/primitive/arrays/default.v
@@ -0,0 +1,10 @@
+From Coq Require Import Int63 PArray.
+
+Definition t : array nat := [| 1; 3; 2 | 4 |].
+Definition foo1 := (eq_refl : default t = 4).
+Definition foo2 := (eq_refl 4 <: default t = 4).
+Definition foo3 := (eq_refl 4 <<: default t = 4).
+Definition x1 := Eval compute in default t.
+Definition foo4 := (eq_refl : x1 = 4).
+Definition x2 := Eval cbn in default t.
+Definition foo5 := (eq_refl : x2 = 4).
diff --git a/test-suite/primitive/arrays/get.v b/test-suite/primitive/arrays/get.v
new file mode 100644
index 0000000000..9a6f09a83b
--- /dev/null
+++ b/test-suite/primitive/arrays/get.v
@@ -0,0 +1,86 @@
+From Coq Require Import Int63 PArray.
+
+Open Scope array_scope.
+
+(* Test reduction of primitives on array with kernel conversion, vm_compute,
+native_compute, cbv, cbn *)
+
+(* Immediate values *)
+Definition t : array nat := [| 1; 3; 2 | 4 |].
+Definition foo1 := (eq_refl : t.[0] = 1).
+Definition foo2 := (eq_refl 1 <: t.[0] = 1).
+Definition foo3 := (eq_refl 1 <<: t.[0] = 1).
+Definition x1 := Eval compute in t.[0].
+Definition foo4 := (eq_refl : x1 = 1).
+Definition x2 := Eval cbn in t.[0].
+Definition foo5 := (eq_refl : x2 = 1).
+
+Definition foo6 := (eq_refl : t.[2] = 2).
+Definition foo7 := (eq_refl 2 <: t.[2] = 2).
+Definition foo8 := (eq_refl 2 <<: t.[2] = 2).
+Definition x3 := Eval compute in t.[2].
+Definition foo9 := (eq_refl : x3 = 2).
+Definition x4 := Eval cbn in t.[2].
+Definition foo10 := (eq_refl : x4 = 2).
+
+Definition foo11 := (eq_refl : t.[99] = 4).
+Definition foo12 := (eq_refl 4 <: t.[99] = 4).
+Definition foo13 := (eq_refl 4 <<: t.[99] = 4).
+Definition x5 := Eval compute in t.[4].
+Definition foo14 := (eq_refl : x5 = 4).
+Definition x6 := Eval cbn in t.[4].
+Definition foo15 := (eq_refl : x6 = 4).
+
+(* Computations inside the array *)
+Definition t2 : array nat := [| 1 + 3 | 5 |].
+Definition foo16 := (eq_refl : t2.[0] = 4).
+Definition foo17 := (eq_refl 4 <: t2.[0] = 4).
+Definition foo18 := (eq_refl 4 <<: t2.[0] = 4).
+Definition x7 := Eval compute in t2.[0].
+Definition foo19 := (eq_refl : x7 = 4).
+Definition x8 := Eval cbn in t2.[0].
+Definition foo20 := (eq_refl : x8 = 4).
+
+(* Functions inside the array *)
+Definition t3 : array (nat -> nat) := [| fun x => x | fun x => O |].
+Definition foo21 := (eq_refl : t3.[0] 2 = 2).
+Definition foo22 := (eq_refl 2 <: t3.[0] 2 = 2).
+Definition foo23 := (eq_refl 2 <<: t3.[0] 2 = 2).
+Definition x9 := Eval compute in t3.[0] 2.
+Definition foo24 := (eq_refl : x9 = 2).
+Definition x10 := Eval cbn in t3.[0] 2.
+Definition foo25 := (eq_refl : x10 = 2).
+
+Ltac check_const_eq name constr :=
+  let v := (eval cbv delta [name] in name) in
+  tryif constr_eq v constr
+  then idtac
+  else fail 0 "Not syntactically equal:" name ":=" v "<>" constr.
+
+Notation check_const_eq name constr := (ltac:(check_const_eq name constr; exact constr)) (only parsing).
+
+(* Stuck primitive *)
+Definition lazy_stuck_get := Eval lazy in (fun A (t : array A) => t.[0]).
+Definition vm_stuck_get := Eval vm_compute in (fun A (t : array A) => t.[0]).
+Definition native_stuck_get := Eval native_compute in (fun A (t : array A) => t.[0]).
+Definition compute_stuck_get := Eval compute in (fun A (t : array A) => t.[0]).
+Definition cbn_stuck_get := Eval cbn in (fun A (t : array A) => t.[0]).
+
+Check check_const_eq lazy_stuck_get (fun A (t : array A) => t.[0]).
+Check check_const_eq vm_stuck_get (fun A (t : array A) => t.[0]).
+Check check_const_eq native_stuck_get (fun A (t : array A) => t.[0]).
+Check check_const_eq compute_stuck_get (fun A (t : array A) => t.[0]).
+Check check_const_eq cbn_stuck_get (fun A (t : array A) => t.[0]).
+
+(* Under-application *)
+Definition lazy_get := Eval lazy in @PArray.get.
+Definition vm_get := Eval vm_compute in @PArray.get.
+Definition native_get := Eval native_compute in @PArray.get.
+Definition compute_get := Eval compute in @PArray.get.
+Definition cbn_get := Eval cbn in @PArray.get.
+
+Check check_const_eq lazy_get (@PArray.get).
+Check check_const_eq vm_get (fun A (t : array A) i => t.[i]).
+Check check_const_eq native_get (fun A (t : array A) i => t.[i]).
+Check check_const_eq compute_get (@PArray.get).
+Check check_const_eq cbn_get (@PArray.get).
diff --git a/test-suite/primitive/arrays/length.v b/test-suite/primitive/arrays/length.v
new file mode 100644
index 0000000000..67f686f2fb
--- /dev/null
+++ b/test-suite/primitive/arrays/length.v
@@ -0,0 +1,12 @@
+From Coq Require Import Int63 PArray.
+
+Open Scope int63_scope.
+
+Definition t : array nat := [| 1; 3; 2 | 4 |]%nat.
+Definition foo1 := (eq_refl : PArray.length t = 3).
+Definition foo2 := (eq_refl 3 <: PArray.length t = 3).
+Definition foo3 := (eq_refl 3 <<: PArray.length t = 3).
+Definition x1 := Eval compute in PArray.length t.
+Definition foo4 := (eq_refl : x1 = 3).
+Definition x2 := Eval cbn in PArray.length t.
+Definition foo5 := (eq_refl : x2 = 3).
diff --git a/test-suite/primitive/arrays/literal.v b/test-suite/primitive/arrays/literal.v
new file mode 100644
index 0000000000..13e57adbbe
--- /dev/null
+++ b/test-suite/primitive/arrays/literal.v
@@ -0,0 +1,6 @@
+From Coq Require Import Int63 PArray.
+
+Open Scope array_scope.
+
+Definition t1 : array nat := [| 3; 3; 3; 3 | 3 |].
+Definition t2 := [|Type|Type|].
diff --git a/test-suite/primitive/arrays/make.v b/test-suite/primitive/arrays/make.v
new file mode 100644
index 0000000000..a3a39470ed
--- /dev/null
+++ b/test-suite/primitive/arrays/make.v
@@ -0,0 +1,18 @@
+From Coq Require Import Int63 PArray.
+
+Open Scope array_scope.
+
+(* Immediate values *)
+Definition t1 : array nat := [| 3; 3; 3; 3 | 3 |].
+Definition t2 := PArray.make 4 3.
+Definition foo1 := (eq_refl : t1 = t2).
+Definition foo2 := (eq_refl t1 <: t1 = t2).
+Definition foo3 := (eq_refl t1 <<: t1 = t2).
+Definition x1 := Eval compute in t2.
+Definition foo4 := (eq_refl : x1 = t1).
+Definition x2 := Eval cbn in t2.
+Definition foo5 := (eq_refl : x2 = t1).
+
+Definition partial1 := Eval lazy in @PArray.make.
+Definition partial2 := Eval vm_compute in @PArray.make.
+Definition partial3 := Eval native_compute in @PArray.make.
diff --git a/test-suite/primitive/arrays/max_length.v b/test-suite/primitive/arrays/max_length.v
new file mode 100644
index 0000000000..54a6af7a19
--- /dev/null
+++ b/test-suite/primitive/arrays/max_length.v
@@ -0,0 +1,13 @@
+From Coq Require Import Int63 PArray.
+
+Open Scope int63_scope.
+
+Definition max_length := 4194303.
+
+Definition foo1 := (eq_refl max_length : PArray.max_length = max_length).
+Definition foo2 := (eq_refl max_length <: PArray.max_length = max_length).
+Definition foo3 := (eq_refl max_length <<: PArray.max_length = max_length).
+Definition max_length2 := Eval compute in PArray.max_length.
+Definition foo4 := (eq_refl : max_length = max_length2).
+Definition max_length3 := Eval cbn in PArray.max_length.
+Definition foo5 := (eq_refl : max_length = max_length3).
diff --git a/test-suite/primitive/arrays/nested.v b/test-suite/primitive/arrays/nested.v
new file mode 100644
index 0000000000..841cee4463
--- /dev/null
+++ b/test-suite/primitive/arrays/nested.v
@@ -0,0 +1,47 @@
+From Coq Require Import Int63 PArray.
+
+Open Scope array_scope.
+
+Module OneLevel.
+
+Inductive foo : Set :=
+  C : array foo -> foo.
+
+Fixpoint f1 (x : foo) {struct x} : False :=
+  match x with
+  | C t => f1 (t.[0])
+  end.
+
+Fixpoint f2 (x : foo) {struct x} : False :=
+  f2 match x with
+  | C t => t.[0]
+  end.
+
+Fixpoint f3 (x : foo) {struct x} : False :=
+  match x with
+  | C t => f3 (PArray.default t)
+  end.
+
+End OneLevel.
+
+Module TwoLevels.
+
+Inductive foo : Set :=
+  C : array (array foo) -> foo.
+
+Fixpoint f1 (x : foo) {struct x} : False :=
+  match x with
+  | C t => f1 (t.[0].[0])
+  end.
+
+Fixpoint f2 (x : foo) {struct x} : False :=
+  f2 match x with
+  | C t => t.[0].[0]
+  end.
+
+Fixpoint f3 (x : foo) {struct x} : False :=
+  match x with
+  | C t => f3 (PArray.default (PArray.default t))
+  end.
+
+End TwoLevels.
diff --git a/test-suite/primitive/arrays/reroot.v b/test-suite/primitive/arrays/reroot.v
new file mode 100644
index 0000000000..172a118cc7
--- /dev/null
+++ b/test-suite/primitive/arrays/reroot.v
@@ -0,0 +1,22 @@
+From Coq Require Import Int63 PArray.
+
+Open Scope array_scope.
+
+Definition t : array nat := [| 1; 5; 2 | 4 |].
+Definition t' : array nat := PArray.reroot t.
+
+Definition foo1 := (eq_refl : t'.[1] = 5).
+Definition foo2 := (eq_refl 5 <: t'.[1] = 5).
+Definition foo3 := (eq_refl 5 <<: t'.[1] = 5).
+Definition x1 := Eval compute in t'.[1].
+Definition foo4 := (eq_refl : x1 = 5).
+Definition x2 := Eval cbn in t'.[1].
+Definition foo5 := (eq_refl : x2 = 5).
+
+Definition foo6 := (eq_refl : t.[1] = 5).
+Definition foo7 := (eq_refl 5 <: t.[1] = 5).
+Definition foo8 := (eq_refl 5 <<: t.[1] = 5).
+Definition x3 := Eval compute in t.[1].
+Definition foo9 := (eq_refl : x3 = 5).
+Definition x4 := Eval cbn in t.[1].
+Definition foo10 := (eq_refl : x4 = 5).
diff --git a/test-suite/primitive/arrays/set.v b/test-suite/primitive/arrays/set.v
new file mode 100644
index 0000000000..f265c37ea8
--- /dev/null
+++ b/test-suite/primitive/arrays/set.v
@@ -0,0 +1,22 @@
+From Coq Require Import Int63 PArray.
+
+Open Scope array_scope.
+
+Definition t : array nat := [| 1; 3; 2 | 4 |].
+Definition t' : array nat := t.[1 <- 5].
+
+Definition foo1 := (eq_refl : t'.[1] = 5).
+Definition foo2 := (eq_refl 5 <: t'.[1] = 5).
+Definition foo3 := (eq_refl 5 <<: t'.[1] = 5).
+Definition x1 := Eval compute in t'.[1].
+Definition foo4 := (eq_refl : x1 = 5).
+Definition x2 := Eval cbn in t'.[1].
+Definition foo5 := (eq_refl : x2 = 5).
+
+Definition foo6 := (eq_refl : t.[1] = 3).
+Definition foo7 := (eq_refl 3 <: t.[1] = 3).
+Definition foo8 := (eq_refl 3 <<: t.[1] = 3).
+Definition x3 := Eval compute in t.[1].
+Definition foo9 := (eq_refl : x3 = 3).
+Definition x4 := Eval cbn in t.[1].
+Definition foo10 := (eq_refl : x4 = 3).