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>

5 files changed, 41 insertions, 8 deletions

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 =