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, 48 insertions, 7 deletions

diff --git a/dev/ci/user-overlays/11604-persistent-arrays.sh b/dev/ci/user-overlays/11604-persistent-arrays.sh
new file mode 100644
index 0000000000..aec5c4fa3d
--- /dev/null
+++ b/dev/ci/user-overlays/11604-persistent-arrays.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "11604" ] || [ "$CI_BRANCH" = "persistent-arrays" ]; then
+
+    unicoq_CI_REF=persistent-arrays
+    unicoq_CI_GITURL=https://github.com/maximedenes/unicoq
+
+    elpi_CI_REF=persistent-arrays
+    elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
+
+    #relation_algebra_CI_REF=persistent-arrays
+    #relation_algebra_CI_GITURL=https://github.com/maximedenes/relation-algebra
+
+    coqhammer_CI_REF=persistent-arrays
+    coqhammer_CI_GITURL=https://github.com/maximedenes/coqhammer
+
+    metacoq_CI_REF=persistent-arrays
+    metacoq_CI_GITURL=https://github.com/maximedenes/metacoq
+
+fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 3df6f986ce..ea90e83a83 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -50,13 +50,8 @@ let ppqualid qid = pp(pr_qualid qid)
 let ppclindex cl = pp(Coercionops.pr_cl_index cl)
 let ppscheme k = pp (Ind_tables.pr_scheme_kind k)
 
-let prrecarg = function
-  | Declarations.Norec -> str "Norec"
-  | Declarations.Mrec (mind,i) ->
-     str "Mrec[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
-  | Declarations.Imbr (mind,i) ->
-     str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
-let ppwf_paths x = pp (Rtree.pp_tree prrecarg x)
+let prrecarg = Declareops.pp_recarg
+let ppwf_paths x = pp (Declareops.pp_wf_paths x)
 
 let get_current_context () =
   try Vernacstate.Declare.get_current_context ()
@@ -316,6 +311,7 @@ let constr_display csr =
       "Int("^(Uint63.to_string i)^")"
   | Float f ->
       "Float("^(Float64.to_string f)^")"
+  | Array (u,t,def,ty) -> "Array("^(array_display t)^","^(term_display def)^","^(term_display ty)^")@{" ^universes_display u^"\n"
 
   and array_display v =
     "[|"^
@@ -450,6 +446,16 @@ let print_pure_constr csr =
      print_string ("Int("^(Uint63.to_string i)^")")
   | Float f ->
       print_string ("Float("^(Float64.to_string f)^")")
+  | Array (u,t,def,ty) ->
+      print_string "Array(";
+      Array.iter (fun x -> box_display x; print_space()) t;
+      print_string "|";
+      box_display def;
+      print_string ":";
+      box_display ty;
+      print_string ")@{";
+      universes_display u;
+      print_string "}"
 
   and box_display c = open_hovbox 1; term_display c; close_box()
 
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 73cf1b0195..aa650fbdc8 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -17,6 +17,8 @@ let ppripos (ri,pos) =
     print_string ("getglob "^(Constant.to_string kn)^"\n")
   | Reloc_proj_name p ->
     print_string ("proj "^(Projection.Repr.to_string p)^"\n")
+  | Reloc_caml_prim op ->
+    print_string ("caml primitive "^CPrimitives.to_string op)
   );
    print_flush ()
 
@@ -85,6 +87,7 @@ and ppwhd whd =
   | Vconstr_block b -> ppvblock b
   | Vint64 i -> printf "int64(%LiL)" i
   | Vfloat64 f -> printf "float64(%.17g)" f
+  | Varray t -> ppvarray t
   | Vatom_stk(a,s) ->
       open_hbox();ppatom a;close_box();
       print_string"@";ppstack s
@@ -100,6 +103,20 @@ and ppvblock b =
   print_string")";
   close_box()
 
+and ppvarray t =
+  let length = Parray.length_int t in
+  open_hbox();
+  print_string "[|";
+  for i = 0 to length - 2 do
+    ppvalues (Parray.get t (Uint63.of_int i));
+    print_string "; "
+  done;
+  ppvalues (Parray.get t (Uint63.of_int (length - 1)));
+  print_string " | ";
+  ppvalues (Parray.default t);
+  print_string " |]";
+  close_box()
+
 and ppvalues v =
   open_hovbox 0;ppwhd (whd_val v);close_box();
   print_flush()