src/containers/balanced_search_tree.bend source
src/containers/balanced_search_tree.bend on the hub · documented module
# Generated by tools/generators/tree_map.py; edit algorithm definitions there.import Baseimport ./dynamic_array.bend as Dimport ./types/dynamic_array.bend as DE# Indexed CLRS red-black map. Keys and payloads are Data for this version.# Comparator is a type index: changing comparator requires rebuilding a map.# Node links are slot indices plus one; zero is the black NIL sentinel.type Node<-K: Data> is Data: Free{next: Nat} N{red: Bool, left: Nat, right: Nat, parent: Nat, key: K}# Node storage: one array per node field instead of one array of Node# records. Reading a record out of an array hands back a shared copy that the# runtime reference-counts and takes apart field by field; a field read out of# its own array is a plain word. The store has the shape of a dynamic array# of nodes: slots [0, used) are live, the capacity is 2^depth <= 2^limit, and# it grows by doubling. A slot holds the encoding of its node by ntag (0 free,# 1 black, 2 red), nleft (the free-list link of a free slot), nright, nparent# and nkey (None when free); every other slot holds the encoding of Free{0},# so each array is exactly its field of the node list, padded.type NodeStore<-K: Data> is Type: NS{limit: Nat, depth: Nat, cap: Nat, used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>}type TreeMap<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type: TM{size: Nat, root: Nat, first: Nat, last: Nat, free: Nat, nodes: NodeStore<K>, payloads: D.DynArray<&2, Maybe<&2, V>>}type Entry<-K: Data, -V: Data> is Data: Entry{key: K, value: V}type Error is Data: CapacityExceeded{} OutOfRange{} NoCurrent{} InvalidBounds{}type Rejected<-K: Data, -V: Data> is Data: Rejected{error: Error, key: K, value: V}type Search is Data: Search{found: Nat, parent: Nat, left: Bool}type Fix is Data: Fix{node: Nat, more: Bool}type Ascend is Data: Ascend{child: Nat, parent: Nat, done: Bool}# A direct branch preserves scalar traversal state in native code. Passing# these records through pick(-T: Type) erases their layout and boxes both arms.type DeleteFix is Data: DF{node: Nat, parent: Nat, more: Bool}type NavEnd is Data: NavBest{id: Nat} NavEqual{id: Nat}type Bound<-K: Data> is Data: Unbounded{} Inclusive{key: K} Exclusive{key: K}type View<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type: View{map: TreeMap<K, V, cmp>, lower: Bound<K>, upper: Bound<K>, descending: Bool}type InvalidView<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type: InvalidView{map: TreeMap<K, V, cmp>, error: Error}type Cursor<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type: Cursor{map: TreeMap<K, V, cmp>, next: Nat, current: Nat, lower: Bound<K>, upper: Bound<K>, forward: Bool}def ntag(~K: Data, n: Node<K>) -> Nat: match n: case Free{x}: 0n case N{c, l, r, p, k}: match c: case True{}: 2n case False{}: 1ndef nleft(~K: Data, n: Node<K>) -> Nat: match n: case Free{x}: x case N{c, l, r, p, k}: ldef nright(~K: Data, n: Node<K>) -> Nat: match n: case Free{x}: 0n case N{c, l, r, p, k}: rdef nparent(~K: Data, n: Node<K>) -> Nat: match n: case Free{x}: 0n case N{c, l, r, p, k}: pdef nkey(~K: Data, n: Node<K>) -> Maybe<&2, K>: match n: case Free{x}: None{} case N{c, l, r, p, k}: Some{k}def mk_node(~K: Data, +t: Nat, +l: Nat, +r: Nat, +p: Nat, k: Maybe<&2, K>) -> Node<K>: match t k: case 0n _: Free{l} case 1n+ +c Some{key}: N{Nat.is_eq(c, 1n), l, r, p, key} case 1n+ +c None{}: Free{l}def ns_nats(+d: Nat) -> Array<Nat>: Array.new(Nat, d, 0n)def ns_nokeys(~K: Data, +d: Nat) -> Array<Maybe<&2, K>>: Array.new(Maybe<&2, K>, d, None{})def ns_length(~K: Data, s: NodeStore<K>) -> NodeStore<K> & Nat: NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, used)# ---- reading a slot ----def ns_tag_fin(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, q: Array<Nat> & Nat) -> NodeStore<K> & Nat: (tags, +x) = q (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)def ns_left_fin(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, q: Array<Nat> & Nat) -> NodeStore<K> & Nat: (lefts, +x) = q (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)def ns_right_fin(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, q: Array<Nat> & Nat) -> NodeStore<K> & Nat: (rights, +x) = q (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)def ns_parent_fin(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, keys: Array<Maybe<&2, K>>, q: Array<Nat> & Nat) -> NodeStore<K> & Nat: (parents, +x) = q (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)def ns_key_fin(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, q: Array<Maybe<&2, K>> & Maybe<&2, K>) -> NodeStore<K> & Maybe<&2, K>: (keys, x) = q (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)def ns_red_tag(red: Bool) -> Nat: match red: case True{}: 2n case False{}: 1ndef ns_set_left_tag(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, q: Array<Nat> & Nat) -> NodeStore<K>: match q: case Tuple{tags, 0n}: NS{limit, depth, cap, used, tags, lefts, rights, parents, keys} case Tuple{tags, 1n+c}: NS{limit, depth, cap, used, tags, Array.set(Nat, lefts, U32.from_nat(i), v), rights, parents, keys}def ns_set_right_tag(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, q: Array<Nat> & Nat) -> NodeStore<K>: match q: case Tuple{tags, 0n}: NS{limit, depth, cap, used, tags, lefts, rights, parents, keys} case Tuple{tags, 1n+c}: NS{limit, depth, cap, used, tags, lefts, Array.set(Nat, rights, U32.from_nat(i), v), parents, keys}def ns_set_parent_tag(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, q: Array<Nat> & Nat) -> NodeStore<K>: match q: case Tuple{tags, 0n}: NS{limit, depth, cap, used, tags, lefts, rights, parents, keys} case Tuple{tags, 1n+c}: NS{limit, depth, cap, used, tags, lefts, rights, Array.set(Nat, parents, U32.from_nat(i), v), keys}def pick(-T: Type, b: Bool, yes: T, no: T) -> T: match b: case True{}: yes case False{}: nodef node_red(~K: Data, n: Node<K>) -> Bool: match n: case Free{x}: False{} case N{c, l, r, p, k}: cdef node_left(~K: Data, n: Node<K>) -> Nat: match n: case Free{x}: 0n case N{c, l, r, p, k}: ldef node_right(~K: Data, n: Node<K>) -> Nat: match n: case Free{x}: 0n case N{c, l, r, p, k}: rdef node_parent(~K: Data, n: Node<K>) -> Nat: match n: case Free{x}: 0n case N{c, l, r, p, k}: pdef node_key(~K: Data, n: Node<K>) -> Maybe<&2, K>: match n: case Free{x}: None{} case N{c, l, r, p, k}: Some{k}def size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat: TM{+n, root, lo, hi, free, nodes, payloads} = m (TM{n, root, lo, hi, free, nodes, payloads}, n)def root_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat: TM{n, +root, lo, hi, free, nodes, payloads} = m (TM{n, root, lo, hi, free, nodes, payloads}, root)def first_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat: TM{n, root, +lo, hi, free, nodes, payloads} = m (TM{n, root, lo, hi, free, nodes, payloads}, lo)def last_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat: TM{n, root, lo, +hi, free, nodes, payloads} = m (TM{n, root, lo, hi, free, nodes, payloads}, hi)def read_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>) -> TreeMap<K, V, cmp> & Node<K>: match r: case Tuple{nodes, Done{x}}: (TM{n, root, lo, hi, free, nodes, payloads}, x) case Tuple{nodes, Fail{e}}: (TM{n, root, lo, hi, free, nodes, payloads}, Free{0n})def write_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: NodeStore<K> & Result<&2, &2, DE.Error, Unit>) -> TreeMap<K, V, cmp>: (nodes, status) = r TM{n, root, lo, hi, free, nodes, payloads}def set_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +root: Nat) -> TreeMap<K, V, cmp>: TM{n, old, lo, hi, free, nodes, payloads} = m TM{n, root, lo, hi, free, nodes, payloads}def probe_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +k: K, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & (Node<K> & Cmp): match r: case Tuple{m, Free{next}}: (m, (Free{next}, EQ{})) case Tuple{m, N{c, l, r, p, +key}}: (m, (N{c, l, r, p, key}, cmp(k, key)))def search_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +k: K, r: NodeStore<K> & Maybe<&2, K>) -> NodeStore<K> & (Nat & Maybe<&2, Cmp>): match r: case Tuple{nodes, None{}}: (nodes, (id, None{})) case Tuple{nodes, Some{key}}: (nodes, (id, Some{cmp(k, key)}))def search_fin(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: NodeStore<K> & Search) -> TreeMap<K, V, cmp> & Search: (nodes, s) = r (TM{n, root, lo, hi, free, nodes, payloads}, s)def exchange_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: NodeStore<K>, r: D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>) -> TreeMap<K, V, cmp> & Maybe<&2, V>: match r: case Tuple{payloads, Done{old}}: (TM{n, root, lo, hi, free, nodes, payloads}, old) case Tuple{payloads, Fail{e}}: (TM{n, root, lo, hi, free, nodes, payloads}, None{})def append_rollback(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +k: K, +v: V, r: NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>: (nodes, dropped) = r (TM{n, root, lo, hi, free, nodes, payloads}, Fail{Rejected{CapacityExceeded{}, k, v}})def free_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +free: Nat) -> TreeMap<K, V, cmp>: TM{n, root, lo, hi, old, nodes, payloads} = m TM{n, root, lo, hi, free, nodes, payloads}def reuse_slot_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>: (m1, old) = pair_result (m1, Done{id})def put_replaced(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>: (m, old) = r (m, Done{old})def get_id_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: NodeStore<K>, r: D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>) -> TreeMap<K, V, cmp> & Maybe<&2, V>: match r: case Tuple{payloads, Done{x}}: (TM{n, root, lo, hi, free, nodes, payloads}, x) case Tuple{payloads, Fail{e}}: (TM{n, root, lo, hi, free, nodes, payloads}, None{})def contains_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Bool: (m, Search{id, p, left}) = r (m, Nat.is_lt(0n, id))def ascend_choice(x: Nat, p: Nat, q: Nat, found: Bool) -> Ascend: match found: case True{}: Ascend{0n, p, True{}} case False{}: Ascend{x, q, False{}}def neighbor_slots_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: NodeStore<K> & Nat) -> TreeMap<K, V, cmp> & Nat: (nodes, id) = r (TM{n, root, lo, hi, free, nodes, payloads}, id)def move_successor_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +source: Nat, pair_result: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Nat: (m3, old) = pair_result (m3, source)def release_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>: TM{n, root, lo, hi, free, nodes, payloads} = m TM{Nat.sub(n, 1n), root, lo, hi, id, nodes, payloads}def set_ends(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +lo: Nat, +hi: Nat) -> TreeMap<K, V, cmp>: TM{n, root, oldlo, oldhi, free, nodes, payloads} = m TM{n, root, lo, hi, free, nodes, payloads}def is_empty_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Bool: (m1, +n) = pair_result (m1, Nat.is_eq(n, 0n))def entry_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, k: Maybe<&2, K>, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: match k r: case Some{key} Tuple{m, Some{v}}: (m, Some{Entry{key, v}}) case _ Tuple{m, value}: (m, None{})def snap_kv(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, nodes: NodeStore<K>, mk: Maybe<&2, K>, mv: Maybe<&2, V>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: match mk mv: case Some{key} Some{v}: (TM{n, root, lo, hi, free, nodes, payloads}, Some{Entry{key, v}}) case _ _: (TM{n, root, lo, hi, free, nodes, payloads}, None{})def default_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fallback: V, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & V: match r: case Tuple{m, None{}}: (m, fallback) case Tuple{m, Some{v}}: (m, v)def ordering_ok(order: Cmp, inclusive: Bool) -> Bool: match order: case LT{}: True{} case EQ{}: inclusive case GT{}: False{}def view_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, lower: Bound<K>, upper: Bound<K>, +descending: Bool, +valid: Bool) -> Result<&1, &1, InvalidView<K, V, cmp>, View<K, V, cmp>>: match valid: case True{}: Done{View{m, lower, upper, descending}} case False{}: Fail{InvalidView{m, InvalidBounds{}}}def head_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, upper: Bound<K>) -> View<K, V, cmp>: View{m, Unbounded{}, upper, False{}}def tail_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, lower: Bound<K>) -> View<K, V, cmp>: View{m, lower, Unbounded{}, False{}}def descending_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> View<K, V, cmp>: View{m, Unbounded{}, Unbounded{}, True{}}def view_reverse(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp>: View{m, lower, upper, descending} = view View{m, lower, upper, Bool.not(descending)}def view_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> TreeMap<K, V, cmp>: View{m, lower, upper, descending} = view mdef view_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: Bound<K>, upper: Bound<K>, +descending: Bool, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> View<K, V, cmp> & Maybe<&2, V>: (m, v) = r (View{m, lower, upper, descending}, v)def view_put_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: Bound<K>, upper: Bound<K>, +descending: Bool, r: TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>) -> View<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>: (m, status) = r (View{m, lower, upper, descending}, status)def cursor_started(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: Bound<K>, upper: Bound<K>, +forward: Bool, r: TreeMap<K, V, cmp> & Nat) -> Cursor<K, V, cmp>: (m, id) = r Cursor{m, id, 0n, lower, upper, forward}def iterator_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> TreeMap<K, V, cmp>: Cursor{m, next, current, lower, upper, forward} = cursor mdef iterator_view(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> View<K, V, cmp>: Cursor{m, next, current, lower, upper, forward} = cursor View{m, lower, upper, Bool.not(forward)}def iterator_yield(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, entry: Entry<K, V>, r: TreeMap<K, V, cmp> & Nat) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>: (m, next) = r (Cursor{m, next, id, lower, upper, forward}, Some{entry})def iterator_set_done(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +next: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> Cursor<K, V, cmp> & Result<&2, &2, Error, V>: match r: case Tuple{m, Some{old}}: (Cursor{m, next, current, lower, upper, forward}, Done{old}) case Tuple{m, None{}}: (Cursor{m, next, current, lower, upper, forward}, Fail{NoCurrent{}})def iterator_relocated(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: Bound<K>, upper: Bound<K>, +forward: Bool, removed: Maybe<&2, V>, r: TreeMap<K, V, cmp> & Search) -> Cursor<K, V, cmp> & Maybe<&2, V>: (m, Search{id, p, on_left}) = r (Cursor{m, id, 0n, lower, upper, forward}, removed)def iterator_key_result(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>) -> Cursor<K, V, cmp> & Maybe<&2, K>: match r: case Tuple{cursor, None{}}: (cursor, None{}) case Tuple{cursor, Some{Entry{k, v}}}: (cursor, Some{k})def iterator_value_result(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>) -> Cursor<K, V, cmp> & Maybe<&2, V>: match r: case Tuple{cursor, None{}}: (cursor, None{}) case Tuple{cursor, Some{Entry{k, v}}}: (cursor, Some{v})def changed_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Bool: match r: case Tuple{m, None{}}: (m, False{}) case Tuple{m, Some{old}}: (m, True{})def view_contains_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: View<K, V, cmp> & Maybe<&2, V>) -> View<K, V, cmp> & Bool: match r: case Tuple{view, None{}}: (view, False{}) case Tuple{view, Some{x}}: (view, True{})def view_entry_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, lower: Bound<K>, upper: Bound<K>, +descending: Bool, entry: Entry<K, V>, +valid: Bool) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>: match valid: case True{}: (View{m, lower, upper, descending}, Some{entry}) case False{}: (View{m, lower, upper, descending}, None{})def ns_empty(~K: Data, +limit: Nat) -> NodeStore<K>: NS{limit, 0n, 1n, 0n, ns_nats(0n), ns_nats(0n), ns_nats(0n), ns_nats(0n), ns_nokeys(~K, 0n)}def ns_rk(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, +t: Nat, +l: Nat, +r: Nat, +p: Nat, q: Array<Maybe<&2, K>> & Maybe<&2, K>) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>: (keys, k) = q (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Done{mk_node(~K, t, l, r, p, k)})def ns_tag_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Nat: match ok: case True{}: ns_tag_fin(~K, limit, depth, cap, used, lefts, rights, parents, keys, Array.get(Nat, tags, U32.from_nat(i))) case False{}: (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)def ns_left_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Nat: match ok: case True{}: ns_left_fin(~K, limit, depth, cap, used, tags, rights, parents, keys, Array.get(Nat, lefts, U32.from_nat(i))) case False{}: (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)def ns_right_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Nat: match ok: case True{}: ns_right_fin(~K, limit, depth, cap, used, tags, lefts, parents, keys, Array.get(Nat, rights, U32.from_nat(i))) case False{}: (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)def ns_parent_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Nat: match ok: case True{}: ns_parent_fin(~K, limit, depth, cap, used, tags, lefts, rights, keys, Array.get(Nat, parents, U32.from_nat(i))) case False{}: (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)def ns_key_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Maybe<&2, K>: match ok: case True{}: ns_key_fin(~K, limit, depth, cap, used, tags, lefts, rights, parents, Array.get(Maybe<&2, K>, keys, U32.from_nat(i))) case False{}: (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, None{})def ns_set_left_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, ok: Bool) -> NodeStore<K>: match ok: case True{}: ns_set_left_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i))) case False{}: NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}def ns_set_right_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, ok: Bool) -> NodeStore<K>: match ok: case True{}: ns_set_right_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i))) case False{}: NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}def ns_set_parent_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, ok: Bool) -> NodeStore<K>: match ok: case True{}: ns_set_parent_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i))) case False{}: NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}def ns_set_red_tag(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Bool, q: Array<Nat> & Nat) -> NodeStore<K>: match q: case Tuple{tags, 0n}: NS{limit, depth, cap, used, tags, lefts, rights, parents, keys} case Tuple{tags, 1n+c}: NS{limit, depth, cap, used, Array.set(Nat, tags, U32.from_nat(i), ns_red_tag(v)), lefts, rights, parents, keys}def ns_put(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: U32, +node: Node<K>) -> NodeStore<K>: NS{limit, depth, cap, used, Array.set(Nat, tags, i, ntag(~K, node)), Array.set(Nat, lefts, i, nleft(~K, node)), Array.set(Nat, rights, i, nright(~K, node)), Array.set(Nat, parents, i, nparent(~K, node)), Array.set(Maybe<&2, K>, keys, i, nkey(~K, node))}def ns_grow_nats(+depth: Nat, a: Array<Nat>) -> Array<Nat>: ANode{a, ns_nats(depth)}def ns_grow_keys(~K: Data, +depth: Nat, a: Array<Maybe<&2, K>>) -> Array<Maybe<&2, K>>: ANode{a, ns_nokeys(~K, depth)}def child(~K: Data, +n: Node<K>, forward: Bool) -> Nat: pick(Nat, forward, node_right(~K, n), node_left(~K, n))# All links reference live slots. Free slots contain no key and no value.def exchange(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, value: Maybe<&2, V>) -> TreeMap<K, V, cmp> & Maybe<&2, V>: match m id: case mm 0n: (mm, None{}) case TM{n, root, lo, hi, free, nodes, payloads} 1n+i: exchange_finish(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, D.swap_at(~Maybe<&2, V>, payloads, i, value))def insert_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +p: Nat, +on_left: Bool) -> TreeMap<K, V, cmp>: TM{+n, root, +lo, +hi, free, nodes, payloads} = m TM{1n+n, root, pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(on_left, Nat.is_eq(p, lo))), id, lo), pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(on_left), Nat.is_eq(p, hi))), id, hi), free, nodes, payloads}def get_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Maybe<&2, V>: match m id: case mm 0n: (mm, None{}) case TM{n, root, lo, hi, free, nodes, payloads} 1n+i: get_id_finish(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, D.get_at(~Maybe<&2, V>, payloads, i))def ascend_step_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +forward: Bool, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Ascend: match r: case Tuple{m, Free{next}}: (m, Ascend{0n, 0n, True{}}) case Tuple{m, N{c, l, r, q, key}}: (m, ascend_choice(p, p, q, Nat.is_eq(x, pick(Nat, forward, l, r))))def ascend_par(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +s: Nat, r: NodeStore<K> & Nat) -> NodeStore<K> & Ascend: (nodes, +q) = r (nodes, ascend_choice(p, p, q, Nat.is_eq(x, s)))def refresh_ends_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo: Nat, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>: (m3, +hi) = pair_result set_ends(~K, ~V, ~cmp, m3, lo, hi)def is_empty(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Bool: is_empty_1(~K, ~V, ~cmp, size(~K, ~V, ~cmp, m))def key_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Maybe<&2, K>: (m, node) = r (m, node_key(~K, node))def snap_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, mv: Maybe<&2, V>, r: NodeStore<K> & Maybe<&2, K>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: (nodes, mk) = r snap_kv(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, nodes, mk, mv)def above_lower(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, bound: Bound<K>) -> Bool: match bound: case Unbounded{}: True{} case Inclusive{lo}: ordering_ok(cmp(lo, k), True{}) case Exclusive{lo}: ordering_ok(cmp(lo, k), False{})def below_upper(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, bound: Bound<K>) -> Bool: match bound: case Unbounded{}: True{} case Inclusive{hi}: ordering_ok(cmp(k, hi), True{}) case Exclusive{hi}: ordering_ok(cmp(k, hi), False{})def bounds_valid(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: Bound<K>, upper: Bound<K>) -> Bool: match lower upper: case Unbounded{} _: True{} case _ Unbounded{}: True{} case Inclusive{lo} Inclusive{hi}: ordering_ok(cmp(lo, hi), True{}) case Inclusive{lo} Exclusive{hi}: ordering_ok(cmp(lo, hi), True{}) case Exclusive{lo} Inclusive{hi}: ordering_ok(cmp(lo, hi), True{}) case Exclusive{lo} Exclusive{hi}: ordering_ok(cmp(lo, hi), True{})def range_unbounded(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +forward: Bool) -> TreeMap<K, V, cmp> & Nat: match forward: case True{}: first_id(~K, ~V, ~cmp, m) case False{}: last_id(~K, ~V, ~cmp, m)def iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>: cursor_started(~K, ~V, ~cmp, Unbounded{}, Unbounded{}, True{}, first_id(~K, ~V, ~cmp, m))def descending_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>: cursor_started(~K, ~V, ~cmp, Unbounded{}, Unbounded{}, False{}, last_id(~K, ~V, ~cmp, m))def ns_new(~K: Data) -> NodeStore<K>: ns_empty(~K, D.max_depth())def ns_with_limit(~K: Data, +k: Nat) -> NodeStore<K>: ns_empty(~K, D.clamp_limit(k, Nat.is_lt(k, D.max_depth())))def ns_rp(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: U32, +t: Nat, +l: Nat, +r: Nat, q: Array<Nat> & Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>: (parents, +p) = q ns_rk(~K, limit, depth, cap, used, tags, lefts, rights, parents, t, l, r, p, Array.get(Maybe<&2, K>, keys, i))def ns_tag_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat: NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s ns_tag_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))def ns_left_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat: NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s ns_left_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))def ns_right_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat: NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s ns_right_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))def ns_parent_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat: NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s ns_parent_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))def ns_key_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Maybe<&2, K>: NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s ns_key_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))# ---- writing one field of a live slot (free slots and ids past the length unchanged) ----def ns_set_left(~K: Data, s: NodeStore<K>, +i: Nat, +v: Nat) -> NodeStore<K>: NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s ns_set_left_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))def ns_set_right(~K: Data, s: NodeStore<K>, +i: Nat, +v: Nat) -> NodeStore<K>: NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s ns_set_right_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))def ns_set_parent(~K: Data, s: NodeStore<K>, +i: Nat, +v: Nat) -> NodeStore<K>: NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s ns_set_parent_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))def ns_set_red_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Bool, ok: Bool) -> NodeStore<K>: match ok: case True{}: ns_set_red_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i))) case False{}: NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}def ns_set_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +node: Node<K>, ok: Bool) -> NodeStore<K> & Result<&2, &2, DE.Error, Unit>: match ok: case True{}: (ns_put(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, U32.from_nat(i), node), Done{Unit{}}) case False{}: (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Fail{DE.IndexOutOfRange{}})def ns_push_room(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +node: Node<K>, room: Bool, grow: Bool) -> NodeStore<K> & Result<&2, &2, DE.Error, Unit>: match room grow: case True{} _: (ns_put(~K, limit, depth, cap, 1n+used, tags, lefts, rights, parents, keys, U32.from_nat(used), node), Done{Unit{}}) case False{} True{}: (ns_put(~K, limit, 1n+depth, Nat.double(cap), 1n+used, ns_grow_nats(depth, tags), ns_grow_nats(depth, lefts), ns_grow_nats(depth, rights), ns_grow_nats(depth, parents), ns_grow_keys(~K, depth, keys), U32.from_nat(used), node), Done{Unit{}}) case False{} False{}: (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Fail{DE.CapacityExceeded{}})def ns_drop(~K: Data, s: NodeStore<K>, +m: Nat) -> NodeStore<K>: NS{limit, depth, cap, used, tags, lefts, rights, parents, keys} = s ns_put(~K, limit, depth, cap, m, tags, lefts, rights, parents, keys, U32.from_nat(m), Free{0n})def get_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Maybe<&2, V>: (m, Search{id, p, on_left}) = r get_id(~K, ~V, ~cmp, m, id)def replace_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +v: V, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Maybe<&2, V>: match r: case Tuple{m, Search{0n, p, on_left}}: (m, None{}) case Tuple{m, Search{1n+i, p, on_left}}: exchange(~K, ~V, ~cmp, m, 1n+i, Some{v})def in_range(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, lower: Bound<K>, upper: Bound<K>) -> Bool: Bool.and(above_lower(~K, ~V, ~cmp, k, lower), below_upper(~K, ~V, ~cmp, k, upper))def sub_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +lower: Bound<K>, +upper: Bound<K>) -> Result<&1, &1, InvalidView<K, V, cmp>, View<K, V, cmp>>: view_checked(~K, ~V, ~cmp, m, lower, upper, False{}, bounds_valid(~K, ~V, ~cmp, lower, upper))def iterator_set_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>, +v: V) -> Cursor<K, V, cmp> & Result<&2, &2, Error, V>: match cursor: case Cursor{m, next, 0n, lower, upper, forward}: (Cursor{m, next, 0n, lower, upper, forward}, Fail{NoCurrent{}}) case Cursor{m, next, 1n+ +id, lower, upper, forward}: iterator_set_done(~K, ~V, ~cmp, next, 1n+id, lower, upper, forward, exchange(~K, ~V, ~cmp, m, 1n+id, Some{v}))def entry_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>: iterator(~K, ~V, ~cmp, m)def key_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>: iterator(~K, ~V, ~cmp, m)def values(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>: iterator(~K, ~V, ~cmp, m)def replace_if_apply(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +replacement: V, +equal: Bool) -> TreeMap<K, V, cmp> & Bool: match equal: case False{}: (m, False{}) case True{}: changed_value(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, m, id, Some{replacement}))def ns_rr(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: U32, +t: Nat, +l: Nat, q: Array<Nat> & Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>: (rights, +r) = q ns_rp(~K, limit, depth, cap, used, tags, lefts, rights, keys, i, t, l, r, Array.get(Nat, parents, i))def ns_set_red(~K: Data, s: NodeStore<K>, +i: Nat, +v: Bool) -> NodeStore<K>: NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s ns_set_red_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))# ---- writing a slot: the encoding of the node in all five arrays ----def ns_set(~K: Data, s: NodeStore<K>, +i: Nat, +node: Node<K>) -> NodeStore<K> & Result<&2, &2, DE.Error, Unit>: NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s ns_set_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, node, Nat.is_lt(i, used))# ---- appending a slot ----def ns_push(~K: Data, s: NodeStore<K>, +node: Node<K>) -> NodeStore<K> & Result<&2, &2, DE.Error, Unit>: NS{+limit, +depth, +cap, +used, tags, lefts, rights, parents, keys} = s ns_push_room(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, node, Nat.is_lt(used, cap), Nat.is_lt(depth, limit))# ---- dropping slots: the dropped slots get the encoding of Free{0} back ----def ns_pop_fin(~K: Data, +m: Nat, r: NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>: (s, x) = r (ns_drop(~K, s, m), x)def ns_clear_go(~K: Data, k: Nat, s: NodeStore<K>) -> NodeStore<K>: match k: case 0n: s case 1n+ +m: ns_clear_go(~K, m, ns_drop(~K, s, m))# O(used): resets the live slots top down and keeps the capacity.def new(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp) -> TreeMap<K, V, cmp>: TM{0n, 0n, 0n, 0n, 0n, ns_new(~K), D.new_at(~Maybe<&2, V>)}def set_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>: match m id: case mm 0n: mm case TM{n, root, lo, hi, free, nodes, payloads} 1n+i: TM{n, root, lo, hi, free, ns_set_left(~K, nodes, i, v), payloads}def set_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>: match m id: case mm 0n: mm case TM{n, root, lo, hi, free, nodes, payloads} 1n+i: TM{n, root, lo, hi, free, ns_set_right(~K, nodes, i, v), payloads}def set_parent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>: match m id: case mm 0n: mm case TM{n, root, lo, hi, free, nodes, payloads} 1n+i: TM{n, root, lo, hi, free, ns_set_parent(~K, nodes, i, v), payloads}def search_probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +id: Nat, +k: K) -> NodeStore<K> & (Nat & Maybe<&2, Cmp>): match id: case 0n: (nodes, (0n, None{})) case 1n+ +i: search_key(~K, ~V, ~cmp, 1n+i, k, ns_key_at(~K, nodes, i))def side_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +left: Bool, +i: Nat) -> NodeStore<K> & Nat: match left: case True{}: ns_left_at(~K, nodes, i) case False{}: ns_right_at(~K, nodes, i)def ascend_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +i: Nat, r: NodeStore<K> & Nat) -> NodeStore<K> & Ascend: (nodes, +s) = r ascend_par(~K, ~V, ~cmp, x, p, s, ns_parent_at(~K, nodes, i))def snap_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +i: Nat, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: (TM{+n, +root, +lo, +hi, +free, nodes, payloads}, mv) = r snap_key(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, mv, ns_key_at(~K, nodes, i))def with_limit(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +limit: Nat) -> TreeMap<K, V, cmp>: TM{0n, 0n, 0n, 0n, 0n, ns_with_limit(~K, limit), D.with_limit_at(~Maybe<&2, V>, limit)}def replace_if_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +id: Nat, +expected: V, +replacement: V, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Bool: match r: case Tuple{m, None{}}: (m, False{}) case Tuple{m, Some{old}}: replace_if_apply(~K, ~V, ~cmp, m, id, replacement, eq(old, expected))def iterator_has_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +next: Nat, +current: Nat, +lower: Bound<K>, +upper: Bound<K>, +forward: Bool, r: TreeMap<K, V, cmp> & Node<K>) -> Cursor<K, V, cmp> & Bool: match r: case Tuple{m, Free{free}}: (Cursor{m, next, current, lower, upper, forward}, False{}) case Tuple{m, N{c, l, rr, p, key}}: (Cursor{m, next, current, lower, upper, forward}, in_range(~K, ~V, ~cmp, key, lower, upper))def view_entry_result(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lower: Bound<K>, +upper: Bound<K>, +descending: Bool, r: TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>: match r: case Tuple{m, None{}}: (View{m, lower, upper, descending}, None{}) case Tuple{m, Some{Entry{+k, v}}}: view_entry_checked(~K, ~V, ~cmp, m, lower, upper, descending, Entry{k, v}, in_range(~K, ~V, ~cmp, k, lower, upper))def ns_rl(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: U32, +t: Nat, q: Array<Nat> & Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>: (lefts, +l) = q ns_rr(~K, limit, depth, cap, used, tags, lefts, parents, keys, i, t, l, Array.get(Nat, rights, i))def ns_clear(~K: Data, s: NodeStore<K>) -> NodeStore<K>: NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s ns_clear_go(~K, used, NS{limit, depth, cap, used, tags, lefts, rights, parents, keys})def write(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>: match m id: case mm 0n: mm case TM{n, root, lo, hi, free, nodes, payloads} 1n+i: write_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, ns_set(~K, nodes, i, node))def set_red(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Bool) -> TreeMap<K, V, cmp>: match m id: case mm 0n: mm case TM{n, root, lo, hi, free, nodes, payloads} 1n+i: TM{n, root, lo, hi, free, ns_set_red(~K, nodes, i, v), payloads}def attach_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +x: Nat, +on_left: Bool) -> TreeMap<K, V, cmp>: match p on_left: case 0n _: set_root(~K, ~V, ~cmp, m, x) case 1n+q True{}: set_left(~K, ~V, ~cmp, m, 1n+q, x) case 1n+q False{}: set_right(~K, ~V, ~cmp, m, 1n+q, x)def search_down2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, r: NodeStore<K> & Nat) -> NodeStore<K> & (Nat & Maybe<&2, Cmp>): (nodes, +c) = r search_probe(~K, ~V, ~cmp, nodes, c, k)def ascend_tag(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +i: Nat, +forward: Bool, r: NodeStore<K> & Nat) -> NodeStore<K> & Ascend: match r: case Tuple{nodes, 0n}: (nodes, Ascend{0n, 0n, True{}}) case Tuple{nodes, 1n+c}: ascend_side(~K, ~V, ~cmp, x, p, i, side_at(~K, ~V, ~cmp, nodes, forward, i))def extreme_tag(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, +i: Nat, r: NodeStore<K> & Nat) -> NodeStore<K> & Nat: match r: case Tuple{nodes, 0n}: (nodes, 0n) case Tuple{nodes, 1n+c}: side_at(~K, ~V, ~cmp, nodes, Bool.not(forward), i)def snap_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: match id: case 0n: (m, None{}) case 1n+ +i: snap_value(~K, ~V, ~cmp, i, get_id(~K, ~V, ~cmp, m, 1n+i))def replace_if_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +expected: V, +replacement: V, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Bool: (m, Search{+id, p, on_left}) = r replace_if_value(~K, ~V, ~cmp, ~eq, id, expected, replacement, get_id(~K, ~V, ~cmp, m, id))def ns_rt(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: U32, q: Array<Nat> & Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>: (tags, +t) = q ns_rl(~K, limit, depth, cap, used, tags, rights, parents, keys, i, t, Array.get(Nat, lefts, i))def attach(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +x: Nat, +on_left: Bool) -> TreeMap<K, V, cmp>: set_parent(~K, ~V, ~cmp, attach_side(~K, ~V, ~cmp, m, p, x, on_left), x, p)def search_down(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +id: Nat, +left: Bool, +k: K) -> NodeStore<K> & (Nat & Maybe<&2, Cmp>): match id: case 0n: (nodes, (0n, None{})) case 1n+ +i: search_down2(~K, ~V, ~cmp, k, side_at(~K, ~V, ~cmp, nodes, left, i))def black_root_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>: (m1, +r) = pair_result set_red(~K, ~V, ~cmp, m1, r, False{})def reuse_slot(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +next: Nat, +p: Nat, +k: K, +v: V) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>: reuse_slot_1(~K, ~V, ~cmp, id, exchange(~K, ~V, ~cmp, write(~K, ~V, ~cmp, free_header(~K, ~V, ~cmp, m, next), id, N{True{}, 0n, 0n, p, k}), id, Some{v}))def ascend_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +forward: Bool, nodes: NodeStore<K>) -> NodeStore<K> & Ascend: match p: case 0n: (nodes, Ascend{0n, 0n, True{}}) case 1n+ +i: ascend_tag(~K, ~V, ~cmp, x, 1n+i, i, forward, ns_tag_at(~K, nodes, i))def extreme_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, nodes: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat: extreme_tag(~K, ~V, ~cmp, forward, i, ns_tag_at(~K, nodes, i))def set_key_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +k: K, +node: Node<K>) -> TreeMap<K, V, cmp>: match node: case Free{next}: m case N{c, l, r, p, old}: write(~K, ~V, ~cmp, m, id, N{c, l, r, p, k})def recycle(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>: TM{n, root, lo, hi, +free, nodes, payloads} = m release_header(~K, ~V, ~cmp, write(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, id, Free{free}), id)def clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>: TM{n, root, lo, hi, free, nodes, payloads} = m TM{0n, 0n, 0n, 0n, 0n, ns_clear(~K, nodes), D.clear_at(~Maybe<&2, V>, payloads)}def entry_snapshot(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: (m, +id) = r snap_at(~K, ~V, ~cmp, id, m)def ns_get_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>: match ok: case True{}: ns_rt(~K, limit, depth, cap, used, lefts, rights, parents, keys, U32.from_nat(i), Array.get(Nat, tags, U32.from_nat(i))) case False{}: (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Fail{DE.IndexOutOfRange{}})def rotate_left_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: Node<K>, +yn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>: (m3, +pn) = pair_result set_parent(~K, ~V, ~cmp, set_left(~K, ~V, ~cmp, attach(~K, ~V, ~cmp, set_parent(~K, ~V, ~cmp, set_right(~K, ~V, ~cmp, m3, x, node_left(~K, yn)), node_left(~K, yn), x), node_parent(~K, xn), node_right(~K, xn), Nat.is_eq(node_left(~K, pn), x)), node_right(~K, xn), x), x, node_right(~K, xn))def rotate_right_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: Node<K>, +yn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>: (m3, +pn) = pair_result set_parent(~K, ~V, ~cmp, set_right(~K, ~V, ~cmp, attach(~K, ~V, ~cmp, set_parent(~K, ~V, ~cmp, set_left(~K, ~V, ~cmp, m3, x, node_right(~K, yn)), node_right(~K, yn), x), node_parent(~K, xn), node_left(~K, xn), Nat.is_eq(node_left(~K, pn), x)), node_left(~K, xn), x), x, node_left(~K, xn))def search_fast(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +k: K, +p: Nat, +on_left: Bool, st: NodeStore<K> & (Nat & Maybe<&2, Cmp>)) -> NodeStore<K> & Search: match fuel st: case 0n Tuple{nodes, x}: (nodes, Search{0n, p, on_left}) case 1n+f Tuple{nodes, Tuple{id, None{}}}: (nodes, Search{0n, p, on_left}) case 1n+f Tuple{nodes, Tuple{+id, Some{LT{}}}}: search_fast(~K, ~V, ~cmp, f, k, id, True{}, search_down(~K, ~V, ~cmp, nodes, id, True{}, k)) case 1n+f Tuple{nodes, Tuple{+id, Some{GT{}}}}: search_fast(~K, ~V, ~cmp, f, k, id, False{}, search_down(~K, ~V, ~cmp, nodes, id, False{}, k)) case 1n+f Tuple{nodes, Tuple{+id, Some{EQ{}}}}: (nodes, Search{id, p, on_left})def black_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>: black_root_1(~K, ~V, ~cmp, root_id(~K, ~V, ~cmp, m))def alloc_read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +p: Nat, +k: K, +v: V, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>: match r: case Tuple{m, Free{next}}: reuse_slot(~K, ~V, ~cmp, m, id, next, p, k, v) case Tuple{m, N{c, l, r, q, oldk}}: (m, Fail{Rejected{CapacityExceeded{}, k, v}})def ascend_slots_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, st: NodeStore<K> & Ascend) -> NodeStore<K> & Nat: match fuel st: case 0n Tuple{nodes, state}: (nodes, 0n) case 1n+f Tuple{nodes, Ascend{x, p, True{}}}: (nodes, p) case 1n+f Tuple{nodes, Ascend{+x, +p, False{}}}: ascend_slots_loop(~K, ~V, ~cmp, f, forward, ascend_at(~K, ~V, ~cmp, x, p, forward, nodes))def extreme_slots_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, +id: Nat, st: NodeStore<K> & Nat) -> NodeStore<K> & Nat: match fuel st: case 0n Tuple{nodes, next}: (nodes, id) case 1n+f Tuple{nodes, 0n}: (nodes, id) case 1n+f Tuple{nodes, 1n+ +j}: extreme_slots_loop(~K, ~V, ~cmp, f, forward, 1n+j, extreme_at(~K, ~V, ~cmp, forward, nodes, j))def set_key_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +k: K, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>: (m1, +node) = pair_result set_key_node(~K, ~V, ~cmp, m1, id, k, node)def nav_fast(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +k: K, +higher: Bool, +best: Nat, st: NodeStore<K> & (Nat & Maybe<&2, Cmp>)) -> NodeStore<K> & NavEnd: match fuel st: case 0n Tuple{nodes, x}: (nodes, NavBest{best}) case 1n+f Tuple{nodes, Tuple{id, None{}}}: (nodes, NavBest{best}) case 1n+f Tuple{nodes, Tuple{+id, Some{LT{}}}}: nav_fast(~K, ~V, ~cmp, f, k, higher, pick(Nat, higher, id, best), search_down(~K, ~V, ~cmp, nodes, id, True{}, k)) case 1n+f Tuple{nodes, Tuple{+id, Some{GT{}}}}: nav_fast(~K, ~V, ~cmp, f, k, higher, pick(Nat, higher, best, id), search_down(~K, ~V, ~cmp, nodes, id, False{}, k)) case 1n+f Tuple{nodes, Tuple{+id, Some{EQ{}}}}: (nodes, NavEqual{id})def first_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: entry_snapshot(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))def last_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: entry_snapshot(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))def ns_get(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>: NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s ns_get_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))# ---- reading one field of a slot (0, the encoding of Free{0}, past the length) ----def search(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Search: TM{+n, +root, lo, hi, free, nodes, payloads} = m search_fin(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, search_fast(~K, ~V, ~cmp, 1n+n, k, 0n, False{}, search_probe(~K, ~V, ~cmp, nodes, root, k)))def neighbor_slots(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +n: Nat, +id: Nat, +p: Nat, +forward: Bool, +c: Nat) -> NodeStore<K> & Nat: match c: case 0n: ascend_slots_loop(~K, ~V, ~cmp, 1n+n, forward, (nodes, Ascend{id, p, False{}})) case 1n+ +j: extreme_slots_loop(~K, ~V, ~cmp, 1n+n, Bool.not(forward), 1n+j, extreme_at(~K, ~V, ~cmp, Bool.not(forward), nodes, j))def extreme_start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +n: Nat, +id: Nat, +forward: Bool) -> NodeStore<K> & Nat: match id: case 0n: (nodes, 0n) case 1n+ +j: extreme_slots_loop(~K, ~V, ~cmp, 1n+n, forward, 1n+j, extreme_at(~K, ~V, ~cmp, forward, nodes, j))def ns_pop_n(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>: match used: case 0n: (NS{limit, depth, cap, 0n, tags, lefts, rights, parents, keys}, Fail{DE.EmptyArray{}}) case 1n+ +m: ns_pop_fin(~K, m, ns_get(~K, NS{limit, depth, cap, 1n+m, tags, lefts, rights, parents, keys}, m))def read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Node<K>: match m id: case mm 0n: (mm, Free{0n}) case TM{n, root, lo, hi, free, nodes, payloads} 1n+i: read_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, ns_get(~K, nodes, i))def get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, V>: get_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))def contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Bool: contains_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))def extreme(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +forward: Bool) -> TreeMap<K, V, cmp> & Nat: TM{+n, root, lo, hi, free, nodes, payloads} = m neighbor_slots_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, extreme_start(~K, ~V, ~cmp, nodes, n, id, forward))def neighbor_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +forward: Bool, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Nat: (TM{+n, root, lo, hi, free, nodes, payloads}, +node) = r neighbor_slots_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, neighbor_slots(~K, ~V, ~cmp, nodes, n, id, node_parent(~K, node), forward, child(~K, node, forward)))def replace(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, +v: V) -> TreeMap<K, V, cmp> & Maybe<&2, V>: replace_found(~K, ~V, ~cmp, v, search(~K, ~V, ~cmp, m, k))def iter_child(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +id: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, entry: Entry<K, V>, +p: Nat, r: NodeStore<K> & Nat) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>: (nodes, +c) = r iterator_yield(~K, ~V, ~cmp, id, lower, upper, forward, entry, neighbor_slots_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, neighbor_slots(~K, ~V, ~cmp, nodes, n, id, p, forward, c)))def iterator_reseek(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, k: Maybe<&2, K>, lower: Bound<K>, upper: Bound<K>, +forward: Bool, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> Cursor<K, V, cmp> & Maybe<&2, V>: match k r: case None{} Tuple{m, removed}: (Cursor{m, 0n, 0n, lower, upper, forward}, removed) case Some{key} Tuple{m, removed}: iterator_relocated(~K, ~V, ~cmp, lower, upper, forward, removed, search(~K, ~V, ~cmp, m, key))def replace_if_equal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, m: TreeMap<K, V, cmp>, +k: K, +expected: V, +replacement: V) -> TreeMap<K, V, cmp> & Bool: replace_if_found(~K, ~V, ~cmp, ~eq, expected, replacement, search(~K, ~V, ~cmp, m, k))def ns_pop(~K: Data, s: NodeStore<K>) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>: NS{+limit, +depth, +cap, used, tags, lefts, rights, parents, keys} = s ns_pop_n(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys)def rotate_left_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>: (m2, +yn) = pair_result rotate_left_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, node_parent(~K, xn)))def rotate_right_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>: (m2, +yn) = pair_result rotate_right_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, node_parent(~K, xn)))def probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +k: K) -> TreeMap<K, V, cmp> & (Node<K> & Cmp): probe_node(~K, ~V, ~cmp, id, k, read(~K, ~V, ~cmp, m, id))def ascend_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, st: TreeMap<K, V, cmp> & Ascend) -> TreeMap<K, V, cmp> & Nat: match fuel st: case 0n Tuple{m, state}: (m, 0n) case 1n+f Tuple{m, Ascend{x, p, True{}}}: (m, p) case 1n+f Tuple{m, Ascend{+x, +p, False{}}}: ascend_loop(~K, ~V, ~cmp, f, forward, ascend_step_node(~K, ~V, ~cmp, x, p, forward, read(~K, ~V, ~cmp, m, p)))def neighbor(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +forward: Bool) -> TreeMap<K, V, cmp> & Nat: neighbor_node(~K, ~V, ~cmp, id, forward, read(~K, ~V, ~cmp, m, id))def set_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +k: K) -> TreeMap<K, V, cmp>: set_key_1(~K, ~V, ~cmp, id, k, read(~K, ~V, ~cmp, m, id))def refresh_ends_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +r: Nat, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>: (m2, +lo) = pair_result refresh_ends_3(~K, ~V, ~cmp, lo, extreme(~K, ~V, ~cmp, m2, r, True{}))def key_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Maybe<&2, K>: (m, id) = r key_finish(~K, ~V, ~cmp, read(~K, ~V, ~cmp, m, id))def get_or_default(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, +fallback: V) -> TreeMap<K, V, cmp> & V: default_value(~K, ~V, ~cmp, fallback, get(~K, ~V, ~cmp, m, k))def view_get_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, lower: Bound<K>, upper: Bound<K>, +descending: Bool, +valid: Bool) -> View<K, V, cmp> & Maybe<&2, V>: match valid: case True{}: view_value(~K, ~V, ~cmp, lower, upper, descending, get(~K, ~V, ~cmp, m, k)) case False{}: (View{m, lower, upper, descending}, None{})def iter_link(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +i: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, entry: Entry<K, V>, r: NodeStore<K> & Nat) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>: (nodes, +p) = r iter_child(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, 1n+i, lower, upper, forward, entry, p, side_at(~K, ~V, ~cmp, nodes, Bool.not(forward), i))def iterator_has_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Bool: Cursor{m, +next, current, lower, upper, forward} = cursor iterator_has_checked(~K, ~V, ~cmp, next, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))def rotate_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>: (m1, +xn) = pair_result rotate_left_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, node_right(~K, xn)))def rotate_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>: (m1, +xn) = pair_result rotate_right_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, node_left(~K, xn)))def search_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +k: K, +id: Nat, +p: Nat, +on_left: Bool, st: TreeMap<K, V, cmp> & (Node<K> & Cmp)) -> TreeMap<K, V, cmp> & Search: match fuel st: case 0n Tuple{m, node}: (m, Search{0n, p, on_left}) case 1n+f Tuple{m, Tuple{Free{next}, order}}: (m, Search{0n, p, on_left}) case 1n+f Tuple{m, Tuple{N{c, +l, r, p0, key}, LT{}}}: search_loop(~K, ~V, ~cmp, f, k, l, id, True{}, probe(~K, ~V, ~cmp, m, l, k)) case 1n+f Tuple{m, Tuple{N{c, l, +r, p0, key}, GT{}}}: search_loop(~K, ~V, ~cmp, f, k, r, id, False{}, probe(~K, ~V, ~cmp, m, r, k)) case 1n+f Tuple{m, Tuple{N{c, l, r, p0, key}, EQ{}}}: (m, Search{id, p, on_left})def append_values(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: NodeStore<K>, +k: K, +v: V, +id: Nat, r: D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Unit>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>: match r: case Tuple{payloads, Done{u}}: (TM{n, root, lo, hi, free, nodes, payloads}, Done{id}) case Tuple{payloads, Fail{e}}: append_rollback(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, ns_pop(~K, nodes))def copy_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +target: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>: match node: case Free{next}: m case N{c, l, r, p, k}: set_key(~K, ~V, ~cmp, m, target, k)def refresh_ends_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>: (m1, +r) = pair_result refresh_ends_2(~K, ~V, ~cmp, r, extreme(~K, ~V, ~cmp, m1, r, False{}))def nav_equal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +higher: Bool, +inclusive: Bool) -> TreeMap<K, V, cmp> & Nat: match inclusive: case True{}: (m, id) case False{}: neighbor(~K, ~V, ~cmp, m, id, higher)def first_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, K>: key_id(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))def last_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, K>: key_id(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))def view_get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, V>: View{m, +lower, +upper, descending} = view view_get_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))def iter_valid(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, nodes: NodeStore<K>, +i: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, entry: Entry<K, V>, +valid: Bool) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>: match valid: case True{}: iter_link(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, i, lower, upper, forward, entry, ns_parent_at(~K, nodes, i)) case False{}: (Cursor{TM{n, root, lo, hi, free, nodes, payloads}, 0n, current, lower, upper, forward}, None{})def rotate_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat) -> TreeMap<K, V, cmp>: rotate_left_1(~K, ~V, ~cmp, x, read(~K, ~V, ~cmp, m, x))def rotate_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat) -> TreeMap<K, V, cmp>: rotate_right_1(~K, ~V, ~cmp, x, read(~K, ~V, ~cmp, m, x))def append_nodes(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +k: K, +v: V, +id: Nat, r: NodeStore<K> & Result<&2, &2, DE.Error, Unit>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>: match r: case Tuple{nodes, Done{u}}: append_values(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, k, v, id, D.push_at(~Maybe<&2, V>, payloads, Some{v})) case Tuple{nodes, Fail{e}}: (TM{n, root, lo, hi, free, nodes, payloads}, Fail{Rejected{CapacityExceeded{}, k, v}})def move_successor_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, +source: Nat, +source_node: Node<K>, pair_result: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Nat: (m2, value) = pair_result move_successor_3(~K, ~V, ~cmp, source, exchange(~K, ~V, ~cmp, copy_key(~K, ~V, ~cmp, m2, target, source_node), target, value))def refresh_ends(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>: refresh_ends_1(~K, ~V, ~cmp, root_id(~K, ~V, ~cmp, m))def nav_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +k: K, +higher: Bool, +inclusive: Bool, +id: Nat, +best: Nat, st: TreeMap<K, V, cmp> & (Node<K> & Cmp)) -> TreeMap<K, V, cmp> & Nat: match fuel st: case 0n Tuple{m, node}: (m, best) case 1n+f Tuple{m, Tuple{Free{next}, order}}: (m, best) case 1n+f Tuple{m, Tuple{N{c, +l, r, p, key}, LT{}}}: nav_loop(~K, ~V, ~cmp, f, k, higher, inclusive, l, pick(Nat, higher, id, best), probe(~K, ~V, ~cmp, m, l, k)) case 1n+f Tuple{m, Tuple{N{c, l, +r, p, key}, GT{}}}: nav_loop(~K, ~V, ~cmp, f, k, higher, inclusive, r, pick(Nat, higher, best, id), probe(~K, ~V, ~cmp, m, r, k)) case 1n+f Tuple{m, Tuple{node, EQ{}}}: nav_equal(~K, ~V, ~cmp, m, id, higher, inclusive)def nav_end(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +higher: Bool, +inclusive: Bool, r: NodeStore<K> & NavEnd) -> TreeMap<K, V, cmp> & Nat: match r: case Tuple{nodes, NavBest{b}}: (TM{n, root, lo, hi, free, nodes, payloads}, b) case Tuple{nodes, NavEqual{+id}}: nav_equal(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, id, higher, inclusive)def iter_kv(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, nodes: NodeStore<K>, +i: Nat, +current: Nat, +lower: Bound<K>, +upper: Bound<K>, +forward: Bool, mk: Maybe<&2, K>, mv: Maybe<&2, V>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>: match mk mv: case Some{+key} Some{v}: iter_valid(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, nodes, i, current, lower, upper, forward, Entry{key, v}, in_range(~K, ~V, ~cmp, key, lower, upper)) case _ _: (Cursor{TM{n, root, lo, hi, free, nodes, payloads}, 0n, current, lower, upper, forward}, None{})def view_contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Bool: view_contains_value(~K, ~V, ~cmp, view_get(~K, ~V, ~cmp, view, k))def insert_black_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +g: Nat, +triangle: Bool) -> TreeMap<K, V, cmp> & Fix: match triangle: case True{}: (rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, rotate_left(~K, ~V, ~cmp, m, p), z, False{}), g, True{}), g), Fix{0n, False{}}) case False{}: (rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), g, True{}), g), Fix{0n, False{}})def insert_black_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +g: Nat, +triangle: Bool) -> TreeMap<K, V, cmp> & Fix: match triangle: case True{}: (rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, rotate_right(~K, ~V, ~cmp, m, p), z, False{}), g, True{}), g), Fix{0n, False{}}) case False{}: (rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), g, True{}), g), Fix{0n, False{}})def append_count(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +k: K, +v: V, +p: Nat, r: NodeStore<K> & Nat) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>: (nodes, +used) = r append_nodes(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, 1n+used, ns_push(~K, nodes, N{True{}, 0n, 0n, p, k}))def move_successor_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, +source: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Nat: (m1, +source_node) = pair_result move_successor_2(~K, ~V, ~cmp, target, source, source_node, exchange(~K, ~V, ~cmp, m1, source, None{}))def delete_borrow_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +pn: Node<K>, +wn: Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, w, node_red(~K, pn)), p, False{}), node_right(~K, wn), False{}), p), DF{0n, 0n, False{}})def delete_borrow_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +pn: Node<K>, +wn: Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, w, node_red(~K, pn)), p, False{}), node_left(~K, wn), False{}), p), DF{0n, 0n, False{}})def navigate(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, +higher: Bool, +inclusive: Bool) -> TreeMap<K, V, cmp> & Nat: TM{+n, +root, lo, hi, free, nodes, payloads} = m nav_end(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, higher, inclusive, nav_fast(~K, ~V, ~cmp, 1n+n, k, higher, 0n, search_probe(~K, ~V, ~cmp, nodes, root, k)))def iter_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +i: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, mv: Maybe<&2, V>, r: NodeStore<K> & Maybe<&2, K>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>: (nodes, mk) = r iter_kv(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, nodes, i, current, lower, upper, forward, mk, mv)def insert_uncle_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +g: Nat, +u: Nat, +triangle: Bool, +uncle: Node<K>) -> TreeMap<K, V, cmp> & Fix: match uncle: case N{True{}, l, r, gp, k}: (set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), u, False{}), g, True{}), Fix{g, True{}}) case _: insert_black_left(~K, ~V, ~cmp, m, z, p, g, triangle)def insert_uncle_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +g: Nat, +u: Nat, +triangle: Bool, +uncle: Node<K>) -> TreeMap<K, V, cmp> & Fix: match uncle: case N{True{}, l, r, gp, k}: (set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), u, False{}), g, True{}), Fix{g, True{}}) case _: insert_black_right(~K, ~V, ~cmp, m, z, p, g, triangle)def append(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, +v: V, +p: Nat) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>: TM{n, root, lo, hi, free, nodes, payloads} = m append_count(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, p, ns_length(~K, nodes))def move_successor(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +target: Nat, +source: Nat) -> TreeMap<K, V, cmp> & Nat: move_successor_1(~K, ~V, ~cmp, target, source, read(~K, ~V, ~cmp, m, source))def delete_borrow_read_left_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m2, +wn) = pair_result delete_borrow_left(~K, ~V, ~cmp, m2, p, node_right(~K, pn), pn, wn)def delete_borrow_read_right_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m2, +wn) = pair_result delete_borrow_right(~K, ~V, ~cmp, m2, p, node_left(~K, pn), pn, wn)def lower_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>: key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, False{}))def floor_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>: key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, True{}))def ceiling_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>: key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, True{}))def higher_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>: key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, False{}))def lower_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, k: K) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, False{}))def floor_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, k: K) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, True{}))def ceiling_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, k: K) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, True{}))def higher_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, k: K) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, False{}))def range_start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, bound: Bound<K>, +forward: Bool) -> TreeMap<K, V, cmp> & Nat: match bound: case Unbounded{}: range_unbounded(~K, ~V, ~cmp, m, forward) case Inclusive{k}: navigate(~K, ~V, ~cmp, m, k, forward, True{}) case Exclusive{k}: navigate(~K, ~V, ~cmp, m, k, forward, False{})def iter_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +i: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>: (TM{+n, +root, +lo, +hi, +free, nodes, payloads}, mv) = r iter_key(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, i, current, lower, upper, forward, mv, ns_key_at(~K, nodes, i))def insert_side_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, +p: Nat, +g: Nat, +pn: Node<K>, +gn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Fix: (m1, +un) = pair_result insert_uncle_left(~K, ~V, ~cmp, m1, z, p, g, node_right(~K, gn), Nat.is_eq(z, node_right(~K, pn)), un)def insert_side_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, +p: Nat, +g: Nat, +pn: Node<K>, +gn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Fix: (m1, +un) = pair_result insert_uncle_right(~K, ~V, ~cmp, m1, z, p, g, node_left(~K, gn), Nat.is_eq(z, node_left(~K, pn)), un)def allocate(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +k: K, +v: V) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>: TM{n, root, lo, hi, free, nodes, payloads} = m match free: case 0n: append(~K, ~V, ~cmp, TM{n, root, lo, hi, 0n, nodes, payloads}, k, v, p) case 1n+ +f: alloc_read(~K, ~V, ~cmp, 1n+f, p, k, v, read(~K, ~V, ~cmp, TM{n, root, lo, hi, 1n+f, nodes, payloads}, 1n+f))def successor_ready(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Nat: (m, source) = r move_successor(~K, ~V, ~cmp, m, target, source)def delete_borrow_read_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m1, +pn) = pair_result delete_borrow_read_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_right(~K, pn)))def delete_borrow_read_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m1, +pn) = pair_result delete_borrow_read_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_left(~K, pn)))def view_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> Cursor<K, V, cmp>: View{m, +lower, +upper, +descending} = view cursor_started(~K, ~V, ~cmp, lower, upper, Bool.not(descending), range_start(~K, ~V, ~cmp, m, pick(Bound<K>, descending, upper, lower), Bool.not(descending)))def iter_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +next: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>: match next: case 0n: (Cursor{m, 0n, current, lower, upper, forward}, None{}) case 1n+ +i: iter_value(~K, ~V, ~cmp, i, current, lower, upper, forward, get_id(~K, ~V, ~cmp, m, 1n+i))def view_nav_start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, lower: Bound<K>, upper: Bound<K>, +higher: Bool, +inclusive: Bool, +within: Bool) -> TreeMap<K, V, cmp> & Nat: match within: case True{}: navigate(~K, ~V, ~cmp, m, k, higher, inclusive) case False{}: range_start(~K, ~V, ~cmp, m, pick(Bound<K>, higher, lower, upper), higher)def view_extreme(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +first: Bool) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>: View{m, +lower, +upper, +descending} = view +up = pick(Bool, descending, Bool.not(first), first) view_entry_result(~K, ~V, ~cmp, lower, upper, descending, entry_snapshot(~K, ~V, ~cmp, range_start(~K, ~V, ~cmp, m, pick(Bound<K>, up, lower, upper), up)))def insert_side_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +g: Nat, +pn: Node<K>, +gn: Node<K>) -> TreeMap<K, V, cmp> & Fix: insert_side_left_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, node_right(~K, gn)))def insert_side_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +g: Nat, +pn: Node<K>, +gn: Node<K>) -> TreeMap<K, V, cmp> & Fix: insert_side_right_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, node_left(~K, gn)))def delete_target(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Nat: match r: case Tuple{m, N{c, 1n+l, 1n+r, p, k}}: successor_ready(~K, ~V, ~cmp, id, extreme(~K, ~V, ~cmp, m, 1n+r, False{})) case Tuple{m, node}: (m, id)def delete_borrow_read_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix: delete_borrow_read_left_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))def delete_borrow_read_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix: delete_borrow_read_right_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))def iterator_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>: Cursor{m, +next, current, lower, upper, forward} = cursor iter_at(~K, ~V, ~cmp, next, current, lower, upper, forward, m)def view_nav(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K, +higher: Bool, +inclusive: Bool) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>: View{m, +lower, +upper, +descending} = view +up = pick(Bool, descending, Bool.not(higher), higher) view_entry_result(~K, ~V, ~cmp, lower, upper, descending, entry_snapshot(~K, ~V, ~cmp, view_nav_start(~K, ~V, ~cmp, m, k, lower, upper, up, inclusive, pick(Bool, up, above_lower(~K, ~V, ~cmp, k, lower), below_upper(~K, ~V, ~cmp, k, upper)))))def view_first_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>: view_extreme(~K, ~V, ~cmp, view, True{})def view_last_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>: view_extreme(~K, ~V, ~cmp, view, False{})def insert_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +g: Nat, +pn: Node<K>, +gn: Node<K>, +on_left: Bool) -> TreeMap<K, V, cmp> & Fix: match on_left: case True{}: insert_side_left(~K, ~V, ~cmp, m, z, p, g, pn, gn) case False{}: insert_side_right(~K, ~V, ~cmp, m, z, p, g, pn, gn)def delete_far_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +pn: Node<K>, +wn: Node<K>, +far_red: Bool) -> TreeMap<K, V, cmp> & DeleteFix: match far_red: case True{}: delete_borrow_left(~K, ~V, ~cmp, m, p, w, pn, wn) case False{}: delete_borrow_read_left(~K, ~V, ~cmp, rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, node_left(~K, wn), False{}), w, True{}), w), p)def delete_far_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +pn: Node<K>, +wn: Node<K>, +far_red: Bool) -> TreeMap<K, V, cmp> & DeleteFix: match far_red: case True{}: delete_borrow_right(~K, ~V, ~cmp, m, p, w, pn, wn) case False{}: delete_borrow_read_right(~K, ~V, ~cmp, rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, node_right(~K, wn), False{}), w, True{}), w), p)def iterator_next_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, K>: iterator_key_result(~K, ~V, ~cmp, iterator_next(~K, ~V, ~cmp, cursor))def iterator_next_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, V>: iterator_value_result(~K, ~V, ~cmp, iterator_next(~K, ~V, ~cmp, cursor))def contains_value_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +fuel: Nat, +wanted: V, +found: Bool, st: Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>) -> TreeMap<K, V, cmp> & Bool: match fuel found st: case _ True{} Tuple{cursor, item}: (iterator_finish(~K, ~V, ~cmp, cursor), True{}) case 0n False{} Tuple{cursor, item}: (iterator_finish(~K, ~V, ~cmp, cursor), False{}) case 1n+f False{} Tuple{cursor, None{}}: (iterator_finish(~K, ~V, ~cmp, cursor), False{}) case 1n+f False{} Tuple{cursor, Some{Entry{k, v}}}: contains_value_loop(~K, ~V, ~cmp, ~eq, f, wanted, eq(v, wanted), iterator_next(~K, ~V, ~cmp, cursor))def view_lower_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>: view_nav(~K, ~V, ~cmp, view, k, False{}, False{})def view_floor_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>: view_nav(~K, ~V, ~cmp, view, k, False{}, True{})def view_ceiling_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>: view_nav(~K, ~V, ~cmp, view, k, True{}, True{})def view_higher_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>: view_nav(~K, ~V, ~cmp, view, k, True{}, False{})def view_count_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +count: Nat, st: Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>) -> View<K, V, cmp> & Nat: match fuel st: case 0n Tuple{cursor, item}: (iterator_view(~K, ~V, ~cmp, cursor), count) case 1n+f Tuple{cursor, None{}}: (iterator_view(~K, ~V, ~cmp, cursor), count) case 1n+f Tuple{cursor, Some{item}}: view_count_loop(~K, ~V, ~cmp, f, 1n+count, iterator_next(~K, ~V, ~cmp, cursor))def view_clear_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: Cursor<K, V, cmp> & Maybe<&2, V>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>: (cursor, removed) = r iterator_next(~K, ~V, ~cmp, cursor)def insert_grand_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, +p: Nat, +pn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Fix: (m1, +gn) = pair_result insert_side(~K, ~V, ~cmp, m1, z, p, node_parent(~K, pn), pn, gn, Nat.is_eq(p, node_left(~K, gn)))def delete_children_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +pn: Node<K>, +wn: Node<K>, +near_red: Bool, +far_red: Bool) -> TreeMap<K, V, cmp> & DeleteFix: match near_red far_red: case False{} False{}: (set_red(~K, ~V, ~cmp, m, w, True{}), DF{p, node_parent(~K, pn), True{}}) case _ _: delete_far_left(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)def delete_children_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +pn: Node<K>, +wn: Node<K>, +near_red: Bool, +far_red: Bool) -> TreeMap<K, V, cmp> & DeleteFix: match near_red far_red: case False{} False{}: (set_red(~K, ~V, ~cmp, m, w, True{}), DF{p, node_parent(~K, pn), True{}}) case _ _: delete_far_right(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)def contains_value_start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +wanted: V, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Bool: (m, n) = r contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+n, wanted, False{}, iterator_next(~K, ~V, ~cmp, iterator(~K, ~V, ~cmp, m)))def view_size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp> & Nat: View{TM{+n, root, lo, hi, free, nodes, payloads}, lower, upper, descending} = view view_count_loop(~K, ~V, ~cmp, 1n+n, 0n, iterator_next(~K, ~V, ~cmp, view_iterator(~K, ~V, ~cmp, View{TM{n, root, lo, hi, free, nodes, payloads}, lower, upper, descending})))def insert_grand(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +pn: Node<K>) -> TreeMap<K, V, cmp> & Fix: insert_grand_1(~K, ~V, ~cmp, z, p, pn, read(~K, ~V, ~cmp, m, node_parent(~K, pn)))def delete_sibling_left_4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, +wn: Node<K>, +near_node: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m4, +far_node) = pair_result delete_children_left(~K, ~V, ~cmp, m4, p, node_right(~K, pn), pn, wn, node_red(~K, near_node), node_red(~K, far_node))def delete_sibling_right_4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, +wn: Node<K>, +near_node: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m4, +far_node) = pair_result delete_children_right(~K, ~V, ~cmp, m4, p, node_left(~K, pn), pn, wn, node_red(~K, near_node), node_red(~K, far_node))def contains_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, m: TreeMap<K, V, cmp>, +wanted: V) -> TreeMap<K, V, cmp> & Bool: contains_value_start(~K, ~V, ~cmp, ~eq, wanted, size(~K, ~V, ~cmp, m))def insert_parent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +pn: Node<K>, +is_red: Bool) -> TreeMap<K, V, cmp> & Fix: match is_red: case False{}: (m, Fix{0n, False{}}) case True{}: insert_grand(~K, ~V, ~cmp, m, z, p, pn)def delete_sibling_left_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, +wn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m3, +near_node) = pair_result delete_sibling_left_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, node_right(~K, wn)))def delete_sibling_right_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, +wn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m3, +near_node) = pair_result delete_sibling_right_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, node_left(~K, wn)))def insert_fix_step_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, +zn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Fix: (m2, +pn) = pair_result insert_parent(~K, ~V, ~cmp, m2, z, node_parent(~K, zn), pn, node_red(~K, pn))def delete_sibling_left_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m2, +wn) = pair_result delete_sibling_left_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, node_left(~K, wn)))def delete_sibling_right_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m2, +wn) = pair_result delete_sibling_right_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, node_right(~K, wn)))def insert_fix_step_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Fix: (m1, +zn) = pair_result insert_fix_step_2(~K, ~V, ~cmp, z, zn, read(~K, ~V, ~cmp, m1, node_parent(~K, zn)))def delete_sibling_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m1, +pn) = pair_result delete_sibling_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_right(~K, pn)))def delete_sibling_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m1, +pn) = pair_result delete_sibling_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_left(~K, pn)))def insert_fix_step(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat) -> TreeMap<K, V, cmp> & Fix: insert_fix_step_1(~K, ~V, ~cmp, z, read(~K, ~V, ~cmp, m, z))def delete_sibling_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix: delete_sibling_left_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))def delete_sibling_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix: delete_sibling_right_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))def insert_fix_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: TreeMap<K, V, cmp> & Fix) -> TreeMap<K, V, cmp>: match fuel st: case 0n Tuple{m, f}: black_root(~K, ~V, ~cmp, m) case 1n+p Tuple{m, Fix{z, False{}}}: black_root(~K, ~V, ~cmp, m) case 1n+p Tuple{m, Fix{z, True{}}}: insert_fix_loop(~K, ~V, ~cmp, p, insert_fix_step(~K, ~V, ~cmp, m, z))def delete_red_sibling_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +red_sibling: Bool) -> TreeMap<K, V, cmp> & DeleteFix: match red_sibling: case True{}: delete_sibling_left(~K, ~V, ~cmp, rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, w, False{}), p, True{}), p), p) case False{}: delete_sibling_left(~K, ~V, ~cmp, m, p)def delete_red_sibling_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +red_sibling: Bool) -> TreeMap<K, V, cmp> & DeleteFix: match red_sibling: case True{}: delete_sibling_right(~K, ~V, ~cmp, rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, w, False{}), p, True{}), p), p) case False{}: delete_sibling_right(~K, ~V, ~cmp, m, p)def insert_fixed(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>: (m, n) = r insert_fix_loop(~K, ~V, ~cmp, 1n+n, (m, Fix{id, True{}}))def delete_side_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m1, +wn) = pair_result delete_red_sibling_left(~K, ~V, ~cmp, m1, p, node_right(~K, pn), node_red(~K, wn))def delete_side_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m1, +wn) = pair_result delete_red_sibling_right(~K, ~V, ~cmp, m1, p, node_left(~K, pn), node_red(~K, wn))def put_allocated(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +on_left: Bool, r: TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>: match r: case Tuple{m, Done{+id}}: (insert_fixed(~K, ~V, ~cmp, id, size(~K, ~V, ~cmp, insert_header(~K, ~V, ~cmp, attach(~K, ~V, ~cmp, m, p, id, on_left), id, p, on_left))), Done{None{}}) case Tuple{m, Fail{e}}: (m, Fail{e})def delete_side_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +pn: Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: delete_side_left_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, node_right(~K, pn)))def delete_side_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +pn: Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: delete_side_right_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, node_left(~K, pn)))def put_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>: match r: case Tuple{m, Search{0n, +p, +on_left}}: put_allocated(~K, ~V, ~cmp, p, on_left, allocate(~K, ~V, ~cmp, m, p, k, v)) case Tuple{m, Search{1n+i, p, on_left}}: put_replaced(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, m, 1n+i, Some{v}))def delete_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat, +p: Nat, +pn: Node<K>, +on_left: Bool) -> TreeMap<K, V, cmp> & DeleteFix: match on_left: case True{}: delete_side_left(~K, ~V, ~cmp, m, p, pn) case False{}: delete_side_right(~K, ~V, ~cmp, m, p, pn)def put_absent_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>: match r: case Tuple{m, Search{0n, +p, +on_left}}: put_allocated(~K, ~V, ~cmp, p, on_left, allocate(~K, ~V, ~cmp, m, p, k, v)) case Tuple{m, Search{1n+i, p, on_left}}: put_replaced(~K, ~V, ~cmp, get_id(~K, ~V, ~cmp, m, 1n+i))def put(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, +v: V) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>: put_found(~K, ~V, ~cmp, k, v, search(~K, ~V, ~cmp, m, k))def delete_stop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat, +p: Nat, +pn: Node<K>, +stop: Bool) -> TreeMap<K, V, cmp> & DeleteFix: match stop: case True{}: (set_red(~K, ~V, ~cmp, m, x, False{}), DF{0n, 0n, False{}}) case False{}: delete_side(~K, ~V, ~cmp, m, x, p, pn, Nat.is_eq(x, node_left(~K, pn)))def put_if_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, +v: V) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>: put_absent_found(~K, ~V, ~cmp, k, v, search(~K, ~V, ~cmp, m, k))def delete_fix_step_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +root_node: Nat, +xn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m3, +pn) = pair_result delete_stop(~K, ~V, ~cmp, m3, x, p, pn, Bool.or(Nat.is_eq(x, root_node), node_red(~K, xn)))def view_put_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, +v: V, lower: Bound<K>, upper: Bound<K>, +descending: Bool, +valid: Bool) -> View<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>: match valid: case True{}: view_put_finish(~K, ~V, ~cmp, lower, upper, descending, put(~K, ~V, ~cmp, m, k, v)) case False{}: (View{m, lower, upper, descending}, Fail{Rejected{OutOfRange{}, k, v}})def delete_fix_step_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +root_node: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix: (m2, +xn) = pair_result delete_fix_step_3(~K, ~V, ~cmp, x, p, root_node, xn, read(~K, ~V, ~cmp, m2, p))def view_put(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K, +v: V) -> View<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>: View{m, +lower, +upper, descending} = view view_put_checked(~K, ~V, ~cmp, m, k, v, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))def delete_fix_step_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & DeleteFix: (m1, +root_node) = pair_result delete_fix_step_2(~K, ~V, ~cmp, x, p, root_node, read(~K, ~V, ~cmp, m1, x))def delete_fix_step(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix: delete_fix_step_1(~K, ~V, ~cmp, x, p, root_id(~K, ~V, ~cmp, m))def delete_fix_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: TreeMap<K, V, cmp> & DeleteFix) -> TreeMap<K, V, cmp>: match fuel st: case 0n Tuple{m, fix}: black_root(~K, ~V, ~cmp, m) case 1n+f Tuple{m, DF{x, p, False{}}}: black_root(~K, ~V, ~cmp, m) case 1n+f Tuple{m, DF{x, p, True{}}}: delete_fix_loop(~K, ~V, ~cmp, f, delete_fix_step(~K, ~V, ~cmp, m, x, p))def delete_repair(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat, +p: Nat, +was_red: Bool) -> TreeMap<K, V, cmp>: TM{+n, root, lo, hi, free, nodes, payloads} = m delete_fix_loop(~K, ~V, ~cmp, 1n+n, (TM{n, root, lo, hi, free, nodes, payloads}, DF{x, p, Bool.not(was_red)}))def unlink_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +node: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>: (m2, +pn) = pair_result delete_repair(~K, ~V, ~cmp, recycle(~K, ~V, ~cmp, attach(~K, ~V, ~cmp, m2, node_parent(~K, node), pick(Nat, Nat.is_lt(0n, node_left(~K, node)), node_left(~K, node), node_right(~K, node)), Nat.is_eq(id, node_left(~K, pn))), id), pick(Nat, Nat.is_lt(0n, node_left(~K, node)), node_left(~K, node), node_right(~K, node)), node_parent(~K, node), node_red(~K, node))def unlink_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>: (m1, +node) = pair_result unlink_2(~K, ~V, ~cmp, id, node, read(~K, ~V, ~cmp, m1, node_parent(~K, node)))def unlink(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>: unlink_1(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))def unlink_target(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>: (m, id) = r refresh_ends(~K, ~V, ~cmp, unlink(~K, ~V, ~cmp, m, id))def remove_present_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Maybe<&2, V>: (m1, value) = pair_result (unlink_target(~K, ~V, ~cmp, delete_target(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m1, id))), value)def remove_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Maybe<&2, V>: remove_present_1(~K, ~V, ~cmp, id, exchange(~K, ~V, ~cmp, m, id, None{}))def remove_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Maybe<&2, V>: match id: case 0n: (m, None{}) case 1n+i: remove_present(~K, ~V, ~cmp, m, 1n+i)def remove_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Maybe<&2, V>: (m, Search{id, p, on_left}) = r remove_id(~K, ~V, ~cmp, m, id)def remove_entry_id_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: (m1, +node) = pair_result entry_value(~K, ~V, ~cmp, node_key(~K, node), remove_id(~K, ~V, ~cmp, m1, id))def iterator_delete_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, pair_result: TreeMap<K, V, cmp> & Node<K>) -> Cursor<K, V, cmp> & Maybe<&2, V>: (m1, +node) = pair_result iterator_reseek(~K, ~V, ~cmp, node_key(~K, node), lower, upper, forward, remove_id(~K, ~V, ~cmp, m1, current))def remove_if_apply(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +replacement: V, +equal: Bool) -> TreeMap<K, V, cmp> & Bool: match equal: case False{}: (m, False{}) case True{}: changed_value(~K, ~V, ~cmp, remove_id(~K, ~V, ~cmp, m, id))def remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, V>: remove_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))def remove_entry_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: remove_entry_id_1(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))def iterator_delete(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +next: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool) -> Cursor<K, V, cmp> & Maybe<&2, V>: iterator_delete_1(~K, ~V, ~cmp, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))def remove_if_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +id: Nat, +expected: V, +replacement: V, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Bool: match r: case Tuple{m, None{}}: (m, False{}) case Tuple{m, Some{old}}: remove_if_apply(~K, ~V, ~cmp, m, id, replacement, eq(old, expected))def poll_ready(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: (m, id) = r remove_entry_id(~K, ~V, ~cmp, m, id)def view_remove_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, lower: Bound<K>, upper: Bound<K>, +descending: Bool, +valid: Bool) -> View<K, V, cmp> & Maybe<&2, V>: match valid: case True{}: view_value(~K, ~V, ~cmp, lower, upper, descending, remove(~K, ~V, ~cmp, m, k)) case False{}: (View{m, lower, upper, descending}, None{})def iterator_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, V>: Cursor{m, next, current, lower, upper, forward} = cursor iterator_delete(~K, ~V, ~cmp, m, next, current, lower, upper, forward)def remove_if_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +expected: V, +replacement: V, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Bool: (m, Search{+id, p, on_left}) = r remove_if_value(~K, ~V, ~cmp, ~eq, id, expected, replacement, get_id(~K, ~V, ~cmp, m, id))def poll_first_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: poll_ready(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))def poll_last_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>: poll_ready(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))def view_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, V>: View{m, +lower, +upper, descending} = view view_remove_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))def remove_if_equal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, m: TreeMap<K, V, cmp>, +k: K, +expected: V) -> TreeMap<K, V, cmp> & Bool: remove_if_found(~K, ~V, ~cmp, ~eq, expected, expected, search(~K, ~V, ~cmp, m, k))def view_clear_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>) -> View<K, V, cmp>: match fuel st: case 0n Tuple{cursor, item}: iterator_view(~K, ~V, ~cmp, cursor) case 1n+f Tuple{cursor, None{}}: iterator_view(~K, ~V, ~cmp, cursor) case 1n+f Tuple{cursor, Some{item}}: view_clear_loop(~K, ~V, ~cmp, f, view_clear_next(~K, ~V, ~cmp, iterator_remove(~K, ~V, ~cmp, cursor)))def view_clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp>: View{TM{+n, root, lo, hi, free, nodes, payloads}, lower, upper, descending} = view view_clear_loop(~K, ~V, ~cmp, 1n+n, iterator_next(~K, ~V, ~cmp, view_iterator(~K, ~V, ~cmp, View{TM{n, root, lo, hi, free, nodes, payloads}, lower, upper, descending})))