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

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