1	import Base
2	import ./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.
10	type Links is Type:
11	  Links{nexts: Array<U32>, prevs: Array<U32>, heads: Array<U32>}
12	
13	def 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	
16	def decode_pick(+x: U32, zero: Bool) -> Maybe<&2, U32>:
17	  match zero:
18	    case True{}:
19	      None{}
20	    case False{}:
21	      Some{x}
22	
23	def decode(+x: U32) -> Maybe<&2, U32>:
24	  decode_pick(x, U32.is_eq(x, 0))
25	
26	def encode(m: Maybe<&2, U32>) -> U32:
27	  match m:
28	    case None{}:
29	      0
30	    case Some{x}:
31	      x
32	
33	def 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	
37	def 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	
41	def 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	
45	def 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	
49	def 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	
53	def 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	
57	def 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	
61	def 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	
65	def 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	
69	def 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).
73	def 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).
77	def 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)