1	# Generated by tools/generators/intrusive_list.py; edit that source.
2	import Base
3	import ./internal/intrusive_list.bend as Impl
4	import ./types/intrusive_doubly_linked_list.bend as E
5	
6	# Application-owned membership. Bind static accessors once; see docs/INTRUSIVE_LIST.md.
7	# Known-member edits require valid membership; callbacks must obey the documented
8	# traversal contract. clear visits the suffix before the original head; the
9	# map_* builders visit tail-first.
10	
11	# Read the next identity without changing membership.
12	def next(~S: Type, ~N: Data, ~next_of: S -> N -> S & Maybe<&2, N>, s: S, +node: N) -> S & Maybe<&2, N>:
13	  Impl.next(~S, ~N, ~next_of, s, node)
14	
15	# Read the previous identity without changing membership.
16	def prev(~S: Type, ~N: Data, ~prev_of: S -> N -> S & Maybe<&2, N>, s: S, +node: N) -> S & Maybe<&2, N>:
17	  Impl.prev(~S, ~N, ~prev_of, s, node)
18	
19	# Observe a Data value (often the entity identity); payload ownership stays in S.
20	def value(~S: Type, ~N: Data, ~V: Data, ~value_of: S -> N -> S & V, s: S, +node: N) -> S & V:
21	  Impl.value(~S, ~N, ~V, ~value_of, s, node)
22	
23	# Read a root; requires no writer context.
24	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>:
25	  Impl.get_head(~S, ~N, ~H, ~get_head, s, h)
26	
27	# Detach a known member in O(1). Uses the nullable root setter only for a head.
28	# Requires no root reader; preserves the node identity and payload.
29	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:
30	  Impl.remove(~S, ~N, ~I, ~next, ~prev, ~set_next, ~set_prev, ~set_head, s, i, node)
31	
32	# Prepend a detached node in O(1), using separate read/write contexts.
33	# Calls the nonempty root setter exactly once.
34	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:
35	  Impl.prepend_as(~S, ~N, ~H, ~I, ~get_head, ~set_next, ~set_prev, ~set_head_nonempty, s, h, i, node)
36	
37	# Prepend with the same context used to read and write the root.
38	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:
39	  Impl.prepend(~S, ~N, ~H, ~get_head, ~set_next, ~set_prev, ~set_head_nonempty, s, h, node)
40	
41	# O(1) empty-root query.
42	def is_empty(~S: Type, ~N: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, s: S, +h: H) -> S & Bool:
43	  Impl.is_empty(~S, ~N, ~H, ~get_head, s, h)
44	
45	# O(1) nonempty-root query.
46	def non_empty(~S: Type, ~N: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, s: S, +h: H) -> S & Bool:
47	  Impl.non_empty(~S, ~N, ~H, ~get_head, s, h)
48	
49	# O(1) query: head exists and has a successor.
50	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:
51	  Impl.at_least_two(~S, ~N, ~H, ~get_head, ~next, s, h)
52	
53	# Forward fold, saving next before each callback. The accumulator may own Type data.
54	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>:
55	  Impl.fold_left(~S, ~N, ~V, ~A, ~C, ~H, ~get_head, ~next, ~value, ~fn, fuel, s, h, c, acc)
56	
57	# Forward visit, saving next before each callback; removing current is supported.
58	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>:
59	  Impl.foreach(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~fn, fuel, s, h, c)
60	
61	# Return the first matching node identity; next is read after a failed predicate.
62	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>>:
63	  Impl.find(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~pred, fuel, s, h, c)
64	
65	# Compatibility alias of find; Bend needs no preallocated Option wrapper.
66	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>>:
67	  Impl.find_some_this(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~pred, fuel, s, h, c)
68	
69	# Short-circuit on the first true predicate; False for an empty list.
70	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>:
71	  Impl.exists(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~pred, fuel, s, h, c)
72	
73	# Short-circuit on the first false predicate; True for an empty list.
74	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>:
75	  Impl.forall(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~pred, fuel, s, h, c)
76	
77	# Count matching values; read next after each predicate. O(n).
78	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>:
79	  Impl.count(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~pred, fuel, s, h, c)
80	
81	# Count members in O(n); no cached count is required in the root.
82	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>:
83	  Impl.length(~S, ~N, ~H, ~get_head, ~next, fuel, s, h)
84	
85	# Convert once per visited value, skip failed conversions, return the original node.
86	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>>:
87	  Impl.find_convert(~S, ~N, ~V, ~D, ~C, ~H, ~get_head, ~next, ~value, ~convert, ~pred, fuel, s, h, c)
88	
89	# Find with eq(wanted, observed_value), returning the node identity.
90	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>>:
91	  Impl.find_value(~S, ~N, ~V, ~H, ~get_head, ~next, ~value, ~eq, fuel, s, h, wanted)
92	
93	# Find with eq(converted_value, wanted), returning the original node.
94	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>>:
95	  Impl.find_value_convert(~S, ~N, ~V, ~D, ~H, ~get_head, ~next, ~value, ~convert, ~eq, fuel, s, h, wanted)
96	
97	# Preflight the bound, publish an empty root, detach suffix then original head.
98	# Call post_remove once per detached node; a no-op callback needs no allocation.
99	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>:
100	  Impl.clear_list_as(~S, ~N, ~H, ~I, ~C, ~get_head, ~next, ~set_next, ~set_prev, ~set_head, ~post_remove, fuel, s, h, i, c)
101	
102	# Clear using one root context; see clear_list_as for callback order.
103	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>:
104	  Impl.clear_list(~S, ~N, ~H, ~C, ~get_head, ~next, ~set_next, ~set_prev, ~set_head, ~post_remove, fuel, s, h, c)
105	
106	# Clear using a callback that returns each detached node to an application pool.
107	# The pool argument locates that pool in S; post_remove performs the free.
108	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>:
109	  Impl.clear_list_with_pool_as(~S, ~N, ~H, ~I, ~C, ~get_head, ~next, ~set_next, ~set_prev, ~set_head, ~post_remove, fuel, s, h, i, pool)
110	
111	# Clear to a pool using one root context.
112	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>:
113	  Impl.clear_list_with_pool(~S, ~N, ~H, ~C, ~get_head, ~next, ~set_next, ~set_prev, ~set_head, ~post_remove, fuel, s, h, pool)
114	
115	# Keep true values, detach false values, then call post_remove on the removed node.
116	# Re-read the live head in the prefix; save next when visiting the retained tail.
117	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>:
118	  Impl.foreach_remove_filter_as(~S, ~N, ~V, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, fuel, s, h, i, c)
119	
120	# Removal filter with one root context.
121	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>:
122	  Impl.foreach_remove_filter(~S, ~N, ~V, ~H, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~pred, ~post_remove, fuel, s, h, c)
123	
124	# Remove failed conversions and false predicates; convert each visited value once.
125	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>:
126	  Impl.foreach_remove_convert_filter_as(~S, ~N, ~V, ~D, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~convert, ~pred, ~post_remove, fuel, s, h, i, c)
127	
128	# Conversion/removal filter with one root context.
129	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>:
130	  Impl.foreach_remove_convert_filter(~S, ~N, ~V, ~D, ~H, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~convert, ~pred, ~post_remove, fuel, s, h, c)
131	
132	# Visit successfully converted values, remove failed conversions.
133	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>:
134	  Impl.foreach_remove_convert_as(~S, ~N, ~V, ~D, ~H, ~I, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~convert, ~fn, ~post_remove, fuel, s, h, i, c)
135	
136	# Conversion/removal visitor with one root context.
137	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>:
138	  Impl.foreach_remove_convert(~S, ~N, ~V, ~D, ~H, ~C, ~get_head, ~next, ~prev, ~set_next, ~set_prev, ~set_head, ~value, ~convert, ~fn, ~post_remove, fuel, s, h, c)
139	
140	# Option filter-map: zero or one output per input. Callbacks run tail to head;
141	# the newly allocated owning result list retains forward input order.
142	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>>:
143	  Impl.flat_map_to_list(~S, ~N, ~V, ~T, ~C, ~H, ~get_head, ~next, ~prev, ~value, ~fn, fuel, s, h, c)
144	
145	# Allocate a result list in forward order; evaluate callbacks tail to head.
146	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>>:
147	  Impl.map_to_list(~S, ~N, ~V, ~T, ~C, ~H, ~get_head, ~next, ~prev, ~value, ~fn, fuel, s, h, c)
148	
149	# Allocate an owning list of observed values in forward order.
150	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>>:
151	  Impl.to_list(~S, ~N, ~V, ~H, ~get_head, ~next, ~prev, ~value, fuel, s, h)
152	
153	# Build from values in forward order using an application factory; return the head.
154	# Factories must return distinct detached nodes. The root is not published here.
155	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>:
156	  Impl.from_values(~S, ~N, ~V, ~C, ~set_next, ~set_prev, ~make, s, xs, c)
157	
158	# Link distinct detached nodes in input order; return the head without allocating nodes.
159	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>:
160	  Impl.from_nodes(~S, ~N, ~set_next, ~set_prev, s, xs)
161	
162	# Convert then construct each node, both in forward order; return the head.
163	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>:
164	  Impl.map_from_values(~S, ~N, ~V, ~D, ~C, ~set_next, ~set_prev, ~convert, ~make, s, xs, c)
165	
166	# Map each input to a detached node in forward order; return the head.
167	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>:
168	  Impl.map_from_nodes(~S, ~N, ~V, ~C, ~set_next, ~set_prev, ~make, s, xs, c)
169	
170	# Push a detached node onto the LIFO pool; leave its payload unchanged. O(1).
171	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>:
172	  Impl.pool_free(~S, ~N, ~set_next, s, pool, node)
173	
174	# Pop and clear the next link, or call make only when empty. O(1) before make.
175	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):
176	  Impl.pool_next(~S, ~N, ~C, ~next, ~set_next, ~make, s, pool, c)
177	
178	# Construct max(size, 1) nodes in a LIFO pool, using the application factory.
179	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>:
180	  Impl.pool_new(~S, ~N, ~C, ~set_next, ~make, size, s, c)
181	
182	# Optional detached value wrapper. The application owns its storage and identities.
183	def new_node(~N: Data, ~V: Data, +v: V) -> E.DefaultNode<N, V>:
184	  Impl.new_node(~N, ~V, v)