src/containers/internal/dlist_storage.bend
bend-collections-laws-containers@1.0.0.0 · 574 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/types/internal_dlist.bend as E
3
4# Doubly linked list with stable opaque handles, values of an erased type T.
5#
6# Representation: PARALLEL INDEXED ARENAS. Three `Base.Array` blocks of
7# 2^depth slots share one index space:
8# vals Maybe<T> the element stored at an id (None: never used or removed)
9# prevs U32 the LINK to the preceding element
10# nexts U32 the LINK to the following element
11# A link is id + 1, and `nil()` = 0 is the "no neighbour" link (as are the
12# head and tail fields), so testing for a neighbour is a comparison with 0
13# and following a link is one subtraction. Ids are slot indices below 2^31,
14# so id + 1 never wraps. The element id IS its slot index;
15# ids come from a monotone counter and are never reused, so a handle to a
16# removed element is stale (its `vals` slot is None) and a handle whose tag
17# differs from the list's is foreign. The blocks double when the counter
18# reaches the capacity (the old block becomes the lower half, so every id
19# keeps its slot), exactly as the dynamic array grows.
20#
21# The prev/next links are the doubly linked list's own links - what the
22# structure is for - stored as arena indices. Keeping them in their own
23# blocks makes relinking a neighbour ONE indexed write (no read-modify-write
24# of a node record). Nothing is stored in a search tree or a cons list.
25#
26# Cost (n = number of elements ever inserted): every handle operation and
27# push is O(1) indexed reads and writes; `length` is the cached count;
28# `to_list` reads O(count) slots. A push that finds the blocks full doubles
29# them (one `Base.Array` node and one fresh half per block), amortised O(1).
30# Because ids are never reused the blocks grow with n, not with the live
31# count - the same trade the reference C implementation makes.
32#
33# Errors: a foreign handle gives Fail{ForeignHandle}, a stale one
34# Fail{StaleHandle}; every failure returns the list unchanged.
35
36type DList<-T: Data> is Type:
37 DL{tag: U32, fresh: U32, free: U32, count: Nat, head: U32, tail: U32, depth: Nat, cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>}
38
39def nil() -> U32:
40 0
41
42# The link to an element, and the element a (non-nil) link points to.
43def link(+i: U32) -> U32:
44 U32.inc(i)
45
46def slot(+l: U32) -> U32:
47 U32.sub(l, 1)
48
49def new_vals(~T: Data, +depth: Nat) -> Array<Maybe<&2, T>>:
50 Array.new(Maybe<&2, T>, depth, None{})
51
52def new_links(+depth: Nat) -> Array<U32>:
53 Array.new(U32, depth, nil())
54
55def new(~T: Data, tag: U32) -> DList<T>:
56 DL{tag, 0, 0, 0n, nil(), nil(), 0n, 1, new_vals(~T, 0n), new_links(0n), new_links(0n)}
57
58# A link as the Maybe the public API reports.
59def pick_link(none: Bool, +l: U32) -> Maybe<&2, U32>:
60 match none:
61 case True{}:
62 None{}
63 case False{}:
64 Some{l}
65
66# ---- relinking ----
67
68# Point the link stored at element a (if a is a link, not nil) at q.
69def link_of(+l: U32) -> Maybe<&2, U32>:
70 pick_link(U32.is_eq(l, nil()), l)
71
72def set_next_go(nexts: Array<U32>, +a: U32, +q: U32, none: Bool) -> Array<U32>:
73 match none:
74 case True{}:
75 nexts
76 case False{}:
77 Array.set(U32, nexts, slot(a), q)
78
79# ---- insertion ----
80
81def set_next(nexts: Array<U32>, +a: U32, +q: U32) -> Array<U32>:
82 set_next_go(nexts, a, q, U32.is_eq(a, nil()))
83
84def grown_vals(~T: Data, +depth: Nat, a: Array<Maybe<&2, T>>) -> Array<Maybe<&2, T>>:
85 ANode{a, new_vals(~T, depth)}
86
87def grown_links(+depth: Nat, a: Array<U32>) -> Array<U32>:
88 ANode{a, new_links(depth)}
89
90# The end pointer after linking n next to a (nil: n becomes that end).
91def pick_end(none: Bool, +n: U32, +e: U32) -> U32:
92 match none:
93 case True{}:
94 n
95 case False{}:
96 e
97
98# Store x at slot n between the links a and b (either may be nil) and relink them.
99def link_in(~T: Data, +tag: U32, +n: U32, +nfresh: U32, +nfree: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +a: U32, +b: U32, x: T) -> DList<T> & E.Handle:
100 (DL{tag, nfresh, nfree, 1n+count, pick_end(U32.is_eq(a, nil()), link(n), head), pick_end(U32.is_eq(b, nil()), link(n), tail), depth, cap,
101 Array.set(Maybe<&2, T>, vals, n, Some{x}),
102 set_next(Array.set(U32, prevs, n, a), b, link(n)),
103 set_next(Array.set(U32, nexts, n, b), a, link(n))}, E.H{tag, n})
104
105def insert_room(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +a: U32, +b: U32, x: T, room: Bool) -> DList<T> & E.Handle:
106 match room:
107 case True{}:
108 link_in(~T, tag, fresh, U32.inc(fresh), free, count, head, tail, depth, cap, vals, prevs, nexts, a, b, x)
109 case False{}:
110 link_in(~T, tag, fresh, U32.inc(fresh), free, count, head, tail, 1n+depth, U32.shl(cap), grown_vals(~T, depth, vals), grown_links(depth, prevs), grown_links(depth, nexts), a, b, x)
111
112def insert_between(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +a: U32, +b: U32, x: T) -> DList<T> & E.Handle:
113 insert_room(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, a, b, x, U32.is_lt(fresh, cap))
114
115def length(~T: Data, s: DList<T>) -> DList<T> & Nat:
116 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
117 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, count)
118
119def push_front(~T: Data, s: DList<T>, x: T) -> DList<T> & E.Handle:
120 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
121 insert_between(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, nil(), head, x)
122
123def push_back(~T: Data, s: DList<T>, x: T) -> DList<T> & E.Handle:
124 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
125 insert_between(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, tail, nil(), x)
126
127def done_handle(~T: Data, r: DList<T> & E.Handle) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
128 (s, h) = r
129 (s, Done{h})
130
131# ---- validating a handle ----
132#
133# `live(i)` reads the value slot; every handle operation branches on it.
134
135def fail_same(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, e: E.Error) -> DList<T> & E.Error:
136 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, e)
137
138# The neighbour link on one side of a live element.
139def link_at(links: Array<U32>, +i: U32) -> Array<U32> & U32:
140 Array.get(U32, links, i)
141
142def ins_side(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +i: U32, +p: U32, +n: U32, x: T) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
143 match after:
144 case False{}:
145 done_handle(~T, insert_between(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, p, link(i), x))
146 case True{}:
147 done_handle(~T, insert_between(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, link(i), n, x))
148
149def ins_live2(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, +i: U32, x: T, pr: Array<U32> & U32, nx: Array<U32> & U32) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
150 (prevs, p) = pr
151 (nexts, n) = nx
152 ins_side(~T, after, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, p, n, x)
153
154def ins_found(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array<U32>, nexts: Array<U32>, +i: U32, x: T, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
155 (vals, m) = r
156 match m:
157 case None{}:
158 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}})
159 case Some{v}:
160 ins_live2(~T, after, tag, fresh, free, count, head, tail, depth, cap, vals, i, x, link_at(prevs, i), link_at(nexts, i))
161
162def insert_checked(~T: Data, after: Bool, ok: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +i: U32, x: T, same: Bool) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
163 match ok same:
164 case _ False{}:
165 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.ForeignHandle{}})
166 case False{} True{}:
167 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}})
168 case True{} True{}:
169 ins_found(~T, after, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, i, x, Array.get(Maybe<&2, T>, vals, i))
170
171def insert_before(~T: Data, s: DList<T>, h: E.Handle, x: T) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
172 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
173 E.H{+l, +i} = h
174 insert_checked(~T, False{}, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, x, U32.is_eq(l, tag))
175
176def insert_after(~T: Data, s: DList<T>, h: E.Handle, x: T) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
177 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
178 E.H{+l, +i} = h
179 insert_checked(~T, True{}, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, x, U32.is_eq(l, tag))
180
181# ---- removal ----
182
183def rm_links(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, +v: T, pr: Array<U32> & U32, nx: Array<U32> & U32) -> DList<T> & Result<&2, &2, E.Error, T>:
184 (prevs, +p) = pr
185 (nexts, +n) = nx
186 (DL{tag, fresh, free, Nat.sub(count, 1n), pick_end(U32.is_eq(p, nil()), n, head), pick_end(U32.is_eq(n, nil()), p, tail), depth, cap,
187 vals, set_next(prevs, n, p), set_next(nexts, p, n)}, Done{v})
188
189def rm_found(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array<U32>, nexts: Array<U32>, +i: U32, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> DList<T> & Result<&2, &2, E.Error, T>:
190 (vals, m) = r
191 match m:
192 case None{}:
193 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}})
194 case Some{+v}:
195 rm_links(~T, tag, fresh, free, count, head, tail, depth, cap, Array.set(Maybe<&2, T>, vals, i, None{}), v, link_at(prevs, i), link_at(nexts, i))
196
197def remove_checked(~T: Data, ok: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +i: U32, same: Bool) -> DList<T> & Result<&2, &2, E.Error, T>:
198 match ok same:
199 case _ False{}:
200 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.ForeignHandle{}})
201 case False{} True{}:
202 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}})
203 case True{} True{}:
204 rm_found(~T, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, i, Array.get(Maybe<&2, T>, vals, i))
205
206def remove(~T: Data, s: DList<T>, h: E.Handle) -> DList<T> & Result<&2, &2, E.Error, T>:
207 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
208 E.H{+l, +i} = h
209 remove_checked(~T, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, U32.is_eq(l, tag))
210
211# ---- reading and writing one element ----
212
213def value_of(~T: Data, m: Maybe<&2, T>) -> Result<&2, &2, E.Error, T>:
214 match m:
215 case None{}:
216 Fail{E.StaleHandle{}}
217 case Some{v}:
218 Done{v}
219
220def get_fin(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array<U32>, nexts: Array<U32>, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> DList<T> & Result<&2, &2, E.Error, T>:
221 (vals, m) = r
222 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, value_of(~T, m))
223
224def get_checked(~T: Data, ok: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +i: U32, same: Bool) -> DList<T> & Result<&2, &2, E.Error, T>:
225 match ok same:
226 case _ False{}:
227 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.ForeignHandle{}})
228 case False{} True{}:
229 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}})
230 case True{} True{}:
231 get_fin(~T, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, Array.get(Maybe<&2, T>, vals, i))
232
233def get(~T: Data, s: DList<T>, h: E.Handle) -> DList<T> & Result<&2, &2, E.Error, T>:
234 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
235 E.H{+l, +i} = h
236 get_checked(~T, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, U32.is_eq(l, tag))
237
238def set_fin(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array<U32>, nexts: Array<U32>, +i: U32, x: T, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> DList<T> & Result<&2, &2, E.Error, Unit>:
239 (vals, m) = r
240 match m:
241 case None{}:
242 (DL{tag, fresh, free, count, head, tail, depth, cap, Array.set(Maybe<&2, T>, vals, i, None{}), prevs, nexts}, Fail{E.StaleHandle{}})
243 case Some{v}:
244 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Done{Unit{}})
245
246# set swaps the new value in: one indexed access when the element is live;
247# a stale slot is None and is written back as None.
248def set_checked(~T: Data, ok: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +i: U32, +x: T, same: Bool) -> DList<T> & Result<&2, &2, E.Error, Unit>:
249 match ok same:
250 case _ False{}:
251 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.ForeignHandle{}})
252 case False{} True{}:
253 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}})
254 case True{} True{}:
255 set_fin(~T, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, i, x, Array.swap(Maybe<&2, T>, vals, i, Some{x}))
256
257def set(~T: Data, s: DList<T>, h: E.Handle, x: T) -> DList<T> & Result<&2, &2, E.Error, Unit>:
258 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
259 E.H{+l, +i} = h
260 set_checked(~T, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, x, U32.is_eq(l, tag))
261
262# ---- neighbours ----
263
264def handle_go(+tag: U32, +l: U32, none: Bool) -> Maybe<&2, E.Handle>:
265 match none:
266 case True{}:
267 None{}
268 case False{}:
269 Some{E.H{tag, slot(l)}}
270
271def handle(+tag: U32, +l: U32) -> Maybe<&2, E.Handle>:
272 handle_go(tag, l, U32.is_eq(l, nil()))
273
274def nbr_n(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, r: Array<U32> & U32) -> DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>:
275 (nexts, +n) = r
276 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Done{handle(tag, n)})
277
278def nbr_p(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, nexts: Array<U32>, r: Array<U32> & U32) -> DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>:
279 (prevs, +p) = r
280 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Done{handle(tag, p)})
281
282def nbr_fin(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +i: U32, m: Maybe<&2, T>) -> DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>:
283 match after m:
284 case _ None{}:
285 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}})
286 case True{} Some{v}:
287 nbr_n(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, link_at(nexts, i))
288 case False{} Some{v}:
289 nbr_p(~T, tag, fresh, free, count, head, tail, depth, cap, vals, nexts, link_at(prevs, i))
290
291def nbr_read(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array<U32>, nexts: Array<U32>, +i: U32, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>:
292 (vals, m) = r
293 nbr_fin(~T, after, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, m)
294
295def nbr_checked(~T: Data, after: Bool, ok: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +i: U32, same: Bool) -> DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>:
296 match ok same:
297 case _ False{}:
298 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.ForeignHandle{}})
299 case False{} True{}:
300 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}})
301 case True{} True{}:
302 nbr_read(~T, after, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, i, Array.get(Maybe<&2, T>, vals, i))
303
304def next(~T: Data, s: DList<T>, h: E.Handle) -> DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>:
305 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
306 E.H{+l, +i} = h
307 nbr_checked(~T, True{}, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, U32.is_eq(l, tag))
308
309def prev(~T: Data, s: DList<T>, h: E.Handle) -> DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>:
310 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
311 E.H{+l, +i} = h
312 nbr_checked(~T, False{}, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, U32.is_eq(l, tag))
313
314# ---- to_list ----
315#
316# Walk BACKWARDS from the tail, consing onto an accumulator, so the list
317# comes out in order and the walk is a tail call; the count bounds it.
318
319# One loop, no mutual recursion: the state carries the next id to read.
320type Cur<-T: Data> is Type:
321 C{vals: Array<Maybe<&2, T>>, prevs: Array<U32>, acc: List<&2, T>, at: U32}
322
323def step_p(~T: Data, vals: Array<Maybe<&2, T>>, acc: List<&2, T>, r: Array<U32> & U32) -> Cur<T>:
324 (prevs, p) = r
325 C{vals, prevs, acc, p}
326
327def step_m(~T: Data, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, acc: List<&2, T>, +at: U32, m: Maybe<&2, T>) -> Cur<T>:
328 match m:
329 case None{}:
330 C{vals, prevs, acc, nil()}
331 case Some{v}:
332 step_p(~T, vals, Con{v, acc}, Array.get(U32, prevs, slot(at)))
333
334def step_v(~T: Data, prevs: Array<U32>, acc: List<&2, T>, +at: U32, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> Cur<T>:
335 (vals, m) = r
336 step_m(~T, vals, prevs, acc, at, m)
337
338def step_back(~T: Data, c: Cur<T>) -> Cur<T>:
339 C{vals, prevs, acc, +at} = c
340 step_v(~T, prevs, acc, at, Array.get(Maybe<&2, T>, vals, slot(at)))
341
342def walk(~T: Data, fuel: Nat, c: Cur<T>) -> Cur<T>:
343 match fuel:
344 case 0n:
345 c
346 case 1n+f:
347 walk(~T, f, step_back(~T, c))
348
349def tl_fin(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, nexts: Array<U32>, c: Cur<T>) -> DList<T> & List<&2, T>:
350 C{vals, prevs, acc, at} = c
351 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, acc)
352
353def to_list(~T: Data, s: DList<T>) -> DList<T> & List<&2, T>:
354 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
355 tl_fin(~T, tag, fresh, free, count, head, tail, depth, cap, nexts, walk(~T, count, C{vals, prevs, Nil{}, tail}))
356
357# ---- recycling end operations: the deque's storage API ----
358#
359# `free` is a STACK of retired slots chained through `nexts`: the record's
360# field is the link to the top (nil() = empty) and `nexts[s]` of a retired
361# slot s is the link to the next retired one. A retired slot holds None in
362# `vals` and is not in the list.
363#
364# The handle-stable API above NEVER touches this stack: its ids come from the
365# monotone `fresh` counter and are never reused, so a handle to a removed
366# element stays unambiguously stale (the objective's handle contract). The
367# operations below DO recycle, and they are the storage operations
368# src/deque.bend runs on: a deque exposes no handles at all, so reissuing an
369# id is unobservable through it, and the arenas then grow with the PEAK
370# number of live elements instead of with the number of pushes. They are not
371# members of `Op`, so the list's trace laws are unaffected by them; they have
372# component laws under proofs/dlist/reuse_*.bend and free_chain.bend.
373# The general deque refinement is still being composed.
374#
375# Every one of them is O(1) indexed reads and writes.
376
377# Allocate the top of the free stack: `nx` is the link it stored, which
378# becomes the new top. `nexts[i]` is overwritten by `link_in`, after the read.
379def ins_free_pop(~T: Data, +tag: U32, +fresh: U32, +f: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, +a: U32, +b: U32, x: T, r: Array<U32> & U32) -> DList<T> & E.Handle:
380 (nexts, +nx) = r
381 link_in(~T, tag, slot(f), fresh, nx, count, head, tail, depth, cap, vals, prevs, nexts, a, b, x)
382
383def ins_free_pick(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +a: U32, +b: U32, x: T, empty: Bool) -> DList<T> & E.Handle:
384 match empty:
385 case True{}:
386 insert_between(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, a, b, x)
387 case False{}:
388 ins_free_pop(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, a, b, x, link_at(nexts, slot(free)))
389
390def insert_between_free(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +a: U32, +b: U32, x: T) -> DList<T> & E.Handle:
391 ins_free_pick(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, a, b, x, U32.is_eq(free, nil()))
392
393def push_front_free(~T: Data, s: DList<T>, x: T) -> DList<T> & E.Handle:
394 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
395 insert_between_free(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, nil(), head, x)
396
397def push_back_free(~T: Data, s: DList<T>, x: T) -> DList<T> & E.Handle:
398 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
399 insert_between_free(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, tail, nil(), x)
400
401# Unlink the element at slot i and push i on the free stack. `set_next` writes
402# at the NEIGHBOUR slots (both different from i), so the last write, which
403# stores the old top in nexts[i], cannot be overwritten.
404def rmf_links(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, +i: U32, v: T, pr: Array<U32> & U32, nx: Array<U32> & U32) -> DList<T> & Maybe<&2, T>:
405 (prevs, +p) = pr
406 (nexts, +n) = nx
407 (DL{tag, fresh, link(i), Nat.sub(count, 1n), pick_end(U32.is_eq(p, nil()), n, head), pick_end(U32.is_eq(n, nil()), p, tail), depth, cap,
408 vals, set_next(prevs, n, p), Array.set(U32, set_next(nexts, p, n), i, free)}, Some{v})
409
410def rmf_found(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array<U32>, nexts: Array<U32>, +i: U32, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> DList<T> & Maybe<&2, T>:
411 (vals, m) = r
412 match m:
413 case None{}:
414 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, None{})
415 case Some{v}:
416 rmf_links(~T, tag, fresh, free, count, head, tail, depth, cap, Array.set(Maybe<&2, T>, vals, i, None{}), i, v, link_at(prevs, i), link_at(nexts, i))
417
418def pop_end(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +l: U32, empty: Bool) -> DList<T> & Maybe<&2, T>:
419 match empty:
420 case True{}:
421 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, None{})
422 case False{}:
423 rmf_found(~T, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, slot(l), Array.get(Maybe<&2, T>, vals, slot(l)))
424
425def pop_front_free(~T: Data, s: DList<T>) -> DList<T> & Maybe<&2, T>:
426 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
427 pop_end(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, head, U32.is_eq(head, nil()))
428
429def pop_back_free(~T: Data, s: DList<T>) -> DList<T> & Maybe<&2, T>:
430 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
431 pop_end(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, tail, U32.is_eq(tail, nil()))
432
433def peek_fin(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array<U32>, nexts: Array<U32>, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> DList<T> & Maybe<&2, T>:
434 (vals, m) = r
435 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, m)
436
437def peek_end(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +l: U32, empty: Bool) -> DList<T> & Maybe<&2, T>:
438 match empty:
439 case True{}:
440 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, None{})
441 case False{}:
442 peek_fin(~T, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, Array.get(Maybe<&2, T>, vals, slot(l)))
443
444def peek_front(~T: Data, s: DList<T>) -> DList<T> & Maybe<&2, T>:
445 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
446 peek_end(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, head, U32.is_eq(head, nil()))
447
448def peek_back(~T: Data, s: DList<T>) -> DList<T> & Maybe<&2, T>:
449 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
450 peek_end(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, tail, U32.is_eq(tail, nil()))
451
452# ---- trace runner ----
453
454def obs_nat(~T: Data, r: DList<T> & Nat) -> DList<T> & E.Obs<T>:
455 (s, n) = r
456 (s, E.ONat{n})
457
458def obs_handle(~T: Data, r: DList<T> & E.Handle) -> DList<T> & E.Obs<T>:
459 (s, h) = r
460 (s, E.OHandle{h})
461
462def obs_insert(~T: Data, r: DList<T> & Result<&2, &2, E.Error, E.Handle>) -> DList<T> & E.Obs<T>:
463 (s, x) = r
464 (s, E.OInsert{x})
465
466def obs_val(~T: Data, r: DList<T> & Result<&2, &2, E.Error, T>) -> DList<T> & E.Obs<T>:
467 (s, x) = r
468 (s, E.OVal{x})
469
470def obs_unit(~T: Data, r: DList<T> & Result<&2, &2, E.Error, Unit>) -> DList<T> & E.Obs<T>:
471 (s, x) = r
472 (s, E.OUnit{x})
473
474def obs_nbr(~T: Data, r: DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>) -> DList<T> & E.Obs<T>:
475 (s, x) = r
476 (s, E.ONbr{x})
477
478def obs_list(~T: Data, r: DList<T> & List<&2, T>) -> DList<T> & E.Obs<T>:
479 (s, xs) = r
480 (s, E.OList{xs})
481
482def step(~T: Data, s: DList<T>, op: E.Op<T>) -> DList<T> & E.Obs<T>:
483 match op:
484 case E.Length{}:
485 obs_nat(~T, length(~T, s))
486 case E.PushFront{x}:
487 obs_handle(~T, push_front(~T, s, x))
488 case E.PushBack{x}:
489 obs_handle(~T, push_back(~T, s, x))
490 case E.InsertBefore{h, x}:
491 obs_insert(~T, insert_before(~T, s, h, x))
492 case E.InsertAfter{h, x}:
493 obs_insert(~T, insert_after(~T, s, h, x))
494 case E.Remove{h}:
495 obs_val(~T, remove(~T, s, h))
496 case E.Get{h}:
497 obs_val(~T, get(~T, s, h))
498 case E.Set{h, x}:
499 obs_unit(~T, set(~T, s, h, x))
500 case E.Next{h}:
501 obs_nbr(~T, next(~T, s, h))
502 case E.Prev{h}:
503 obs_nbr(~T, prev(~T, s, h))
504 case E.ToList{}:
505 obs_list(~T, to_list(~T, s))
506
507def record(~T: Data, acc: List<&2, E.Obs<T>>, r: DList<T> & E.Obs<T>) -> DList<T> & List<&2, E.Obs<T>>:
508 (s, o) = r
509 (s, Con{o, acc})
510
511def step_acc(~T: Data, op: E.Op<T>, st: DList<T> & List<&2, E.Obs<T>>) -> DList<T> & List<&2, E.Obs<T>>:
512 (s, acc) = st
513 record(~T, acc, step(~T, s, op))
514
515def run_acc(~T: Data, ops: List<&2, E.Op<T>>, st: DList<T> & List<&2, E.Obs<T>>) -> DList<T> & List<&2, E.Obs<T>>:
516 match ops:
517 case Nil{}:
518 st
519 case Con{op, rest}:
520 run_acc(~T, rest, step_acc(~T, op, st))
521
522def finish(~T: Data, st: DList<T> & List<&2, E.Obs<T>>) -> DList<T> & List<&2, E.Obs<T>>:
523 (s, acc) = st
524 (s, List.reverse(&2, E.Obs<T>, acc))
525
526def run(~T: Data, ops: List<&2, E.Op<T>>, s: DList<T>) -> DList<T> & List<&2, E.Obs<T>>:
527 finish(~T, run_acc(~T, ops, (s, Nil{})))
528
529# Internal insertion variants for a generational public handle owner.
530def ins_side_reuse(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +i: U32, +p: U32, +n: U32, x: T) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
531 match after:
532 case False{}:
533 done_handle(~T, insert_between_free(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, p, link(i), x))
534 case True{}:
535 done_handle(~T, insert_between_free(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, link(i), n, x))
536
537def ins_live2_reuse(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, +i: U32, x: T, pr: Array<U32> & U32, nx: Array<U32> & U32) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
538 (prevs, p) = pr
539 (nexts, n) = nx
540 ins_side_reuse(~T, after, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, p, n, x)
541
542def ins_found_reuse(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array<U32>, nexts: Array<U32>, +i: U32, x: T, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
543 (vals, m) = r
544 match m:
545 case None{}:
546 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}})
547 case Some{v}:
548 ins_live2_reuse(~T, after, tag, fresh, free, count, head, tail, depth, cap, vals, i, x, link_at(prevs, i), link_at(nexts, i))
549
550def insert_checked_reuse(~T: Data, after: Bool, ok: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, nexts: Array<U32>, +i: U32, x: T, same: Bool) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
551 match ok same:
552 case _ False{}:
553 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.ForeignHandle{}})
554 case False{} True{}:
555 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}})
556 case True{} True{}:
557 ins_found_reuse(~T, after, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, i, x, Array.get(Maybe<&2, T>, vals, i))
558
559def insert_before_reuse(~T: Data, s: DList<T>, h: E.Handle, x: T) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
560 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
561 E.H{+l, +i} = h
562 insert_checked_reuse(~T, False{}, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, x, U32.is_eq(l, tag))
563
564def insert_after_reuse(~T: Data, s: DList<T>, h: E.Handle, x: T) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
565 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s
566 E.H{+l, +i} = h
567 insert_checked_reuse(~T, True{}, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, x, U32.is_eq(l, tag))
568
569
570# Called only after a successful remove, by an owner that invalidated the
571# removed handle's generation. The slot is already absent from the live list.
572def recycle_slot(~T: Data, s: DList<T>, +i: U32) -> DList<T>:
573 DL{tag, fresh, +free, count, head, tail, depth, cap, vals, prevs, nexts} = s
574 DL{tag, fresh, link(i), count, head, tail, depth, cap, vals, prevs, Array.set(U32, nexts, i, free)}