1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/array.bend as AR
5	import ../../lib/list.bend as LL
6	import ../../../spec/lib/common.bend as SC
7	import ../../../src/containers/dynamic_array.bend as D
8	import ../../../src/containers/types/dynamic_array.bend as DE
9	import ../dynamic_array/layout.bend as LY
10	import ../dynamic_array/state.bend as DAS
11	import ./mk.bend as MK
12	import ./da.bend as DA
13	
14	# The dynamic array operations over canonical blocks of item lists.
15	
16	
17	def somes_mk(-T: Data, +d: Nat, +xs: List<&2, T>, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}) -> {LY.somes(T, AR.slots(Maybe<&2, T>, MK.mk(T, d, xs))) == xs : List<&2, T>}:
18	  %Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, MK.mk(T, d, xs)), MK.fill(T, SC.pow2(d), xs), MK.mk_slots(T, d, xs)) : {LY.somes(T, _) == xs : List<&2, T>}
19	  MK.fill_somes(T, SC.pow2(d), xs, hc)
20	
21	def good_mk(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}) -> {DAS.good(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}) == True{} : Bool}:
22	  +hlay = L.subst(List<&2, Maybe<&2, T>>, z => {LY.lay(T, z, SC.length(T, xs)) == True{} : Bool}, MK.fill(T, SC.pow2(d), xs), AR.slots(Maybe<&2, T>, MK.mk(T, d, xs)), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, MK.mk(T, d, xs)), MK.fill(T, SC.pow2(d), xs), MK.mk_slots(T, d, xs)), MK.fill_lay(T, SC.pow2(d), xs, hc))
23	  DAS.good_intro(T, l, d, SC.length(T, xs), MK.mk(T, d, xs), hl, hd, MK.mk_perfect(T, d, xs), hlay)
24	
25	
26	def blk_get(~T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat) -> {D.get_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), i) == (DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), DA.item(T, SC.nth(T, xs, i))) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}:
27	  %somes_mk(T, d, xs, hc) : {D.get_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), i) == (DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), DA.item(T, SC.nth(T, _, i))) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}
28	  DA.da_get(~T, l, d, SC.length(T, xs), MK.mk(T, d, xs), good_mk(T, l, d, xs, hl, hd, hc), i)
29	
30	def len_upd(-T: Data, +xs: List<&2, T>, +i: Nat, +v: T) -> {SC.length(T, SC.update(T, xs, i, v)) == SC.length(T, xs) : Nat}:
31	  LL.length_update(T, xs, i, v)
32	
33	def blk_set(~T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}) -> {D.set_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), i, v) == (DAS.real(T, DAS.Sh{l, d, SC.length(T, SC.update(T, xs, i, v)), MK.mk(T, d, SC.update(T, xs, i, v))}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}:
34	  +hi = L.subst(List<&2, T>, z => {Nat.is_lt(i, SC.length(T, z)) == True{} : Bool}, xs, LY.somes(T, AR.slots(Maybe<&2, T>, MK.mk(T, d, xs))), Equal.sym(List<&2, T>, LY.somes(T, AR.slots(Maybe<&2, T>, MK.mk(T, d, xs))), xs, somes_mk(T, d, xs, hc)), h)
35	  %Equal.sym(Nat, SC.length(T, SC.update(T, xs, i, v)), SC.length(T, xs), len_upd(T, xs, i, v)) : {D.set_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), i, v) == (DAS.real(T, DAS.Sh{l, d, _, MK.mk(T, d, SC.update(T, xs, i, v))}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
36	  %MK.mk_set(T, d, xs, i, v, h, hc) : {D.set_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), i, v) == (DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), _}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
37	  DA.da_set(~T, l, d, SC.length(T, xs), MK.mk(T, d, xs), good_mk(T, l, d, xs, hl, hd, hc), i, v, h)
38	
39	def blk_set_out(~T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == False{} : Bool}) -> {D.set_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), i, v) == (DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), Fail{DE.IndexOutOfRange{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}:
40	  DA.da_set_out(~T, l, d, SC.length(T, xs), MK.mk(T, d, xs), good_mk(T, l, d, xs, hl, hd, hc), i, v, h)
41	
42	def blk_swap(~T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}) -> {D.swap_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), i, v) == (DAS.real(T, DAS.Sh{l, d, SC.length(T, SC.update(T, xs, i, v)), MK.mk(T, d, SC.update(T, xs, i, v))}), DA.item(T, SC.nth(T, xs, i))) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}:
43	  %Equal.sym(Nat, SC.length(T, SC.update(T, xs, i, v)), SC.length(T, xs), len_upd(T, xs, i, v)) : {D.swap_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), i, v) == (DAS.real(T, DAS.Sh{l, d, _, MK.mk(T, d, SC.update(T, xs, i, v))}), DA.item(T, SC.nth(T, xs, i))) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}
44	  %MK.mk_set(T, d, xs, i, v, h, hc) : {D.swap_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), i, v) == (DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), _}), DA.item(T, SC.nth(T, xs, i))) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}
45	  %somes_mk(T, d, xs, hc) : {D.swap_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), i, v) == (DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), AR.upd(Maybe<&2, T>, d, MK.mk(T, d, xs), i, Some{v})}), DA.item(T, SC.nth(T, _, i))) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}
46	  DA.da_swap(~T, l, d, SC.length(T, xs), MK.mk(T, d, xs), good_mk(T, l, d, xs, hl, hd, hc), i, v, h)
47	
48	def blk_swap_out(~T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == False{} : Bool}) -> {D.swap_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), i, v) == (DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), Fail{DE.IndexOutOfRange{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}:
49	  DA.da_swap_out(~T, l, d, SC.length(T, xs), MK.mk(T, d, xs), good_mk(T, l, d, xs, hl, hd, hc), i, v, h)
50	
51	def len_snoc(-T: Data, +xs: List<&2, T>, +v: T) -> {SC.length(T, SC.snoc(T, xs, v)) == 1n+SC.length(T, xs) : Nat}:
52	  LL.length_snoc(T, xs, v)
53	
54	def blk_push_room(~T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}, +v: T, +hn: {Nat.is_lt(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}) -> {D.push_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), v) == (DAS.real(T, DAS.Sh{l, d, SC.length(T, SC.snoc(T, xs, v)), MK.mk(T, d, SC.snoc(T, xs, v))}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}:
55	  %Equal.sym(Nat, SC.length(T, SC.snoc(T, xs, v)), 1n+SC.length(T, xs), len_snoc(T, xs, v)) : {D.push_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), v) == (DAS.real(T, DAS.Sh{l, d, _, MK.mk(T, d, SC.snoc(T, xs, v))}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
56	  %MK.mk_push(T, d, xs, v, hn) : {D.push_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), v) == (DAS.real(T, DAS.Sh{l, d, 1n+SC.length(T, xs), _}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
57	  DA.da_push_room(~T, l, d, SC.length(T, xs), MK.mk(T, d, xs), good_mk(T, l, d, xs, hl, hd, hc), v, hn)
58	
59	def blk_push_grow(~T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}, +v: T, +hn: {Nat.is_lt(SC.length(T, xs), SC.pow2(d)) == False{} : Bool}, +hdl: {Nat.is_lt(d, l) == True{} : Bool}) -> {D.push_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), v) == (DAS.real(T, DAS.Sh{l, 1n+d, SC.length(T, SC.snoc(T, xs, v)), MK.mk(T, 1n+d, SC.snoc(T, xs, v))}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}:
60	  +hn1 = N.le_lt_trans(SC.length(T, xs), SC.pow2(d), SC.pow2(1n+d), hc, N.pow2_lt_succ(d))
61	  %Equal.sym(Nat, SC.length(T, SC.snoc(T, xs, v)), 1n+SC.length(T, xs), len_snoc(T, xs, v)) : {D.push_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), v) == (DAS.real(T, DAS.Sh{l, 1n+d, _, MK.mk(T, 1n+d, SC.snoc(T, xs, v))}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
62	  %MK.mk_push(T, 1n+d, xs, v, hn1) : {D.push_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), v) == (DAS.real(T, DAS.Sh{l, 1n+d, 1n+SC.length(T, xs), _}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
63	  %MK.mk_grow(T, d, xs, hc) : {D.push_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), v) == (DAS.real(T, DAS.Sh{l, 1n+d, 1n+SC.length(T, xs), AR.upd(Maybe<&2, T>, 1n+d, _, SC.length(T, xs), Some{v})}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
64	  DA.da_push_grow(~T, l, d, SC.length(T, xs), MK.mk(T, d, xs), good_mk(T, l, d, xs, hl, hd, hc), v, hn, hdl)
65	
66	def blk_push_full(~T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}, +v: T, +hn: {Nat.is_lt(SC.length(T, xs), SC.pow2(d)) == False{} : Bool}, +hdl: {Nat.is_lt(d, l) == False{} : Bool}) -> {D.push_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), v) == (DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)}), Fail{DE.CapacityExceeded{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}:
67	  DA.da_push_full(~T, l, d, SC.length(T, xs), MK.mk(T, d, xs), good_mk(T, l, d, xs, hl, hd, hc), v, hn, hdl)
68	
69	def blk_clear(~T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}) -> {D.clear_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)})) == DAS.real(T, DAS.Sh{l, d, 0n, MK.mk(T, d, Nil{})}) : D.DynArray<&2, T>}:
70	  %MK.mk_empty(T, d) : {D.clear_at(~T, DAS.real(T, DAS.Sh{l, d, SC.length(T, xs), MK.mk(T, d, xs)})) == DAS.real(T, DAS.Sh{l, d, 0n, _}) : D.DynArray<&2, T>}
71	  DA.da_clear(~T, l, d, SC.length(T, xs), MK.mk(T, d, xs), good_mk(T, l, d, xs, hl, hd, hc))