src/containers/balanced_search_tree.bend

bend-collections@1.0.0.0 · 1,846 lines · 361 definitions

1# Generated by tools/generators/tree_map.py; edit algorithm definitions there.
2import Base
3import bend-collections@1.0.0.0/src/containers/dynamic_array.bend as D
4import bend-collections@1.0.0.0/src/containers/types/dynamic_array.bend as DE
5
6# Indexed CLRS red-black map. Keys and payloads are Data for this version.
7# Comparator is a type index: changing comparator requires rebuilding a map.
8# Node links are slot indices plus one; zero is the black NIL sentinel.
9type Node<-K: Data> is Data:
10  Free{next: Nat}
11  N{red: Bool, left: Nat, right: Nat, parent: Nat, key: K}
12
13# Node storage: one array per node field instead of one array of Node
14# records. Reading a record out of an array hands back a shared copy that the
15# runtime reference-counts and takes apart field by field; a field read out of
16# its own array is a plain word. The store has the shape of a dynamic array
17# of nodes: slots [0, used) are live, the capacity is 2^depth <= 2^limit, and
18# it grows by doubling. A slot holds the encoding of its node by ntag (0 free,
19# 1 black, 2 red), nleft (the free-list link of a free slot), nright, nparent
20# and nkey (None when free); every other slot holds the encoding of Free{0},
21# so each array is exactly its field of the node list, padded.
22type NodeStore<-K: Data> is Type:
23  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>>}
24
25type TreeMap<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
26  TM{size: Nat, root: Nat, first: Nat, last: Nat, free: Nat,
27     nodes: NodeStore<K>, payloads: D.DynArray<&2, Maybe<&2, V>>}
28
29type Entry<-K: Data, -V: Data> is Data:
30  Entry{key: K, value: V}
31
32type Error is Data:
33  CapacityExceeded{}
34  OutOfRange{}
35  NoCurrent{}
36  InvalidBounds{}
37
38type Rejected<-K: Data, -V: Data> is Data:
39  Rejected{error: Error, key: K, value: V}
40
41type Search is Data:
42  Search{found: Nat, parent: Nat, left: Bool}
43
44type Fix is Data:
45  Fix{node: Nat, more: Bool}
46
47type Ascend is Data:
48  Ascend{child: Nat, parent: Nat, done: Bool}
49
50# A direct branch preserves scalar traversal state in native code. Passing
51# these records through pick(-T: Type) erases their layout and boxes both arms.
52type DeleteFix is Data:
53  DF{node: Nat, parent: Nat, more: Bool}
54
55type NavEnd is Data:
56  NavBest{id: Nat}
57  NavEqual{id: Nat}
58
59type Bound<-K: Data> is Data:
60  Unbounded{}
61  Inclusive{key: K}
62  Exclusive{key: K}
63
64type View<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
65  View{map: TreeMap<K, V, cmp>, lower: Bound<K>, upper: Bound<K>, descending: Bool}
66
67type InvalidView<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
68  InvalidView{map: TreeMap<K, V, cmp>, error: Error}
69
70type Cursor<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
71  Cursor{map: TreeMap<K, V, cmp>, next: Nat, current: Nat,
72         lower: Bound<K>, upper: Bound<K>, forward: Bool}
73
74def ntag(~K: Data, n: Node<K>) -> Nat:
75  match n:
76    case Free{x}:
77      0n
78    case N{c, l, r, p, k}:
79      match c:
80        case True{}:
81          2n
82        case False{}:
83          1n
84
85def nleft(~K: Data, n: Node<K>) -> Nat:
86  match n:
87    case Free{x}:
88      x
89    case N{c, l, r, p, k}:
90      l
91
92def nright(~K: Data, n: Node<K>) -> Nat:
93  match n:
94    case Free{x}:
95      0n
96    case N{c, l, r, p, k}:
97      r
98
99def nparent(~K: Data, n: Node<K>) -> Nat:
100  match n:
101    case Free{x}:
102      0n
103    case N{c, l, r, p, k}:
104      p
105
106def nkey(~K: Data, n: Node<K>) -> Maybe<&2, K>:
107  match n:
108    case Free{x}:
109      None{}
110    case N{c, l, r, p, k}:
111      Some{k}
112
113def mk_node(~K: Data, +t: Nat, +l: Nat, +r: Nat, +p: Nat, k: Maybe<&2, K>) -> Node<K>:
114  match t k:
115    case 0n _:
116      Free{l}
117    case 1n+ +c Some{key}:
118      N{Nat.is_eq(c, 1n), l, r, p, key}
119    case 1n+ +c None{}:
120      Free{l}
121
122def ns_nats(+d: Nat) -> Array<Nat>:
123  Array.new(Nat, d, 0n)
124
125def ns_nokeys(~K: Data, +d: Nat) -> Array<Maybe<&2, K>>:
126  Array.new(Maybe<&2, K>, d, None{})
127
128def ns_length(~K: Data, s: NodeStore<K>) -> NodeStore<K> & Nat:
129  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
130  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, used)
131
132# ---- reading a slot ----
133
134def 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:
135  (tags, +x) = q
136  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)
137
138def 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:
139  (lefts, +x) = q
140  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)
141
142def 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:
143  (rights, +x) = q
144  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)
145
146def 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:
147  (parents, +x) = q
148  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)
149
150def 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>:
151  (keys, x) = q
152  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)
153
154def ns_red_tag(red: Bool) -> Nat:
155  match red:
156    case True{}:
157      2n
158    case False{}:
159      1n
160
161def 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>:
162  match q:
163    case Tuple{tags, 0n}:
164      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
165    case Tuple{tags, 1n+c}:
166      NS{limit, depth, cap, used, tags, Array.set(Nat, lefts, U32.from_nat(i), v), rights, parents, keys}
167
168def 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>:
169  match q:
170    case Tuple{tags, 0n}:
171      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
172    case Tuple{tags, 1n+c}:
173      NS{limit, depth, cap, used, tags, lefts, Array.set(Nat, rights, U32.from_nat(i), v), parents, keys}
174
175def 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>:
176  match q:
177    case Tuple{tags, 0n}:
178      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
179    case Tuple{tags, 1n+c}:
180      NS{limit, depth, cap, used, tags, lefts, rights, Array.set(Nat, parents, U32.from_nat(i), v), keys}
181
182def pick(-T: Type, b: Bool, yes: T, no: T) -> T:
183  match b:
184    case True{}:
185      yes
186    case False{}:
187      no
188
189def node_red(~K: Data, n: Node<K>) -> Bool:
190  match n:
191    case Free{x}:
192      False{}
193    case N{c, l, r, p, k}:
194      c
195
196def node_left(~K: Data, n: Node<K>) -> Nat:
197  match n:
198    case Free{x}:
199      0n
200    case N{c, l, r, p, k}:
201      l
202
203def node_right(~K: Data, n: Node<K>) -> Nat:
204  match n:
205    case Free{x}:
206      0n
207    case N{c, l, r, p, k}:
208      r
209
210def node_parent(~K: Data, n: Node<K>) -> Nat:
211  match n:
212    case Free{x}:
213      0n
214    case N{c, l, r, p, k}:
215      p
216
217def node_key(~K: Data, n: Node<K>) -> Maybe<&2, K>:
218  match n:
219    case Free{x}:
220      None{}
221    case N{c, l, r, p, k}:
222      Some{k}
223
224def size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
225  TM{+n, root, lo, hi, free, nodes, payloads} = m
226  (TM{n, root, lo, hi, free, nodes, payloads}, n)
227
228def root_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
229  TM{n, +root, lo, hi, free, nodes, payloads} = m
230  (TM{n, root, lo, hi, free, nodes, payloads}, root)
231
232def first_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
233  TM{n, root, +lo, hi, free, nodes, payloads} = m
234  (TM{n, root, lo, hi, free, nodes, payloads}, lo)
235
236def last_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
237  TM{n, root, lo, +hi, free, nodes, payloads} = m
238  (TM{n, root, lo, hi, free, nodes, payloads}, hi)
239
240def 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>:
241  match r:
242    case Tuple{nodes, Done{x}}:
243      (TM{n, root, lo, hi, free, nodes, payloads}, x)
244    case Tuple{nodes, Fail{e}}:
245      (TM{n, root, lo, hi, free, nodes, payloads}, Free{0n})
246
247def 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>:
248  (nodes, status) = r
249  TM{n, root, lo, hi, free, nodes, payloads}
250
251def set_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +root: Nat) -> TreeMap<K, V, cmp>:
252  TM{n, old, lo, hi, free, nodes, payloads} = m
253  TM{n, root, lo, hi, free, nodes, payloads}
254
255def 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):
256  match r:
257    case Tuple{m, Free{next}}:
258      (m, (Free{next}, EQ{}))
259    case Tuple{m, N{c, l, r, p, +key}}:
260      (m, (N{c, l, r, p, key}, cmp(k, key)))
261
262def 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>):
263  match r:
264    case Tuple{nodes, None{}}:
265      (nodes, (id, None{}))
266    case Tuple{nodes, Some{key}}:
267      (nodes, (id, Some{cmp(k, key)}))
268
269def 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:
270  (nodes, s) = r
271  (TM{n, root, lo, hi, free, nodes, payloads}, s)
272
273def 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>:
274  match r:
275    case Tuple{payloads, Done{old}}:
276      (TM{n, root, lo, hi, free, nodes, payloads}, old)
277    case Tuple{payloads, Fail{e}}:
278      (TM{n, root, lo, hi, free, nodes, payloads}, None{})
279
280def 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>:
281  (nodes, dropped) = r
282  (TM{n, root, lo, hi, free, nodes, payloads}, Fail{Rejected{CapacityExceeded{}, k, v}})
283
284def free_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +free: Nat) -> TreeMap<K, V, cmp>:
285  TM{n, root, lo, hi, old, nodes, payloads} = m
286  TM{n, root, lo, hi, free, nodes, payloads}
287
288def 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>:
289  (m1, old) = pair_result
290  (m1, Done{id})
291
292def 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>>:
293  (m, old) = r
294  (m, Done{old})
295
296def 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>:
297  match r:
298    case Tuple{payloads, Done{x}}:
299      (TM{n, root, lo, hi, free, nodes, payloads}, x)
300    case Tuple{payloads, Fail{e}}:
301      (TM{n, root, lo, hi, free, nodes, payloads}, None{})
302
303def contains_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Bool:
304  (m, Search{id, p, left}) = r
305  (m, Nat.is_lt(0n, id))
306
307def ascend_choice(x: Nat, p: Nat, q: Nat, found: Bool) -> Ascend:
308  match found:
309    case True{}:
310      Ascend{0n, p, True{}}
311    case False{}:
312      Ascend{x, q, False{}}
313
314def 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:
315  (nodes, id) = r
316  (TM{n, root, lo, hi, free, nodes, payloads}, id)
317
318def 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:
319  (m3, old) = pair_result
320  (m3, source)
321
322def release_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>:
323  TM{n, root, lo, hi, free, nodes, payloads} = m
324  TM{Nat.sub(n, 1n), root, lo, hi, id, nodes, payloads}
325
326def set_ends(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +lo: Nat, +hi: Nat) -> TreeMap<K, V, cmp>:
327  TM{n, root, oldlo, oldhi, free, nodes, payloads} = m
328  TM{n, root, lo, hi, free, nodes, payloads}
329
330def is_empty_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Bool:
331  (m1, +n) = pair_result
332  (m1, Nat.is_eq(n, 0n))
333
334def 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>>:
335  match k r:
336    case Some{key} Tuple{m, Some{v}}:
337      (m, Some{Entry{key, v}})
338    case _ Tuple{m, value}:
339      (m, None{})
340
341def 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>>:
342  match mk mv:
343    case Some{key} Some{v}:
344      (TM{n, root, lo, hi, free, nodes, payloads}, Some{Entry{key, v}})
345    case _ _:
346      (TM{n, root, lo, hi, free, nodes, payloads}, None{})
347
348def 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:
349  match r:
350    case Tuple{m, None{}}:
351      (m, fallback)
352    case Tuple{m, Some{v}}:
353      (m, v)
354
355def ordering_ok(order: Cmp, inclusive: Bool) -> Bool:
356  match order:
357    case LT{}:
358      True{}
359    case EQ{}:
360      inclusive
361    case GT{}:
362      False{}
363
364def 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>>:
365  match valid:
366    case True{}:
367      Done{View{m, lower, upper, descending}}
368    case False{}:
369      Fail{InvalidView{m, InvalidBounds{}}}
370
371def head_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, upper: Bound<K>) -> View<K, V, cmp>:
372  View{m, Unbounded{}, upper, False{}}
373
374def tail_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, lower: Bound<K>) -> View<K, V, cmp>:
375  View{m, lower, Unbounded{}, False{}}
376
377def descending_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> View<K, V, cmp>:
378  View{m, Unbounded{}, Unbounded{}, True{}}
379
380def view_reverse(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp>:
381  View{m, lower, upper, descending} = view
382  View{m, lower, upper, Bool.not(descending)}
383
384def view_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> TreeMap<K, V, cmp>:
385  View{m, lower, upper, descending} = view
386  m
387
388def 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>:
389  (m, v) = r
390  (View{m, lower, upper, descending}, v)
391
392def 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>>:
393  (m, status) = r
394  (View{m, lower, upper, descending}, status)
395
396def 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>:
397  (m, id) = r
398  Cursor{m, id, 0n, lower, upper, forward}
399
400def iterator_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> TreeMap<K, V, cmp>:
401  Cursor{m, next, current, lower, upper, forward} = cursor
402  m
403
404def iterator_view(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> View<K, V, cmp>:
405  Cursor{m, next, current, lower, upper, forward} = cursor
406  View{m, lower, upper, Bool.not(forward)}
407
408def 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>>:
409  (m, next) = r
410  (Cursor{m, next, id, lower, upper, forward}, Some{entry})
411
412def 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>:
413  match r:
414    case Tuple{m, Some{old}}:
415      (Cursor{m, next, current, lower, upper, forward}, Done{old})
416    case Tuple{m, None{}}:
417      (Cursor{m, next, current, lower, upper, forward}, Fail{NoCurrent{}})
418
419def 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>:
420  (m, Search{id, p, on_left}) = r
421  (Cursor{m, id, 0n, lower, upper, forward}, removed)
422
423def 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>:
424  match r:
425    case Tuple{cursor, None{}}:
426      (cursor, None{})
427    case Tuple{cursor, Some{Entry{k, v}}}:
428      (cursor, Some{k})
429
430def 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>:
431  match r:
432    case Tuple{cursor, None{}}:
433      (cursor, None{})
434    case Tuple{cursor, Some{Entry{k, v}}}:
435      (cursor, Some{v})
436
437def changed_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Bool:
438  match r:
439    case Tuple{m, None{}}:
440      (m, False{})
441    case Tuple{m, Some{old}}:
442      (m, True{})
443
444def view_contains_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: View<K, V, cmp> & Maybe<&2, V>) -> View<K, V, cmp> & Bool:
445  match r:
446    case Tuple{view, None{}}:
447      (view, False{})
448    case Tuple{view, Some{x}}:
449      (view, True{})
450
451def 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>>:
452  match valid:
453    case True{}:
454      (View{m, lower, upper, descending}, Some{entry})
455    case False{}:
456      (View{m, lower, upper, descending}, None{})
457
458def ns_empty(~K: Data, +limit: Nat) -> NodeStore<K>:
459  NS{limit, 0n, 1n, 0n, ns_nats(0n), ns_nats(0n), ns_nats(0n), ns_nats(0n), ns_nokeys(~K, 0n)}
460
461def 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>>:
462  (keys, k) = q
463  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Done{mk_node(~K, t, l, r, p, k)})
464
465def 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:
466  match ok:
467    case True{}:
468      ns_tag_fin(~K, limit, depth, cap, used, lefts, rights, parents, keys, Array.get(Nat, tags, U32.from_nat(i)))
469    case False{}:
470      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)
471
472def 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:
473  match ok:
474    case True{}:
475      ns_left_fin(~K, limit, depth, cap, used, tags, rights, parents, keys, Array.get(Nat, lefts, U32.from_nat(i)))
476    case False{}:
477      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)
478
479def 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:
480  match ok:
481    case True{}:
482      ns_right_fin(~K, limit, depth, cap, used, tags, lefts, parents, keys, Array.get(Nat, rights, U32.from_nat(i)))
483    case False{}:
484      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)
485
486def 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:
487  match ok:
488    case True{}:
489      ns_parent_fin(~K, limit, depth, cap, used, tags, lefts, rights, keys, Array.get(Nat, parents, U32.from_nat(i)))
490    case False{}:
491      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)
492
493def 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>:
494  match ok:
495    case True{}:
496      ns_key_fin(~K, limit, depth, cap, used, tags, lefts, rights, parents, Array.get(Maybe<&2, K>, keys, U32.from_nat(i)))
497    case False{}:
498      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, None{})
499
500def 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>:
501  match ok:
502    case True{}:
503      ns_set_left_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i)))
504    case False{}:
505      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
506
507def 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>:
508  match ok:
509    case True{}:
510      ns_set_right_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i)))
511    case False{}:
512      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
513
514def 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>:
515  match ok:
516    case True{}:
517      ns_set_parent_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i)))
518    case False{}:
519      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
520
521def 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>:
522  match q:
523    case Tuple{tags, 0n}:
524      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
525    case Tuple{tags, 1n+c}:
526      NS{limit, depth, cap, used, Array.set(Nat, tags, U32.from_nat(i), ns_red_tag(v)), lefts, rights, parents, keys}
527
528def 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>:
529  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))}
530
531def ns_grow_nats(+depth: Nat, a: Array<Nat>) -> Array<Nat>:
532  ANode{a, ns_nats(depth)}
533
534def ns_grow_keys(~K: Data, +depth: Nat, a: Array<Maybe<&2, K>>) -> Array<Maybe<&2, K>>:
535  ANode{a, ns_nokeys(~K, depth)}
536
537def child(~K: Data, +n: Node<K>, forward: Bool) -> Nat:
538  pick(Nat, forward, node_right(~K, n), node_left(~K, n))
539
540# All links reference live slots. Free slots contain no key and no value.
541
542def 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>:
543  match m id:
544    case mm 0n:
545      (mm, None{})
546    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
547      exchange_finish(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, D.swap_at(~Maybe<&2, V>, payloads, i, value))
548
549def 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>:
550  TM{+n, root, +lo, +hi, free, nodes, payloads} = m
551  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}
552
553def get_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
554  match m id:
555    case mm 0n:
556      (mm, None{})
557    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
558      get_id_finish(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, D.get_at(~Maybe<&2, V>, payloads, i))
559
560def 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:
561  match r:
562    case Tuple{m, Free{next}}:
563      (m, Ascend{0n, 0n, True{}})
564    case Tuple{m, N{c, l, r, q, key}}:
565      (m, ascend_choice(p, p, q, Nat.is_eq(x, pick(Nat, forward, l, r))))
566
567def ascend_par(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +s: Nat, r: NodeStore<K> & Nat) -> NodeStore<K> & Ascend:
568  (nodes, +q) = r
569  (nodes, ascend_choice(p, p, q, Nat.is_eq(x, s)))
570
571def refresh_ends_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo: Nat, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
572  (m3, +hi) = pair_result
573  set_ends(~K, ~V, ~cmp, m3, lo, hi)
574
575def is_empty(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Bool:
576  is_empty_1(~K, ~V, ~cmp, size(~K, ~V, ~cmp, m))
577
578def key_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
579  (m, node) = r
580  (m, node_key(~K, node))
581
582def 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>>:
583  (nodes, mk) = r
584  snap_kv(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, nodes, mk, mv)
585
586def above_lower(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, bound: Bound<K>) -> Bool:
587  match bound:
588    case Unbounded{}:
589      True{}
590    case Inclusive{lo}:
591      ordering_ok(cmp(lo, k), True{})
592    case Exclusive{lo}:
593      ordering_ok(cmp(lo, k), False{})
594
595def below_upper(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, bound: Bound<K>) -> Bool:
596  match bound:
597    case Unbounded{}:
598      True{}
599    case Inclusive{hi}:
600      ordering_ok(cmp(k, hi), True{})
601    case Exclusive{hi}:
602      ordering_ok(cmp(k, hi), False{})
603
604def bounds_valid(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: Bound<K>, upper: Bound<K>) -> Bool:
605  match lower upper:
606    case Unbounded{} _:
607      True{}
608    case _ Unbounded{}:
609      True{}
610    case Inclusive{lo} Inclusive{hi}:
611      ordering_ok(cmp(lo, hi), True{})
612    case Inclusive{lo} Exclusive{hi}:
613      ordering_ok(cmp(lo, hi), True{})
614    case Exclusive{lo} Inclusive{hi}:
615      ordering_ok(cmp(lo, hi), True{})
616    case Exclusive{lo} Exclusive{hi}:
617      ordering_ok(cmp(lo, hi), True{})
618
619def range_unbounded(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
620  match forward:
621    case True{}:
622      first_id(~K, ~V, ~cmp, m)
623    case False{}:
624      last_id(~K, ~V, ~cmp, m)
625
626def iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
627  cursor_started(~K, ~V, ~cmp, Unbounded{}, Unbounded{}, True{}, first_id(~K, ~V, ~cmp, m))
628
629def descending_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
630  cursor_started(~K, ~V, ~cmp, Unbounded{}, Unbounded{}, False{}, last_id(~K, ~V, ~cmp, m))
631
632def ns_new(~K: Data) -> NodeStore<K>:
633  ns_empty(~K, D.max_depth())
634
635def ns_with_limit(~K: Data, +k: Nat) -> NodeStore<K>:
636  ns_empty(~K, D.clamp_limit(k, Nat.is_lt(k, D.max_depth())))
637
638def 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>>:
639  (parents, +p) = q
640  ns_rk(~K, limit, depth, cap, used, tags, lefts, rights, parents, t, l, r, p, Array.get(Maybe<&2, K>, keys, i))
641
642def ns_tag_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat:
643  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
644  ns_tag_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))
645
646def ns_left_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat:
647  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
648  ns_left_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))
649
650def ns_right_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat:
651  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
652  ns_right_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))
653
654def ns_parent_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat:
655  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
656  ns_parent_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))
657
658def ns_key_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Maybe<&2, K>:
659  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
660  ns_key_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))
661
662# ---- writing one field of a live slot (free slots and ids past the length unchanged) ----
663
664def ns_set_left(~K: Data, s: NodeStore<K>, +i: Nat, +v: Nat) -> NodeStore<K>:
665  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
666  ns_set_left_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))
667
668def ns_set_right(~K: Data, s: NodeStore<K>, +i: Nat, +v: Nat) -> NodeStore<K>:
669  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
670  ns_set_right_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))
671
672def ns_set_parent(~K: Data, s: NodeStore<K>, +i: Nat, +v: Nat) -> NodeStore<K>:
673  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
674  ns_set_parent_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))
675
676def 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>:
677  match ok:
678    case True{}:
679      ns_set_red_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i)))
680    case False{}:
681      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
682
683def 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>:
684  match ok:
685    case True{}:
686      (ns_put(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, U32.from_nat(i), node), Done{Unit{}})
687    case False{}:
688      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Fail{DE.IndexOutOfRange{}})
689
690def 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>:
691  match room grow:
692    case True{} _:
693      (ns_put(~K, limit, depth, cap, 1n+used, tags, lefts, rights, parents, keys, U32.from_nat(used), node), Done{Unit{}})
694    case False{} True{}:
695      (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{}})
696    case False{} False{}:
697      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Fail{DE.CapacityExceeded{}})
698
699def ns_drop(~K: Data, s: NodeStore<K>, +m: Nat) -> NodeStore<K>:
700  NS{limit, depth, cap, used, tags, lefts, rights, parents, keys} = s
701  ns_put(~K, limit, depth, cap, m, tags, lefts, rights, parents, keys, U32.from_nat(m), Free{0n})
702
703def get_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
704  (m, Search{id, p, on_left}) = r
705  get_id(~K, ~V, ~cmp, m, id)
706
707def 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>:
708  match r:
709    case Tuple{m, Search{0n, p, on_left}}:
710      (m, None{})
711    case Tuple{m, Search{1n+i, p, on_left}}:
712      exchange(~K, ~V, ~cmp, m, 1n+i, Some{v})
713
714def in_range(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, lower: Bound<K>, upper: Bound<K>) -> Bool:
715  Bool.and(above_lower(~K, ~V, ~cmp, k, lower), below_upper(~K, ~V, ~cmp, k, upper))
716
717def 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>>:
718  view_checked(~K, ~V, ~cmp, m, lower, upper, False{}, bounds_valid(~K, ~V, ~cmp, lower, upper))
719
720def 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>:
721  match cursor:
722    case Cursor{m, next, 0n, lower, upper, forward}:
723      (Cursor{m, next, 0n, lower, upper, forward}, Fail{NoCurrent{}})
724    case Cursor{m, next, 1n+ +id, lower, upper, forward}:
725      iterator_set_done(~K, ~V, ~cmp, next, 1n+id, lower, upper, forward, exchange(~K, ~V, ~cmp, m, 1n+id, Some{v}))
726
727def entry_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
728  iterator(~K, ~V, ~cmp, m)
729
730def key_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
731  iterator(~K, ~V, ~cmp, m)
732
733def values(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
734  iterator(~K, ~V, ~cmp, m)
735
736def 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:
737  match equal:
738    case False{}:
739      (m, False{})
740    case True{}:
741      changed_value(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, m, id, Some{replacement}))
742
743def 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>>:
744  (rights, +r) = q
745  ns_rp(~K, limit, depth, cap, used, tags, lefts, rights, keys, i, t, l, r, Array.get(Nat, parents, i))
746
747def ns_set_red(~K: Data, s: NodeStore<K>, +i: Nat, +v: Bool) -> NodeStore<K>:
748  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
749  ns_set_red_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))
750
751# ---- writing a slot: the encoding of the node in all five arrays ----
752
753def ns_set(~K: Data, s: NodeStore<K>, +i: Nat, +node: Node<K>) -> NodeStore<K> & Result<&2, &2, DE.Error, Unit>:
754  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
755  ns_set_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, node, Nat.is_lt(i, used))
756
757# ---- appending a slot ----
758
759def ns_push(~K: Data, s: NodeStore<K>, +node: Node<K>) -> NodeStore<K> & Result<&2, &2, DE.Error, Unit>:
760  NS{+limit, +depth, +cap, +used, tags, lefts, rights, parents, keys} = s
761  ns_push_room(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, node, Nat.is_lt(used, cap), Nat.is_lt(depth, limit))
762
763# ---- dropping slots: the dropped slots get the encoding of Free{0} back ----
764
765def 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>>:
766  (s, x) = r
767  (ns_drop(~K, s, m), x)
768
769def ns_clear_go(~K: Data, k: Nat, s: NodeStore<K>) -> NodeStore<K>:
770  match k:
771    case 0n:
772      s
773    case 1n+ +m:
774      ns_clear_go(~K, m, ns_drop(~K, s, m))
775
776# O(used): resets the live slots top down and keeps the capacity.
777def new(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp) -> TreeMap<K, V, cmp>:
778  TM{0n, 0n, 0n, 0n, 0n, ns_new(~K), D.new_at(~Maybe<&2, V>)}
779
780def set_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:
781  match m id:
782    case mm 0n:
783      mm
784    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
785      TM{n, root, lo, hi, free, ns_set_left(~K, nodes, i, v), payloads}
786
787def set_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:
788  match m id:
789    case mm 0n:
790      mm
791    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
792      TM{n, root, lo, hi, free, ns_set_right(~K, nodes, i, v), payloads}
793
794def set_parent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:
795  match m id:
796    case mm 0n:
797      mm
798    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
799      TM{n, root, lo, hi, free, ns_set_parent(~K, nodes, i, v), payloads}
800
801def search_probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +id: Nat, +k: K) -> NodeStore<K> & (Nat & Maybe<&2, Cmp>):
802  match id:
803    case 0n:
804      (nodes, (0n, None{}))
805    case 1n+ +i:
806      search_key(~K, ~V, ~cmp, 1n+i, k, ns_key_at(~K, nodes, i))
807
808def side_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +left: Bool, +i: Nat) -> NodeStore<K> & Nat:
809  match left:
810    case True{}:
811      ns_left_at(~K, nodes, i)
812    case False{}:
813      ns_right_at(~K, nodes, i)
814
815def ascend_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +i: Nat, r: NodeStore<K> & Nat) -> NodeStore<K> & Ascend:
816  (nodes, +s) = r
817  ascend_par(~K, ~V, ~cmp, x, p, s, ns_parent_at(~K, nodes, i))
818
819def 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>>:
820  (TM{+n, +root, +lo, +hi, +free, nodes, payloads}, mv) = r
821  snap_key(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, mv, ns_key_at(~K, nodes, i))
822
823def with_limit(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +limit: Nat) -> TreeMap<K, V, cmp>:
824  TM{0n, 0n, 0n, 0n, 0n, ns_with_limit(~K, limit), D.with_limit_at(~Maybe<&2, V>, limit)}
825
826def 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:
827  match r:
828    case Tuple{m, None{}}:
829      (m, False{})
830    case Tuple{m, Some{old}}:
831      replace_if_apply(~K, ~V, ~cmp, m, id, replacement, eq(old, expected))
832
833def 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:
834  match r:
835    case Tuple{m, Free{free}}:
836      (Cursor{m, next, current, lower, upper, forward}, False{})
837    case Tuple{m, N{c, l, rr, p, key}}:
838      (Cursor{m, next, current, lower, upper, forward}, in_range(~K, ~V, ~cmp, key, lower, upper))
839
840def 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>>:
841  match r:
842    case Tuple{m, None{}}:
843      (View{m, lower, upper, descending}, None{})
844    case Tuple{m, Some{Entry{+k, v}}}:
845      view_entry_checked(~K, ~V, ~cmp, m, lower, upper, descending, Entry{k, v}, in_range(~K, ~V, ~cmp, k, lower, upper))
846
847def 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>>:
848  (lefts, +l) = q
849  ns_rr(~K, limit, depth, cap, used, tags, lefts, parents, keys, i, t, l, Array.get(Nat, rights, i))
850
851def ns_clear(~K: Data, s: NodeStore<K>) -> NodeStore<K>:
852  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
853  ns_clear_go(~K, used, NS{limit, depth, cap, used, tags, lefts, rights, parents, keys})
854
855
856def write(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:
857  match m id:
858    case mm 0n:
859      mm
860    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
861      write_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, ns_set(~K, nodes, i, node))
862
863def set_red(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Bool) -> TreeMap<K, V, cmp>:
864  match m id:
865    case mm 0n:
866      mm
867    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
868      TM{n, root, lo, hi, free, ns_set_red(~K, nodes, i, v), payloads}
869
870def 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>:
871  match p on_left:
872    case 0n _:
873      set_root(~K, ~V, ~cmp, m, x)
874    case 1n+q True{}:
875      set_left(~K, ~V, ~cmp, m, 1n+q, x)
876    case 1n+q False{}:
877      set_right(~K, ~V, ~cmp, m, 1n+q, x)
878
879def search_down2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, r: NodeStore<K> & Nat) -> NodeStore<K> & (Nat & Maybe<&2, Cmp>):
880  (nodes, +c) = r
881  search_probe(~K, ~V, ~cmp, nodes, c, k)
882
883def 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:
884  match r:
885    case Tuple{nodes, 0n}:
886      (nodes, Ascend{0n, 0n, True{}})
887    case Tuple{nodes, 1n+c}:
888      ascend_side(~K, ~V, ~cmp, x, p, i, side_at(~K, ~V, ~cmp, nodes, forward, i))
889
890def extreme_tag(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, +i: Nat, r: NodeStore<K> & Nat) -> NodeStore<K> & Nat:
891  match r:
892    case Tuple{nodes, 0n}:
893      (nodes, 0n)
894    case Tuple{nodes, 1n+c}:
895      side_at(~K, ~V, ~cmp, nodes, Bool.not(forward), i)
896
897def 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>>:
898  match id:
899    case 0n:
900      (m, None{})
901    case 1n+ +i:
902      snap_value(~K, ~V, ~cmp, i, get_id(~K, ~V, ~cmp, m, 1n+i))
903
904def 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:
905  (m, Search{+id, p, on_left}) = r
906  replace_if_value(~K, ~V, ~cmp, ~eq, id, expected, replacement, get_id(~K, ~V, ~cmp, m, id))
907
908def 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>>:
909  (tags, +t) = q
910  ns_rl(~K, limit, depth, cap, used, tags, rights, parents, keys, i, t, Array.get(Nat, lefts, i))
911
912def 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>:
913  set_parent(~K, ~V, ~cmp, attach_side(~K, ~V, ~cmp, m, p, x, on_left), x, p)
914
915def 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>):
916  match id:
917    case 0n:
918      (nodes, (0n, None{}))
919    case 1n+ +i:
920      search_down2(~K, ~V, ~cmp, k, side_at(~K, ~V, ~cmp, nodes, left, i))
921
922def black_root_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
923  (m1, +r) = pair_result
924  set_red(~K, ~V, ~cmp, m1, r, False{})
925
926def 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>:
927  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}))
928
929def ascend_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +forward: Bool, nodes: NodeStore<K>) -> NodeStore<K> & Ascend:
930  match p:
931    case 0n:
932      (nodes, Ascend{0n, 0n, True{}})
933    case 1n+ +i:
934      ascend_tag(~K, ~V, ~cmp, x, 1n+i, i, forward, ns_tag_at(~K, nodes, i))
935
936def extreme_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, nodes: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat:
937  extreme_tag(~K, ~V, ~cmp, forward, i, ns_tag_at(~K, nodes, i))
938
939def 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>:
940  match node:
941    case Free{next}:
942      m
943    case N{c, l, r, p, old}:
944      write(~K, ~V, ~cmp, m, id, N{c, l, r, p, k})
945
946def recycle(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>:
947  TM{n, root, lo, hi, +free, nodes, payloads} = m
948  release_header(~K, ~V, ~cmp, write(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, id, Free{free}), id)
949
950def clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>:
951  TM{n, root, lo, hi, free, nodes, payloads} = m
952  TM{0n, 0n, 0n, 0n, 0n, ns_clear(~K, nodes), D.clear_at(~Maybe<&2, V>, payloads)}
953
954def 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>>:
955  (m, +id) = r
956  snap_at(~K, ~V, ~cmp, id, m)
957
958def 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>>:
959  match ok:
960    case True{}:
961      ns_rt(~K, limit, depth, cap, used, lefts, rights, parents, keys, U32.from_nat(i), Array.get(Nat, tags, U32.from_nat(i)))
962    case False{}:
963      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Fail{DE.IndexOutOfRange{}})
964
965def 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>:
966  (m3, +pn) = pair_result
967  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))
968
969def 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>:
970  (m3, +pn) = pair_result
971  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))
972
973def 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:
974  match fuel st:
975    case 0n Tuple{nodes, x}:
976      (nodes, Search{0n, p, on_left})
977    case 1n+f Tuple{nodes, Tuple{id, None{}}}:
978      (nodes, Search{0n, p, on_left})
979    case 1n+f Tuple{nodes, Tuple{+id, Some{LT{}}}}:
980      search_fast(~K, ~V, ~cmp, f, k, id, True{}, search_down(~K, ~V, ~cmp, nodes, id, True{}, k))
981    case 1n+f Tuple{nodes, Tuple{+id, Some{GT{}}}}:
982      search_fast(~K, ~V, ~cmp, f, k, id, False{}, search_down(~K, ~V, ~cmp, nodes, id, False{}, k))
983    case 1n+f Tuple{nodes, Tuple{+id, Some{EQ{}}}}:
984      (nodes, Search{id, p, on_left})
985
986def black_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>:
987  black_root_1(~K, ~V, ~cmp, root_id(~K, ~V, ~cmp, m))
988
989
990def 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>:
991  match r:
992    case Tuple{m, Free{next}}:
993      reuse_slot(~K, ~V, ~cmp, m, id, next, p, k, v)
994    case Tuple{m, N{c, l, r, q, oldk}}:
995      (m, Fail{Rejected{CapacityExceeded{}, k, v}})
996
997def ascend_slots_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, st: NodeStore<K> & Ascend) -> NodeStore<K> & Nat:
998  match fuel st:
999    case 0n Tuple{nodes, state}:
1000      (nodes, 0n)
1001    case 1n+f Tuple{nodes, Ascend{x, p, True{}}}:
1002      (nodes, p)
1003    case 1n+f Tuple{nodes, Ascend{+x, +p, False{}}}:
1004      ascend_slots_loop(~K, ~V, ~cmp, f, forward, ascend_at(~K, ~V, ~cmp, x, p, forward, nodes))
1005
1006def extreme_slots_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, +id: Nat, st: NodeStore<K> & Nat) -> NodeStore<K> & Nat:
1007  match fuel st:
1008    case 0n Tuple{nodes, next}:
1009      (nodes, id)
1010    case 1n+f Tuple{nodes, 0n}:
1011      (nodes, id)
1012    case 1n+f Tuple{nodes, 1n+ +j}:
1013      extreme_slots_loop(~K, ~V, ~cmp, f, forward, 1n+j, extreme_at(~K, ~V, ~cmp, forward, nodes, j))
1014
1015def 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>:
1016  (m1, +node) = pair_result
1017  set_key_node(~K, ~V, ~cmp, m1, id, k, node)
1018
1019def 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:
1020  match fuel st:
1021    case 0n Tuple{nodes, x}:
1022      (nodes, NavBest{best})
1023    case 1n+f Tuple{nodes, Tuple{id, None{}}}:
1024      (nodes, NavBest{best})
1025    case 1n+f Tuple{nodes, Tuple{+id, Some{LT{}}}}:
1026      nav_fast(~K, ~V, ~cmp, f, k, higher, pick(Nat, higher, id, best), search_down(~K, ~V, ~cmp, nodes, id, True{}, k))
1027    case 1n+f Tuple{nodes, Tuple{+id, Some{GT{}}}}:
1028      nav_fast(~K, ~V, ~cmp, f, k, higher, pick(Nat, higher, best, id), search_down(~K, ~V, ~cmp, nodes, id, False{}, k))
1029    case 1n+f Tuple{nodes, Tuple{+id, Some{EQ{}}}}:
1030      (nodes, NavEqual{id})
1031
1032def first_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
1033  entry_snapshot(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))
1034
1035def last_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
1036  entry_snapshot(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))
1037
1038def ns_get(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
1039  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
1040  ns_get_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))
1041
1042# ---- reading one field of a slot (0, the encoding of Free{0}, past the length) ----
1043
1044def search(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Search:
1045  TM{+n, +root, lo, hi, free, nodes, payloads} = m
1046  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)))
1047
1048def 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:
1049  match c:
1050    case 0n:
1051      ascend_slots_loop(~K, ~V, ~cmp, 1n+n, forward, (nodes, Ascend{id, p, False{}}))
1052    case 1n+ +j:
1053      extreme_slots_loop(~K, ~V, ~cmp, 1n+n, Bool.not(forward), 1n+j, extreme_at(~K, ~V, ~cmp, Bool.not(forward), nodes, j))
1054
1055def extreme_start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +n: Nat, +id: Nat, +forward: Bool) -> NodeStore<K> & Nat:
1056  match id:
1057    case 0n:
1058      (nodes, 0n)
1059    case 1n+ +j:
1060      extreme_slots_loop(~K, ~V, ~cmp, 1n+n, forward, 1n+j, extreme_at(~K, ~V, ~cmp, forward, nodes, j))
1061
1062def 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>>:
1063  match used:
1064    case 0n:
1065      (NS{limit, depth, cap, 0n, tags, lefts, rights, parents, keys}, Fail{DE.EmptyArray{}})
1066    case 1n+ +m:
1067      ns_pop_fin(~K, m, ns_get(~K, NS{limit, depth, cap, 1n+m, tags, lefts, rights, parents, keys}, m))
1068
1069def read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Node<K>:
1070  match m id:
1071    case mm 0n:
1072      (mm, Free{0n})
1073    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
1074      read_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, ns_get(~K, nodes, i))
1075
1076def get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
1077  get_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))
1078
1079def contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Bool:
1080  contains_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))
1081
1082
1083def extreme(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
1084  TM{+n, root, lo, hi, free, nodes, payloads} = m
1085  neighbor_slots_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, extreme_start(~K, ~V, ~cmp, nodes, n, id, forward))
1086
1087def 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:
1088  (TM{+n, root, lo, hi, free, nodes, payloads}, +node) = r
1089  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)))
1090
1091def 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>:
1092  replace_found(~K, ~V, ~cmp, v, search(~K, ~V, ~cmp, m, k))
1093
1094def 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>>:
1095  (nodes, +c) = r
1096  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)))
1097
1098def 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>:
1099  match k r:
1100    case None{} Tuple{m, removed}:
1101      (Cursor{m, 0n, 0n, lower, upper, forward}, removed)
1102    case Some{key} Tuple{m, removed}:
1103      iterator_relocated(~K, ~V, ~cmp, lower, upper, forward, removed, search(~K, ~V, ~cmp, m, key))
1104
1105def 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:
1106  replace_if_found(~K, ~V, ~cmp, ~eq, expected, replacement, search(~K, ~V, ~cmp, m, k))
1107
1108def ns_pop(~K: Data, s: NodeStore<K>) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
1109  NS{+limit, +depth, +cap, used, tags, lefts, rights, parents, keys} = s
1110  ns_pop_n(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys)
1111
1112def 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>:
1113  (m2, +yn) = pair_result
1114  rotate_left_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, node_parent(~K, xn)))
1115
1116def 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>:
1117  (m2, +yn) = pair_result
1118  rotate_right_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, node_parent(~K, xn)))
1119
1120def 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):
1121  probe_node(~K, ~V, ~cmp, id, k, read(~K, ~V, ~cmp, m, id))
1122
1123def 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:
1124  match fuel st:
1125    case 0n Tuple{m, state}:
1126      (m, 0n)
1127    case 1n+f Tuple{m, Ascend{x, p, True{}}}:
1128      (m, p)
1129    case 1n+f Tuple{m, Ascend{+x, +p, False{}}}:
1130      ascend_loop(~K, ~V, ~cmp, f, forward, ascend_step_node(~K, ~V, ~cmp, x, p, forward, read(~K, ~V, ~cmp, m, p)))
1131
1132def neighbor(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
1133  neighbor_node(~K, ~V, ~cmp, id, forward, read(~K, ~V, ~cmp, m, id))
1134
1135def set_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +k: K) -> TreeMap<K, V, cmp>:
1136  set_key_1(~K, ~V, ~cmp, id, k, read(~K, ~V, ~cmp, m, id))
1137
1138def refresh_ends_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +r: Nat, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
1139  (m2, +lo) = pair_result
1140  refresh_ends_3(~K, ~V, ~cmp, lo, extreme(~K, ~V, ~cmp, m2, r, True{}))
1141
1142def key_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
1143  (m, id) = r
1144  key_finish(~K, ~V, ~cmp, read(~K, ~V, ~cmp, m, id))
1145
1146def 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:
1147  default_value(~K, ~V, ~cmp, fallback, get(~K, ~V, ~cmp, m, k))
1148
1149
1150def 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>:
1151  match valid:
1152    case True{}:
1153      view_value(~K, ~V, ~cmp, lower, upper, descending, get(~K, ~V, ~cmp, m, k))
1154    case False{}:
1155      (View{m, lower, upper, descending}, None{})
1156
1157def 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>>:
1158  (nodes, +p) = r
1159  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))
1160
1161def iterator_has_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Bool:
1162  Cursor{m, +next, current, lower, upper, forward} = cursor
1163  iterator_has_checked(~K, ~V, ~cmp, next, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))
1164
1165def 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>:
1166  (m1, +xn) = pair_result
1167  rotate_left_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, node_right(~K, xn)))
1168
1169def 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>:
1170  (m1, +xn) = pair_result
1171  rotate_right_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, node_left(~K, xn)))
1172
1173def 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:
1174  match fuel st:
1175    case 0n Tuple{m, node}:
1176      (m, Search{0n, p, on_left})
1177    case 1n+f Tuple{m, Tuple{Free{next}, order}}:
1178      (m, Search{0n, p, on_left})
1179    case 1n+f Tuple{m, Tuple{N{c, +l, r, p0, key}, LT{}}}:
1180      search_loop(~K, ~V, ~cmp, f, k, l, id, True{}, probe(~K, ~V, ~cmp, m, l, k))
1181    case 1n+f Tuple{m, Tuple{N{c, l, +r, p0, key}, GT{}}}:
1182      search_loop(~K, ~V, ~cmp, f, k, r, id, False{}, probe(~K, ~V, ~cmp, m, r, k))
1183    case 1n+f Tuple{m, Tuple{N{c, l, r, p0, key}, EQ{}}}:
1184      (m, Search{id, p, on_left})
1185
1186def 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>:
1187  match r:
1188    case Tuple{payloads, Done{u}}:
1189      (TM{n, root, lo, hi, free, nodes, payloads}, Done{id})
1190    case Tuple{payloads, Fail{e}}:
1191      append_rollback(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, ns_pop(~K, nodes))
1192
1193def copy_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +target: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:
1194  match node:
1195    case Free{next}:
1196      m
1197    case N{c, l, r, p, k}:
1198      set_key(~K, ~V, ~cmp, m, target, k)
1199
1200def refresh_ends_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
1201  (m1, +r) = pair_result
1202  refresh_ends_2(~K, ~V, ~cmp, r, extreme(~K, ~V, ~cmp, m1, r, False{}))
1203
1204def 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:
1205  match inclusive:
1206    case True{}:
1207      (m, id)
1208    case False{}:
1209      neighbor(~K, ~V, ~cmp, m, id, higher)
1210
1211
1212def first_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
1213  key_id(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))
1214
1215def last_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
1216  key_id(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))
1217
1218def view_get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, V>:
1219  View{m, +lower, +upper, descending} = view
1220  view_get_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))
1221
1222def 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>>:
1223  match valid:
1224    case True{}:
1225      iter_link(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, i, lower, upper, forward, entry, ns_parent_at(~K, nodes, i))
1226    case False{}:
1227      (Cursor{TM{n, root, lo, hi, free, nodes, payloads}, 0n, current, lower, upper, forward}, None{})
1228
1229def rotate_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat) -> TreeMap<K, V, cmp>:
1230  rotate_left_1(~K, ~V, ~cmp, x, read(~K, ~V, ~cmp, m, x))
1231
1232def rotate_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat) -> TreeMap<K, V, cmp>:
1233  rotate_right_1(~K, ~V, ~cmp, x, read(~K, ~V, ~cmp, m, x))
1234
1235def 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>:
1236  match r:
1237    case Tuple{nodes, Done{u}}:
1238      append_values(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, k, v, id, D.push_at(~Maybe<&2, V>, payloads, Some{v}))
1239    case Tuple{nodes, Fail{e}}:
1240      (TM{n, root, lo, hi, free, nodes, payloads}, Fail{Rejected{CapacityExceeded{}, k, v}})
1241
1242def 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:
1243  (m2, value) = pair_result
1244  move_successor_3(~K, ~V, ~cmp, source, exchange(~K, ~V, ~cmp, copy_key(~K, ~V, ~cmp, m2, target, source_node), target, value))
1245
1246def refresh_ends(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>:
1247  refresh_ends_1(~K, ~V, ~cmp, root_id(~K, ~V, ~cmp, m))
1248
1249def 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:
1250  match fuel st:
1251    case 0n Tuple{m, node}:
1252      (m, best)
1253    case 1n+f Tuple{m, Tuple{Free{next}, order}}:
1254      (m, best)
1255    case 1n+f Tuple{m, Tuple{N{c, +l, r, p, key}, LT{}}}:
1256      nav_loop(~K, ~V, ~cmp, f, k, higher, inclusive, l, pick(Nat, higher, id, best), probe(~K, ~V, ~cmp, m, l, k))
1257    case 1n+f Tuple{m, Tuple{N{c, l, +r, p, key}, GT{}}}:
1258      nav_loop(~K, ~V, ~cmp, f, k, higher, inclusive, r, pick(Nat, higher, best, id), probe(~K, ~V, ~cmp, m, r, k))
1259    case 1n+f Tuple{m, Tuple{node, EQ{}}}:
1260      nav_equal(~K, ~V, ~cmp, m, id, higher, inclusive)
1261
1262def 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:
1263  match r:
1264    case Tuple{nodes, NavBest{b}}:
1265      (TM{n, root, lo, hi, free, nodes, payloads}, b)
1266    case Tuple{nodes, NavEqual{+id}}:
1267      nav_equal(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, id, higher, inclusive)
1268
1269def 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>>:
1270  match mk mv:
1271    case Some{+key} Some{v}:
1272      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))
1273    case _ _:
1274      (Cursor{TM{n, root, lo, hi, free, nodes, payloads}, 0n, current, lower, upper, forward}, None{})
1275
1276def view_contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Bool:
1277  view_contains_value(~K, ~V, ~cmp, view_get(~K, ~V, ~cmp, view, k))
1278
1279def 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:
1280  match triangle:
1281    case True{}:
1282      (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{}})
1283    case False{}:
1284      (rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), g, True{}), g), Fix{0n, False{}})
1285
1286def 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:
1287  match triangle:
1288    case True{}:
1289      (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{}})
1290    case False{}:
1291      (rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), g, True{}), g), Fix{0n, False{}})
1292
1293def 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>:
1294  (nodes, +used) = r
1295  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}))
1296
1297def 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:
1298  (m1, +source_node) = pair_result
1299  move_successor_2(~K, ~V, ~cmp, target, source, source_node, exchange(~K, ~V, ~cmp, m1, source, None{}))
1300
1301def 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:
1302  (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{}})
1303
1304def 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:
1305  (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{}})
1306
1307def 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:
1308  TM{+n, +root, lo, hi, free, nodes, payloads} = m
1309  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)))
1310
1311def 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>>:
1312  (nodes, mk) = r
1313  iter_kv(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, nodes, i, current, lower, upper, forward, mk, mv)
1314
1315def 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:
1316  match uncle:
1317    case N{True{}, l, r, gp, k}:
1318      (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{}})
1319    case _:
1320      insert_black_left(~K, ~V, ~cmp, m, z, p, g, triangle)
1321
1322def 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:
1323  match uncle:
1324    case N{True{}, l, r, gp, k}:
1325      (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{}})
1326    case _:
1327      insert_black_right(~K, ~V, ~cmp, m, z, p, g, triangle)
1328
1329def 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>:
1330  TM{n, root, lo, hi, free, nodes, payloads} = m
1331  append_count(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, p, ns_length(~K, nodes))
1332
1333def move_successor(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +target: Nat, +source: Nat) -> TreeMap<K, V, cmp> & Nat:
1334  move_successor_1(~K, ~V, ~cmp, target, source, read(~K, ~V, ~cmp, m, source))
1335
1336def 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:
1337  (m2, +wn) = pair_result
1338  delete_borrow_left(~K, ~V, ~cmp, m2, p, node_right(~K, pn), pn, wn)
1339
1340def 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:
1341  (m2, +wn) = pair_result
1342  delete_borrow_right(~K, ~V, ~cmp, m2, p, node_left(~K, pn), pn, wn)
1343
1344def lower_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
1345  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, False{}))
1346
1347def floor_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
1348  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, True{}))
1349
1350def ceiling_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
1351  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, True{}))
1352
1353def higher_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
1354  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, False{}))
1355
1356def 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>>:
1357  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, False{}))
1358
1359def 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>>:
1360  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, True{}))
1361
1362def 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>>:
1363  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, True{}))
1364
1365def 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>>:
1366  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, False{}))
1367
1368def 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:
1369  match bound:
1370    case Unbounded{}:
1371      range_unbounded(~K, ~V, ~cmp, m, forward)
1372    case Inclusive{k}:
1373      navigate(~K, ~V, ~cmp, m, k, forward, True{})
1374    case Exclusive{k}:
1375      navigate(~K, ~V, ~cmp, m, k, forward, False{})
1376
1377def 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>>:
1378  (TM{+n, +root, +lo, +hi, +free, nodes, payloads}, mv) = r
1379  iter_key(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, i, current, lower, upper, forward, mv, ns_key_at(~K, nodes, i))
1380
1381def 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:
1382  (m1, +un) = pair_result
1383  insert_uncle_left(~K, ~V, ~cmp, m1, z, p, g, node_right(~K, gn), Nat.is_eq(z, node_right(~K, pn)), un)
1384
1385def 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:
1386  (m1, +un) = pair_result
1387  insert_uncle_right(~K, ~V, ~cmp, m1, z, p, g, node_left(~K, gn), Nat.is_eq(z, node_left(~K, pn)), un)
1388
1389def 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>:
1390  TM{n, root, lo, hi, free, nodes, payloads} = m
1391  match free:
1392    case 0n:
1393      append(~K, ~V, ~cmp, TM{n, root, lo, hi, 0n, nodes, payloads}, k, v, p)
1394    case 1n+ +f:
1395      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))
1396
1397def successor_ready(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Nat:
1398  (m, source) = r
1399  move_successor(~K, ~V, ~cmp, m, target, source)
1400
1401def 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:
1402  (m1, +pn) = pair_result
1403  delete_borrow_read_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_right(~K, pn)))
1404
1405def 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:
1406  (m1, +pn) = pair_result
1407  delete_borrow_read_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_left(~K, pn)))
1408
1409def view_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> Cursor<K, V, cmp>:
1410  View{m, +lower, +upper, +descending} = view
1411  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)))
1412
1413def 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>>:
1414  match next:
1415    case 0n:
1416      (Cursor{m, 0n, current, lower, upper, forward}, None{})
1417    case 1n+ +i:
1418      iter_value(~K, ~V, ~cmp, i, current, lower, upper, forward, get_id(~K, ~V, ~cmp, m, 1n+i))
1419
1420def 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:
1421  match within:
1422    case True{}:
1423      navigate(~K, ~V, ~cmp, m, k, higher, inclusive)
1424    case False{}:
1425      range_start(~K, ~V, ~cmp, m, pick(Bound<K>, higher, lower, upper), higher)
1426
1427def 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>>:
1428  View{m, +lower, +upper, +descending} = view
1429  +up = pick(Bool, descending, Bool.not(first), first)
1430  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)))
1431
1432def 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:
1433  insert_side_left_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, node_right(~K, gn)))
1434
1435def 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:
1436  insert_side_right_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, node_left(~K, gn)))
1437
1438def delete_target(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Nat:
1439  match r:
1440    case Tuple{m, N{c, 1n+l, 1n+r, p, k}}:
1441      successor_ready(~K, ~V, ~cmp, id, extreme(~K, ~V, ~cmp, m, 1n+r, False{}))
1442    case Tuple{m, node}:
1443      (m, id)
1444
1445
1446def delete_borrow_read_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
1447  delete_borrow_read_left_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1448
1449def delete_borrow_read_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
1450  delete_borrow_read_right_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1451
1452def iterator_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
1453  Cursor{m, +next, current, lower, upper, forward} = cursor
1454  iter_at(~K, ~V, ~cmp, next, current, lower, upper, forward, m)
1455
1456def 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>>:
1457  View{m, +lower, +upper, +descending} = view
1458  +up = pick(Bool, descending, Bool.not(higher), higher)
1459  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)))))
1460
1461def 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>>:
1462  view_extreme(~K, ~V, ~cmp, view, True{})
1463
1464def 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>>:
1465  view_extreme(~K, ~V, ~cmp, view, False{})
1466
1467def 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:
1468  match on_left:
1469    case True{}:
1470      insert_side_left(~K, ~V, ~cmp, m, z, p, g, pn, gn)
1471    case False{}:
1472      insert_side_right(~K, ~V, ~cmp, m, z, p, g, pn, gn)
1473
1474def 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:
1475  match far_red:
1476    case True{}:
1477      delete_borrow_left(~K, ~V, ~cmp, m, p, w, pn, wn)
1478    case False{}:
1479      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)
1480
1481def 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:
1482  match far_red:
1483    case True{}:
1484      delete_borrow_right(~K, ~V, ~cmp, m, p, w, pn, wn)
1485    case False{}:
1486      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)
1487
1488def iterator_next_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, K>:
1489  iterator_key_result(~K, ~V, ~cmp, iterator_next(~K, ~V, ~cmp, cursor))
1490
1491def iterator_next_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, V>:
1492  iterator_value_result(~K, ~V, ~cmp, iterator_next(~K, ~V, ~cmp, cursor))
1493
1494def 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:
1495  match fuel found st:
1496    case _ True{} Tuple{cursor, item}:
1497      (iterator_finish(~K, ~V, ~cmp, cursor), True{})
1498    case 0n False{} Tuple{cursor, item}:
1499      (iterator_finish(~K, ~V, ~cmp, cursor), False{})
1500    case 1n+f False{} Tuple{cursor, None{}}:
1501      (iterator_finish(~K, ~V, ~cmp, cursor), False{})
1502    case 1n+f False{} Tuple{cursor, Some{Entry{k, v}}}:
1503      contains_value_loop(~K, ~V, ~cmp, ~eq, f, wanted, eq(v, wanted), iterator_next(~K, ~V, ~cmp, cursor))
1504
1505def 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>>:
1506  view_nav(~K, ~V, ~cmp, view, k, False{}, False{})
1507
1508def 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>>:
1509  view_nav(~K, ~V, ~cmp, view, k, False{}, True{})
1510
1511def 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>>:
1512  view_nav(~K, ~V, ~cmp, view, k, True{}, True{})
1513
1514def 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>>:
1515  view_nav(~K, ~V, ~cmp, view, k, True{}, False{})
1516
1517def 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:
1518  match fuel st:
1519    case 0n Tuple{cursor, item}:
1520      (iterator_view(~K, ~V, ~cmp, cursor), count)
1521    case 1n+f Tuple{cursor, None{}}:
1522      (iterator_view(~K, ~V, ~cmp, cursor), count)
1523    case 1n+f Tuple{cursor, Some{item}}:
1524      view_count_loop(~K, ~V, ~cmp, f, 1n+count, iterator_next(~K, ~V, ~cmp, cursor))
1525
1526def 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>>:
1527  (cursor, removed) = r
1528  iterator_next(~K, ~V, ~cmp, cursor)
1529
1530def 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:
1531  (m1, +gn) = pair_result
1532  insert_side(~K, ~V, ~cmp, m1, z, p, node_parent(~K, pn), pn, gn, Nat.is_eq(p, node_left(~K, gn)))
1533
1534def 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:
1535  match near_red far_red:
1536    case False{} False{}:
1537      (set_red(~K, ~V, ~cmp, m, w, True{}), DF{p, node_parent(~K, pn), True{}})
1538    case _ _:
1539      delete_far_left(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)
1540
1541def 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:
1542  match near_red far_red:
1543    case False{} False{}:
1544      (set_red(~K, ~V, ~cmp, m, w, True{}), DF{p, node_parent(~K, pn), True{}})
1545    case _ _:
1546      delete_far_right(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)
1547
1548def 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:
1549  (m, n) = r
1550  contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+n, wanted, False{}, iterator_next(~K, ~V, ~cmp, iterator(~K, ~V, ~cmp, m)))
1551
1552def view_size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp> & Nat:
1553  View{TM{+n, root, lo, hi, free, nodes, payloads}, lower, upper, descending} = view
1554  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})))
1555
1556def 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:
1557  insert_grand_1(~K, ~V, ~cmp, z, p, pn, read(~K, ~V, ~cmp, m, node_parent(~K, pn)))
1558
1559def 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:
1560  (m4, +far_node) = pair_result
1561  delete_children_left(~K, ~V, ~cmp, m4, p, node_right(~K, pn), pn, wn, node_red(~K, near_node), node_red(~K, far_node))
1562
1563def 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:
1564  (m4, +far_node) = pair_result
1565  delete_children_right(~K, ~V, ~cmp, m4, p, node_left(~K, pn), pn, wn, node_red(~K, near_node), node_red(~K, far_node))
1566
1567def 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:
1568  contains_value_start(~K, ~V, ~cmp, ~eq, wanted, size(~K, ~V, ~cmp, m))
1569
1570def 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:
1571  match is_red:
1572    case False{}:
1573      (m, Fix{0n, False{}})
1574    case True{}:
1575      insert_grand(~K, ~V, ~cmp, m, z, p, pn)
1576
1577def 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:
1578  (m3, +near_node) = pair_result
1579  delete_sibling_left_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, node_right(~K, wn)))
1580
1581def 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:
1582  (m3, +near_node) = pair_result
1583  delete_sibling_right_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, node_left(~K, wn)))
1584
1585def 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:
1586  (m2, +pn) = pair_result
1587  insert_parent(~K, ~V, ~cmp, m2, z, node_parent(~K, zn), pn, node_red(~K, pn))
1588
1589def 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:
1590  (m2, +wn) = pair_result
1591  delete_sibling_left_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, node_left(~K, wn)))
1592
1593def 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:
1594  (m2, +wn) = pair_result
1595  delete_sibling_right_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, node_right(~K, wn)))
1596
1597def 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:
1598  (m1, +zn) = pair_result
1599  insert_fix_step_2(~K, ~V, ~cmp, z, zn, read(~K, ~V, ~cmp, m1, node_parent(~K, zn)))
1600
1601def 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:
1602  (m1, +pn) = pair_result
1603  delete_sibling_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_right(~K, pn)))
1604
1605def 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:
1606  (m1, +pn) = pair_result
1607  delete_sibling_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_left(~K, pn)))
1608
1609def insert_fix_step(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat) -> TreeMap<K, V, cmp> & Fix:
1610  insert_fix_step_1(~K, ~V, ~cmp, z, read(~K, ~V, ~cmp, m, z))
1611
1612def delete_sibling_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
1613  delete_sibling_left_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1614
1615def delete_sibling_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
1616  delete_sibling_right_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1617
1618def insert_fix_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: TreeMap<K, V, cmp> & Fix) -> TreeMap<K, V, cmp>:
1619  match fuel st:
1620    case 0n Tuple{m, f}:
1621      black_root(~K, ~V, ~cmp, m)
1622    case 1n+p Tuple{m, Fix{z, False{}}}:
1623      black_root(~K, ~V, ~cmp, m)
1624    case 1n+p Tuple{m, Fix{z, True{}}}:
1625      insert_fix_loop(~K, ~V, ~cmp, p, insert_fix_step(~K, ~V, ~cmp, m, z))
1626
1627def 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:
1628  match red_sibling:
1629    case True{}:
1630      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)
1631    case False{}:
1632      delete_sibling_left(~K, ~V, ~cmp, m, p)
1633
1634def 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:
1635  match red_sibling:
1636    case True{}:
1637      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)
1638    case False{}:
1639      delete_sibling_right(~K, ~V, ~cmp, m, p)
1640
1641def insert_fixed(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
1642  (m, n) = r
1643  insert_fix_loop(~K, ~V, ~cmp, 1n+n, (m, Fix{id, True{}}))
1644
1645def 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:
1646  (m1, +wn) = pair_result
1647  delete_red_sibling_left(~K, ~V, ~cmp, m1, p, node_right(~K, pn), node_red(~K, wn))
1648
1649def 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:
1650  (m1, +wn) = pair_result
1651  delete_red_sibling_right(~K, ~V, ~cmp, m1, p, node_left(~K, pn), node_red(~K, wn))
1652
1653def 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>>:
1654  match r:
1655    case Tuple{m, Done{+id}}:
1656      (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{}})
1657    case Tuple{m, Fail{e}}:
1658      (m, Fail{e})
1659
1660def 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:
1661  delete_side_left_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, node_right(~K, pn)))
1662
1663def 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:
1664  delete_side_right_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, node_left(~K, pn)))
1665
1666def 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>>:
1667  match r:
1668    case Tuple{m, Search{0n, +p, +on_left}}:
1669      put_allocated(~K, ~V, ~cmp, p, on_left, allocate(~K, ~V, ~cmp, m, p, k, v))
1670    case Tuple{m, Search{1n+i, p, on_left}}:
1671      put_replaced(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, m, 1n+i, Some{v}))
1672
1673def 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:
1674  match on_left:
1675    case True{}:
1676      delete_side_left(~K, ~V, ~cmp, m, p, pn)
1677    case False{}:
1678      delete_side_right(~K, ~V, ~cmp, m, p, pn)
1679
1680def 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>>:
1681  match r:
1682    case Tuple{m, Search{0n, +p, +on_left}}:
1683      put_allocated(~K, ~V, ~cmp, p, on_left, allocate(~K, ~V, ~cmp, m, p, k, v))
1684    case Tuple{m, Search{1n+i, p, on_left}}:
1685      put_replaced(~K, ~V, ~cmp, get_id(~K, ~V, ~cmp, m, 1n+i))
1686
1687def 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>>:
1688  put_found(~K, ~V, ~cmp, k, v, search(~K, ~V, ~cmp, m, k))
1689
1690def 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:
1691  match stop:
1692    case True{}:
1693      (set_red(~K, ~V, ~cmp, m, x, False{}), DF{0n, 0n, False{}})
1694    case False{}:
1695      delete_side(~K, ~V, ~cmp, m, x, p, pn, Nat.is_eq(x, node_left(~K, pn)))
1696
1697def 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>>:
1698  put_absent_found(~K, ~V, ~cmp, k, v, search(~K, ~V, ~cmp, m, k))
1699
1700def 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:
1701  (m3, +pn) = pair_result
1702  delete_stop(~K, ~V, ~cmp, m3, x, p, pn, Bool.or(Nat.is_eq(x, root_node), node_red(~K, xn)))
1703
1704def 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>>:
1705  match valid:
1706    case True{}:
1707      view_put_finish(~K, ~V, ~cmp, lower, upper, descending, put(~K, ~V, ~cmp, m, k, v))
1708    case False{}:
1709      (View{m, lower, upper, descending}, Fail{Rejected{OutOfRange{}, k, v}})
1710
1711def 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:
1712  (m2, +xn) = pair_result
1713  delete_fix_step_3(~K, ~V, ~cmp, x, p, root_node, xn, read(~K, ~V, ~cmp, m2, p))
1714
1715def 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>>:
1716  View{m, +lower, +upper, descending} = view
1717  view_put_checked(~K, ~V, ~cmp, m, k, v, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))
1718
1719def 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:
1720  (m1, +root_node) = pair_result
1721  delete_fix_step_2(~K, ~V, ~cmp, x, p, root_node, read(~K, ~V, ~cmp, m1, x))
1722
1723def 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:
1724  delete_fix_step_1(~K, ~V, ~cmp, x, p, root_id(~K, ~V, ~cmp, m))
1725
1726def delete_fix_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: TreeMap<K, V, cmp> & DeleteFix) -> TreeMap<K, V, cmp>:
1727  match fuel st:
1728    case 0n Tuple{m, fix}:
1729      black_root(~K, ~V, ~cmp, m)
1730    case 1n+f Tuple{m, DF{x, p, False{}}}:
1731      black_root(~K, ~V, ~cmp, m)
1732    case 1n+f Tuple{m, DF{x, p, True{}}}:
1733      delete_fix_loop(~K, ~V, ~cmp, f, delete_fix_step(~K, ~V, ~cmp, m, x, p))
1734
1735def 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>:
1736  TM{+n, root, lo, hi, free, nodes, payloads} = m
1737  delete_fix_loop(~K, ~V, ~cmp, 1n+n, (TM{n, root, lo, hi, free, nodes, payloads}, DF{x, p, Bool.not(was_red)}))
1738
1739def 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>:
1740  (m2, +pn) = pair_result
1741  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))
1742
1743def unlink_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
1744  (m1, +node) = pair_result
1745  unlink_2(~K, ~V, ~cmp, id, node, read(~K, ~V, ~cmp, m1, node_parent(~K, node)))
1746
1747def unlink(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>:
1748  unlink_1(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))
1749
1750def unlink_target(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
1751  (m, id) = r
1752  refresh_ends(~K, ~V, ~cmp, unlink(~K, ~V, ~cmp, m, id))
1753
1754def 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>:
1755  (m1, value) = pair_result
1756  (unlink_target(~K, ~V, ~cmp, delete_target(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m1, id))), value)
1757
1758def remove_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
1759  remove_present_1(~K, ~V, ~cmp, id, exchange(~K, ~V, ~cmp, m, id, None{}))
1760
1761def remove_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
1762  match id:
1763    case 0n:
1764      (m, None{})
1765    case 1n+i:
1766      remove_present(~K, ~V, ~cmp, m, 1n+i)
1767
1768def remove_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
1769  (m, Search{id, p, on_left}) = r
1770  remove_id(~K, ~V, ~cmp, m, id)
1771
1772def 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>>:
1773  (m1, +node) = pair_result
1774  entry_value(~K, ~V, ~cmp, node_key(~K, node), remove_id(~K, ~V, ~cmp, m1, id))
1775
1776def 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>:
1777  (m1, +node) = pair_result
1778  iterator_reseek(~K, ~V, ~cmp, node_key(~K, node), lower, upper, forward, remove_id(~K, ~V, ~cmp, m1, current))
1779
1780def 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:
1781  match equal:
1782    case False{}:
1783      (m, False{})
1784    case True{}:
1785      changed_value(~K, ~V, ~cmp, remove_id(~K, ~V, ~cmp, m, id))
1786
1787def remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
1788  remove_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))
1789
1790def 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>>:
1791  remove_entry_id_1(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))
1792
1793def 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>:
1794  iterator_delete_1(~K, ~V, ~cmp, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))
1795
1796def 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:
1797  match r:
1798    case Tuple{m, None{}}:
1799      (m, False{})
1800    case Tuple{m, Some{old}}:
1801      remove_if_apply(~K, ~V, ~cmp, m, id, replacement, eq(old, expected))
1802
1803def 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>>:
1804  (m, id) = r
1805  remove_entry_id(~K, ~V, ~cmp, m, id)
1806
1807def 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>:
1808  match valid:
1809    case True{}:
1810      view_value(~K, ~V, ~cmp, lower, upper, descending, remove(~K, ~V, ~cmp, m, k))
1811    case False{}:
1812      (View{m, lower, upper, descending}, None{})
1813
1814def iterator_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, V>:
1815  Cursor{m, next, current, lower, upper, forward} = cursor
1816  iterator_delete(~K, ~V, ~cmp, m, next, current, lower, upper, forward)
1817
1818def 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:
1819  (m, Search{+id, p, on_left}) = r
1820  remove_if_value(~K, ~V, ~cmp, ~eq, id, expected, replacement, get_id(~K, ~V, ~cmp, m, id))
1821
1822def 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>>:
1823  poll_ready(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))
1824
1825def 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>>:
1826  poll_ready(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))
1827
1828def view_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, V>:
1829  View{m, +lower, +upper, descending} = view
1830  view_remove_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))
1831
1832def 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:
1833  remove_if_found(~K, ~V, ~cmp, ~eq, expected, expected, search(~K, ~V, ~cmp, m, k))
1834
1835def 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>:
1836  match fuel st:
1837    case 0n Tuple{cursor, item}:
1838      iterator_view(~K, ~V, ~cmp, cursor)
1839    case 1n+f Tuple{cursor, None{}}:
1840      iterator_view(~K, ~V, ~cmp, cursor)
1841    case 1n+f Tuple{cursor, Some{item}}:
1842      view_clear_loop(~K, ~V, ~cmp, f, view_clear_next(~K, ~V, ~cmp, iterator_remove(~K, ~V, ~cmp, cursor)))
1843
1844def view_clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp>:
1845  View{TM{+n, root, lo, hi, free, nodes, payloads}, lower, upper, descending} = view
1846  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})))