src/containers/dynamic_array.bend
bend-collections-laws-containers@1.0.0.0 · 692 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/math/pow2.bend as P2
3import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as E
4
5# Growable, bounds-checked array over native Base.Array.
6# DynArray<&2, T> is the existing Data API; DynArray<T> stores owning Type
7# elements through the _owned API below. See docs/DYNAMIC_ARRAY_OWNERSHIP.md.
8#
9# Representation: DA{limit, depth, cap, length, slots} with cap = 2^depth kept
10# in the record (recomputing 2^depth per operation would make every push,
11# capacity and reserve cost O(depth)). `slots` is a Base.Array of
12# 2^depth slots. ALeaf/ANode is the LOGICAL model the checker reasons about;
13# stock Bend 2.0.16 lowers a Base.Array to one indexed memory block, and
14# get/set/swap compile to a `blk_at` index computation plus a direct
15# `blk_read`/`blk_write` (docs/C_EQUIVALENCE.md). Slots [0, length)
16# hold Some{x}; the rest hold None. Capacity is 2^depth. `limit` (<= 31) caps
17# depth, so every capacity is representable as the U32 size Base computes, and
18# every index passed to Base is < 2^depth <= 2^31 (so Base's masking is the
19# identity). Out-of-range indices never reach Base.
20#
21# Errors return the state unchanged (see docs/API.md):
22# get/set out of range -> IndexOutOfRange; pop on empty -> EmptyArray;
23# push/reserve beyond 2^limit -> CapacityExceeded.
24# Cost (n = length, c = capacity): get/set/push/pop are one indexed load or
25# store into the block (no tree descent in the native lowering), growth O(c)
26# (a fresh half is allocated and the merged block copied, like a C realloc),
27# reserve O(target capacity), clear O(n), to_list O(c).
28
29type DynArray<a, -T: Kind(a)> is Type:
30 DA{limit: Nat, depth: Nat, cap: Nat, length: Nat, slots: Array<Maybe<a, T>>}
31
32def max_depth() -> Nat:
33 31n
34
35# 2^d (structural doubling; Base Nat.pow is avoided, see docs/VALIDATION.md).
36def pow2(d: Nat) -> Nat:
37 match d:
38 case 0n:
39 1n
40 case 1n+p:
41 Nat.double(pow2(p))
42
43def empty_slots(-T: Data, +depth: Nat) -> Array<Maybe<&2, T>>:
44 Array.new(Maybe<&2, T>, depth, None{})
45
46def new(-T: Data) -> DynArray<&2, T>:
47 DA{max_depth(), 0n, 1n, 0n, empty_slots(T, 0n)}
48
49# Depth limit min(k, 31). (Written with an explicit match: Base Nat.min is a
50# Bool.pick over shared arguments, which miscompiled at runtime; docs/VALIDATION.md.)
51def clamp_limit(k: Nat, small: Bool) -> Nat:
52 match small:
53 case True{}:
54 k
55 case False{}:
56 max_depth()
57
58# Same as new, with capacity bounded by 2^min(k, 31).
59def with_limit(-T: Data, +k: Nat) -> DynArray<&2, T>:
60 DA{clamp_limit(k, Nat.is_lt(k, max_depth())), 0n, 1n, 0n, empty_slots(T, 0n)}
61
62def length(-T: Data, da: DynArray<&2, T>) -> DynArray<&2, T> & Nat:
63 DA{limit, depth, cap, +len, arr} = da
64 (DA{limit, depth, cap, len, arr}, len)
65
66def capacity(-T: Data, da: DynArray<&2, T>) -> DynArray<&2, T> & Nat:
67 DA{limit, depth, +cap, len, arr} = da
68 (DA{limit, depth, cap, len, arr}, cap)
69
70def slot_result(-T: Data, slot: Maybe<&2, T>) -> Result<&2, &2, E.Error, T>:
71 match slot:
72 case None{}:
73 Fail{E.IndexOutOfRange{}}
74 case Some{x}:
75 Done{x}
76
77# ---- get ----
78
79def get_found(-T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
80 (arr, slot) = r
81 (DA{limit, depth, cap, len, arr}, slot_result(T, slot))
82
83def get_checked(-T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, i: Nat, ok: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
84 match ok:
85 case True{}:
86 get_found(T, limit, depth, cap, len, Array.get(Maybe<&2, T>, arr, U32.from_nat(i)))
87 case False{}:
88 (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
89
90def get(-T: Data, da: DynArray<&2, T>, +i: Nat) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
91 DA{limit, depth, cap, +len, arr} = da
92 get_checked(T, limit, depth, cap, len, arr, i, Nat.is_lt(i, len))
93
94# ---- set ----
95
96def set_checked(-T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, i: Nat, v: T, ok: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
97 match ok:
98 case True{}:
99 (DA{limit, depth, cap, len, Array.set(Maybe<&2, T>, arr, U32.from_nat(i), Some{v})}, Done{Unit{}})
100 case False{}:
101 (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
102
103def set(-T: Data, da: DynArray<&2, T>, +i: Nat, v: T) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
104 DA{limit, depth, cap, +len, arr} = da
105 set_checked(T, limit, depth, cap, len, arr, i, v, Nat.is_lt(i, len))
106
107# ---- growth ----
108
109# Doubling: the old tree becomes the left half of a tree one level deeper.
110def grown(-T: Data, +depth: Nat, arr: Array<Maybe<&2, T>>) -> Array<Maybe<&2, T>>:
111 ANode{arr, empty_slots(T, depth)}
112
113def push_room(-T: Data, limit: Nat, +depth: Nat, +cap: Nat, +len: Nat, arr: Array<Maybe<&2, T>>, v: T, room: Bool, grow: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
114 match room grow:
115 case True{} _:
116 (DA{limit, depth, cap, 1n+len, Array.set(Maybe<&2, T>, arr, U32.from_nat(len), Some{v})}, Done{Unit{}})
117 case False{} True{}:
118 (DA{limit, 1n+depth, Nat.double(cap), 1n+len, Array.set(Maybe<&2, T>, grown(T, depth, arr), U32.from_nat(len), Some{v})}, Done{Unit{}})
119 case False{} False{}:
120 (DA{limit, depth, cap, len, arr}, Fail{E.CapacityExceeded{}})
121
122def push(-T: Data, da: DynArray<&2, T>, v: T) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
123 DA{+limit, +depth, +cap, +len, arr} = da
124 push_room(T, limit, depth, cap, len, arr, v, Nat.is_lt(len, cap), Nat.is_lt(depth, limit))
125
126# ---- pop ----
127
128def pop_found(-T: Data, limit: Nat, depth: Nat, +cap: Nat, m: Nat, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
129 (arr, old) = r
130 (DA{limit, depth, cap, m, arr}, slot_result(T, old))
131
132def pop_len(-T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
133 match len:
134 case 0n:
135 (DA{limit, depth, cap, 0n, arr}, Fail{E.EmptyArray{}})
136 case 1n+ +m:
137 pop_found(T, limit, depth, cap, m, Array.swap(Maybe<&2, T>, arr, U32.from_nat(m), None{}))
138
139def pop(-T: Data, da: DynArray<&2, T>) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
140 DA{limit, depth, cap, len, arr} = da
141 pop_len(T, limit, depth, cap, len, arr)
142
143# ---- reserve ----
144
145def grow_if(-T: Data, limit: Nat, +depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, fits: Bool) -> DynArray<&2, T>:
146 match fits:
147 case True{}:
148 DA{limit, depth, cap, len, arr}
149 case False{}:
150 DA{limit, 1n+depth, Nat.double(cap), len, grown(T, depth, arr)}
151
152def grow_step(-T: Data, +n: Nat, st: DynArray<&2, T>) -> DynArray<&2, T>:
153 DA{limit, +depth, +cap, len, arr} = st
154 grow_if(T, limit, depth, cap, len, arr, Nat.is_le(n, cap))
155
156# Doubles until n fits; `fuel` = limit - depth bounds the number of doublings.
157def grow_until(-T: Data, fuel: Nat, +n: Nat, st: DynArray<&2, T>) -> DynArray<&2, T>:
158 match fuel:
159 case 0n:
160 st
161 case 1n+f:
162 grow_until(T, f, n, grow_step(T, n, st))
163
164# The feasibility test (n <= 2^limit) is only reached when the cached capacity
165# does not already suffice: computing 2^limit is O(limit) and reserve is
166# otherwise O(1).
167def reserve_room(-T: Data, +limit: Nat, +depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, +n: Nat, feasible: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
168 match feasible:
169 case True{}:
170 (grow_until(T, Nat.sub(limit, depth), n, DA{limit, depth, cap, len, arr}), Done{Unit{}})
171 case False{}:
172 (DA{limit, depth, cap, len, arr}, Fail{E.CapacityExceeded{}})
173
174def reserve_checked(-T: Data, +limit: Nat, +depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, +n: Nat, fits: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
175 match fits:
176 case True{}:
177 (DA{limit, depth, cap, len, arr}, Done{Unit{}})
178 case False{}:
179 reserve_room(T, limit, depth, cap, len, arr, n, Nat.is_le(n, pow2(limit)))
180
181# Ensures capacity >= n (new capacity: least 2^k >= n with k >= depth).
182def reserve(-T: Data, da: DynArray<&2, T>, +n: Nat) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
183 DA{+limit, +depth, +cap, len, arr} = da
184 reserve_checked(T, limit, depth, cap, len, arr, n, Nat.is_le(n, cap))
185
186# ---- clear / to_list ----
187
188# Keeps the capacity; all slots become None.
189def clear(-T: Data, da: DynArray<&2, T>) -> DynArray<&2, T>:
190 DA{limit, +depth, +cap, len, arr} = da
191 DA{limit, depth, cap, 0n, empty_slots(T, depth)}
192
193# to_list walks the occupied slots BY INDEX, newest first, and conses them:
194# the walk gives the array back, so nothing is cloned, and a `Base.Array` is
195# never matched structurally (that destroys the flat representation, see
196# docs/VALIDATION.md).
197def cons_some(-T: Data, x: Maybe<&2, T>, acc: List<&2, T>) -> List<&2, T>:
198 match x:
199 case None{}:
200 acc
201 case Some{v}:
202 Con{v, acc}
203
204def dec1(n: Nat) -> Nat:
205 match n:
206 case 0n:
207 0n
208 case 1n+p:
209 p
210
211# k slots are still to be read, the last of them first: the pair `r` is slot
212# k - 1, already read.
213def tl_go(k: Nat, -T: Data, acc: List<&2, T>, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> Array<Maybe<&2, T>> & List<&2, T>:
214 match k r:
215 case 0n Tuple{a, x}:
216 (a, acc)
217 case 1n+ +m Tuple{a, x}:
218 tl_go(m, T, cons_some(T, x, acc), Array.get(Maybe<&2, T>, a, U32.from_nat(dec1(m))))
219
220def tl_done(-T: Data, limit: Nat, depth: Nat, +cap: Nat, +len: Nat, r: Array<Maybe<&2, T>> & List<&2, T>) -> DynArray<&2, T> & List<&2, T>:
221 (a, xs) = r
222 (DA{limit, depth, cap, len, a}, xs)
223
224def tl_start(-T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>) -> DynArray<&2, T> & List<&2, T>:
225 match len:
226 case 0n:
227 (DA{limit, depth, cap, 0n, arr}, Nil{})
228 case 1n+ +m:
229 tl_done(T, limit, depth, cap, 1n+m, tl_go(1n+m, T, Nil{}, Array.get(Maybe<&2, T>, arr, U32.from_nat(m))))
230
231def to_list(-T: Data, da: DynArray<&2, T>) -> DynArray<&2, T> & List<&2, T>:
232 DA{limit, depth, +cap, len, arr} = da
233 tl_start(T, limit, depth, cap, len, arr)
234
235# ---- operation traces ----
236
237def obs_nat(-T: Data, r: DynArray<&2, T> & Nat) -> DynArray<&2, T> & E.Obs<T>:
238 (d, n) = r
239 (d, E.ONat{n})
240
241def obs_item(-T: Data, r: DynArray<&2, T> & Result<&2, &2, E.Error, T>) -> DynArray<&2, T> & E.Obs<T>:
242 (d, x) = r
243 (d, E.OItem{x})
244
245def obs_unit(-T: Data, r: DynArray<&2, T> & Result<&2, &2, E.Error, Unit>) -> DynArray<&2, T> & E.Obs<T>:
246 (d, x) = r
247 (d, E.OUnit{x})
248
249def obs_list(-T: Data, r: DynArray<&2, T> & List<&2, T>) -> DynArray<&2, T> & E.Obs<T>:
250 (d, xs) = r
251 (d, E.OList{xs})
252
253def step(-T: Data, da: DynArray<&2, T>, op: E.Op<T>) -> DynArray<&2, T> & E.Obs<T>:
254 match op:
255 case E.Length{}:
256 obs_nat(T, length(T, da))
257 case E.Capacity{}:
258 obs_nat(T, capacity(T, da))
259 case E.Get{i}:
260 obs_item(T, get(T, da, i))
261 case E.Set{i, v}:
262 obs_unit(T, set(T, da, i, v))
263 case E.Push{v}:
264 obs_unit(T, push(T, da, v))
265 case E.Pop{}:
266 obs_item(T, pop(T, da))
267 case E.Reserve{n}:
268 obs_unit(T, reserve(T, da, n))
269 case E.Clear{}:
270 (clear(T, da), E.OUnit{Done{Unit{}}})
271 case E.ToList{}:
272 obs_list(T, to_list(T, da))
273
274def record(-T: Data, acc: List<&2, E.Obs<T>>, r: DynArray<&2, T> & E.Obs<T>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
275 (da, o) = r
276 (da, Con{o, acc})
277
278def step_acc(-T: Data, op: E.Op<T>, st: DynArray<&2, T> & List<&2, E.Obs<T>>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
279 (da, acc) = st
280 record(T, acc, step(T, da, op))
281
282# Runs ops left to right; observations are accumulated newest-first.
283def run_acc(-T: Data, ops: List<&2, E.Op<T>>, st: DynArray<&2, T> & List<&2, E.Obs<T>>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
284 match ops:
285 case Nil{}:
286 st
287 case Con{op, rest}:
288 run_acc(T, rest, step_acc(T, op, st))
289
290def finish(-T: Data, st: DynArray<&2, T> & List<&2, E.Obs<T>>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
291 (da, acc) = st
292 (da, List.reverse(&2, E.Obs<T>, acc))
293
294# Final state and the observation of every operation, in order.
295def run(-T: Data, ops: List<&2, E.Op<T>>, da: DynArray<&2, T>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
296 finish(T, run_acc(T, ops, (da, Nil{})))
297
298# ---- executable specializations at a closed element type ----
299#
300# Bend 2.0.16's native C backend miscompiles Base.Array operations whose
301# element type is still open (an erased `-T` parameter): `Array.new` at a bare
302# type variable is rejected outright ("an open Array element type"), and
303# `Array.get`/`Array.set`/`Array.swap`/`Array.clone` under `Maybe<&2, T>`
304# silently read back wrong data for any element that is not a machine
305# immediate. See docs/VALIDATION.md and tests/runtime_defects/.
306#
307# The definitions above stay parametric, so their proofs are universal in T.
308# The `*_at` definitions below are template specializations: `~T` is a
309# compile-time parameter, so every Base.Array call is compiled at a closed
310# element type. They are the entry points used by tests and benchmarks, and
311# proofs/dynamic_array/closed.bend proves each of them equal to the
312# parametric definition at its instance, so every law above transfers.
313#
314# Only the definitions that (transitively) reach a Base.Array call need a
315# specialization; the purely structural helpers are shared.
316
317def empty_slots_at(~T: Data, +depth: Nat) -> Array<Maybe<&2, T>>:
318 Array.new(Maybe<&2, T>, depth, None{})
319
320def new_at(~T: Data) -> DynArray<&2, T>:
321 DA{max_depth(), 0n, 1n, 0n, empty_slots_at(~T, 0n)}
322
323def with_limit_at(~T: Data, +k: Nat) -> DynArray<&2, T>:
324 DA{clamp_limit(k, Nat.is_lt(k, max_depth())), 0n, 1n, 0n, empty_slots_at(~T, 0n)}
325
326# Keep the element type specialized through the returned payload. Calling the
327# erased generic get_found here boxes composite Data on every indexed read.
328def get_found_at(~T: Data, limit: Nat, depth: Nat, cap: Nat, len: Nat, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
329 match r:
330 case Tuple{arr, None{}}:
331 (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
332 case Tuple{arr, Some{x}}:
333 (DA{limit, depth, cap, len, arr}, Done{x})
334
335def get_checked_at(~T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, i: Nat, ok: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
336 match ok:
337 case True{}:
338 get_found_at(~T, limit, depth, cap, len, Array.get(Maybe<&2, T>, arr, U32.from_nat(i)))
339 case False{}:
340 (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
341
342def get_at(~T: Data, da: DynArray<&2, T>, +i: Nat) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
343 DA{limit, depth, cap, +len, arr} = da
344 get_checked_at(~T, limit, depth, cap, len, arr, i, Nat.is_lt(i, len))
345
346def set_checked_at(~T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, i: Nat, v: T, ok: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
347 match ok:
348 case True{}:
349 (DA{limit, depth, cap, len, Array.set(Maybe<&2, T>, arr, U32.from_nat(i), Some{v})}, Done{Unit{}})
350 case False{}:
351 (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
352
353def set_at(~T: Data, da: DynArray<&2, T>, +i: Nat, v: T) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
354 DA{limit, depth, cap, +len, arr} = da
355 set_checked_at(~T, limit, depth, cap, len, arr, i, v, Nat.is_lt(i, len))
356
357def grown_at(~T: Data, +depth: Nat, arr: Array<Maybe<&2, T>>) -> Array<Maybe<&2, T>>:
358 ANode{arr, empty_slots_at(~T, depth)}
359
360def push_room_at(~T: Data, limit: Nat, +depth: Nat, +cap: Nat, +len: Nat, arr: Array<Maybe<&2, T>>, v: T, room: Bool, grow: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
361 match room grow:
362 case True{} _:
363 (DA{limit, depth, cap, 1n+len, Array.set(Maybe<&2, T>, arr, U32.from_nat(len), Some{v})}, Done{Unit{}})
364 case False{} True{}:
365 (DA{limit, 1n+depth, Nat.double(cap), 1n+len, Array.set(Maybe<&2, T>, grown_at(~T, depth, arr), U32.from_nat(len), Some{v})}, Done{Unit{}})
366 case False{} False{}:
367 (DA{limit, depth, cap, len, arr}, Fail{E.CapacityExceeded{}})
368
369def push_at(~T: Data, da: DynArray<&2, T>, v: T) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
370 DA{+limit, +depth, +cap, +len, arr} = da
371 push_room_at(~T, limit, depth, cap, len, arr, v, Nat.is_lt(len, cap), Nat.is_lt(depth, limit))
372
373def pop_len_at(~T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
374 match len:
375 case 0n:
376 (DA{limit, depth, cap, 0n, arr}, Fail{E.EmptyArray{}})
377 case 1n+ +m:
378 pop_found(T, limit, depth, cap, m, Array.swap(Maybe<&2, T>, arr, U32.from_nat(m), None{}))
379
380def pop_at(~T: Data, da: DynArray<&2, T>) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
381 DA{limit, depth, cap, len, arr} = da
382 pop_len_at(~T, limit, depth, cap, len, arr)
383
384def grow_if_at(~T: Data, limit: Nat, +depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, fits: Bool) -> DynArray<&2, T>:
385 match fits:
386 case True{}:
387 DA{limit, depth, cap, len, arr}
388 case False{}:
389 DA{limit, 1n+depth, Nat.double(cap), len, grown_at(~T, depth, arr)}
390
391def grow_step_at(~T: Data, +n: Nat, st: DynArray<&2, T>) -> DynArray<&2, T>:
392 DA{limit, +depth, +cap, len, arr} = st
393 grow_if_at(~T, limit, depth, cap, len, arr, Nat.is_le(n, cap))
394
395def grow_until_at(~T: Data, fuel: Nat, +n: Nat, st: DynArray<&2, T>) -> DynArray<&2, T>:
396 match fuel:
397 case 0n:
398 st
399 case 1n+f:
400 grow_until_at(~T, f, n, grow_step_at(~T, n, st))
401
402# The feasibility test (n <= 2^limit) is only reached when the cached capacity
403# does not already suffice: computing 2^limit is O(limit) and reserve is
404# otherwise O(1).
405def reserve_room_at(~T: Data, +limit: Nat, +depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, +n: Nat, feasible: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
406 match feasible:
407 case True{}:
408 (grow_until_at(~T, Nat.sub(limit, depth), n, DA{limit, depth, cap, len, arr}), Done{Unit{}})
409 case False{}:
410 (DA{limit, depth, cap, len, arr}, Fail{E.CapacityExceeded{}})
411
412def reserve_checked_at(~T: Data, +limit: Nat, +depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, +n: Nat, fits: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
413 match fits:
414 case True{}:
415 (DA{limit, depth, cap, len, arr}, Done{Unit{}})
416 case False{}:
417 reserve_room_at(~T, limit, depth, cap, len, arr, n, Nat.is_le(n, P2.pow2t(limit)))
418
419def reserve_at(~T: Data, da: DynArray<&2, T>, +n: Nat) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
420 DA{+limit, +depth, +cap, len, arr} = da
421 reserve_checked_at(~T, limit, depth, cap, len, arr, n, Nat.is_le(n, cap))
422
423# The executable clear resets the occupied slots [0, length) to None, top
424# down, and keeps the block: O(length), no allocation. Dropping the old block
425# and allocating a fresh one (what the parametric `clear` describes) walks
426# every one of the 2^depth slots twice in the runtime. Every slot at or past
427# the length already holds None, so the result is the same all-None block;
428# proofs/containers/dynamic_array/clear.bend proves it on every good state.
429def clear_go_at(~T: Data, k: Nat, arr: Array<Maybe<&2, T>>) -> Array<Maybe<&2, T>>:
430 match k:
431 case 0n:
432 arr
433 case 1n+ +m:
434 clear_go_at(~T, m, Array.set(Maybe<&2, T>, arr, U32.from_nat(m), None{}))
435
436def clear_at(~T: Data, da: DynArray<&2, T>) -> DynArray<&2, T>:
437 DA{+limit, +depth, +cap, len, arr} = da
438 DA{limit, depth, cap, 0n, clear_go_at(~T, len, arr)}
439
440# The executable to_list is the same indexed walk, compiled at a closed
441# element type; proofs/dynamic_array/closed.bend proves the two agree.
442def tl_go_at(~T: Data, k: Nat, acc: List<&2, T>, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> Array<Maybe<&2, T>> & List<&2, T>:
443 match k r:
444 case 0n Tuple{a, x}:
445 (a, acc)
446 case 1n+ +m Tuple{a, x}:
447 tl_go_at(~T, m, cons_some(T, x, acc), Array.get(Maybe<&2, T>, a, U32.from_nat(dec1(m))))
448
449def tl_start_at(~T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>) -> DynArray<&2, T> & List<&2, T>:
450 match len:
451 case 0n:
452 (DA{limit, depth, cap, 0n, arr}, Nil{})
453 case 1n+ +m:
454 tl_done(T, limit, depth, cap, 1n+m, tl_go_at(~T, 1n+m, Nil{}, Array.get(Maybe<&2, T>, arr, U32.from_nat(m))))
455
456def to_list_at(~T: Data, da: DynArray<&2, T>) -> DynArray<&2, T> & List<&2, T>:
457 DA{limit, depth, +cap, len, arr} = da
458 tl_start_at(~T, limit, depth, cap, len, arr)
459
460def step_at(~T: Data, da: DynArray<&2, T>, op: E.Op<T>) -> DynArray<&2, T> & E.Obs<T>:
461 match op:
462 case E.Length{}:
463 obs_nat(T, length(T, da))
464 case E.Capacity{}:
465 obs_nat(T, capacity(T, da))
466 case E.Get{i}:
467 obs_item(T, get_at(~T, da, i))
468 case E.Set{i, v}:
469 obs_unit(T, set_at(~T, da, i, v))
470 case E.Push{v}:
471 obs_unit(T, push_at(~T, da, v))
472 case E.Pop{}:
473 obs_item(T, pop_at(~T, da))
474 case E.Reserve{n}:
475 obs_unit(T, reserve_at(~T, da, n))
476 case E.Clear{}:
477 (clear_at(~T, da), E.OUnit{Done{Unit{}}})
478 case E.ToList{}:
479 obs_list(T, to_list_at(~T, da))
480
481def step_acc_at(~T: Data, op: E.Op<T>, st: DynArray<&2, T> & List<&2, E.Obs<T>>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
482 (da, acc) = st
483 record(T, acc, step_at(~T, da, op))
484
485def run_acc_at(~T: Data, ops: List<&2, E.Op<T>>, st: DynArray<&2, T> & List<&2, E.Obs<T>>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
486 match ops:
487 case Nil{}:
488 st
489 case Con{op, rest}:
490 run_acc_at(~T, rest, step_acc_at(~T, op, st))
491
492def run_at(~T: Data, ops: List<&2, E.Op<T>>, da: DynArray<&2, T>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
493 finish(T, run_acc_at(~T, ops, (da, Nil{})))
494
495# ---- owning elements (Type) ----
496# Same DA representation and native Base.Array storage. No operation copies T.
497# Data clients keep their existing get/to_list API at quantity &2. Owning
498# clients use quantity &1 and move values with pop/swap/update/into_list.
499# A failed push or swap returns the supplied value in E.Rejected.
500
501# Stock Array.new requires Data. This fresh-empty initializer is O(c log c)
502# in the native backend because ANode merges blocks; see ownership docs.
503def empty_owned(~T: Type, depth: Nat) -> Array<Maybe<&1, T>>:
504 match depth:
505 case 0n:
506 ALeaf{None{}}
507 case 1n+ +p:
508 ANode{empty_owned(~T, p), empty_owned(~T, p)}
509
510def new_owned(~T: Type) -> DynArray<&1, T>:
511 DA{max_depth(), 0n, 1n, 0n, empty_owned(~T, 0n)}
512
513def with_limit_owned(~T: Type, +k: Nat) -> DynArray<&1, T>:
514 DA{clamp_limit(k, Nat.is_lt(k, max_depth())), 0n, 1n, 0n, empty_owned(~T, 0n)}
515
516def length_owned(~T: Type, da: DynArray<&1, T>) -> DynArray<&1, T> & Nat:
517 DA{limit, depth, cap, +len, arr} = da
518 (DA{limit, depth, cap, len, arr}, len)
519
520def capacity_owned(~T: Type, da: DynArray<&1, T>) -> DynArray<&1, T> & Nat:
521 DA{limit, depth, +cap, len, arr} = da
522 (DA{limit, depth, cap, len, arr}, cap)
523
524def grown_owned(~T: Type, +depth: Nat, arr: Array<Maybe<&1, T>>) -> Array<Maybe<&1, T>>:
525 ANode{arr, empty_owned(~T, depth)}
526
527def push_room_owned(~T: Type, limit: Nat, +depth: Nat, +cap: Nat, +len: Nat, arr: Array<Maybe<&1, T>>, v: T, room: Bool, grow: Bool) -> DynArray<&1, T> & Result<&1, &2, E.Rejected<T>, Unit>:
528 match room grow:
529 case True{} _:
530 (DA{limit, depth, cap, 1n+len, Array.set(Maybe<&1, T>, arr, U32.from_nat(len), Some{v})}, Done{Unit{}})
531 case False{} True{}:
532 (DA{limit, 1n+depth, Nat.double(cap), 1n+len, Array.set(Maybe<&1, T>, grown_owned(~T, depth, arr), U32.from_nat(len), Some{v})}, Done{Unit{}})
533 case False{} False{}:
534 (DA{limit, depth, cap, len, arr}, Fail{E.Rejected{E.CapacityExceeded{}, v}})
535
536def push_owned(~T: Type, da: DynArray<&1, T>, v: T) -> DynArray<&1, T> & Result<&1, &2, E.Rejected<T>, Unit>:
537 DA{+limit, +depth, +cap, +len, arr} = da
538 push_room_owned(~T, limit, depth, cap, len, arr, v, Nat.is_lt(len, cap), Nat.is_lt(depth, limit))
539
540def owned_result(~T: Type, slot: Maybe<&1, T>) -> Result<&2, &1, E.Error, T>:
541 match slot:
542 case None{}:
543 Fail{E.IndexOutOfRange{}}
544 case Some{x}:
545 Done{x}
546
547def pop_found_owned(~T: Type, limit: Nat, depth: Nat, cap: Nat, n: Nat, r: Array<Maybe<&1, T>> & Maybe<&1, T>) -> DynArray<&1, T> & Result<&2, &1, E.Error, T>:
548 (arr, old) = r
549 (DA{limit, depth, cap, n, arr}, owned_result(~T, old))
550
551def pop_len_owned(~T: Type, limit: Nat, depth: Nat, cap: Nat, len: Nat, arr: Array<Maybe<&1, T>>) -> DynArray<&1, T> & Result<&2, &1, E.Error, T>:
552 match len:
553 case 0n:
554 (DA{limit, depth, cap, 0n, arr}, Fail{E.EmptyArray{}})
555 case 1n+ +n:
556 pop_found_owned(~T, limit, depth, cap, n, Array.swap(Maybe<&1, T>, arr, U32.from_nat(n), None{}))
557
558def pop_owned(~T: Type, da: DynArray<&1, T>) -> DynArray<&1, T> & Result<&2, &1, E.Error, T>:
559 DA{limit, depth, cap, len, arr} = da
560 pop_len_owned(~T, limit, depth, cap, len, arr)
561
562# The result on success is the previous value. Invalid indices return v.
563# None can occur only in an invalid externally constructed DA representation.
564def swap_found_owned(~T: Type, limit: Nat, depth: Nat, cap: Nat, len: Nat, r: Array<Maybe<&1, T>> & Maybe<&1, T>) -> DynArray<&1, T> & Result<&1, &1, E.Rejected<T>, Maybe<&1, T>>:
565 (arr, old) = r
566 (DA{limit, depth, cap, len, arr}, Done{old})
567
568def swap_checked_owned(~T: Type, limit: Nat, depth: Nat, cap: Nat, len: Nat, arr: Array<Maybe<&1, T>>, i: Nat, v: T, ok: Bool) -> DynArray<&1, T> & Result<&1, &1, E.Rejected<T>, Maybe<&1, T>>:
569 match ok:
570 case True{}:
571 swap_found_owned(~T, limit, depth, cap, len, Array.swap(Maybe<&1, T>, arr, U32.from_nat(i), Some{v}))
572 case False{}:
573 (DA{limit, depth, cap, len, arr}, Fail{E.Rejected{E.IndexOutOfRange{}, v}})
574
575def swap_owned(~T: Type, da: DynArray<&1, T>, +i: Nat, v: T) -> DynArray<&1, T> & Result<&1, &1, E.Rejected<T>, Maybe<&1, T>>:
576 DA{limit, depth, cap, +len, arr} = da
577 swap_checked_owned(~T, limit, depth, cap, len, arr, i, v, Nat.is_lt(i, len))
578
579def set_done_owned(~T: Type, r: DynArray<T> & Result<&1, &1, E.Rejected<T>, Maybe<T>>) -> DynArray<T> & Result<&1, &2, E.Rejected<T>, Unit>:
580 match r:
581 case Tuple{da, Done{old}}:
582 (da, Done{Unit{}})
583 case Tuple{da, Fail{rejected}}:
584 (da, Fail{rejected})
585
586# Replace and release the previous element. Use swap_owned to retain it.
587def set_owned(~T: Type, da: DynArray<T>, i: Nat, value: T) -> DynArray<T> & Result<&1, &2, E.Rejected<T>, Unit>:
588 set_done_owned(~T, swap_owned(~T, da, i, value))
589
590# Scoped ownership: f receives the element and must return a replacement.
591# No placeholder escapes the call. f is not called for an invalid index.
592def update_put_owned(~T: Type, ~R: Type, limit: Nat, depth: Nat, cap: Nat, len: Nat, arr: Array<Maybe<&1, T>>, i: Nat, r: T & R) -> DynArray<&1, T> & Result<&2, &1, E.Error, R>:
593 (value, result) = r
594 (DA{limit, depth, cap, len, Array.set(Maybe<&1, T>, arr, U32.from_nat(i), Some{value})}, Done{result})
595
596def update_found_owned(~T: Type, ~R: Type, limit: Nat, depth: Nat, cap: Nat, len: Nat, i: Nat, f: T -> T & R, r: Array<Maybe<&1, T>> & Maybe<&1, T>) -> DynArray<&1, T> & Result<&2, &1, E.Error, R>:
597 match r:
598 case Tuple{arr, None{}}:
599 (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
600 case Tuple{arr, Some{x}}:
601 update_put_owned(~T, ~R, limit, depth, cap, len, arr, i, f(x))
602
603def update_checked_owned(~T: Type, ~R: Type, limit: Nat, depth: Nat, cap: Nat, len: Nat, arr: Array<Maybe<&1, T>>, +i: Nat, f: T -> T & R, ok: Bool) -> DynArray<&1, T> & Result<&2, &1, E.Error, R>:
604 match ok:
605 case False{}:
606 (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
607 case True{}:
608 update_found_owned(~T, ~R, limit, depth, cap, len, i, f, Array.swap(Maybe<&1, T>, arr, U32.from_nat(i), None{}))
609
610def update_owned(~T: Type, ~R: Type, da: DynArray<&1, T>, +i: Nat, f: T -> T & R) -> DynArray<&1, T> & Result<&2, &1, E.Error, R>:
611 DA{limit, depth, cap, +len, arr} = da
612 update_checked_owned(~T, ~R, limit, depth, cap, len, arr, i, f, Nat.is_lt(i, len))
613
614def grow_if_owned(~T: Type, limit: Nat, +depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&1, T>>, fits: Bool) -> DynArray<&1, T>:
615 match fits:
616 case True{}:
617 DA{limit, depth, cap, len, arr}
618 case False{}:
619 DA{limit, 1n+depth, Nat.double(cap), len, grown_owned(~T, depth, arr)}
620
621def grow_step_owned(~T: Type, +n: Nat, st: DynArray<&1, T>) -> DynArray<&1, T>:
622 DA{limit, +depth, +cap, len, arr} = st
623 grow_if_owned(~T, limit, depth, cap, len, arr, Nat.is_le(n, cap))
624
625def grow_until_owned(~T: Type, fuel: Nat, +n: Nat, st: DynArray<&1, T>) -> DynArray<&1, T>:
626 match fuel:
627 case 0n:
628 st
629 case 1n+f:
630 grow_until_owned(~T, f, n, grow_step_owned(~T, n, st))
631
632def reserve_room_owned(~T: Type, +limit: Nat, +depth: Nat, cap: Nat, len: Nat, arr: Array<Maybe<&1, T>>, +n: Nat, feasible: Bool) -> DynArray<&1, T> & Result<&2, &2, E.Error, Unit>:
633 match feasible:
634 case False{}:
635 (DA{limit, depth, cap, len, arr}, Fail{E.CapacityExceeded{}})
636 case True{}:
637 (grow_until_owned(~T, Nat.sub(limit, depth), n, DA{limit, depth, cap, len, arr}), Done{Unit{}})
638
639def reserve_checked_owned(~T: Type, +limit: Nat, depth: Nat, cap: Nat, len: Nat, arr: Array<Maybe<&1, T>>, +n: Nat, fits: Bool) -> DynArray<&1, T> & Result<&2, &2, E.Error, Unit>:
640 match fits:
641 case True{}:
642 (DA{limit, depth, cap, len, arr}, Done{Unit{}})
643 case False{}:
644 reserve_room_owned(~T, limit, depth, cap, len, arr, n, Nat.is_le(n, pow2(limit)))
645
646def reserve_owned(~T: Type, da: DynArray<&1, T>, +n: Nat) -> DynArray<&1, T> & Result<&2, &2, E.Error, Unit>:
647 DA{+limit, depth, +cap, len, arr} = da
648 reserve_checked_owned(~T, limit, depth, cap, len, arr, n, Nat.is_le(n, cap))
649
650def clear_owned(~T: Type, da: DynArray<&1, T>) -> DynArray<&1, T>:
651 DA{limit, +depth, cap, len, arr} = da
652 DA{limit, depth, cap, 0n, empty_owned(~T, depth)}
653
654def cons_owned(~T: Type, x: Maybe<&1, T>, acc: List<&1, T>) -> List<&1, T>:
655 match x:
656 case None{}:
657 acc
658 case Some{v}:
659 Con{v, acc}
660
661def drain_go_owned(~T: Type, k: Nat, acc: List<&1, T>, r: Array<Maybe<&1, T>> & Maybe<&1, T>) -> List<&1, T>:
662 match k r:
663 case 0n Tuple{arr, x}:
664 cons_owned(~T, x, acc)
665 case 1n+ +m Tuple{arr, x}:
666 drain_go_owned(~T, m, cons_owned(~T, x, acc), Array.swap(Maybe<&1, T>, arr, U32.from_nat(m), None{}))
667
668def drain_len_owned(~T: Type, len: Nat, arr: Array<Maybe<&1, T>>) -> List<&1, T>:
669 match len:
670 case 0n:
671 Nil{}
672 case 1n+ +m:
673 drain_go_owned(~T, m, Nil{}, Array.swap(Maybe<&1, T>, arr, U32.from_nat(m), None{}))
674
675# Consumes the container; values move into the returned list, in order.
676def into_list_owned(~T: Type, da: DynArray<&1, T>) -> List<&1, T>:
677 DA{limit, depth, cap, len, arr} = da
678 drain_len_owned(~T, len, arr)
679
680# Copyable-element exchange, used by indexed collection storage. The previous
681# value is returned and all other slots remain unchanged. Like set_at, an
682# invalid index leaves the array unchanged and reports IndexOutOfRange.
683def swap_checked_at(~T: Data, limit: Nat, depth: Nat, cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, i: Nat, v: T, ok: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
684 match ok:
685 case True{}:
686 get_found_at(~T, limit, depth, cap, len, Array.swap(Maybe<&2, T>, arr, U32.from_nat(i), Some{v}))
687 case False{}:
688 (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
689
690def swap_at(~T: Data, da: DynArray<&2, T>, +i: Nat, v: T) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
691 DA{limit, depth, cap, +len, arr} = da
692 swap_checked_at(~T, limit, depth, cap, len, arr, i, v, Nat.is_lt(i, len))