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

diff --git a/kernel/constr.ml b/kernel/constr.ml
index d0598bdad1..1837a39764 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -109,6 +109,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Proj      of Projection.t * 'constr
   | Int       of Uint63.t
   | Float     of Float64.t
+  | Array     of 'univs * 'constr array * 'constr * 'types
 (* constr is the fixpoint of the previous type. Requires option
    -rectypes of the Caml compiler to be set *)
 type t = (t, t, Sorts.t, Instance.t) kind_of_term
@@ -246,6 +247,9 @@ let mkRef (gr,u) = let open GlobRef in match gr with
 (* Constructs a primitive integer *)
 let mkInt i = Int i
 
+(* Constructs an array *)
+let mkArray (u,t,def,ty) = Array (u,t,def,ty)
+
 (* Constructs a primitive float number *)
 let mkFloat f = Float f
 
@@ -485,6 +489,8 @@ let fold f acc c = match kind c with
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
   | CoFix (_,(_lna,tl,bl)) ->
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
+  | Array(_u,t,def,ty) ->
+    f (f (Array.fold_left f acc t) def) ty
 
 (* [iter f c] iters [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
@@ -508,6 +514,7 @@ let iter f c = match kind c with
   | Case (_,p,iv,c,bl) -> f p; iter_invert f iv; f c; Array.iter f bl
   | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
   | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
+  | Array(_u,t,def,ty) -> Array.iter f t; f def; f ty
 
 (* [iter_with_binders g f n c] iters [f n] on the immediate
    subterms of [c]; it carries an extra data [n] (typically a lift
@@ -532,6 +539,8 @@ let iter_with_binders g f n c = match kind c with
   | CoFix (_,(_,tl,bl)) ->
       Array.Fun1.iter f n tl;
       Array.Fun1.iter f (iterate g (Array.length tl) n) bl
+  | Array(_u,t,def,ty) ->
+    Array.iter (f n) t; f n def; f n ty
 
 (* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
    subterms of [c] starting from [acc] and proceeding from left to
@@ -560,6 +569,8 @@ let fold_constr_with_binders g f n acc c =
       let n' = iterate g (Array.length tl) n in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+  | Array(_u,t,def,ty) ->
+    f n (f n (Array.fold_left (f n) acc t) def) ty
 
 (* [map f c] maps [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
@@ -705,6 +716,12 @@ let map_gen userview f c = match kind c with
       let bl' = Array.Smart.map f bl in
       if tl'==tl && bl'==bl then c
       else mkCoFix (ln,(lna,tl',bl'))
+  | Array(u,t,def,ty) ->
+    let t' = Array.Smart.map f t in
+    let def' = f def in
+    let ty' = f ty in
+    if def'==def && t==t' && ty==ty' then c
+    else mkArray(u,t',def',ty')
 
 let map_user_view = map_gen true
 let map = map_gen false
@@ -773,6 +790,12 @@ let fold_map f accu c = match kind c with
       let accu, bl' = Array.Smart.fold_left_map f accu bl in
       if tl'==tl && bl'==bl then accu, c
       else accu, mkCoFix (ln,(lna,tl',bl'))
+  | Array(u,t,def,ty) ->
+    let accu, t' = Array.Smart.fold_left_map f accu t in
+    let accu, def' = f accu def in
+    let accu, ty' = f accu ty in
+    if def'==def && t==t' && ty==ty' then accu, c
+    else accu, mkArray(u,t',def',ty')
 
 (* [map_with_binders g f n c] maps [f n] on the immediate
    subterms of [c]; it carries an extra data [n] (typically a lift
@@ -835,6 +858,12 @@ let map_with_binders g f l c0 = match kind c0 with
     let l' = iterate g (Array.length tl) l in
     let bl' = Array.Fun1.Smart.map f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
+  | Array(u,t,def,ty) ->
+    let t' = Array.Fun1.Smart.map f l t in
+    let def' = f l def in
+    let ty' = f l ty in
+    if def'==def && t==t' && ty==ty' then c0
+    else mkArray(u,t',def',ty')
 
 (*********************)
 (*      Lifting      *)
@@ -877,6 +906,7 @@ let fold_with_full_binders g f n acc c =
       let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+  | Array(_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty
 
 
 type 'univs instance_compare_fn = (GlobRef.t * int) option ->
@@ -935,9 +965,13 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
     && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
     Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2
+  | Array(u1,t1,def1,ty1), Array(u2,t2,def2,ty2) ->
+    leq_universes None u1 u2 &&
+    Array.equal_norefl (eq 0) t1 t2 &&
+    eq 0 def1 def2 && eq 0 ty1 ty2
   | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _
     | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _
-    | CoFix _ | Int _ | Float _), _ -> false
+    | CoFix _ | Int _ | Float _| Array _), _ -> false
 
 (* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
    the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
@@ -1129,6 +1163,9 @@ let constr_ord_int f t1 t2 =
     | Int i1, Int i2 -> Uint63.compare i1 i2
     | Int _, _ -> -1 | _, Int _ -> 1
     | Float f1, Float f2 -> Float64.total_compare f1 f2
+    | Array(_u1,t1,def1,ty1), Array(_u2,t2,def2,ty2) ->
+      (((Array.compare f) =? f) ==? f) t1 t2 def1 def2 ty1 ty2
+    | Array _, _ -> -1 | _, Array _ -> 1
 
 let rec compare m n=
   constr_ord_int compare m n
@@ -1222,9 +1259,11 @@ let hasheq t1 t2 =
       && array_eqeq bl1 bl2
     | Int i1, Int i2 -> i1 == i2
     | Float f1, Float f2 -> Float64.equal f1 f2
+    | Array(u1,t1,def1,ty1), Array(u2,t2,def2,ty2) ->
+      u1 == u2 && def1 == def2 && ty1 == ty2 && array_eqeq t1 t2
     | (Rel _ | Meta _ | Var _ | Sort _ | Cast _ | Prod _ | Lambda _ | LetIn _
       | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _
-      | Fix _ | CoFix _ | Int _ | Float _), _ -> false
+      | Fix _ | CoFix _ | Int _ | Float _ | Array _), _ -> false
 
 (** Note that the following Make has the side effect of creating
     once and for all the table we'll use for hash-consing all constr *)
@@ -1332,6 +1371,13 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
         let (h,l) = Uint63.to_int2 i in
         (t, combinesmall 18 (combine h l))
       | Float f -> (t, combinesmall 19 (Float64.hash f))
+      | Array (u,t,def,ty) ->
+        let u, hu = sh_instance u in
+        let t, ht = hash_term_array t in
+        let def, hdef = sh_rec def in
+        let ty, hty = sh_rec ty in
+        let h = combine4 hu ht hdef hty in
+        (Array(u,t,def,ty), combinesmall 20 h)
 
   and sh_invert = function
     | NoInvert -> NoInvert, 0
@@ -1413,6 +1459,8 @@ let rec hash t =
       combinesmall 17 (combine (Projection.hash p) (hash c))
     | Int i -> combinesmall 18 (Uint63.hash i)
     | Float f -> combinesmall 19 (Float64.hash f)
+    | Array(u,t,def,ty) ->
+      combinesmall 20 (combine4 (Instance.hash u) (hash_term_array t) (hash def) (hash ty))
 
 and hash_invert = function
   | NoInvert -> 0
@@ -1566,6 +1614,9 @@ let rec debug_print c =
          str"}")
   | Int i -> str"Int("++str (Uint63.to_string i) ++ str")"
   | Float i -> str"Float("++str (Float64.to_string i) ++ str")"
+  | Array(u,t,def,ty) -> str"Array(" ++ prlist_with_sep pr_comma debug_print (Array.to_list t) ++ str" | "
+      ++ debug_print def ++ str " : " ++ debug_print ty
+      ++ str")@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str"}"
 
 and debug_invert = let open Pp in function
   | NoInvert -> mt()