1	# Generated by tools/generators/intrusive_list.py; edit that source.
2	import Base
3	import ../types/intrusive_doubly_linked_list.bend as E
4	
5	# Intrusive doubly linked lists over application-owned nodes and roots.
6	#
7	# S is the affine application state, N a reusable node identity. Link accessors
8	# select one association; the same entity may have several independent pairs
9	# of links. H and I are independent read/write contexts for the same root.
10	# No container, tail, count, payload copy, or node allocation is required by
11	# prepend/remove. Bind the closed ~ accessors once in an application module.
12	#
13	# Preconditions: valid identities and coherent roots; prepend's node is
14	# detached in this association; remove's node belongs to the supplied root.
15	# Accessors preserve unrelated fields. Raw user input must be validated by
16	# the application before entering this preconditioned API.
17	#
18	# Traversals take an explicit step bound because array links are not a
19	# structurally decreasing Bend value. Exhaustion returns LimitExceeded with
20	# the updated state; callback effects already performed are retained.
21	# Link reads must be observations, and root hooks must preserve coherent links.
22	# clear preflights fuel before any write; callbacks may change only detached
23	# nodes and unrelated state, leaving the unvisited suffix intact.
24	# For finite fixed/decreasing membership, arena capacity is a sufficient
25	# O(1)-available bound. Callbacks must not invalidate a cached successor.
26	
27	# Read the next identity without changing membership.
28	
29	def next(~S: Type, ~N: Data, ~next_of: S -> N -> S & Maybe<&2, N>, s: S, +node: N) -> S & Maybe<&2, N>:
30	  next_of(s, node)
31	
32	# Read the previous identity without changing membership.
33	
34	def prev(~S: Type, ~N: Data, ~prev_of: S -> N -> S & Maybe<&2, N>, s: S, +node: N) -> S & Maybe<&2, N>:
35	  prev_of(s, node)
36	
37	# Observe a Data value (often the entity identity); payload ownership stays in S.
38	
39	def value(~S: Type, ~N: Data, ~V: Data, ~value_of: S -> N -> S & V, s: S, +node: N) -> S & V:
40	  value_of(s, node)
41	
42	# Read a root; requires no writer context.
43	
44	def get_head(~S: Type, ~N: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, s: S, +h: H) -> S & Maybe<&2, N>:
45	  get_head(s, h)
46	
47	def write_next(~S: Type, ~N: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, s: S, +at: Maybe<&2, N>, +node: Maybe<&2, N>) -> S:
48	  match at:
49	    case None{}: s
50	    case Some{a}: set_next(s, a, node)
51	
52	def write_prev(~S: Type, ~N: Data, ~set_prev: S -> N -> Maybe<&2, N> -> S, s: S, +at: Maybe<&2, N>, +node: Maybe<&2, N>) -> S:
53	  match at:
54	    case None{}: s
55	    case Some{a}: set_prev(s, a, node)
56	
57	def remove_left(~S: Type, ~N: Data, ~I: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, s: S, +i: I, +node: N, +before: Maybe<&2, N>, +after: Maybe<&2, N>) -> S:
58	  match before:
59	    case None{}:
60	      set_next(set_head(s, i, after), node, None{})
61	    case Some{+p}:
62	      set_next(set_prev(set_next(s, p, after), node, None{}), node, None{})
63	
64	def remove_3(~S: Type, ~N: Data, ~I: Data, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, +i: I, +node: N, +after: Maybe<&2, N>, +before: Maybe<&2, N>, s: S) -> S:
65	  remove_left(~S, ~N, ~I, ~set_next, ~set_prev, ~set_head, s, i, node, before, after)
66	
67	def remove_2(~S: Type, ~N: Data, ~I: Data, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, +i: I, +node: N, +after: Maybe<&2, N>, r: S & Maybe<&2, N>) -> S:
68	  (s, +before) = r
69	  remove_3(~S, ~N, ~I, ~next, ~prev, ~set_next, ~set_prev, ~set_head, i, node, after, before, write_prev(~S, ~N, ~set_prev, s, after, before))
70	
71	def remove_1(~S: Type, ~N: Data, ~I: Data, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, +i: I, +node: N, r: S & Maybe<&2, N>) -> S:
72	  (s, +after) = r
73	  remove_2(~S, ~N, ~I, ~next, ~prev, ~set_next, ~set_prev, ~set_head, i, node, after, prev(s, node))
74	
75	# Detach a known member in O(1). Uses the nullable root setter only for a head.
76	# Requires no root reader; preserves the node identity and payload.
77	
78	def remove(~S: Type, ~N: Data, ~I: Data, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, s: S, +i: I, +node: N) -> S:
79	  remove_1(~S, ~N, ~I, ~next, ~prev, ~set_next, ~set_prev, ~set_head, i, node, next(s, node))
80	
81	def prepend_as_3(~S: Type, ~N: Data, ~H: Data, ~I: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head_nonempty: S -> I -> N -> S, +i: I, +node: N, s: S) -> S:
82	  set_head_nonempty(s, i, node)
83	
84	def prepend_as_2(~S: Type, ~N: Data, ~H: Data, ~I: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head_nonempty: S -> I -> N -> S, +i: I, +node: N, +head: Maybe<&2, N>, s: S) -> S:
85	  prepend_as_3(~S, ~N, ~H, ~I, ~get_head, ~set_next, ~set_prev, ~set_head_nonempty, i, node, write_prev(~S, ~N, ~set_prev, s, head, Some{node}))
86	
87	def prepend_as_1(~S: Type, ~N: Data, ~H: Data, ~I: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head_nonempty: S -> I -> N -> S, +i: I, +node: N, r: S & Maybe<&2, N>) -> S:
88	  (s, +head) = r
89	  prepend_as_2(~S, ~N, ~H, ~I, ~get_head, ~set_next, ~set_prev, ~set_head_nonempty, i, node, head, set_next(s, node, head))
90	
91	# Prepend a detached node in O(1), using separate read/write contexts.
92	# Calls the nonempty root setter exactly once.
93	
94	def prepend_as(~S: Type, ~N: Data, ~H: Data, ~I: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head_nonempty: S -> I -> N -> S, s: S, +h: H, +i: I, +node: N) -> S:
95	  prepend_as_1(~S, ~N, ~H, ~I, ~get_head, ~set_next, ~set_prev, ~set_head_nonempty, i, node, get_head(s, h))
96	
97	# Prepend with the same context used to read and write the root.
98	
99	def prepend(~S: Type, ~N: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head_nonempty: S -> H -> N -> S, s: S, +h: H, +node: N) -> S:
100	  prepend_as(~S, ~N, ~H, ~H, ~get_head, ~set_next, ~set_prev, ~set_head_nonempty, s, h, h, node)
101	
102	def empty_result(~S: Type, ~N: Data, r: S & Maybe<&2, N>) -> S & Bool:
103	  (s, m) = r
104	  (s, Maybe.is_none(&2, N, m))
105	
106	def nonempty_result(~S: Type, ~N: Data, r: S & Maybe<&2, N>) -> S & Bool:
107	  (s, m) = r
108	  (s, Maybe.is_some(&2, N, m))
109	
110	# O(1) empty-root query.
111	
112	def is_empty(~S: Type, ~N: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, s: S, +h: H) -> S & Bool:
113	  empty_result(~S, ~N, get_head(s, h))
114	
115	# O(1) nonempty-root query.
116	
117	def non_empty(~S: Type, ~N: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, s: S, +h: H) -> S & Bool:
118	  nonempty_result(~S, ~N, get_head(s, h))
119	
120	def two_head(~S: Type, ~N: Data, ~next: S -> N -> S & Maybe<&2, N>, s: S, +head: Maybe<&2, N>) -> S & Bool:
121	  match head:
122	    case None{}: (s, False{})
123	    case Some{n}: nonempty_result(~S, ~N, next(s, n))
124	
125	def at_least_two_1(~S: Type, ~N: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, r: S & Maybe<&2, N>) -> S & Bool:
126	  (s, +head) = r
127	  two_head(~S, ~N, ~next, s, head)
128	
129	# O(1) query: head exists and has a successor.
130	
131	def at_least_two(~S: Type, ~N: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, s: S, +h: H) -> S & Bool:
132	  at_least_two_1(~S, ~N, ~H, ~get_head, ~next, get_head(s, h))
133	
134	# Forward visits save the successor before invoking user code.
135	
136	def fold_step_3(~S: Type, ~N: Data, ~V: Data, ~A: Type, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> A -> V -> S & A, +after: Maybe<&2, N>, r: S & A) -> S & (Maybe<&2, N> & A):
137	  (s, acc) = r
138	  (s, (after, acc))
139	
140	def fold_step_2(~S: Type, ~N: Data, ~V: Data, ~A: Type, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> A -> V -> S & A, +c: C, acc: A, +after: Maybe<&2, N>, r: S & V) -> S & (Maybe<&2, N> & A):
141	  (s, +v) = r
142	  fold_step_3(~S, ~N, ~V, ~A, ~C, ~next, ~value, ~fn, after, fn(s, c, acc, v))
143	
144	def fold_step_1(~S: Type, ~N: Data, ~V: Data, ~A: Type, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> A -> V -> S & A, +node: N, +c: C, acc: A, r: S & Maybe<&2, N>) -> S & (Maybe<&2, N> & A):
145	  (s, +after) = r
146	  fold_step_2(~S, ~N, ~V, ~A, ~C, ~next, ~value, ~fn, c, acc, after, value(s, node))
147	
148	def fold_step(~S: Type, ~N: Data, ~V: Data, ~A: Type, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> A -> V -> S & A, s: S, +node: N, +c: C, acc: A) -> S & (Maybe<&2, N> & A):
149	  fold_step_1(~S, ~N, ~V, ~A, ~C, ~next, ~value, ~fn, node, c, acc, next(s, node))
150	
151	def fold_loop(~S: Type, ~N: Data, ~V: Data, ~A: Type, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> A -> V -> S & A, +fuel: Nat, +c: C, r: S & (Maybe<&2, N> & A)) -> S & Result<&2, &1, E.Error, A>:
152	  match fuel r:
153	    case _ Tuple{s, Tuple{None{}, acc}}: (s, Done{acc})
154	    case 0n Tuple{s, Tuple{Some{node}, acc}}: (s, Fail{E.LimitExceeded{}})
155	    case 1n+p Tuple{s, Tuple{Some{node}, acc}}:
156	      fold_loop(~S, ~N, ~V, ~A, ~C, ~next, ~value, ~fn, p, c, fold_step(~S, ~N, ~V, ~A, ~C, ~next, ~value, ~fn, s, node, c, acc))
157	
158	def fold_left_1(~S: Type, ~N: Data, ~V: Data, ~A: Type, ~C: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> A -> V -> S & A, +fuel: Nat, +c: C, acc: A, r: S & Maybe<&2, N>) -> S & Result<&2, &1, E.Error, A>:
159	  (s, +head) = r
160	  fold_loop(~S, ~N, ~V, ~A, ~C, ~next, ~value, ~fn, fuel, c, (s, (head, acc)))
161	
162	# Forward fold, saving next before each callback. The accumulator may own Type data.
163	
164	def fold_left(~S: Type, ~N: Data, ~V: Data, ~A: Type, ~C: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> A -> V -> S & A, +fuel: Nat, s: S, +h: H, +c: C, acc: A) -> S & Result<&2, &1, E.Error, A>:
165	  fold_left_1(~S, ~N, ~V, ~A, ~C, ~H, ~get_head, ~next, ~value, ~fn, fuel, c, acc, get_head(s, h))
166	
167	def visit_fold(~S: Type, ~V: Data, ~C: Data, ~fn: S -> C -> V -> S, s: S, +c: C, unit: Unit, +v: V) -> S & Unit:
168	  (fn(s, c, v), Unit{})
169	
170	# Forward visit, saving next before each callback; removing current is supported.
171	
172	def foreach(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> V -> S, +fuel: Nat, s: S, +h: H, +c: C) -> S & Result<&2, &1, E.Error, Unit>:
173	  fold_left(~S, ~N, ~V, ~Unit, ~C, ~H, ~get_head, ~next, ~value, ~(s => c => a => v => visit_fold(~S, ~V, ~C, ~fn, s, c, a, v)), fuel, s, h, c, Unit{})
174	
175	def search_next_1(~S: Type, ~N: Data, ~next: S -> N -> S & Maybe<&2, N>, r: S & Maybe<&2, N>) -> S & E.Search<N>:
176	  (s, +after) = r
177	  (s, E.Seeking{after})
178	
179	def search_next(~S: Type, ~N: Data, ~next: S -> N -> S & Maybe<&2, N>, s: S, +node: N) -> S & E.Search<N>:
180	  search_next_1(~S, ~N, ~next, next(s, node))
181	
182	def search_choice(~S: Type, ~N: Data, ~next: S -> N -> S & Maybe<&2, N>, s: S, +node: N, +hit: Bool) -> S & E.Search<N>:
183	  match hit:
184	    case True{}: (s, E.Found{node})
185	    case False{}: search_next(~S, ~N, ~next, s, node)
186	
187	def search_step_2(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, +node: N, r: S & Bool) -> S & E.Search<N>:
188	  (s, +hit) = r
189	  search_choice(~S, ~N, ~next, s, node, hit)
190	
191	def search_step_1(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, +node: N, +c: C, r: S & V) -> S & E.Search<N>:
192	  (s, +v) = r
193	  search_step_2(~S, ~N, ~V, ~C, ~next, ~value, ~pred, node, pred(s, c, v))
194	
195	def search_step(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, s: S, +node: N, +c: C) -> S & E.Search<N>:
196	  search_step_1(~S, ~N, ~V, ~C, ~next, ~value, ~pred, node, c, value(s, node))
197	
198	def search_loop(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, +fuel: Nat, +c: C, r: S & E.Search<N>) -> S & Result<&2, &1, E.Error, Maybe<&2, N>>:
199	  match fuel r:
200	    case _ Tuple{s, E.Found{node}}: (s, Done{Some{node}})
201	    case _ Tuple{s, E.Seeking{None{}}}: (s, Done{None{}})
202	    case 0n Tuple{s, E.Seeking{Some{node}}}: (s, Fail{E.LimitExceeded{}})
203	    case 1n+p Tuple{s, E.Seeking{Some{node}}}:
204	      search_loop(~S, ~N, ~V, ~C, ~next, ~value, ~pred, p, c, search_step(~S, ~N, ~V, ~C, ~next, ~value, ~pred, s, node, c))
205	
206	def find_1(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, +fuel: Nat, +c: C, r: S & Maybe<&2, N>) -> S & Result<&2, &1, E.Error, Maybe<&2, N>>:
207	  (s, +head) = r
208	  search_loop(~S, ~N, ~V, ~C, ~next, ~value, ~pred, fuel, c, (s, E.Seeking{head}))
209	
210	# Return the first matching node identity; next is read after a failed predicate.
211	
212	def find(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, +fuel: Nat, s: S, +h: H, +c: C) -> S & Result<&2, &1, E.Error, Maybe<&2, N>>:
213	  find_1(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~pred, fuel, c, get_head(s, h))
214	
215	# Compatibility alias of find; Bend needs no preallocated Option wrapper.
216	
217	def find_some_this(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, +fuel: Nat, s: S, +h: H, +c: C) -> S & Result<&2, &1, E.Error, Maybe<&2, N>>:
218	  find(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~pred, fuel, s, h, c)
219	
220	def search_bool(~S: Type, ~N: Data, +negate: Bool, r: S & Result<&2, &1, E.Error, Maybe<&2, N>>) -> S & Result<&2, &1, E.Error, Bool>:
221	  match negate r:
222	    case _ Tuple{s, Fail{e}}: (s, Fail{e})
223	    case False{} Tuple{s, Done{m}}: (s, Done{Maybe.is_some(&2, N, m)})
224	    case True{} Tuple{s, Done{m}}: (s, Done{Maybe.is_none(&2, N, m)})
225	
226	# Short-circuit on the first true predicate; False for an empty list.
227	
228	def exists(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, +fuel: Nat, s: S, +h: H, +c: C) -> S & Result<&2, &1, E.Error, Bool>:
229	  search_bool(~S, ~N, False{}, find(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~pred, fuel, s, h, c))
230	
231	def negated_result(~S: Type, r: S & Bool) -> S & Bool:
232	  (s, b) = r
233	  (s, Bool.not(b))
234	
235	def negated_pred(~S: Type, ~V: Data, ~C: Data, ~pred: S -> C -> V -> S & Bool, s: S, +c: C, +v: V) -> S & Bool:
236	  negated_result(~S, pred(s, c, v))
237	
238	# Short-circuit on the first false predicate; True for an empty list.
239	
240	def forall(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, +fuel: Nat, s: S, +h: H, +c: C) -> S & Result<&2, &1, E.Error, Bool>:
241	  search_bool(~S, ~N, True{}, find(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~(s => c => v => negated_pred(~S, ~V, ~C, ~pred, s, c, v)), fuel, s, h, c))
242	
243	def count_pick(~S: Type, +count: Nat, r: S & Bool) -> S & Nat:
244	  match r:
245	    case Tuple{s, True{}}: (s, 1n+count)
246	    case Tuple{s, False{}}: (s, count)
247	
248	def count_step_3(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, +acc: Nat, r: S & Maybe<&2, N>) -> S & (Maybe<&2, N> & Nat):
249	  (s, +after) = r
250	  (s, (after, acc))
251	
252	def count_step_2(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, +node: N, r: S & Nat) -> S & (Maybe<&2, N> & Nat):
253	  (s, +acc) = r
254	  count_step_3(~S, ~N, ~V, ~C, ~next, ~value, ~pred, acc, next(s, node))
255	
256	def count_step_1(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, +node: N, +c: C, +acc: Nat, r: S & V) -> S & (Maybe<&2, N> & Nat):
257	  (s, +v) = r
258	  count_step_2(~S, ~N, ~V, ~C, ~next, ~value, ~pred, node, count_pick(~S, acc, pred(s, c, v)))
259	
260	def count_step(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, s: S, +node: N, +c: C, +acc: Nat) -> S & (Maybe<&2, N> & Nat):
261	  count_step_1(~S, ~N, ~V, ~C, ~next, ~value, ~pred, node, c, acc, value(s, node))
262	
263	def count_loop(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, +fuel: Nat, +c: C, r: S & (Maybe<&2, N> & Nat)) -> S & Result<&2, &1, E.Error, Nat>:
264	  match fuel r:
265	    case _ Tuple{s, Tuple{None{}, acc}}: (s, Done{acc})
266	    case 0n Tuple{s, Tuple{Some{node}, acc}}: (s, Fail{E.LimitExceeded{}})
267	    case 1n+p Tuple{s, Tuple{Some{node}, acc}}:
268	      count_loop(~S, ~N, ~V, ~C, ~next, ~value, ~pred, p, c, count_step(~S, ~N, ~V, ~C, ~next, ~value, ~pred, s, node, c, acc))
269	
270	def count_1(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, +fuel: Nat, +c: C, r: S & Maybe<&2, N>) -> S & Result<&2, &1, E.Error, Nat>:
271	  (s, +head) = r
272	  count_loop(~S, ~N, ~V, ~C, ~next, ~value, ~pred, fuel, c, (s, (head, 0n)))
273	
274	# Count matching values; read next after each predicate. O(n).
275	
276	def count(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, +fuel: Nat, s: S, +h: H, +c: C) -> S & Result<&2, &1, E.Error, Nat>:
277	  count_1(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~pred, fuel, c, get_head(s, h))
278	
279	def node_value(~S: Type, ~N: Data, s: S, +n: N) -> S & N:
280	  (s, n)
281	
282	def count_node(~S: Type, ~N: Data, s: S, c: Unit, +acc: Nat, +node: N) -> S & Nat:
283	  (s, 1n+acc)
284	
285	# Count members in O(n); no cached count is required in the root.
286	
287	def length(~S: Type, ~N: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, +fuel: Nat, s: S, +h: H) -> S & Result<&2, &1, E.Error, Nat>:
288	  fold_left(~S, ~N, ~N, ~Nat, ~Unit, ~H, ~get_head, ~next, ~(s => n => node_value(~S, ~N, s, n)), ~(s => c => a => n => count_node(~S, ~N, s, c, a, n)), fuel, s, h, Unit{}, 0n)
289	
290	def converted_pred_result(~S: Type, ~V: Data, ~D: Data, ~C: Data, ~convert: S -> V -> S & Maybe<&2, D>, ~pred: S -> C -> D -> S & Bool, +c: C, r: S & Maybe<&2, D>) -> S & Bool:
291	  match r:
292	    case Tuple{s, None{}}: (s, False{})
293	    case Tuple{s, Some{v}}: pred(s, c, v)
294	
295	def converted_pred(~S: Type, ~V: Data, ~D: Data, ~C: Data, ~convert: S -> V -> S & Maybe<&2, D>, ~pred: S -> C -> D -> S & Bool, s: S, +c: C, +v: V) -> S & Bool:
296	  converted_pred_result(~S, ~V, ~D, ~C, ~convert, ~pred, c, convert(s, v))
297	
298	# Convert once per visited value, skip failed conversions, return the original node.
299	
300	def find_convert(~S: Type, ~N: Data, ~V: Data, ~D: Data, ~C: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~convert: S -> V -> S & Maybe<&2, D>, ~pred: S -> C -> D -> S & Bool, +fuel: Nat, s: S, +h: H, +c: C) -> S & Result<&2, &1, E.Error, Maybe<&2, N>>:
301	  find(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~(s => c => v => converted_pred(~S, ~V, ~D, ~C, ~convert, ~pred, s, c, v)), fuel, s, h, c)
302	
303	def equal_value(~S: Type, ~V: Data, ~eq: V -> V -> Bool, s: S, +wanted: V, +v: V) -> S & Bool:
304	  (s, eq(wanted, v))
305	
306	# Find with eq(wanted, observed_value), returning the node identity.
307	
308	def find_value(~S: Type, ~N: Data, ~V: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~eq: V -> V -> Bool, +fuel: Nat, s: S, +h: H, +wanted: V) -> S & Result<&2, &1, E.Error, Maybe<&2, N>>:
309	  find(~S, ~N, ~V, ~V, ~H, ~get_head, ~next, ~value, ~(s => c => v => equal_value(~S, ~V, ~eq, s, c, v)), fuel, s, h, wanted)
310	
311	def equal_converted_value(~S: Type, ~V: Data, ~eq: V -> V -> Bool, s: S, +wanted: V, +v: V) -> S & Bool:
312	  (s, eq(v, wanted))
313	
314	# Find with eq(converted_value, wanted), returning the original node.
315	
316	def find_value_convert(~S: Type, ~N: Data, ~V: Data, ~D: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~convert: S -> V -> S & Maybe<&2, D>, ~eq: D -> D -> Bool, +fuel: Nat, s: S, +h: H, +wanted: D) -> S & Result<&2, &1, E.Error, Maybe<&2, N>>:
317	  find_convert(~S, ~N, ~V, ~D, ~D, ~H, ~get_head, ~next, ~value, ~convert, ~(s => c => v => equal_converted_value(~S, ~D, ~eq, s, c, v)), fuel, s, h, wanted)
318	
319	def clear_step_3(~S: Type, ~N: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~post_remove: S -> C -> N -> S, +after: Maybe<&2, N>, s: S) -> S & Maybe<&2, N>:
320	  (s, after)
321	
322	def clear_step_2(~S: Type, ~N: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~post_remove: S -> C -> N -> S, +node: N, +c: C, +after: Maybe<&2, N>, s: S) -> S & Maybe<&2, N>:
323	  clear_step_3(~S, ~N, ~C, ~next, ~set_next, ~set_prev, ~post_remove, after, post_remove(s, c, node))
324	
325	def clear_step_1(~S: Type, ~N: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~post_remove: S -> C -> N -> S, +node: N, +c: C, r: S & Maybe<&2, N>) -> S & Maybe<&2, N>:
326	  (s, +after) = r
327	  clear_step_2(~S, ~N, ~C, ~next, ~set_next, ~set_prev, ~post_remove, node, c, after, set_prev(set_next(s, node, None{}), node, None{}))
328	
329	def clear_step(~S: Type, ~N: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~post_remove: S -> C -> N -> S, s: S, +node: N, +c: C) -> S & Maybe<&2, N>:
330	  clear_step_1(~S, ~N, ~C, ~next, ~set_next, ~set_prev, ~post_remove, node, c, next(s, node))
331	
332	def clear_loop(~S: Type, ~N: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~post_remove: S -> C -> N -> S, +fuel: Nat, +head: N, +c: C, r: S & Maybe<&2, N>) -> S & Result<&2, &1, E.Error, Unit>:
333	  match fuel r:
334	    case 0n Tuple{s, cursor}: (s, Fail{E.LimitExceeded{}})
335	    case 1n+p Tuple{s, None{}}:
336	      (post_remove(set_next(s, head, None{}), c, head), Done{Unit{}})
337	    case 1n+p Tuple{s, Some{node}}:
338	      clear_loop(~S, ~N, ~C, ~next, ~set_next, ~set_prev, ~post_remove, p, head, c, clear_step(~S, ~N, ~C, ~next, ~set_next, ~set_prev, ~post_remove, s, node, c))
339	
340	def clear_head(~S: Type, ~N: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~post_remove: S -> C -> N -> S, +fuel: Nat, s: S, +h: H, +i: I, +c: C, +head: Maybe<&2, N>) -> S & Result<&2, &1, E.Error, Unit>:
341	  match fuel head:
342	    case _ None{}: (s, Done{Unit{}})
343	    case 0n Some{node}: (s, Fail{E.LimitExceeded{}})
344	    case 1n+p Some{node}:
345	      clear_loop(~S, ~N, ~C, ~next, ~set_next, ~set_prev, ~post_remove, 1n+p, node, c, next(set_head(s, i, None{}), node))
346	
347	def chain_fits(~S: Type, ~N: Data, ~next: S -> N -> S & Maybe<&2, N>, +fuel: Nat, r: S & Maybe<&2, N>) -> S & Bool:
348	  match fuel r:
349	    case _ Tuple{s, None{}}: (s, True{})
350	    case 0n Tuple{s, Some{node}}: (s, False{})
351	    case 1n+p Tuple{s, Some{node}}:
352	      chain_fits(~S, ~N, ~next, p, next(s, node))
353	
354	def clear_checked(~S: Type, ~N: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~post_remove: S -> C -> N -> S, +fuel: Nat, +h: H, +i: I, +c: C, +head: Maybe<&2, N>, r: S & Bool) -> S & Result<&2, &1, E.Error, Unit>:
355	  match r:
356	    case Tuple{s, False{}}: (s, Fail{E.LimitExceeded{}})
357	    case Tuple{s, True{}}:
358	      clear_head(~S, ~N, ~H, ~I, ~C, ~get_head, ~next, ~set_next, ~set_prev, ~set_head, ~post_remove, fuel, s, h, i, c, head)
359	
360	def clear_list_as_1(~S: Type, ~N: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~post_remove: S -> C -> N -> S, +fuel: Nat, +h: H, +i: I, +c: C, r: S & Maybe<&2, N>) -> S & Result<&2, &1, E.Error, Unit>:
361	  (s, +head) = r
362	  clear_checked(~S, ~N, ~H, ~I, ~C, ~get_head, ~next, ~set_next, ~set_prev, ~set_head, ~post_remove, fuel, h, i, c, head, chain_fits(~S, ~N, ~next, fuel, (s, head)))
363	
364	# Preflight the bound, publish an empty root, detach suffix then original head.
365	# Call post_remove once per detached node; a no-op callback needs no allocation.
366	
367	def clear_list_as(~S: Type, ~N: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~post_remove: S -> C -> N -> S, +fuel: Nat, s: S, +h: H, +i: I, +c: C) -> S & Result<&2, &1, E.Error, Unit>:
368	  clear_list_as_1(~S, ~N, ~H, ~I, ~C, ~get_head, ~next, ~set_next, ~set_prev, ~set_head, ~post_remove, fuel, h, i, c, get_head(s, h))
369	
370	# Clear using one root context; see clear_list_as for callback order.
371	
372	def clear_list(~S: Type, ~N: Data, ~H: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> H -> Maybe<&2, N> -> S, ~post_remove: S -> C -> N -> S, +fuel: Nat, s: S, +h: H, +c: C) -> S & Result<&2, &1, E.Error, Unit>:
373	  clear_list_as(~S, ~N, ~H, ~H, ~C, ~get_head, ~next, ~set_next, ~set_prev, ~set_head, ~post_remove, fuel, s, h, h, c)
374	
375	def ignore_removed(~S: Type, ~C: Data, ~N: Data, s: S, +c: C, +node: N) -> S:
376	  s
377	
378	# Clear using a callback that returns each detached node to an application pool.
379	# The pool argument locates that pool in S; post_remove performs the free.
380	
381	def clear_list_with_pool_as(~S: Type, ~N: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~post_remove: S -> C -> N -> S, +fuel: Nat, s: S, +h: H, +i: I, +pool: C) -> S & Result<&2, &1, E.Error, Unit>:
382	  clear_list_as(~S, ~N, ~H, ~I, ~C, ~get_head, ~next, ~set_next, ~set_prev, ~set_head, ~post_remove, fuel, s, h, i, pool)
383	
384	# Clear to a pool using one root context.
385	
386	def clear_list_with_pool(~S: Type, ~N: Data, ~H: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> H -> Maybe<&2, N> -> S, ~post_remove: S -> C -> N -> S, +fuel: Nat, s: S, +h: H, +pool: C) -> S & Result<&2, &1, E.Error, Unit>:
387	  clear_list(~S, ~N, ~H, ~C, ~get_head, ~next, ~set_next, ~set_prev, ~set_head, ~post_remove, fuel, s, h, pool)
388	
389	# Prefix predicates re-read the live head; the remaining tail saves next.
390	
391	def unlink_nonhead_links(~S: Type, ~N: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, s: S, +node: N, +before: Maybe<&2, N>, +after: Maybe<&2, N>) -> S & Bool:
392	  match before:
393	    case None{}: (s, False{})
394	    case Some{+p}:
395	      (set_prev(set_next(set_next(write_prev(~S, ~N, ~set_prev, s, after, Some{p}), p, after), node, None{}), node, None{}), True{})
396	
397	def unlink_nonhead_2(~S: Type, ~N: Data, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, +node: N, +after: Maybe<&2, N>, r: S & Maybe<&2, N>) -> S & Bool:
398	  (s, +before) = r
399	  unlink_nonhead_links(~S, ~N, ~set_next, ~set_prev, s, node, before, after)
400	
401	def unlink_nonhead_1(~S: Type, ~N: Data, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, +node: N, r: S & Maybe<&2, N>) -> S & Bool:
402	  (s, +after) = r
403	  unlink_nonhead_2(~S, ~N, ~next, ~prev, ~set_next, ~set_prev, node, after, prev(s, node))
404	
405	def unlink_nonhead(~S: Type, ~N: Data, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, s: S, +node: N) -> S & Bool:
406	  unlink_nonhead_1(~S, ~N, ~next, ~prev, ~set_next, ~set_prev, node, next(s, node))
407	
408	def filter_prefix_result(~S: Type, ~N: Data, r: S & Maybe<&2, N>) -> S & E.Filter<N>:
409	  (s, head) = r
410	  (s, E.Prefix{head})
411	
412	def filter_tail_result(~S: Type, ~N: Data, r: S & Maybe<&2, N>) -> S & E.Filter<N>:
413	  (s, head) = r
414	  (s, E.Tail{head})
415	
416	def filter_kept_head(~S: Type, ~N: Data, ~V: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, ~post_remove: S -> C -> N -> S, r: S & Maybe<&2, N>) -> S & E.Filter<N>:
417	  match r:
418	    case Tuple{s, None{}}: (s, E.FilterFailed{E.InvalidTraversal{}})
419	    case Tuple{s, Some{head}}: filter_tail_result(~S, ~N, next(s, head))
420	
421	def filter_drop_head(~S: Type, ~N: Data, ~V: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, ~post_remove: S -> C -> N -> S, +h: H, +i: I, +c: C, r: S & Maybe<&2, N>) -> S & E.Filter<N>:
422	  match r:
423	    case Tuple{s, None{}}: (s, E.FilterFailed{E.InvalidTraversal{}})
424	    case Tuple{s, Some{+node}}:
425	      filter_prefix_result(~S, ~N, get_head(post_remove(remove(~S, ~N, ~I, ~next, ~prev, ~set_next, ~set_prev, ~set_head, s, i, node), c, node), h))
426	
427	def filter_prefix_choice(~S: Type, ~N: Data, ~V: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, ~post_remove: S -> C -> N -> S, +h: H, +i: I, +c: C, r: S & Bool) -> S & E.Filter<N>:
428	  match r:
429	    case Tuple{s, True{}}:
430	      filter_kept_head(~S, ~N, ~V, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, get_head(s, h))
431	    case Tuple{s, False{}}:
432	      filter_drop_head(~S, ~N, ~V, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, h, i, c, get_head(s, h))
433	
434	def filter_prefix_step_1(~S: Type, ~N: Data, ~V: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, ~post_remove: S -> C -> N -> S, +h: H, +i: I, +c: C, r: S & V) -> S & E.Filter<N>:
435	  (s, +v) = r
436	  filter_prefix_choice(~S, ~N, ~V, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, h, i, c, pred(s, c, v))
437	
438	def filter_prefix_step(~S: Type, ~N: Data, ~V: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, ~post_remove: S -> C -> N -> S, s: S, +h: H, +i: I, +c: C, +node: N) -> S & E.Filter<N>:
439	  filter_prefix_step_1(~S, ~N, ~V, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, h, i, c, value(s, node))
440	
441	def filter_tail_removed(~S: Type, ~N: Data, ~V: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, ~post_remove: S -> C -> N -> S, +c: C, +node: N, +after: Maybe<&2, N>, r: S & Bool) -> S & E.Filter<N>:
442	  match r:
443	    case Tuple{s, False{}}: (s, E.FilterFailed{E.InvalidTraversal{}})
444	    case Tuple{s, True{}}: (post_remove(s, c, node), E.Tail{after})
445	
446	def filter_tail_choice(~S: Type, ~N: Data, ~V: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, ~post_remove: S -> C -> N -> S, +c: C, +node: N, +after: Maybe<&2, N>, r: S & Bool) -> S & E.Filter<N>:
447	  match r:
448	    case Tuple{s, True{}}: (s, E.Tail{after})
449	    case Tuple{s, False{}}:
450	      filter_tail_removed(~S, ~N, ~V, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, c, node, after, unlink_nonhead(~S, ~N, ~next, ~prev, ~set_next, ~set_prev, s, node))
451	
452	def filter_tail_step_2(~S: Type, ~N: Data, ~V: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, ~post_remove: S -> C -> N -> S, +c: C, +node: N, +after: Maybe<&2, N>, r: S & V) -> S & E.Filter<N>:
453	  (s, +v) = r
454	  filter_tail_choice(~S, ~N, ~V, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, c, node, after, pred(s, c, v))
455	
456	def filter_tail_step_1(~S: Type, ~N: Data, ~V: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, ~post_remove: S -> C -> N -> S, +c: C, +node: N, r: S & Maybe<&2, N>) -> S & E.Filter<N>:
457	  (s, +after) = r
458	  filter_tail_step_2(~S, ~N, ~V, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, c, node, after, value(s, node))
459	
460	def filter_tail_step(~S: Type, ~N: Data, ~V: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, ~post_remove: S -> C -> N -> S, s: S, +c: C, +node: N) -> S & E.Filter<N>:
461	  filter_tail_step_1(~S, ~N, ~V, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, c, node, next(s, node))
462	
463	def filter_loop(~S: Type, ~N: Data, ~V: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, ~post_remove: S -> C -> N -> S, +fuel: Nat, +h: H, +i: I, +c: C, r: S & E.Filter<N>) -> S & Result<&2, &1, E.Error, Unit>:
464	  match fuel r:
465	    case _ Tuple{s, E.FilterFailed{e}}: (s, Fail{e})
466	    case _ Tuple{s, E.Prefix{None{}}}: (s, Done{Unit{}})
467	    case _ Tuple{s, E.Tail{None{}}}: (s, Done{Unit{}})
468	    case 0n Tuple{s, E.Prefix{Some{node}}}: (s, Fail{E.LimitExceeded{}})
469	    case 0n Tuple{s, E.Tail{Some{node}}}: (s, Fail{E.LimitExceeded{}})
470	    case 1n+p Tuple{s, E.Prefix{Some{node}}}:
471	      filter_loop(~S, ~N, ~V, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, p, h, i, c, filter_prefix_step(~S, ~N, ~V, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, s, h, i, c, node))
472	    case 1n+p Tuple{s, E.Tail{Some{node}}}:
473	      filter_loop(~S, ~N, ~V, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, p, h, i, c, filter_tail_step(~S, ~N, ~V, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, s, c, node))
474	
475	# Keep true values, detach false values, then call post_remove on the removed node.
476	# Re-read the live head in the prefix; save next when visiting the retained tail.
477	
478	def foreach_remove_filter_as(~S: Type, ~N: Data, ~V: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, ~post_remove: S -> C -> N -> S, +fuel: Nat, s: S, +h: H, +i: I, +c: C) -> S & Result<&2, &1, E.Error, Unit>:
479	  filter_loop(~S, ~N, ~V, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, fuel, h, i, c, filter_prefix_result(~S, ~N, get_head(s, h)))
480	
481	# Removal filter with one root context.
482	
483	def foreach_remove_filter(~S: Type, ~N: Data, ~V: Data, ~H: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> H -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~pred: S -> C -> V -> S & Bool, ~post_remove: S -> C -> N -> S, +fuel: Nat, s: S, +h: H, +c: C) -> S & Result<&2, &1, E.Error, Unit>:
484	  foreach_remove_filter_as(~S, ~N, ~V, ~H, ~H, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, fuel, s, h, h, c)
485	
486	# Remove failed conversions and false predicates; convert each visited value once.
487	
488	def foreach_remove_convert_filter_as(~S: Type, ~N: Data, ~V: Data, ~D: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~convert: S -> V -> S & Maybe<&2, D>, ~pred: S -> C -> D -> S & Bool, ~post_remove: S -> C -> N -> S, +fuel: Nat, s: S, +h: H, +i: I, +c: C) -> S & Result<&2, &1, E.Error, Unit>:
489	  foreach_remove_filter_as(~S, ~N, ~V, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~(s => c => v => converted_pred(~S, ~V, ~D, ~C, ~convert, ~pred, s, c, v)), ~post_remove, fuel, s, h, i, c)
490	
491	# Conversion/removal filter with one root context.
492	
493	def foreach_remove_convert_filter(~S: Type, ~N: Data, ~V: Data, ~D: Data, ~H: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> H -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~convert: S -> V -> S & Maybe<&2, D>, ~pred: S -> C -> D -> S & Bool, ~post_remove: S -> C -> N -> S, +fuel: Nat, s: S, +h: H, +c: C) -> S & Result<&2, &1, E.Error, Unit>:
494	  foreach_remove_convert_filter_as(~S, ~N, ~V, ~D, ~H, ~H, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~convert, ~pred, ~post_remove, fuel, s, h, h, c)
495	
496	def visit_true(~S: Type, ~D: Data, ~C: Data, ~fn: S -> C -> D -> S, s: S, +c: C, +v: D) -> S & Bool:
497	  (fn(s, c, v), True{})
498	
499	# Visit successfully converted values, remove failed conversions.
500	
501	def foreach_remove_convert_as(~S: Type, ~N: Data, ~V: Data, ~D: Data, ~H: Data, ~I: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> I -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~convert: S -> V -> S & Maybe<&2, D>, ~fn: S -> C -> D -> S, ~post_remove: S -> C -> N -> S, +fuel: Nat, s: S, +h: H, +i: I, +c: C) -> S & Result<&2, &1, E.Error, Unit>:
502	  foreach_remove_convert_filter_as(~S, ~N, ~V, ~D, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~convert, ~(s => c => v => visit_true(~S, ~D, ~C, ~fn, s, c, v)), ~post_remove, fuel, s, h, i, c)
503	
504	# Conversion/removal visitor with one root context.
505	
506	def foreach_remove_convert(~S: Type, ~N: Data, ~V: Data, ~D: Data, ~H: Data, ~C: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~set_head: S -> H -> Maybe<&2, N> -> S, ~value: S -> N -> S & V, ~convert: S -> V -> S & Maybe<&2, D>, ~fn: S -> C -> D -> S, ~post_remove: S -> C -> N -> S, +fuel: Nat, s: S, +h: H, +c: C) -> S & Result<&2, &1, E.Error, Unit>:
507	  foreach_remove_convert_as(~S, ~N, ~V, ~D, ~H, ~H, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~convert, ~fn, ~post_remove, fuel, s, h, h, c)
508	
509	def last_fold(~S: Type, ~N: Data, s: S, c: Unit, +acc: Maybe<&2, N>, +node: N) -> S & Maybe<&2, N>:
510	  (s, Some{node})
511	
512	def last(~S: Type, ~N: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, +fuel: Nat, s: S, +h: H) -> S & Result<&2, &1, E.Error, Maybe<&2, N>>:
513	  fold_left(~S, ~N, ~N, ~Maybe<&2, N>, ~Unit, ~H, ~get_head, ~next, ~(s => n => node_value(~S, ~N, s, n)), ~(s => c => a => n => last_fold(~S, ~N, s, c, a, n)), fuel, s, h, Unit{}, None{})
514	
515	def mapped_cons(~T: Type, m: Maybe<&1, T>, xs: List<&1, T>) -> List<&1, T>:
516	  match m:
517	    case None{}: xs
518	    case Some{x}: Con{x, xs}
519	
520	def map_step_4(~S: Type, ~N: Data, ~V: Data, ~T: Type, ~C: Data, ~prev: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> V -> S & Maybe<&1, T>, xs: List<&1, T>, r: S & Maybe<&2, N>) -> S & (Maybe<&2, N> & List<&1, T>):
521	  (s, +before) = r
522	  (s, (before, xs))
523	
524	def map_step_3(~S: Type, ~N: Data, ~V: Data, ~T: Type, ~C: Data, ~prev: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> V -> S & Maybe<&1, T>, +node: N, s: S, xs: List<&1, T>) -> S & (Maybe<&2, N> & List<&1, T>):
525	  map_step_4(~S, ~N, ~V, ~T, ~C, ~prev, ~value, ~fn, xs, prev(s, node))
526	
527	def map_step_2(~S: Type, ~N: Data, ~V: Data, ~T: Type, ~C: Data, ~prev: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> V -> S & Maybe<&1, T>, +node: N, xs: List<&1, T>, r: S & Maybe<&1, T>) -> S & (Maybe<&2, N> & List<&1, T>):
528	  (s, m) = r
529	  map_step_3(~S, ~N, ~V, ~T, ~C, ~prev, ~value, ~fn, node, s, mapped_cons(~T, m, xs))
530	
531	def map_step_1(~S: Type, ~N: Data, ~V: Data, ~T: Type, ~C: Data, ~prev: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> V -> S & Maybe<&1, T>, +c: C, +node: N, xs: List<&1, T>, r: S & V) -> S & (Maybe<&2, N> & List<&1, T>):
532	  (s, +v) = r
533	  map_step_2(~S, ~N, ~V, ~T, ~C, ~prev, ~value, ~fn, node, xs, fn(s, c, v))
534	
535	def map_step(~S: Type, ~N: Data, ~V: Data, ~T: Type, ~C: Data, ~prev: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> V -> S & Maybe<&1, T>, s: S, +c: C, +node: N, xs: List<&1, T>) -> S & (Maybe<&2, N> & List<&1, T>):
536	  map_step_1(~S, ~N, ~V, ~T, ~C, ~prev, ~value, ~fn, c, node, xs, value(s, node))
537	
538	def map_loop(~S: Type, ~N: Data, ~V: Data, ~T: Type, ~C: Data, ~prev: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> V -> S & Maybe<&1, T>, +fuel: Nat, +c: C, r: S & (Maybe<&2, N> & List<&1, T>)) -> S & Result<&2, &1, E.Error, List<&1, T>>:
539	  match fuel r:
540	    case _ Tuple{s, Tuple{None{}, xs}}: (s, Done{xs})
541	    case 0n Tuple{s, Tuple{Some{node}, xs}}: (s, Fail{E.LimitExceeded{}})
542	    case 1n+p Tuple{s, Tuple{Some{node}, xs}}:
543	      map_loop(~S, ~N, ~V, ~T, ~C, ~prev, ~value, ~fn, p, c, map_step(~S, ~N, ~V, ~T, ~C, ~prev, ~value, ~fn, s, c, node, xs))
544	
545	def map_last(~S: Type, ~N: Data, ~V: Data, ~T: Type, ~C: Data, ~prev: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> V -> S & Maybe<&1, T>, +fuel: Nat, +c: C, r: S & Result<&2, &1, E.Error, Maybe<&2, N>>) -> S & Result<&2, &1, E.Error, List<&1, T>>:
546	  match r:
547	    case Tuple{s, Fail{e}}: (s, Fail{e})
548	    case Tuple{s, Done{end}}:
549	      map_loop(~S, ~N, ~V, ~T, ~C, ~prev, ~value, ~fn, fuel, c, (s, (end, Nil{})))
550	
551	# Option filter-map: zero or one output per input. Callbacks run tail to head;
552	# the newly allocated owning result list retains forward input order.
553	
554	def flat_map_to_list(~S: Type, ~N: Data, ~V: Data, ~T: Type, ~C: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> V -> S & Maybe<&1, T>, +fuel: Nat, s: S, +h: H, +c: C) -> S & Result<&2, &1, E.Error, List<&1, T>>:
555	  map_last(~S, ~N, ~V, ~T, ~C, ~prev, ~value, ~fn, fuel, c, last(~S, ~N, ~H, ~get_head, ~next, fuel, s, h))
556	
557	def map_some_result(~S: Type, ~T: Type, r: S & T) -> S & Maybe<&1, T>:
558	  (s, v) = r
559	  (s, Some{v})
560	
561	# Allocate a result list in forward order; evaluate callbacks tail to head.
562	
563	def map_to_list(~S: Type, ~N: Data, ~V: Data, ~T: Type, ~C: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, ~fn: S -> C -> V -> S & T, +fuel: Nat, s: S, +h: H, +c: C) -> S & Result<&2, &1, E.Error, List<&1, T>>:
564	  flat_map_to_list(~S, ~N, ~V, ~T, ~C, ~H, ~get_head, ~next, ~prev, ~value, ~(s => c => v => map_some_result(~S, ~T, fn(s, c, v))), fuel, s, h, c)
565	
566	# Allocate an owning list of observed values in forward order.
567	
568	def to_list(~S: Type, ~N: Data, ~V: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> S & Maybe<&2, N>, ~value: S -> N -> S & V, +fuel: Nat, s: S, +h: H) -> S & Result<&2, &1, E.Error, List<&1, V>>:
569	  map_to_list(~S, ~N, ~V, ~V, ~Unit, ~H, ~get_head, ~next, ~prev, ~value, ~(s => c => v => (s, v)), fuel, s, h, Unit{})
570	
571	def append_node(~S: Type, ~N: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, s: S, +head: Maybe<&2, N>, +tail: Maybe<&2, N>, +node: N) -> S & (Maybe<&2, N> & Maybe<&2, N>):
572	  match head:
573	    case None{}: (s, (Some{node}, Some{node}))
574	    case Some{+h}:
575	      (write_next(~S, ~N, ~set_next, set_next(set_prev(s, node, tail), node, None{}), tail, Some{node}), (Some{h}, Some{node}))
576	
577	def build_step_1(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> V -> S & N, +head: Maybe<&2, N>, +tail: Maybe<&2, N>, r: S & N) -> S & (Maybe<&2, N> & Maybe<&2, N>):
578	  (s, +node) = r
579	  append_node(~S, ~N, ~set_next, ~set_prev, s, head, tail, node)
580	
581	def build_step(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> V -> S & N, s: S, +c: C, +head: Maybe<&2, N>, +tail: Maybe<&2, N>, +v: V) -> S & (Maybe<&2, N> & Maybe<&2, N>):
582	  build_step_1(~S, ~N, ~V, ~C, ~set_next, ~set_prev, ~make, head, tail, make(s, c, v))
583	
584	def build_loop(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> V -> S & N, +xs: List<&2, V>, +c: C, r: S & (Maybe<&2, N> & Maybe<&2, N>)) -> S & Maybe<&2, N>:
585	  match xs r:
586	    case Nil{} Tuple{s, Tuple{head, tail}}: (s, head)
587	    case Con{v, rest} Tuple{s, Tuple{head, tail}}:
588	      build_loop(~S, ~N, ~V, ~C, ~set_next, ~set_prev, ~make, rest, c, build_step(~S, ~N, ~V, ~C, ~set_next, ~set_prev, ~make, s, c, head, tail, v))
589	
590	# Build from values in forward order using an application factory; return the head.
591	# Factories must return distinct detached nodes. The root is not published here.
592	
593	def from_values(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> V -> S & N, s: S, +xs: List<&2, V>, +c: C) -> S & Maybe<&2, N>:
594	  build_loop(~S, ~N, ~V, ~C, ~set_next, ~set_prev, ~make, xs, c, (s, (None{}, None{})))
595	
596	# Link distinct detached nodes in input order; return the head without allocating nodes.
597	
598	def from_nodes(~S: Type, ~N: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, s: S, +xs: List<&2, N>) -> S & Maybe<&2, N>:
599	  from_values(~S, ~N, ~N, ~Unit, ~set_next, ~set_prev, ~(s => c => n => (s, n)), s, xs, Unit{})
600	
601	def mapped_factory_1(~S: Type, ~N: Data, ~V: Data, ~D: Data, ~C: Data, ~convert: S -> C -> V -> S & D, ~make: S -> C -> D -> S & N, +c: C, r: S & D) -> S & N:
602	  (s, +d) = r
603	  make(s, c, d)
604	
605	def mapped_factory(~S: Type, ~N: Data, ~V: Data, ~D: Data, ~C: Data, ~convert: S -> C -> V -> S & D, ~make: S -> C -> D -> S & N, s: S, +c: C, +v: V) -> S & N:
606	  mapped_factory_1(~S, ~N, ~V, ~D, ~C, ~convert, ~make, c, convert(s, c, v))
607	
608	# Convert then construct each node, both in forward order; return the head.
609	
610	def map_from_values(~S: Type, ~N: Data, ~V: Data, ~D: Data, ~C: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~convert: S -> C -> V -> S & D, ~make: S -> C -> D -> S & N, s: S, +xs: List<&2, V>, +c: C) -> S & Maybe<&2, N>:
611	  from_values(~S, ~N, ~V, ~C, ~set_next, ~set_prev, ~(s => c => v => mapped_factory(~S, ~N, ~V, ~D, ~C, ~convert, ~make, s, c, v)), s, xs, c)
612	
613	# Map each input to a detached node in forward order; return the head.
614	
615	def map_from_nodes(~S: Type, ~N: Data, ~V: Data, ~C: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, ~set_prev: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> V -> S & N, s: S, +xs: List<&2, V>, +c: C) -> S & Maybe<&2, N>:
616	  from_values(~S, ~N, ~V, ~C, ~set_next, ~set_prev, ~make, s, xs, c)
617	
618	# Push a detached node onto the LIFO pool; leave its payload unchanged. O(1).
619	
620	def pool_free(~S: Type, ~N: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, s: S, pool: E.Pool<N>, +node: N) -> S & E.Pool<N>:
621	  E.Pool{head, count} = pool
622	  (set_next(s, node, head), E.Pool{Some{node}, 1n+count})
623	
624	def pool_take_1(~S: Type, ~N: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> S & N, +node: N, +count: Nat, r: S & Maybe<&2, N>) -> S & (E.Pool<N> & N):
625	  (s, +after) = r
626	  (set_next(s, node, None{}), (E.Pool{after, Nat.sub(count, 1n)}, node))
627	
628	def pool_take(~S: Type, ~N: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> S & N, s: S, +node: N, +count: Nat) -> S & (E.Pool<N> & N):
629	  pool_take_1(~S, ~N, ~C, ~next, ~set_next, ~make, node, count, next(s, node))
630	
631	def pool_fresh_1(~S: Type, ~N: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> S & N, r: S & N) -> S & (E.Pool<N> & N):
632	  (s, +node) = r
633	  (s, (E.Pool{None{}, 0n}, node))
634	
635	def pool_fresh(~S: Type, ~N: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> S & N, s: S, +c: C) -> S & (E.Pool<N> & N):
636	  pool_fresh_1(~S, ~N, ~C, ~next, ~set_next, ~make, make(s, c))
637	
638	# Pop and clear the next link, or call make only when empty. O(1) before make.
639	
640	def pool_next(~S: Type, ~N: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~set_next: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> S & N, s: S, pool: E.Pool<N>, +c: C) -> S & (E.Pool<N> & N):
641	  match pool:
642	    case E.Pool{None{}, count}: pool_fresh(~S, ~N, ~C, ~next, ~set_next, ~make, s, c)
643	    case E.Pool{Some{node}, count}: pool_take(~S, ~N, ~C, ~next, ~set_next, ~make, s, node, count)
644	
645	def pool_grow_step_1(~S: Type, ~N: Data, ~C: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> S & N, pool: E.Pool<N>, r: S & N) -> S & E.Pool<N>:
646	  (s, +node) = r
647	  pool_free(~S, ~N, ~set_next, s, pool, node)
648	
649	def pool_grow_step(~S: Type, ~N: Data, ~C: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> S & N, s: S, pool: E.Pool<N>, +c: C) -> S & E.Pool<N>:
650	  pool_grow_step_1(~S, ~N, ~C, ~set_next, ~make, pool, make(s, c))
651	
652	def pool_grow(~S: Type, ~N: Data, ~C: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> S & N, +size: Nat, +c: C, r: S & E.Pool<N>) -> S & E.Pool<N>:
653	  match size r:
654	    case 0n Tuple{s, pool}: (s, pool)
655	    case 1n+p Tuple{s, pool}:
656	      pool_grow(~S, ~N, ~C, ~set_next, ~make, p, c, pool_grow_step(~S, ~N, ~C, ~set_next, ~make, s, pool, c))
657	
658	def pool_new_1(~S: Type, ~N: Data, ~C: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> S & N, +size: Nat, +c: C, r: S & N) -> S & E.Pool<N>:
659	  (s, +node) = r
660	  pool_grow(~S, ~N, ~C, ~set_next, ~make, Nat.sub(size, 1n), c, (s, E.Pool{Some{node}, 1n}))
661	
662	# Construct max(size, 1) nodes in a LIFO pool, using the application factory.
663	
664	def pool_new(~S: Type, ~N: Data, ~C: Data, ~set_next: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> S & N, +size: Nat, s: S, +c: C) -> S & E.Pool<N>:
665	  pool_new_1(~S, ~N, ~C, ~set_next, ~make, size, c, make(s, c))
666	
667	# Optional detached value wrapper. The application owns its storage and identities.
668	
669	def new_node(~N: Data, ~V: Data, +v: V) -> E.DefaultNode<N, V>:
670	  E.Node{None{}, None{}, v}