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>

17 files changed, 83 insertions, 10 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 ->
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f2658a395f..14d0c04212 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -645,6 +645,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
       match EConstr.kind sigma f with
       | Int _ -> user_err Pp.(str "integer cannot be applied")
       | Float _ -> user_err Pp.(str "float cannot be applied")
+      | Array _ -> user_err Pp.(str "array cannot be applied")
       | App _ ->
         assert false (* we have collected all the app in decompose_app *)
       | Proj _ -> assert false (*FIXME*)
@@ -696,6 +697,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
         ; build_proof do_finalize new_infos ]
         g
     | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
+    | Array _ -> CErrors.user_err Pp.(str "Arrays not handled yet")
   and build_proof do_finalize dyn_infos g =
     (*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
     Indfun_common.observe_tac
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index f773157c52..ffce2f8c85 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -103,6 +103,8 @@ let is_rec names =
               names nal)
            b
     | GApp (f, args) -> List.exists (lookup names) (f :: args)
+    | GArray (_u, t, def, ty) ->
+      Array.exists (lookup names) t || lookup names def || lookup names ty
     | GCases (_, _, el, brl) ->
       List.exists (fun (e, _) -> lookup names e) el
       || List.exists (lookup_br names) brl
@@ -2047,7 +2049,8 @@ let rec add_args id new_args =
     | CGeneralization _ ->
       CErrors.anomaly ~label:"add_args " (Pp.str "CGeneralization.")
     | CDelimiters _ ->
-      CErrors.anomaly ~label:"add_args " (Pp.str "CDelimiters."))
+      CErrors.anomaly ~label:"add_args " (Pp.str "CDelimiters.")
+    | CArray _ -> CErrors.anomaly ~label:"add_args " (Pp.str "CArray."))
 
 let rec get_args b t :
     Constrexpr.local_binder_expr list
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 11e4fa0ac7..6ed61043f9 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -568,6 +568,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
     | GProd _ -> user_err Pp.(str "Cannot apply a type")
     | GInt _ -> user_err Pp.(str "Cannot apply an integer")
     | GFloat _ -> user_err Pp.(str "Cannot apply a float")
+    | GArray _ -> user_err Pp.(str "Cannot apply an array")
     (* end of the application treatement *) )
   | GLambda (n, _, t, b) ->
     (* we first compute the list of constructor
@@ -672,6 +673,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
     build_entry_lc env sigma funnames avoid match_expr
   | GRec _ -> user_err Pp.(str "Not handled GRec")
   | GCast (b, _) -> build_entry_lc env sigma funnames avoid b
+  | GArray _ -> user_err Pp.(str "Not handled GArray")
 
 and build_entry_lc_from_case env sigma funname make_discr (el : tomatch_tuples)
     (brl : Glob_term.cases_clauses) avoid : glob_constr build_entry_return =
@@ -1196,7 +1198,7 @@ let rec compute_cst_params relnames params gt =
            discrimination ones *)
       | GSort _ -> params
       | GHole _ -> params
-      | GIf _ | GRec _ | GCast _ ->
+      | GIf _ | GRec _ | GCast _ | GArray _ ->
         CErrors.user_err ~hdr:"compute_cst_params" (str "Not handled case"))
     gt
 
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 5026120849..8e1331ace9 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -109,7 +109,13 @@ let change_vars =
         | GCast (b, c) ->
           GCast
             ( change_vars mapping b
-            , Glob_ops.map_cast_type (change_vars mapping) c ))
+            , Glob_ops.map_cast_type (change_vars mapping) c )
+        | GArray (u, t, def, ty) ->
+          GArray
+            ( u
+            , Array.map (change_vars mapping) t
+            , change_vars mapping def
+            , change_vars mapping ty ))
       rt
   and change_vars_br mapping ({CAst.loc; v = idl, patl, res} as br) =
     let new_mapping = List.fold_right Id.Map.remove idl mapping in
@@ -282,6 +288,12 @@ let rec alpha_rt excluded rt =
       GCast (alpha_rt excluded b, Glob_ops.map_cast_type (alpha_rt excluded) c)
     | GApp (f, args) ->
       GApp (alpha_rt excluded f, List.map (alpha_rt excluded) args)
+    | GArray (u, t, def, ty) ->
+      GArray
+        ( u
+        , Array.map (alpha_rt excluded) t
+        , alpha_rt excluded def
+        , alpha_rt excluded ty )
   in
   new_rt
 
@@ -331,7 +343,9 @@ let is_free_in id =
         | GHole _ -> false
         | GCast (b, (CastConv t | CastVM t | CastNative t)) ->
           is_free_in b || is_free_in t | GCast (b, CastCoerce) -> is_free_in b
-        | GInt _ | GFloat _ -> false)
+        | GInt _ | GFloat _ -> false
+        | GArray (_u, t, def, ty) ->
+          Array.exists is_free_in t || is_free_in def || is_free_in ty)
       x
   and is_free_in_br {CAst.v = ids, _, rt} =
     (not (Id.List.mem id ids)) && is_free_in rt
@@ -404,6 +418,12 @@ let replace_var_by_term x_id term =
         | (GSort _ | GHole _) as rt -> rt
         | GInt _ as rt -> rt
         | GFloat _ as rt -> rt
+        | GArray (u, t, def, ty) ->
+          GArray
+            ( u
+            , Array.map replace_var_by_pattern t
+            , replace_var_by_pattern def
+            , replace_var_by_pattern ty )
         | GCast (b, c) ->
           GCast
             ( replace_var_by_pattern b
@@ -510,7 +530,10 @@ let expand_as =
           ( sty
           , Option.map (expand_as map) po
           , List.map (fun (rt, t) -> (expand_as map rt, t)) el
-          , List.map (expand_as_br map) brl ))
+          , List.map (expand_as_br map) brl )
+      | GArray (u, t, def, ty) ->
+        GArray
+          (u, Array.map (expand_as map) t, expand_as map def, expand_as map ty))
   and expand_as_br map {CAst.loc; v = idl, cpl, rt} =
     CAst.make ?loc (idl, cpl, expand_as (List.fold_left add_as map cpl) rt)
   in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 701ea56c2a..64f62ba1fb 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -305,9 +305,11 @@ let check_not_nested env sigma forbidden e =
     | Lambda (_, t, b) -> check_not_nested t; check_not_nested b
     | LetIn (_, v, t, b) ->
       check_not_nested t; check_not_nested b; check_not_nested v
-    | App (f, l) ->
-      check_not_nested f;
-      Array.iter check_not_nested l
+    | App (f, l) -> check_not_nested f
+    | Array (_u, t, def, ty) ->
+      Array.iter check_not_nested t;
+      check_not_nested def;
+      check_not_nested ty
     | Proj (p, c) -> check_not_nested c
     | Const _ -> ()
     | Ind _ -> ()
@@ -447,6 +449,7 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g =
   match EConstr.kind sigma expr_info.info with
   | CoFix _ | Fix _ ->
     user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint")
+  | Array _ -> user_err Pp.(str "Function cannot treat arrays")
   | Proj _ -> user_err Pp.(str "Function cannot treat projections")
   | LetIn (na, b, t, e) ->
     let new_continuation_tac =
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 1ed632f03f..5dedae6388 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -312,6 +312,7 @@ let iter_constr_LR f c = match kind c with
   | Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) ->
     for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done
   | Proj(_,a) -> f a
+  | Array(_u,t,def,ty) -> Array.iter f t; f def; f ty
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _
      | Int _ | Float _) -> ()