# Generated by tools/generators/intrusive_list.py; edit that source.
import Base
import ../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}