From 0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 3 Feb 2020 18:19:42 +0100 Subject: 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 Co-authored-by: Gaëtan Gilbert --- engine/termops.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'engine/termops.ml') 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 -- cgit v1.2.3