src/containers/doubly_linked_list.bend
bend-collections@1.0.0.0 · 375 lines · 62 definitions
1import Base
2import bend-collections@1.0.0.0/src/containers/internal/dlist_storage.bend as R
3import bend-collections@1.0.0.0/src/containers/types/internal_dlist.bend as I
4import bend-collections@1.0.0.0/src/containers/types/doubly_linked_list.bend as E
5
6
7
8
9
10type DList<-T: Data> is Type:
11 DL{tag: U32, depth: Nat, cap: U32, storage: R.DList<T>, generations: Array<U32>}
12
13def new(~T: Data, +tag: U32) -> DList<T>:
14 DL{tag, 0n, 1, R.new(~T, tag), Array.new(U32, 0n, 0)}
15
16def error(e: I.Error) -> E.Error:
17 match e:
18 case I.ForeignHandle{}:
19 E.ForeignHandle{}
20 case I.StaleHandle{}:
21 E.StaleHandle{}
22
23def old_handle(h: E.Handle) -> I.Handle:
24 E.H{tag, id, generation} = h
25 I.H{tag, id}
26
27def inserted_gen(~T: Data, +tag: U32, depth: Nat, cap: U32, raw: R.DList<T>, id: U32, r: Array<U32> & U32) -> DList<T> & E.Handle:
28 (gens, generation) = r
29 (DL{tag, depth, cap, raw, gens}, E.H{tag, id, generation})
30
31def inserted_room(~T: Data, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList<T>, gens: Array<U32>, +id: U32, grow: Bool) -> DList<T> & E.Handle:
32 match grow:
33 case False{}:
34 inserted_gen(~T, tag, depth, cap, raw, id, Array.get(U32, gens, id))
35 case True{}:
36 inserted_gen(~T, tag, 1n+depth, U32.shl(cap), raw, id, Array.get(U32, ANode{gens, Array.new(U32, depth, 0)}, id))
37
38def inserted(~T: Data, +tag: U32, depth: Nat, +cap: U32, gens: Array<U32>, r: R.DList<T> & I.Handle) -> DList<T> & E.Handle:
39 (raw, I.H{rtag, +id}) = r
40 inserted_room(~T, tag, depth, cap, raw, gens, id, U32.is_eq(id, cap))
41
42def push_front(~T: Data, s: DList<T>, x: T) -> DList<T> & E.Handle:
43 DL{+tag, depth, +cap, raw, gens} = s
44 inserted(~T, tag, depth, cap, gens, R.push_front_free(~T, raw, x))
45
46def push_back(~T: Data, s: DList<T>, x: T) -> DList<T> & E.Handle:
47 DL{+tag, depth, +cap, raw, gens} = s
48 inserted(~T, tag, depth, cap, gens, R.push_back_free(~T, raw, x))
49
50def generation_error(same: Bool) -> Maybe<&2, E.Error>:
51 match same:
52 case True{}:
53 None{}
54 case False{}:
55 Some{E.StaleHandle{}}
56
57def valid_gen(~T: Data, tag: U32, depth: Nat, cap: U32, raw: R.DList<T>, expected: U32, r: Array<U32> & U32) -> DList<T> & Maybe<&2, E.Error>:
58 (gens, actual) = r
59 (DL{tag, depth, cap, raw, gens}, generation_error(U32.is_eq(actual, expected)))
60
61def valid_bounds(~T: Data, tag: U32, depth: Nat, cap: U32, raw: R.DList<T>, gens: Array<U32>, id: U32, expected: U32, same: Bool, inside: Bool) -> DList<T> & Maybe<&2, E.Error>:
62 match same inside:
63 case False{} _:
64 (DL{tag, depth, cap, raw, gens}, Some{E.ForeignHandle{}})
65 case True{} False{}:
66 (DL{tag, depth, cap, raw, gens}, Some{E.StaleHandle{}})
67 case True{} True{}:
68 valid_gen(~T, tag, depth, cap, raw, expected, Array.get(U32, gens, id))
69
70def validate(~T: Data, s: DList<T>, h: E.Handle) -> DList<T> & Maybe<&2, E.Error>:
71 DL{+tag, depth, +cap, raw, gens} = s
72 E.H{owner, +id, expected} = h
73 valid_bounds(~T, tag, depth, cap, raw, gens, id, expected, U32.is_eq(tag, owner), U32.is_lt(id, cap))
74
75def item_result(~T: Data, r: Result<&2, &2, I.Error, T>) -> Result<&2, &2, E.Error, T>:
76 match r:
77 case Done{x}:
78 Done{x}
79 case Fail{e}:
80 Fail{error(e)}
81
82def value_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, r: R.DList<T> & Result<&2, &2, I.Error, T>) -> DList<T> & E.Obs<T>:
83 (raw, result) = r
84 (DL{tag, depth, cap, raw, gens}, E.OVal{item_result(~T, result)})
85
86def unit_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, r: R.DList<T> & Result<&2, &2, I.Error, Unit>) -> DList<T> & E.Obs<T>:
87 (raw, result) = r
88 (DL{tag, depth, cap, raw, gens}, E.OUnit{item_result(~Unit, result)})
89
90def retire(~T: Data, tag: U32, depth: Nat, cap: U32, raw: R.DList<T>, gens: Array<U32>, +id: U32, +generation: U32, v: T, exhausted: Bool) -> DList<T> & E.Obs<T>:
91 match exhausted:
92 case True{}:
93 (DL{tag, depth, cap, raw, gens}, E.OVal{Done{v}})
94 case False{}:
95 (DL{tag, depth, cap, R.recycle_slot(~T, raw, id), Array.set(U32, gens, id, U32.inc(generation))}, E.OVal{Done{v}})
96
97def removed(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, id: U32, +generation: U32, r: R.DList<T> & Result<&2, &2, I.Error, T>) -> DList<T> & E.Obs<T>:
98 match r:
99 case Tuple{raw, Fail{e}}:
100 (DL{tag, depth, cap, raw, gens}, E.OVal{Fail{error(e)}})
101 case Tuple{raw, Done{v}}:
102 retire(~T, tag, depth, cap, raw, gens, id, generation, v, U32.is_eq(generation, 4294967295))
103
104def relative_done(~T: Data, r: DList<T> & E.Handle) -> DList<T> & E.Obs<T>:
105 (s, h) = r
106 (s, E.OInsert{Done{h}})
107
108def relative_result(~T: Data, +tag: U32, depth: Nat, +cap: U32, gens: Array<U32>, r: R.DList<T> & Result<&2, &2, I.Error, I.Handle>) -> DList<T> & E.Obs<T>:
109 match r:
110 case Tuple{raw, Fail{e}}:
111 (DL{tag, depth, cap, raw, gens}, E.OInsert{Fail{error(e)}})
112 case Tuple{raw, Done{I.H{owner, +id}}}:
113 relative_done(~T, inserted_room(~T, tag, depth, cap, raw, gens, id, U32.is_eq(id, cap)))
114
115def neighbour_gen(~T: Data, tag: U32, depth: Nat, cap: U32, raw: R.DList<T>, owner: U32, id: U32, r: Array<U32> & U32) -> DList<T> & E.Obs<T>:
116 (gens, generation) = r
117 (DL{tag, depth, cap, raw, gens}, E.ONbr{Done{Some{E.H{owner, id, generation}}}})
118
119def neighbour_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, r: R.DList<T> & Result<&2, &2, I.Error, Maybe<&2, I.Handle>>) -> DList<T> & E.Obs<T>:
120 match r:
121 case Tuple{raw, Fail{e}}:
122 (DL{tag, depth, cap, raw, gens}, E.ONbr{Fail{error(e)}})
123 case Tuple{raw, Done{None{}}}:
124 (DL{tag, depth, cap, raw, gens}, E.ONbr{Done{None{}}})
125 case Tuple{raw, Done{Some{I.H{owner, +id}}}}:
126 neighbour_gen(~T, tag, depth, cap, raw, owner, id, Array.get(U32, gens, id))
127
128def length_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, r: R.DList<T> & Nat) -> DList<T> & E.Obs<T>:
129 (raw, n) = r
130 (DL{tag, depth, cap, raw, gens}, E.ONat{n})
131
132def list_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, r: R.DList<T> & List<&2, T>) -> DList<T> & E.Obs<T>:
133 (raw, xs) = r
134 (DL{tag, depth, cap, raw, gens}, E.OList{xs})
135
136def pushed_obs(~T: Data, r: DList<T> & E.Handle) -> DList<T> & E.Obs<T>:
137 (s, h) = r
138 (s, E.OHandle{h})
139
140def dispatch(~T: Data, s: DList<T>, op: E.Op<T>) -> DList<T> & E.Obs<T>:
141 DL{+tag, +depth, +cap, raw, gens} = s
142 match op:
143 case E.Length{}:
144 length_result(~T, tag, depth, cap, gens, R.length(~T, raw))
145 case E.ToList{}:
146 list_result(~T, tag, depth, cap, gens, R.to_list(~T, raw))
147 case E.PushFront{x}:
148 pushed_obs(~T, inserted(~T, tag, depth, cap, gens, R.push_front_free(~T, raw, x)))
149 case E.PushBack{x}:
150 pushed_obs(~T, inserted(~T, tag, depth, cap, gens, R.push_back_free(~T, raw, x)))
151 case E.Get{h}:
152 value_result(~T, tag, depth, cap, gens, R.get(~T, raw, old_handle(h)))
153 case E.Set{h, x}:
154 unit_result(~T, tag, depth, cap, gens, R.set(~T, raw, old_handle(h), x))
155 case E.Remove{E.H{+owner, +id, generation}}:
156 removed(~T, tag, depth, cap, gens, id, generation, R.remove(~T, raw, I.H{owner, id}))
157 case E.Next{h}:
158 neighbour_result(~T, tag, depth, cap, gens, R.next(~T, raw, old_handle(h)))
159 case E.Prev{h}:
160 neighbour_result(~T, tag, depth, cap, gens, R.prev(~T, raw, old_handle(h)))
161 case E.InsertBefore{h, x}:
162 relative_result(~T, tag, depth, cap, gens, R.insert_before_reuse(~T, raw, old_handle(h), x))
163 case E.InsertAfter{h, x}:
164 relative_result(~T, tag, depth, cap, gens, R.insert_after_reuse(~T, raw, old_handle(h), x))
165
166def op_handle(~T: Data, op: E.Op<T>) -> Maybe<&2, E.Handle>:
167 match op:
168 case E.Get{h}:
169 Some{h}
170 case E.Set{h, x}:
171 Some{h}
172 case E.Remove{h}:
173 Some{h}
174 case E.Next{h}:
175 Some{h}
176 case E.Prev{h}:
177 Some{h}
178 case E.InsertBefore{h, x}:
179 Some{h}
180 case E.InsertAfter{h, x}:
181 Some{h}
182 case _:
183 None{}
184
185def failed(~T: Data, op: E.Op<T>, e: E.Error) -> E.Obs<T>:
186 match op:
187 case E.Set{h, x}:
188 E.OUnit{Fail{e}}
189 case E.Next{h}:
190 E.ONbr{Fail{e}}
191 case E.Prev{h}:
192 E.ONbr{Fail{e}}
193 case E.InsertBefore{h, x}:
194 E.OInsert{Fail{e}}
195 case E.InsertAfter{h, x}:
196 E.OInsert{Fail{e}}
197 case _:
198 E.OVal{Fail{e}}
199
200def checked(~T: Data, op: E.Op<T>, r: DList<T> & Maybe<&2, E.Error>) -> DList<T> & E.Obs<T>:
201 match r:
202 case Tuple{s, None{}}:
203 dispatch(~T, s, op)
204 case Tuple{s, Some{e}}:
205 (s, failed(~T, op, e))
206
207def step_handle(~T: Data, s: DList<T>, op: E.Op<T>, h: Maybe<&2, E.Handle>) -> DList<T> & E.Obs<T>:
208 match h:
209 case None{}:
210 dispatch(~T, s, op)
211 case Some{handle}:
212 checked(~T, op, validate(~T, s, handle))
213
214def step(~T: Data, s: DList<T>, +op: E.Op<T>) -> DList<T> & E.Obs<T>:
215 step_handle(~T, s, op, op_handle(~T, op))
216
217def project_value(~T: Data, r: DList<T> & E.Obs<T>) -> DList<T> & Result<&2, &2, E.Error, T>:
218 match r:
219 case Tuple{s, E.OVal{x}}:
220 (s, x)
221 case Tuple{s, other}:
222 (s, Fail{E.StaleHandle{}})
223
224def project_unit(~T: Data, r: DList<T> & E.Obs<T>) -> DList<T> & Result<&2, &2, E.Error, Unit>:
225 match r:
226 case Tuple{s, E.OUnit{x}}:
227 (s, x)
228 case Tuple{s, other}:
229 (s, Fail{E.StaleHandle{}})
230
231def project_insert(~T: Data, r: DList<T> & E.Obs<T>) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
232 match r:
233 case Tuple{s, E.OInsert{x}}:
234 (s, x)
235 case Tuple{s, other}:
236 (s, Fail{E.StaleHandle{}})
237
238def project_neighbour(~T: Data, r: DList<T> & E.Obs<T>) -> DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>:
239 match r:
240 case Tuple{s, E.ONbr{x}}:
241 (s, x)
242 case Tuple{s, other}:
243 (s, Fail{E.StaleHandle{}})
244
245def project_length(~T: Data, r: DList<T> & E.Obs<T>) -> DList<T> & Nat:
246 match r:
247 case Tuple{s, E.ONat{x}}:
248 (s, x)
249 case Tuple{s, other}:
250 (s, 0n)
251
252def project_list(~T: Data, r: DList<T> & E.Obs<T>) -> DList<T> & List<&2, T>:
253 match r:
254 case Tuple{s, E.OList{x}}:
255 (s, x)
256 case Tuple{s, other}:
257 (s, Nil{})
258
259def length_direct_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, r: R.DList<T> & Nat) -> DList<T> & Nat:
260 (raw, n) = r
261 (DL{tag, depth, cap, raw, gens}, n)
262
263def length(~T: Data, s: DList<T>) -> DList<T> & Nat:
264 DL{tag, depth, cap, raw, gens} = s
265 length_direct_result(~T, tag, depth, cap, gens, R.length(~T, raw))
266
267def to_list_direct_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, r: R.DList<T> & List<&2, T>) -> DList<T> & List<&2, T>:
268 (raw, xs) = r
269 (DL{tag, depth, cap, raw, gens}, xs)
270
271def to_list(~T: Data, s: DList<T>) -> DList<T> & List<&2, T>:
272 DL{tag, depth, cap, raw, gens} = s
273 to_list_direct_result(~T, tag, depth, cap, gens, R.to_list(~T, raw))
274
275
276
277def get_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, r: R.DList<T> & Result<&2, &2, I.Error, T>) -> DList<T> & Result<&2, &2, E.Error, T>:
278 (raw, result) = r
279 (DL{tag, depth, cap, raw, gens}, item_result(~T, result))
280
281def get_ready(~T: Data, h: E.Handle, r: DList<T> & Maybe<&2, E.Error>) -> DList<T> & Result<&2, &2, E.Error, T>:
282 match r:
283 case Tuple{s, Some{e}}:
284 (s, Fail{e})
285 case Tuple{DL{tag, depth, cap, raw, gens}, None{}}:
286 get_result(~T, tag, depth, cap, gens, R.get(~T, raw, old_handle(h)))
287
288def get(~T: Data, s: DList<T>, +h: E.Handle) -> DList<T> & Result<&2, &2, E.Error, T>:
289 get_ready(~T, h, validate(~T, s, h))
290
291def remove_ready(~T: Data, h: E.Handle, r: DList<T> & Maybe<&2, E.Error>) -> DList<T> & Result<&2, &2, E.Error, T>:
292 match h r:
293 case E.H{owner, id, generation} Tuple{s, Some{e}}:
294 (s, Fail{e})
295 case E.H{+owner, +id, generation} Tuple{DL{tag, depth, cap, raw, gens}, None{}}:
296 project_value(~T, removed(~T, tag, depth, cap, gens, id, generation, R.remove(~T, raw, I.H{owner, id})))
297
298def remove(~T: Data, s: DList<T>, +h: E.Handle) -> DList<T> & Result<&2, &2, E.Error, T>:
299 remove_ready(~T, h, validate(~T, s, h))
300
301def set_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, r: R.DList<T> & Result<&2, &2, I.Error, Unit>) -> DList<T> & Result<&2, &2, E.Error, Unit>:
302 (raw, result) = r
303 (DL{tag, depth, cap, raw, gens}, item_result(~Unit, result))
304
305def set_ready(~T: Data, +h: E.Handle, x: T, r: DList<T> & Maybe<&2, E.Error>) -> DList<T> & Result<&2, &2, E.Error, Unit>:
306 match r:
307 case Tuple{s, Some{e}}:
308 (s, Fail{e})
309 case Tuple{DL{tag, depth, cap, raw, gens}, None{}}:
310 set_result(~T, tag, depth, cap, gens, R.set(~T, raw, old_handle(h), x))
311
312def set(~T: Data, s: DList<T>, +h: E.Handle, x: T) -> DList<T> & Result<&2, &2, E.Error, Unit>:
313 set_ready(~T, h, x, validate(~T, s, h))
314
315def next_ready(~T: Data, +h: E.Handle, r: DList<T> & Maybe<&2, E.Error>) -> DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>:
316 match r:
317 case Tuple{s, Some{e}}:
318 (s, Fail{e})
319 case Tuple{DL{tag, depth, cap, raw, gens}, None{}}:
320 project_neighbour(~T, neighbour_result(~T, tag, depth, cap, gens, R.next(~T, raw, old_handle(h))))
321
322def next(~T: Data, s: DList<T>, +h: E.Handle) -> DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>:
323 next_ready(~T, h, validate(~T, s, h))
324
325def prev_ready(~T: Data, +h: E.Handle, r: DList<T> & Maybe<&2, E.Error>) -> DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>:
326 match r:
327 case Tuple{s, Some{e}}:
328 (s, Fail{e})
329 case Tuple{DL{tag, depth, cap, raw, gens}, None{}}:
330 project_neighbour(~T, neighbour_result(~T, tag, depth, cap, gens, R.prev(~T, raw, old_handle(h))))
331
332def prev(~T: Data, s: DList<T>, +h: E.Handle) -> DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>:
333 prev_ready(~T, h, validate(~T, s, h))
334
335def insert_before_ready(~T: Data, +h: E.Handle, +x: T, r: DList<T> & Maybe<&2, E.Error>) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
336 match r:
337 case Tuple{s, Some{e}}:
338 (s, Fail{e})
339 case Tuple{DL{tag, depth, cap, raw, gens}, None{}}:
340 project_insert(~T, relative_result(~T, tag, depth, cap, gens, R.insert_before_reuse(~T, raw, old_handle(h), x)))
341
342def insert_before(~T: Data, s: DList<T>, +h: E.Handle, x: T) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
343 insert_before_ready(~T, h, x, validate(~T, s, h))
344
345def insert_after_ready(~T: Data, +h: E.Handle, +x: T, r: DList<T> & Maybe<&2, E.Error>) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
346 match r:
347 case Tuple{s, Some{e}}:
348 (s, Fail{e})
349 case Tuple{DL{tag, depth, cap, raw, gens}, None{}}:
350 project_insert(~T, relative_result(~T, tag, depth, cap, gens, R.insert_after_reuse(~T, raw, old_handle(h), x)))
351
352def insert_after(~T: Data, s: DList<T>, +h: E.Handle, x: T) -> DList<T> & Result<&2, &2, E.Error, E.Handle>:
353 insert_after_ready(~T, h, x, validate(~T, s, h))
354
355def record(~T: Data, acc: List<&2, E.Obs<T>>, r: DList<T> & E.Obs<T>) -> DList<T> & List<&2, E.Obs<T>>:
356 (s, o) = r
357 (s, Con{o, acc})
358
359def step_acc(~T: Data, op: E.Op<T>, st: DList<T> & List<&2, E.Obs<T>>) -> DList<T> & List<&2, E.Obs<T>>:
360 (s, acc) = st
361 record(~T, acc, step(~T, s, op))
362
363def 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>>:
364 match ops:
365 case Nil{}:
366 st
367 case Con{op, rest}:
368 run_acc(~T, rest, step_acc(~T, op, st))
369
370def finish(~T: Data, st: DList<T> & List<&2, E.Obs<T>>) -> DList<T> & List<&2, E.Obs<T>>:
371 (s, acc) = st
372 (s, List.reverse(&2, E.Obs<T>, acc))
373
374def run(~T: Data, ops: List<&2, E.Op<T>>, s: DList<T>) -> DList<T> & List<&2, E.Obs<T>>:
375 finish(~T, run_acc(~T, ops, (s, Nil{})))