src/containers/intrusive_links.bend
bend-collections-laws-containers@1.0.0.0 · 78 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/intrusive_doubly_linked_list.bend as IL
3
4# A ready-made link table for the intrusive list: entity ids are U32 values
5# 1 .. 2^node_depth - 1 (0 means "no entity"), roots are 0 .. 2^root_depth - 1.
6# One U32 per link, so a membership edit is a few indexed array writes. The
7# accessors below are the ones proved to meet the adapter laws for every size
8# (proofs/containers/intrusive_doubly_linked_list/links.bend); an application
9# that keeps its own entity array can copy this layout.
10type Links is Type:
11 Links{nexts: Array<U32>, prevs: Array<U32>, heads: Array<U32>}
12
13def new(+node_depth: Nat, +root_depth: Nat) -> Links:
14 Links{Array.new(U32, node_depth, 0), Array.new(U32, node_depth, 0), Array.new(U32, root_depth, 0)}
15
16def decode_pick(+x: U32, zero: Bool) -> Maybe<&2, U32>:
17 match zero:
18 case True{}:
19 None{}
20 case False{}:
21 Some{x}
22
23def decode(+x: U32) -> Maybe<&2, U32>:
24 decode_pick(x, U32.is_eq(x, 0))
25
26def encode(m: Maybe<&2, U32>) -> U32:
27 match m:
28 case None{}:
29 0
30 case Some{x}:
31 x
32
33def next_got(prevs: Array<U32>, heads: Array<U32>, r: Array<U32> & U32) -> Links & Maybe<&2, U32>:
34 (nexts, +x) = r
35 (Links{nexts, prevs, heads}, decode(x))
36
37def prev_got(nexts: Array<U32>, heads: Array<U32>, r: Array<U32> & U32) -> Links & Maybe<&2, U32>:
38 (prevs, +x) = r
39 (Links{nexts, prevs, heads}, decode(x))
40
41def head_got(nexts: Array<U32>, prevs: Array<U32>, r: Array<U32> & U32) -> Links & Maybe<&2, U32>:
42 (heads, +x) = r
43 (Links{nexts, prevs, heads}, decode(x))
44
45def next(s: Links, n: U32) -> Links & Maybe<&2, U32>:
46 Links{nexts, prevs, heads} = s
47 next_got(prevs, heads, Array.get(U32, nexts, n))
48
49def prev(s: Links, n: U32) -> Links & Maybe<&2, U32>:
50 Links{nexts, prevs, heads} = s
51 prev_got(nexts, heads, Array.get(U32, prevs, n))
52
53def get_head(s: Links, r: U32) -> Links & Maybe<&2, U32>:
54 Links{nexts, prevs, heads} = s
55 head_got(nexts, prevs, Array.get(U32, heads, r))
56
57def set_next(s: Links, n: U32, m: Maybe<&2, U32>) -> Links:
58 Links{nexts, prevs, heads} = s
59 Links{Array.set(U32, nexts, n, encode(m)), prevs, heads}
60
61def set_prev(s: Links, n: U32, m: Maybe<&2, U32>) -> Links:
62 Links{nexts, prevs, heads} = s
63 Links{nexts, Array.set(U32, prevs, n, encode(m)), heads}
64
65def set_head(s: Links, r: U32, m: Maybe<&2, U32>) -> Links:
66 Links{nexts, prevs, heads} = s
67 Links{nexts, prevs, Array.set(U32, heads, r, encode(m))}
68
69def set_head_nonempty(s: Links, r: U32, n: U32) -> Links:
70 set_head(s, r, Some{n})
71
72# Detach member n of root r in O(1).
73def remove(s: Links, +r: U32, +n: U32) -> Links:
74 IL.remove(~Links, ~U32, ~U32, ~next, ~prev, ~set_next, ~set_prev, ~set_head, s, r, n)
75
76# Link detached entity n at the front of root r in O(1).
77def prepend(s: Links, +r: U32, +n: U32) -> Links:
78 IL.prepend_as(~Links, ~U32, ~U32, ~U32, ~get_head, ~set_next, ~set_prev, ~set_head_nonempty, s, r, r, n)