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, 15 insertions, 10 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