src/containers/internal/intrusive_list.bend
bend-collections-laws-containers@1.0.0.0 · 670 lines · 0 definitions
1# Generated by tools/generators/intrusive_list.py; edit that source.
2import Base
3import bend-collections-laws-containers@1.0.0.0/src/containers/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
29def 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
34def 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
39def 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
44def 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
47def 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
52def 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
57def 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
64def 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
67def 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
71def 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
78def 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
81def 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
84def 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
87def 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
94def 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
99def 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
102def 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
106def 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
112def 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
117def 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
120def 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
125def 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
131def 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
136def 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
140def 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
144def 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
148def 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
151def 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
158def 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
164def 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
167def 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
172def 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
175def 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
179def 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
182def 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
187def 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
191def 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
195def 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
198def 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
206def 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
212def 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
217def 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
220def 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
228def 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
231def negated_result(~S: Type, r: S & Bool) -> S & Bool:
232 (s, b) = r
233 (s, Bool.not(b))
234
235def 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
240def 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
243def 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
248def 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
252def 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
256def 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
260def 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
263def 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
270def 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
276def 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
279def node_value(~S: Type, ~N: Data, s: S, +n: N) -> S & N:
280 (s, n)
281
282def 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
287def 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
290def 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
295def 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
300def 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
303def 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
308def 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
311def 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
316def 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
319def 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
322def 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
325def 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
329def 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
332def 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
340def 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
347def 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
354def 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
360def 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
367def 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
372def 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
375def 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
381def 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
386def 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
391def 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
397def 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
401def 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
405def 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
408def 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
412def 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
416def 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
421def 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
427def 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
434def 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
438def 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
441def 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
446def 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
452def 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
456def 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
460def 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
463def 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
478def 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
483def 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
488def 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
493def 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
496def 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
501def 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
506def 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
509def 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
512def 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
515def 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
520def 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
524def 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
527def 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
531def 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
535def 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
538def 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
545def 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
554def 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
557def 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
563def 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
568def 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
571def 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
577def 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
581def 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
584def 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
593def 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
598def 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
601def 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
605def 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
610def 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
615def 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
620def 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
624def 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
628def 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
631def 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
635def 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
640def 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
645def 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
649def 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
652def 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
658def 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
664def 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
669def new_node(~N: Data, ~V: Data, +v: V) -> E.DefaultNode<N, V>:
670 E.Node{None{}, None{}, v}