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>

11 files changed, 41 insertions, 2 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 0dbc0513b4..4a41f4c890 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -63,6 +63,11 @@ let pp_boxed_tuple f = function
   | [x] -> f x
   | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l))
 
+let pp_array f = function
+  | [] -> mt ()
+  | [x] -> f x
+  | l -> pp_par true (prlist_with_sep (fun () -> str ";" ++ spc ()) f l)
+
 (** By default, in module Format, you can do horizontal placing of blocks
     even if they include newlines, as long as the number of chars in the
     blocks is less that a line length. To avoid this awkward situation,
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index e77d37fb81..0bd9efd255 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -30,6 +30,7 @@ val pp_apply2 : Pp.t -> bool -> Pp.t list -> Pp.t
 
 val pp_tuple_light : (bool -> 'a -> Pp.t) -> 'a list -> Pp.t
 val pp_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
+val pp_array : ('a -> Pp.t) -> 'a list -> Pp.t
 val pp_boxed_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
 
 val pr_binding : Id.t list -> Pp.t
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a7c926f50c..2dca1d5e49 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -351,7 +351,7 @@ let rec extract_type env sg db j c args =
             | (Info, TypeScheme) ->
               extract_type_app env sg db (r, type_sign env sg ty) args
             | (Info, Default) -> Tunknown))
-    | Cast _ | LetIn _ | Construct _ | Int _ | Float _ -> assert false
+    | Cast _ | LetIn _ | Construct _ | Int _ | Float _ | Array _ -> assert false
 
 (*s Auxiliary function dealing with type application.
   Precondition: [r] is a type scheme represented by the signature [s],
@@ -693,6 +693,12 @@ let rec extract_term env sg mle mlt c args =
        extract_app env sg mle mlt extract_var args
     | Int i -> assert (args = []); MLuint i
     | Float f -> assert (args = []); MLfloat f
+    | Array (_u,t,def,_ty) ->
+      assert (args = []);
+      let a = new_meta () in
+      let ml_arr = Array.map (fun c -> extract_term env sg mle a c []) t in
+      let def = extract_term env sg mle a def [] in
+      MLparray(ml_arr, def)
     | Ind _ | Prod _ | Sort _ -> assert false
 
 (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 97fe8a5776..c25285c987 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -218,6 +218,8 @@ let rec pp_expr par env args =
       pp_par par (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
     | MLfloat _ ->
       pp_par par (str "Prelude.error \"EXTRACTION OF FLOAT NOT IMPLEMENTED\"")
+    | MLparray _ ->
+      pp_par par (str "Prelude.error \"EXTRACTION OF ARRAY NOT IMPLEMENTED\"")
 
 and pp_cons_pat par r ppl =
   pp_par par
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index 81b3e1bcdc..974d254d9c 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -165,6 +165,11 @@ let rec json_expr env = function
       ("what", json_str "expr:float");
       ("float", json_str (Float64.to_string f))
     ]
+  | MLparray(t,def) -> json_dict [
+      ("what", json_str "expr:array");
+      ("elems", json_listarr (Array.map (json_expr env) t));
+      ("default", json_expr env def)
+    ]
 
 and json_one_pat env (ids,p,t) =
   let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in json_dict [
diff --git a/plugins/extraction/miniml.ml b/plugins/extraction/miniml.ml
index 451272d554..a5a6564873 100644
--- a/plugins/extraction/miniml.ml
+++ b/plugins/extraction/miniml.ml
@@ -128,6 +128,7 @@ and ml_ast =
   | MLmagic  of ml_ast
   | MLuint   of Uint63.t
   | MLfloat  of Float64.t
+  | MLparray of ml_ast array * ml_ast
 
 and ml_pattern =
   | Pcons   of GlobRef.t * ml_pattern list
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 451272d554..a5a6564873 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -128,6 +128,7 @@ and ml_ast =
   | MLmagic  of ml_ast
   | MLuint   of Uint63.t
   | MLfloat  of Float64.t
+  | MLparray of ml_ast array * ml_ast
 
 and ml_pattern =
   | Pcons   of GlobRef.t * ml_pattern list
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 465ad50e9b..b1ce10985a 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -431,6 +431,7 @@ let ast_iter_rel f =
     | MLapp (a,l) -> iter n a; List.iter (iter n) l
     | MLcons (_,_,l) | MLtuple l ->  List.iter (iter n) l
     | MLmagic a -> iter n a
+    | MLparray (t,def) -> Array.iter (iter n) t; iter n def
     | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> ()
   in iter 0
 
@@ -450,6 +451,7 @@ let ast_map f = function
   | MLcons (typ,c,l) -> MLcons (typ,c, List.map f l)
   | MLtuple l -> MLtuple (List.map f l)
   | MLmagic a -> MLmagic (f a)
+  | MLparray (t,def) -> MLparray (Array.map f t, f def)
   | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom
   | MLuint _ | MLfloat _ as a -> a
 
@@ -469,6 +471,7 @@ let ast_map_lift f n = function
   | MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l)
   | MLtuple l -> MLtuple (List.map (f n) l)
   | MLmagic a -> MLmagic (f n a)
+  | MLparray (t,def) -> MLparray (Array.map (f n) t, f n def)
   | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom
   | MLuint _ | MLfloat _ as a -> a
 
@@ -484,6 +487,7 @@ let ast_iter f = function
   | MLapp (a,l) -> f a; List.iter f l
   | MLcons (_,_,l) | MLtuple l -> List.iter f l
   | MLmagic a -> f a
+  | MLparray (t,def) -> Array.iter f t; f def
   | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom
   | MLuint _ | MLfloat _ -> ()
 
@@ -521,6 +525,7 @@ let nb_occur_match =
     | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
     | MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l
     | MLmagic a -> nb k a
+    | MLparray (t,def) -> Array.fold_left (fun r a -> r+(nb k a)) 0 t + nb k def
     | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> 0
   in nb 1
 
@@ -573,6 +578,11 @@ let dump_unused_vars a =
        let b' = ren env b in
        if b' == b then a else MLmagic b'
 
+    | MLparray(t,def) ->
+       let t' = Array.Smart.map (ren env) t in
+       let def' = ren env def in
+       if def' == def && t' == t then a else MLparray(t',def')
+
     | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> a
 
     and ren_branch env ((ids,p,b) as tr) =
@@ -1406,6 +1416,7 @@ let rec ml_size = function
   | MLfix(_,_,f) -> ml_size_array f
   | MLletin (_,_,t) -> ml_size t
   | MLmagic t -> ml_size t
+  | MLparray(t,def) -> ml_size_array t + ml_size def
   | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom
   | MLuint _ | MLfloat _ -> 0
 
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index d051602844..3a481039bf 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -107,7 +107,7 @@ let ast_iter_references do_term do_cons do_type a =
         Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v
 
       | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _
-      | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ | MLfloat _ -> ()
+      | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ | MLfloat _ | MLparray _ -> ()
   in iter a
 
 let ind_iter_references do_term do_cons do_type kn ind =
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index a2ce47b11f..088405da5d 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -311,6 +311,11 @@ let rec pp_expr par env args =
     | MLfloat f ->
         assert (args=[]);
         str "(" ++ str (Float64.compile f) ++ str ")"
+    | MLparray(t,def) ->
+      assert (args=[]);
+      let tuple = pp_array (pp_expr true env []) (Array.to_list t) in
+      let def = pp_expr true env [] def in
+      str "(ExtrNative.of_array [|" ++ tuple ++ str "|]" ++ spc () ++ def ++ str")"
 
 
 and pp_record_proj par env typ t pv args =
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 1fb605fc9a..ee50476b10 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -133,6 +133,8 @@ let rec pp_expr env args =
       paren (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
     | MLfloat _ ->
       paren (str "Prelude.error \"EXTRACTION OF FLOAT NOT IMPLEMENTED\"")
+    | MLparray _ ->
+            paren (str "Prelude.error \"EXTRACTION OF PARRAY NOT IMPLEMENTED\"")
 
 and pp_cons_args env = function
   | MLcons (_,r,args) when is_coinductive r ->