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, 31 insertions, 5 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3de2cb00a4..326bf0d6ad 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -156,21 +156,47 @@ let hcons_const_body cb =
   }
 
 (** {6 Inductive types } *)
+let eq_nested_type t1 t2 = match t1, t2 with
+| NestedInd ind1, NestedInd ind2 -> Names.eq_ind ind1 ind2
+| NestedInd _, _ -> false
+| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.equal c1 c2
+| NestedPrimitive _, _ -> false
 
 let eq_recarg r1 r2 = match r1, r2 with
 | Norec, Norec -> true
+| Norec, _ -> false
 | Mrec i1, Mrec i2 -> Names.eq_ind i1 i2
-| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2
-| _ -> false
+| Mrec _, _ -> false
+| Nested ty1, Nested ty2 -> eq_nested_type ty1 ty2
+| Nested _, _ -> false
+
+let pp_recarg = let open Pp in function
+  | Declarations.Norec -> str "Norec"
+  | Declarations.Mrec (mind,i) ->
+     str "Mrec[" ++ Names.MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
+  | Declarations.(Nested (NestedInd (mind,i))) ->
+     str "Nested[" ++ Names.MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
+  | Declarations.(Nested (NestedPrimitive c)) ->
+     str "Nested[" ++ Names.Constant.print c ++ str "]"
+
+let pp_wf_paths x = Rtree.pp_tree pp_recarg x
+
+let subst_nested_type sub ty = match ty with
+| NestedInd (kn,i) ->
+  let kn' = subst_mind sub kn in
+  if kn==kn' then ty else NestedInd (kn',i)
+| NestedPrimitive c ->
+  let c',_ = subst_con sub c in
+  if c==c' then ty else NestedPrimitive c'
 
 let subst_recarg sub r = match r with
   | Norec -> r
   | Mrec (kn,i) ->
     let kn' = subst_mind sub kn in
     if kn==kn' then r else Mrec (kn',i)
-  | Imbr (kn,i) ->
-    let kn' = subst_mind sub kn in
-    if kn==kn' then r else Imbr (kn',i)
+  | Nested ty ->
+    let ty' = subst_nested_type sub ty in
+    if ty==ty' then r else Nested ty'
 
 let mk_norec = Rtree.mk_node Norec [||]