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, 22 insertions, 2 deletions

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 54065e8b35..6422e184b5 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -92,9 +92,12 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
    Uint63.equal i1 i2
 | NFloat f1, NFloat f2 ->
   Float64.equal f1 f2
+| NArray(t1,def1,ty1), NArray(t2,def2,ty2) ->
+  Array.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) def1 def2
+    && eq_notation_constr vars ty1 ty2
 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
   | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
-  | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _), _ -> false
+  | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> false
 
 (**********************************************************************)
 (* Re-interpret a notation as a glob_constr, taking care of binders   *)
@@ -249,6 +252,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
   | NRef x -> GRef (x,None)
   | NInt i -> GInt i
   | NFloat f -> GFloat f
+  | NArray (t,def,ty) -> GArray(None, Array.map (f e) t, f e def, f e ty)
 
 let glob_constr_of_notation_constr ?loc x =
   let rec aux () x =
@@ -472,6 +476,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
      if arg != None then has_ltac := true;
      NHole (w, naming, arg)
   | GRef (r,_) -> NRef r
+  | GArray (_u,t,def,ty) -> NArray (Array.map aux t, aux def, aux ty)
   | GEvar _ | GPatVar _ ->
       user_err Pp.(str "Existential variables not allowed in notations.")
   ) x
@@ -675,6 +680,14 @@ let rec subst_notation_constr subst bound raw =
       let k' = smartmap_cast_type (subst_notation_constr subst bound) k in
       if r1' == r1 && k' == k then raw else NCast(r1',k')
 
+  | NArray (t,def,ty) ->
+      let def' = subst_notation_constr subst bound def
+      and t' = Array.Smart.map (subst_notation_constr subst bound) t
+      and ty' = subst_notation_constr subst bound ty
+      in
+        if def' == def && t' == t && ty' == ty then raw else
+          NArray(t',def',ty')
+
 let subst_interpretation subst (metas,pat) =
   let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in
   (metas,subst_notation_constr subst bound pat)
@@ -1254,9 +1267,16 @@ let rec match_ inner u alp metas sigma a1 a2 =
           match_names metas (alp,sigma) (Name id') na in
       match_in u alp metas sigma (mkGApp a1 [DAst.make @@ GVar id']) b2
 
+  | GArray(_u,t,def,ty), NArray(nt,ndef,nty) ->
+    if Int.equal (Array.length t) (Array.length nt) then
+      let sigma = match_in u alp metas sigma def ndef in
+      let sigma = match_in u alp metas sigma ty nty in
+      Array.fold_left2 (match_in u alp metas) sigma t nt
+    else raise No_match
+
   | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
      | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
-     | GCast _ | GInt _ | GFloat _), _ -> raise No_match
+     | GCast _ | GInt _ | GFloat _ | GArray _), _ -> raise No_match
 
 and match_in u = match_ true u