src/containers/internal/intrusive_list.bend source

src/containers/internal/intrusive_list.bend on the hub · documented module

# Generated by tools/generators/intrusive_list.py; edit that source.import Baseimport ../types/intrusive_doubly_linked_list.bend as E# Intrusive doubly linked lists over application-owned nodes and roots.## S is the affine application state, N a reusable node identity. Link accessors# select one association; the same entity may have several independent pairs# of links. H and I are independent read/write contexts for the same root.# No container, tail, count, payload copy, or node allocation is required by# prepend/remove. Bind the closed ~ accessors once in an application module.## Preconditions: valid identities and coherent roots; prepend's node is# detached in this association; remove's node belongs to the supplied root.# Accessors preserve unrelated fields. Raw user input must be validated by# the application before entering this preconditioned API.## Traversals take an explicit step bound because array links are not a# structurally decreasing Bend value. Exhaustion returns LimitExceeded with# the updated state; callback effects already performed are retained.# Link reads must be observations, and root hooks must preserve coherent links.# clear preflights fuel before any write; callbacks may change only detached# nodes and unrelated state, leaving the unvisited suffix intact.# For finite fixed/decreasing membership, arena capacity is a sufficient# O(1)-available bound. Callbacks must not invalidate a cached successor.# Read the next identity without changing membership.def next(~S: Type, ~N: Data, ~next_of: S -> N -> S & Maybe<&2, N>, s: S, +node: N) -> S & Maybe<&2, N>:  next_of(s, node)# Read the previous identity without changing membership.def prev(~S: Type, ~N: Data, ~prev_of: S -> N -> S & Maybe<&2, N>, s: S, +node: N) -> S & Maybe<&2, N>:  prev_of(s, node)# Observe a Data value (often the entity identity); payload ownership stays in S.def value(~S: Type, ~N: Data, ~V: Data, ~value_of: S -> N -> S & V, s: S, +node: N) -> S & V:  value_of(s, node)# Read a root; requires no writer context.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>:  get_head(s, h)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:  match at:    case None{}: s    case Some{a}: set_next(s, a, node)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:  match at:    case None{}: s    case Some{a}: set_prev(s, a, node)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:  match before:    case None{}:      set_next(set_head(s, i, after), node, None{})    case Some{+p}:      set_next(set_prev(set_next(s, p, after), node, None{}), node, None{})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:  remove_left(~S, ~N, ~I, ~set_next, ~set_prev, ~set_head, s, i, node, before, after)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:  (s, +before) = r  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))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:  (s, +after) = r  remove_2(~S, ~N, ~I, ~next, ~prev, ~set_next, ~set_prev, ~set_head, i, node, after, prev(s, node))# Detach a known member in O(1). Uses the nullable root setter only for a head.# Requires no root reader; preserves the node identity and payload.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:  remove_1(~S, ~N, ~I, ~next, ~prev, ~set_next, ~set_prev, ~set_head, i, node, next(s, node))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:  set_head_nonempty(s, i, node)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:  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}))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:  (s, +head) = r  prepend_as_2(~S, ~N, ~H, ~I, ~get_head, ~set_next, ~set_prev, ~set_head_nonempty, i, node, head, set_next(s, node, head))# Prepend a detached node in O(1), using separate read/write contexts.# Calls the nonempty root setter exactly once.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:  prepend_as_1(~S, ~N, ~H, ~I, ~get_head, ~set_next, ~set_prev, ~set_head_nonempty, i, node, get_head(s, h))# Prepend with the same context used to read and write the root.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:  prepend_as(~S, ~N, ~H, ~H, ~get_head, ~set_next, ~set_prev, ~set_head_nonempty, s, h, h, node)def empty_result(~S: Type, ~N: Data, r: S & Maybe<&2, N>) -> S & Bool:  (s, m) = r  (s, Maybe.is_none(&2, N, m))def nonempty_result(~S: Type, ~N: Data, r: S & Maybe<&2, N>) -> S & Bool:  (s, m) = r  (s, Maybe.is_some(&2, N, m))# O(1) empty-root query.def is_empty(~S: Type, ~N: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, s: S, +h: H) -> S & Bool:  empty_result(~S, ~N, get_head(s, h))# O(1) nonempty-root query.def non_empty(~S: Type, ~N: Data, ~H: Data, ~get_head: S -> H -> S & Maybe<&2, N>, s: S, +h: H) -> S & Bool:  nonempty_result(~S, ~N, get_head(s, h))def two_head(~S: Type, ~N: Data, ~next: S -> N -> S & Maybe<&2, N>, s: S, +head: Maybe<&2, N>) -> S & Bool:  match head:    case None{}: (s, False{})    case Some{n}: nonempty_result(~S, ~N, next(s, n))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:  (s, +head) = r  two_head(~S, ~N, ~next, s, head)# O(1) query: head exists and has a successor.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:  at_least_two_1(~S, ~N, ~H, ~get_head, ~next, get_head(s, h))# Forward visits save the successor before invoking user code.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):  (s, acc) = r  (s, (after, acc))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):  (s, +v) = r  fold_step_3(~S, ~N, ~V, ~A, ~C, ~next, ~value, ~fn, after, fn(s, c, acc, v))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):  (s, +after) = r  fold_step_2(~S, ~N, ~V, ~A, ~C, ~next, ~value, ~fn, c, acc, after, value(s, node))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):  fold_step_1(~S, ~N, ~V, ~A, ~C, ~next, ~value, ~fn, node, c, acc, next(s, node))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>:  match fuel r:    case _ Tuple{s, Tuple{None{}, acc}}: (s, Done{acc})    case 0n Tuple{s, Tuple{Some{node}, acc}}: (s, Fail{E.LimitExceeded{}})    case 1n+p Tuple{s, Tuple{Some{node}, acc}}:      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))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>:  (s, +head) = r  fold_loop(~S, ~N, ~V, ~A, ~C, ~next, ~value, ~fn, fuel, c, (s, (head, acc)))# Forward fold, saving next before each callback. The accumulator may own Type data.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>:  fold_left_1(~S, ~N, ~V, ~A, ~C, ~H, ~get_head, ~next, ~value, ~fn, fuel, c, acc, get_head(s, h))def visit_fold(~S: Type, ~V: Data, ~C: Data, ~fn: S -> C -> V -> S, s: S, +c: C, unit: Unit, +v: V) -> S & Unit:  (fn(s, c, v), Unit{})# Forward visit, saving next before each callback; removing current is supported.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>:  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{})def search_next_1(~S: Type, ~N: Data, ~next: S -> N -> S & Maybe<&2, N>, r: S & Maybe<&2, N>) -> S & E.Search<N>:  (s, +after) = r  (s, E.Seeking{after})def search_next(~S: Type, ~N: Data, ~next: S -> N -> S & Maybe<&2, N>, s: S, +node: N) -> S & E.Search<N>:  search_next_1(~S, ~N, ~next, next(s, node))def search_choice(~S: Type, ~N: Data, ~next: S -> N -> S & Maybe<&2, N>, s: S, +node: N, +hit: Bool) -> S & E.Search<N>:  match hit:    case True{}: (s, E.Found{node})    case False{}: search_next(~S, ~N, ~next, s, node)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>:  (s, +hit) = r  search_choice(~S, ~N, ~next, s, node, hit)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>:  (s, +v) = r  search_step_2(~S, ~N, ~V, ~C, ~next, ~value, ~pred, node, pred(s, c, v))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>:  search_step_1(~S, ~N, ~V, ~C, ~next, ~value, ~pred, node, c, value(s, node))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>>:  match fuel r:    case _ Tuple{s, E.Found{node}}: (s, Done{Some{node}})    case _ Tuple{s, E.Seeking{None{}}}: (s, Done{None{}})    case 0n Tuple{s, E.Seeking{Some{node}}}: (s, Fail{E.LimitExceeded{}})    case 1n+p Tuple{s, E.Seeking{Some{node}}}:      search_loop(~S, ~N, ~V, ~C, ~next, ~value, ~pred, p, c, search_step(~S, ~N, ~V, ~C, ~next, ~value, ~pred, s, node, c))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>>:  (s, +head) = r  search_loop(~S, ~N, ~V, ~C, ~next, ~value, ~pred, fuel, c, (s, E.Seeking{head}))# Return the first matching node identity; next is read after a failed predicate.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>>:  find_1(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~pred, fuel, c, get_head(s, h))# Compatibility alias of find; Bend needs no preallocated Option wrapper.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>>:  find(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~pred, fuel, s, h, c)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>:  match negate r:    case _ Tuple{s, Fail{e}}: (s, Fail{e})    case False{} Tuple{s, Done{m}}: (s, Done{Maybe.is_some(&2, N, m)})    case True{} Tuple{s, Done{m}}: (s, Done{Maybe.is_none(&2, N, m)})# Short-circuit on the first true predicate; False for an empty list.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>:  search_bool(~S, ~N, False{}, find(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~pred, fuel, s, h, c))def negated_result(~S: Type, r: S & Bool) -> S & Bool:  (s, b) = r  (s, Bool.not(b))def negated_pred(~S: Type, ~V: Data, ~C: Data, ~pred: S -> C -> V -> S & Bool, s: S, +c: C, +v: V) -> S & Bool:  negated_result(~S, pred(s, c, v))# Short-circuit on the first false predicate; True for an empty list.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>:  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))def count_pick(~S: Type, +count: Nat, r: S & Bool) -> S & Nat:  match r:    case Tuple{s, True{}}: (s, 1n+count)    case Tuple{s, False{}}: (s, count)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):  (s, +after) = r  (s, (after, acc))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):  (s, +acc) = r  count_step_3(~S, ~N, ~V, ~C, ~next, ~value, ~pred, acc, next(s, node))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):  (s, +v) = r  count_step_2(~S, ~N, ~V, ~C, ~next, ~value, ~pred, node, count_pick(~S, acc, pred(s, c, v)))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):  count_step_1(~S, ~N, ~V, ~C, ~next, ~value, ~pred, node, c, acc, value(s, node))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>:  match fuel r:    case _ Tuple{s, Tuple{None{}, acc}}: (s, Done{acc})    case 0n Tuple{s, Tuple{Some{node}, acc}}: (s, Fail{E.LimitExceeded{}})    case 1n+p Tuple{s, Tuple{Some{node}, acc}}:      count_loop(~S, ~N, ~V, ~C, ~next, ~value, ~pred, p, c, count_step(~S, ~N, ~V, ~C, ~next, ~value, ~pred, s, node, c, acc))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>:  (s, +head) = r  count_loop(~S, ~N, ~V, ~C, ~next, ~value, ~pred, fuel, c, (s, (head, 0n)))# Count matching values; read next after each predicate. O(n).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>:  count_1(~S, ~N, ~V, ~C, ~H, ~get_head, ~next, ~value, ~pred, fuel, c, get_head(s, h))def node_value(~S: Type, ~N: Data, s: S, +n: N) -> S & N:  (s, n)def count_node(~S: Type, ~N: Data, s: S, c: Unit, +acc: Nat, +node: N) -> S & Nat:  (s, 1n+acc)# Count members in O(n); no cached count is required in the root.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>:  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)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:  match r:    case Tuple{s, None{}}: (s, False{})    case Tuple{s, Some{v}}: pred(s, c, v)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:  converted_pred_result(~S, ~V, ~D, ~C, ~convert, ~pred, c, convert(s, v))# Convert once per visited value, skip failed conversions, return the original node.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>>:  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)def equal_value(~S: Type, ~V: Data, ~eq: V -> V -> Bool, s: S, +wanted: V, +v: V) -> S & Bool:  (s, eq(wanted, v))# Find with eq(wanted, observed_value), returning the node identity.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>>:  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)def equal_converted_value(~S: Type, ~V: Data, ~eq: V -> V -> Bool, s: S, +wanted: V, +v: V) -> S & Bool:  (s, eq(v, wanted))# Find with eq(converted_value, wanted), returning the original node.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>>:  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)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>:  (s, after)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>:  clear_step_3(~S, ~N, ~C, ~next, ~set_next, ~set_prev, ~post_remove, after, post_remove(s, c, node))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>:  (s, +after) = r  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{}))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>:  clear_step_1(~S, ~N, ~C, ~next, ~set_next, ~set_prev, ~post_remove, node, c, next(s, node))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>:  match fuel r:    case 0n Tuple{s, cursor}: (s, Fail{E.LimitExceeded{}})    case 1n+p Tuple{s, None{}}:      (post_remove(set_next(s, head, None{}), c, head), Done{Unit{}})    case 1n+p Tuple{s, Some{node}}:      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))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>:  match fuel head:    case _ None{}: (s, Done{Unit{}})    case 0n Some{node}: (s, Fail{E.LimitExceeded{}})    case 1n+p Some{node}:      clear_loop(~S, ~N, ~C, ~next, ~set_next, ~set_prev, ~post_remove, 1n+p, node, c, next(set_head(s, i, None{}), node))def chain_fits(~S: Type, ~N: Data, ~next: S -> N -> S & Maybe<&2, N>, +fuel: Nat, r: S & Maybe<&2, N>) -> S & Bool:  match fuel r:    case _ Tuple{s, None{}}: (s, True{})    case 0n Tuple{s, Some{node}}: (s, False{})    case 1n+p Tuple{s, Some{node}}:      chain_fits(~S, ~N, ~next, p, next(s, node))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>:  match r:    case Tuple{s, False{}}: (s, Fail{E.LimitExceeded{}})    case Tuple{s, True{}}:      clear_head(~S, ~N, ~H, ~I, ~C, ~get_head, ~next, ~set_next, ~set_prev, ~set_head, ~post_remove, fuel, s, h, i, c, head)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>:  (s, +head) = r  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)))# Preflight the bound, publish an empty root, detach suffix then original head.# Call post_remove once per detached node; a no-op callback needs no allocation.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>:  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))# Clear using one root context; see clear_list_as for callback order.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>:  clear_list_as(~S, ~N, ~H, ~H, ~C, ~get_head, ~next, ~set_next, ~set_prev, ~set_head, ~post_remove, fuel, s, h, h, c)def ignore_removed(~S: Type, ~C: Data, ~N: Data, s: S, +c: C, +node: N) -> S:  s# Clear using a callback that returns each detached node to an application pool.# The pool argument locates that pool in S; post_remove performs the free.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>:  clear_list_as(~S, ~N, ~H, ~I, ~C, ~get_head, ~next, ~set_next, ~set_prev, ~set_head, ~post_remove, fuel, s, h, i, pool)# Clear to a pool using one root context.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>:  clear_list(~S, ~N, ~H, ~C, ~get_head, ~next, ~set_next, ~set_prev, ~set_head, ~post_remove, fuel, s, h, pool)# Prefix predicates re-read the live head; the remaining tail saves next.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:  match before:    case None{}: (s, False{})    case Some{+p}:      (set_prev(set_next(set_next(write_prev(~S, ~N, ~set_prev, s, after, Some{p}), p, after), node, None{}), node, None{}), True{})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:  (s, +before) = r  unlink_nonhead_links(~S, ~N, ~set_next, ~set_prev, s, node, before, after)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:  (s, +after) = r  unlink_nonhead_2(~S, ~N, ~next, ~prev, ~set_next, ~set_prev, node, after, prev(s, node))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:  unlink_nonhead_1(~S, ~N, ~next, ~prev, ~set_next, ~set_prev, node, next(s, node))def filter_prefix_result(~S: Type, ~N: Data, r: S & Maybe<&2, N>) -> S & E.Filter<N>:  (s, head) = r  (s, E.Prefix{head})def filter_tail_result(~S: Type, ~N: Data, r: S & Maybe<&2, N>) -> S & E.Filter<N>:  (s, head) = r  (s, E.Tail{head})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>:  match r:    case Tuple{s, None{}}: (s, E.FilterFailed{E.InvalidTraversal{}})    case Tuple{s, Some{head}}: filter_tail_result(~S, ~N, next(s, head))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>:  match r:    case Tuple{s, None{}}: (s, E.FilterFailed{E.InvalidTraversal{}})    case Tuple{s, Some{+node}}:      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))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>:  match r:    case Tuple{s, True{}}:      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))    case Tuple{s, False{}}:      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))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>:  (s, +v) = r  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))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>:  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))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>:  match r:    case Tuple{s, False{}}: (s, E.FilterFailed{E.InvalidTraversal{}})    case Tuple{s, True{}}: (post_remove(s, c, node), E.Tail{after})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>:  match r:    case Tuple{s, True{}}: (s, E.Tail{after})    case Tuple{s, False{}}:      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))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>:  (s, +v) = r  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))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>:  (s, +after) = r  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))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>:  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))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>:  match fuel r:    case _ Tuple{s, E.FilterFailed{e}}: (s, Fail{e})    case _ Tuple{s, E.Prefix{None{}}}: (s, Done{Unit{}})    case _ Tuple{s, E.Tail{None{}}}: (s, Done{Unit{}})    case 0n Tuple{s, E.Prefix{Some{node}}}: (s, Fail{E.LimitExceeded{}})    case 0n Tuple{s, E.Tail{Some{node}}}: (s, Fail{E.LimitExceeded{}})    case 1n+p Tuple{s, E.Prefix{Some{node}}}:      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))    case 1n+p Tuple{s, E.Tail{Some{node}}}:      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))# Keep true values, detach false values, then call post_remove on the removed node.# Re-read the live head in the prefix; save next when visiting the retained tail.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>:  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)))# Removal filter with one root context.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>:  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)# Remove failed conversions and false predicates; convert each visited value once.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>:  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)# Conversion/removal filter with one root context.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>:  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)def visit_true(~S: Type, ~D: Data, ~C: Data, ~fn: S -> C -> D -> S, s: S, +c: C, +v: D) -> S & Bool:  (fn(s, c, v), True{})# Visit successfully converted values, remove failed conversions.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>:  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)# Conversion/removal visitor with one root context.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>:  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)def last_fold(~S: Type, ~N: Data, s: S, c: Unit, +acc: Maybe<&2, N>, +node: N) -> S & Maybe<&2, N>:  (s, Some{node})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>>:  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{})def mapped_cons(~T: Type, m: Maybe<&1, T>, xs: List<&1, T>) -> List<&1, T>:  match m:    case None{}: xs    case Some{x}: Con{x, xs}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>):  (s, +before) = r  (s, (before, xs))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>):  map_step_4(~S, ~N, ~V, ~T, ~C, ~prev, ~value, ~fn, xs, prev(s, node))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>):  (s, m) = r  map_step_3(~S, ~N, ~V, ~T, ~C, ~prev, ~value, ~fn, node, s, mapped_cons(~T, m, xs))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>):  (s, +v) = r  map_step_2(~S, ~N, ~V, ~T, ~C, ~prev, ~value, ~fn, node, xs, fn(s, c, v))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>):  map_step_1(~S, ~N, ~V, ~T, ~C, ~prev, ~value, ~fn, c, node, xs, value(s, node))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>>:  match fuel r:    case _ Tuple{s, Tuple{None{}, xs}}: (s, Done{xs})    case 0n Tuple{s, Tuple{Some{node}, xs}}: (s, Fail{E.LimitExceeded{}})    case 1n+p Tuple{s, Tuple{Some{node}, xs}}:      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))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>>:  match r:    case Tuple{s, Fail{e}}: (s, Fail{e})    case Tuple{s, Done{end}}:      map_loop(~S, ~N, ~V, ~T, ~C, ~prev, ~value, ~fn, fuel, c, (s, (end, Nil{})))# Option filter-map: zero or one output per input. Callbacks run tail to head;# the newly allocated owning result list retains forward input order.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>>:  map_last(~S, ~N, ~V, ~T, ~C, ~prev, ~value, ~fn, fuel, c, last(~S, ~N, ~H, ~get_head, ~next, fuel, s, h))def map_some_result(~S: Type, ~T: Type, r: S & T) -> S & Maybe<&1, T>:  (s, v) = r  (s, Some{v})# Allocate a result list in forward order; evaluate callbacks tail to head.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>>:  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)# Allocate an owning list of observed values in forward order.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>>:  map_to_list(~S, ~N, ~V, ~V, ~Unit, ~H, ~get_head, ~next, ~prev, ~value, ~(s => c => v => (s, v)), fuel, s, h, Unit{})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>):  match head:    case None{}: (s, (Some{node}, Some{node}))    case Some{+h}:      (write_next(~S, ~N, ~set_next, set_next(set_prev(s, node, tail), node, None{}), tail, Some{node}), (Some{h}, Some{node}))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>):  (s, +node) = r  append_node(~S, ~N, ~set_next, ~set_prev, s, head, tail, node)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>):  build_step_1(~S, ~N, ~V, ~C, ~set_next, ~set_prev, ~make, head, tail, make(s, c, v))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>:  match xs r:    case Nil{} Tuple{s, Tuple{head, tail}}: (s, head)    case Con{v, rest} Tuple{s, Tuple{head, tail}}:      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))# Build from values in forward order using an application factory; return the head.# Factories must return distinct detached nodes. The root is not published here.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>:  build_loop(~S, ~N, ~V, ~C, ~set_next, ~set_prev, ~make, xs, c, (s, (None{}, None{})))# Link distinct detached nodes in input order; return the head without allocating nodes.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>:  from_values(~S, ~N, ~N, ~Unit, ~set_next, ~set_prev, ~(s => c => n => (s, n)), s, xs, Unit{})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:  (s, +d) = r  make(s, c, d)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:  mapped_factory_1(~S, ~N, ~V, ~D, ~C, ~convert, ~make, c, convert(s, c, v))# Convert then construct each node, both in forward order; return the head.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>:  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)# Map each input to a detached node in forward order; return the head.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>:  from_values(~S, ~N, ~V, ~C, ~set_next, ~set_prev, ~make, s, xs, c)# Push a detached node onto the LIFO pool; leave its payload unchanged. O(1).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>:  E.Pool{head, count} = pool  (set_next(s, node, head), E.Pool{Some{node}, 1n+count})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):  (s, +after) = r  (set_next(s, node, None{}), (E.Pool{after, Nat.sub(count, 1n)}, node))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):  pool_take_1(~S, ~N, ~C, ~next, ~set_next, ~make, node, count, next(s, node))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):  (s, +node) = r  (s, (E.Pool{None{}, 0n}, node))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):  pool_fresh_1(~S, ~N, ~C, ~next, ~set_next, ~make, make(s, c))# Pop and clear the next link, or call make only when empty. O(1) before make.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):  match pool:    case E.Pool{None{}, count}: pool_fresh(~S, ~N, ~C, ~next, ~set_next, ~make, s, c)    case E.Pool{Some{node}, count}: pool_take(~S, ~N, ~C, ~next, ~set_next, ~make, s, node, count)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>:  (s, +node) = r  pool_free(~S, ~N, ~set_next, s, pool, node)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>:  pool_grow_step_1(~S, ~N, ~C, ~set_next, ~make, pool, make(s, c))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>:  match size r:    case 0n Tuple{s, pool}: (s, pool)    case 1n+p Tuple{s, pool}:      pool_grow(~S, ~N, ~C, ~set_next, ~make, p, c, pool_grow_step(~S, ~N, ~C, ~set_next, ~make, s, pool, c))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>:  (s, +node) = r  pool_grow(~S, ~N, ~C, ~set_next, ~make, Nat.sub(size, 1n), c, (s, E.Pool{Some{node}, 1n}))# Construct max(size, 1) nodes in a LIFO pool, using the application factory.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>:  pool_new_1(~S, ~N, ~C, ~set_next, ~make, size, c, make(s, c))# Optional detached value wrapper. The application owns its storage and identities.def new_node(~N: Data, ~V: Data, +v: V) -> E.DefaultNode<N, V>:  E.Node{None{}, None{}, v}