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>

1 files changed, 8 insertions, 1 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 3d99e1d227..ce8e7d3c2c 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -174,10 +174,14 @@ let rec constr_expr_eq e1 e2 =
     | CDelimiters(s1,e1), CDelimiters(s2,e2) ->
       String.equal s1 s2 &&
       constr_expr_eq e1 e2
+    | CArray(u1,t1,def1,ty1), CArray(u2,t2,def2,ty2) ->
+      Array.equal constr_expr_eq t1 t2 &&
+      constr_expr_eq def1 def2 && constr_expr_eq ty1 ty2 &&
+      eq_universes u1 u2
   | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
      | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
      | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
-     | CGeneralization _ | CDelimiters _ ), _ -> false
+     | CGeneralization _ | CDelimiters _ | CArray _), _ -> false
 
 and args_eq (a1,e1) (a2,e2) =
   Option.equal (eq_ast explicitation_eq) e1 e2 &&
@@ -353,6 +357,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
             (fold_local_binders g f n acc t lb) c lb) l acc
     | CCoFix (_,_) ->
       Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc
+    | CArray (_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty
   )
 
 let free_vars_of_constr_expr c =
@@ -439,6 +444,8 @@ let map_constr_expr_with_binders g f e = CAst.map (function
           let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in
           let d' = f e'' d in
           (id,bl',t',d')) dl)
+    | CArray (u, t, def, ty) ->
+      CArray (u, Array.map (f e) t, f e def, f e ty)
   )
 
 (* Used in constrintern *)