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, 36 insertions, 11 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 32eb63a818..334c23c963 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -77,6 +77,7 @@ let mkArrow t1 r t2 = of_kind (Prod (make_annot Anonymous r, t1, t2))
 let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2
 let mkInt i = of_kind (Int i)
 let mkFloat f = of_kind (Float f)
+let mkArray (u,t,def,ty) = of_kind (Array (u,t,def,ty))
 
 let mkRef (gr,u) = let open GlobRef in match gr with
   | ConstRef c -> mkConstU (c,u)
@@ -366,6 +367,7 @@ let iter_with_full_binders sigma g f n c =
     Array.iter (f n) tl;
     let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na,lift i t)) n) n lna tl in
     Array.iter (f n') bl
+  | Array (_u,t,def,ty) -> Array.Fun1.iter f n t; f n def; f n ty
 
 let iter_with_binders sigma g f n c =
   let f l c = f l (of_constr c) in
@@ -546,18 +548,21 @@ let universes_of_constr sigma c =
   let rec aux s c =
     match kind sigma c with
     | Const (c, u) ->
-          LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+      LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
     | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
-          LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+      LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
     | Sort u ->
-       let sort = ESorts.kind sigma u in
-       if Sorts.is_small sort then s
-       else
-         let u = Sorts.univ_of_sort sort in
-         LSet.fold LSet.add (Universe.levels u) s
+      let sort = ESorts.kind sigma u in
+      if Sorts.is_small sort then s
+      else
+        let u = Sorts.univ_of_sort sort in
+        LSet.fold LSet.add (Universe.levels u) s
     | Evar (k, args) ->
-       let concl = Evd.evar_concl (Evd.find sigma k) in
-       fold sigma aux (aux s concl) c
+      let concl = Evd.evar_concl (Evd.find sigma k) in
+      fold sigma aux (aux s concl) c
+    | Array (u,_,_,_) ->
+      let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
+      fold sigma aux s c
     | _ -> fold sigma aux s c
   in aux LSet.empty c
 
@@ -762,7 +767,7 @@ let kind_of_type sigma t = match kind sigma t with
   | (Rel _ | Meta _ | Var _ | Evar _ | Const _
   | Proj _ | Case _ | Fix _ | CoFix _ | Ind _)
     -> AtomicType (t,[||])
-  | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type"
+  | (Lambda _ | Construct _ | Int _ | Float _ | Array _) -> failwith "Not a type"
 
 module Unsafe =
 struct
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 2bf8f69af7..d0f675319d 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -135,6 +135,7 @@ val mkArrow : t -> Sorts.relevance  -> t -> t
 val mkArrowR : t -> t -> t
 val mkInt : Uint63.t -> t
 val mkFloat : Float64.t -> t
+val mkArray : EInstance.t * t array * t * t -> t
 
 val mkRef : GlobRef.t * EInstance.t -> t
 
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 1cf5be10ae..fb9f6db0ea 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -118,7 +118,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
         Some (Nametab.basename_of_global (global_of_constr c))
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
         Some (match lna.(i).binder_name with Name id -> id | _ -> assert false)
-    | Sort _ | Rel _ | Meta _|Evar _|Case _ | Int _ | Float _ -> None
+    | Sort _ | Rel _ | Meta _|Evar _|Case _ | Int _ | Float _ | Array _ -> None
   in
   hdrec c
 
@@ -166,6 +166,7 @@ let hdchar env sigma c =
     | Meta _ | Case _ -> "y"
     | Int _ -> "i"
     | Float _ -> "f"
+    | Array _ -> "a"
   in
   hdrec 0 c
 
diff --git a/engine/termops.ml b/engine/termops.ml
index f6d0807823..e5231ef9cd 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -659,6 +659,12 @@ let map_constr_with_binders_left_to_right sigma g f l c =
         if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
         then c
         else mkCoFix (ln,(lna,tl',bl'))
+  | Array(u,t,def,ty) ->
+      let t' = Array.map_left (f l) t in
+      let def' = f l def in
+      let ty' = f l ty in
+      if def' == def && t' == t && ty' == ty then c
+      else mkArray(u,t',def',ty')
 
 let map_under_context_with_full_binders sigma g f l n d =
   let open EConstr in
@@ -738,6 +744,11 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
       else mkCoFix (ln,(lna,tl',bl'))
+  | Array(u,t,def,ty) ->
+      let t' = Array.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 cstr else mkArray (u,t', def',ty')
 
 let map_constr_with_full_binders sigma g f =
   map_constr_with_full_binders_gen false sigma g f
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index f06aeaf54e..335c2e5e68 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -151,6 +151,13 @@ let nf_evars_and_universes_opt_subst f subst =
       let univs' = Instance.subst_fn lsubst univs in
       if univs' == univs then Constr.map aux c
       else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},t,br))
+    | Array (u,elems,def,ty) ->
+      let u' = Univ.Instance.subst_fn lsubst u in
+      let elems' = CArray.Smart.map aux elems in
+      let def' = aux def in
+      let ty' = aux ty in
+      if u == u' && elems == elems' && def == def' && ty == ty' then c
+      else mkArray (u',elems',def',ty')
     | _ -> Constr.map aux c
   in aux