src/containers/balanced_search_tree.bend
0x9ee2e9a299991dcc089fe22c7f3ceb5f · 1,424 lines · 0 definitions
1# Generated by tools/generators/tree_map.py; edit algorithm definitions there.
2import Base
3import 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/dynamic_array.bend as D
4import 0x9ee2e9a299991dcc089fe22c7f3ceb5f/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
13type TreeMap<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
14 TM{size: Nat, root: Nat, first: Nat, last: Nat, free: Nat,
15 nodes: D.DynArray<&2, Node<K>>, payloads: D.DynArray<&2, Maybe<&2, V>>}
16
17type Entry<-K: Data, -V: Data> is Data:
18 Entry{key: K, value: V}
19
20type Error is Data:
21 CapacityExceeded{}
22 OutOfRange{}
23 NoCurrent{}
24 InvalidBounds{}
25
26type Rejected<-K: Data, -V: Data> is Data:
27 Rejected{error: Error, key: K, value: V}
28
29type Search is Data:
30 Search{found: Nat, parent: Nat, left: Bool}
31
32type Fix is Data:
33 Fix{node: Nat, more: Bool}
34
35type Ascend is Data:
36 Ascend{child: Nat, parent: Nat, done: Bool}
37
38# A direct branch preserves scalar traversal state in native code. Passing
39# these records through pick(-T: Type) erases their layout and boxes both arms.
40type DeleteFix is Data:
41 DF{node: Nat, parent: Nat, more: Bool}
42
43type Bound<-K: Data> is Data:
44 Unbounded{}
45 Inclusive{key: K}
46 Exclusive{key: K}
47
48type View<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
49 View{map: TreeMap<K, V, cmp>, lower: Bound<K>, upper: Bound<K>, descending: Bool}
50
51type InvalidView<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
52 InvalidView{map: TreeMap<K, V, cmp>, error: Error}
53
54type Cursor<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
55 Cursor{map: TreeMap<K, V, cmp>, next: Nat, current: Nat,
56 lower: Bound<K>, upper: Bound<K>, forward: Bool}
57
58def pick(-T: Type, b: Bool, yes: T, no: T) -> T:
59 match b:
60 case True{}:
61 yes
62 case False{}:
63 no
64
65def node_red(~K: Data, n: Node<K>) -> Bool:
66 match n:
67 case Free{x}:
68 False{}
69 case N{c, l, r, p, k}:
70 c
71
72def node_left(~K: Data, n: Node<K>) -> Nat:
73 match n:
74 case Free{x}:
75 0n
76 case N{c, l, r, p, k}:
77 l
78
79def node_right(~K: Data, n: Node<K>) -> Nat:
80 match n:
81 case Free{x}:
82 0n
83 case N{c, l, r, p, k}:
84 r
85
86def node_parent(~K: Data, n: Node<K>) -> Nat:
87 match n:
88 case Free{x}:
89 0n
90 case N{c, l, r, p, k}:
91 p
92
93def node_key(~K: Data, n: Node<K>) -> Maybe<&2, K>:
94 match n:
95 case Free{x}:
96 None{}
97 case N{c, l, r, p, k}:
98 Some{k}
99
100def new(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp) -> TreeMap<K, V, cmp>:
101 TM{0n, 0n, 0n, 0n, 0n, D.new_at(~Node<K>), D.new_at(~Maybe<&2, V>)}
102
103def size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
104 TM{+n, root, lo, hi, free, nodes, payloads} = m
105 (TM{n, root, lo, hi, free, nodes, payloads}, n)
106
107def root_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
108 TM{n, +root, lo, hi, free, nodes, payloads} = m
109 (TM{n, root, lo, hi, free, nodes, payloads}, root)
110
111def first_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
112 TM{n, root, +lo, hi, free, nodes, payloads} = m
113 (TM{n, root, lo, hi, free, nodes, payloads}, lo)
114
115def last_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
116 TM{n, root, lo, +hi, free, nodes, payloads} = m
117 (TM{n, root, lo, hi, free, nodes, payloads}, hi)
118
119def 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: D.DynArray<&2, Node<K>> & Result<&2, &2, DE.Error, Node<K>>) -> TreeMap<K, V, cmp> & Node<K>:
120 match r:
121 case Tuple{nodes, Done{x}}:
122 (TM{n, root, lo, hi, free, nodes, payloads}, x)
123 case Tuple{nodes, Fail{e}}:
124 (TM{n, root, lo, hi, free, nodes, payloads}, Free{0n})
125
126def 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: D.DynArray<&2, Node<K>> & Result<&2, &2, DE.Error, Unit>) -> TreeMap<K, V, cmp>:
127 (nodes, status) = r
128 TM{n, root, lo, hi, free, nodes, payloads}
129
130def set_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +root: Nat) -> TreeMap<K, V, cmp>:
131 TM{n, old, lo, hi, free, nodes, payloads} = m
132 TM{n, root, lo, hi, free, nodes, payloads}
133
134def 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):
135 match r:
136 case Tuple{m, Free{next}}:
137 (m, (Free{next}, EQ{}))
138 case Tuple{m, N{c, l, r, p, +key}}:
139 (m, (N{c, l, r, p, key}, cmp(k, key)))
140
141def exchange_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: D.DynArray<&2, Node<K>>, r: D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
142 match r:
143 case Tuple{payloads, Done{old}}:
144 (TM{n, root, lo, hi, free, nodes, payloads}, old)
145 case Tuple{payloads, Fail{e}}:
146 (TM{n, root, lo, hi, free, nodes, payloads}, None{})
147
148def 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: D.DynArray<&2, Node<K>> & Result<&2, &2, DE.Error, Node<K>>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
149 (nodes, dropped) = r
150 (TM{n, root, lo, hi, free, nodes, payloads}, Fail{Rejected{CapacityExceeded{}, k, v}})
151
152def free_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +free: Nat) -> TreeMap<K, V, cmp>:
153 TM{n, root, lo, hi, old, nodes, payloads} = m
154 TM{n, root, lo, hi, free, nodes, payloads}
155
156def 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>:
157 (m1, old) = pair_result
158 (m1, Done{id})
159
160def 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>>:
161 (m, old) = r
162 (m, Done{old})
163
164def get_id_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: D.DynArray<&2, Node<K>>, r: D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
165 match r:
166 case Tuple{payloads, Done{x}}:
167 (TM{n, root, lo, hi, free, nodes, payloads}, x)
168 case Tuple{payloads, Fail{e}}:
169 (TM{n, root, lo, hi, free, nodes, payloads}, None{})
170
171def contains_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Bool:
172 (m, Search{id, p, left}) = r
173 (m, Nat.is_lt(0n, id))
174
175def ascend_choice(x: Nat, p: Nat, q: Nat, found: Bool) -> Ascend:
176 match found:
177 case True{}:
178 Ascend{0n, p, True{}}
179 case False{}:
180 Ascend{x, q, False{}}
181
182def node_slot_done(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: Array<Maybe<&2, Node<K>>> & Maybe<&2, Node<K>>) -> Array<Maybe<&2, Node<K>>> & Node<K>:
183 match r:
184 case Tuple{nodes, None{}}:
185 (nodes, Free{0n})
186 case Tuple{nodes, Some{node}}:
187 (nodes, node)
188
189def neighbor_slots_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: Array<Maybe<&2, Node<K>>> & Nat) -> TreeMap<K, V, cmp> & Nat:
190 (nodes, id) = r
191 (TM{n, root, lo, hi, free, D.DA{limit, depth, cap, used, nodes}, payloads}, id)
192
193def 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:
194 (m3, old) = pair_result
195 (m3, source)
196
197def release_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>:
198 TM{n, root, lo, hi, free, nodes, payloads} = m
199 TM{Nat.sub(n, 1n), root, lo, hi, id, nodes, payloads}
200
201def set_ends(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +lo: Nat, +hi: Nat) -> TreeMap<K, V, cmp>:
202 TM{n, root, oldlo, oldhi, free, nodes, payloads} = m
203 TM{n, root, lo, hi, free, nodes, payloads}
204
205def clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>:
206 TM{n, root, lo, hi, free, nodes, payloads} = m
207 TM{0n, 0n, 0n, 0n, 0n, D.clear_at(~Node<K>, nodes), D.clear_at(~Maybe<&2, V>, payloads)}
208
209def is_empty_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Bool:
210 (m1, +n) = pair_result
211 (m1, Nat.is_eq(n, 0n))
212
213def 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>>:
214 match k r:
215 case Some{key} Tuple{m, Some{v}}:
216 (m, Some{Entry{key, v}})
217 case _ Tuple{m, value}:
218 (m, None{})
219
220def with_limit(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +limit: Nat) -> TreeMap<K, V, cmp>:
221 TM{0n, 0n, 0n, 0n, 0n, D.with_limit_at(~Node<K>, limit), D.with_limit_at(~Maybe<&2, V>, limit)}
222
223def 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:
224 match r:
225 case Tuple{m, None{}}:
226 (m, fallback)
227 case Tuple{m, Some{v}}:
228 (m, v)
229
230def ordering_ok(order: Cmp, inclusive: Bool) -> Bool:
231 match order:
232 case LT{}:
233 True{}
234 case EQ{}:
235 inclusive
236 case GT{}:
237 False{}
238
239def 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>>:
240 match valid:
241 case True{}:
242 Done{View{m, lower, upper, descending}}
243 case False{}:
244 Fail{InvalidView{m, InvalidBounds{}}}
245
246def head_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, upper: Bound<K>) -> View<K, V, cmp>:
247 View{m, Unbounded{}, upper, False{}}
248
249def tail_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, lower: Bound<K>) -> View<K, V, cmp>:
250 View{m, lower, Unbounded{}, False{}}
251
252def descending_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> View<K, V, cmp>:
253 View{m, Unbounded{}, Unbounded{}, True{}}
254
255def view_reverse(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp>:
256 View{m, lower, upper, descending} = view
257 View{m, lower, upper, Bool.not(descending)}
258
259def view_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> TreeMap<K, V, cmp>:
260 View{m, lower, upper, descending} = view
261 m
262
263def 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>:
264 (m, v) = r
265 (View{m, lower, upper, descending}, v)
266
267def 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>>:
268 (m, status) = r
269 (View{m, lower, upper, descending}, status)
270
271def 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>:
272 (m, id) = r
273 Cursor{m, id, 0n, lower, upper, forward}
274
275def iterator_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> TreeMap<K, V, cmp>:
276 Cursor{m, next, current, lower, upper, forward} = cursor
277 m
278
279def iterator_view(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> View<K, V, cmp>:
280 Cursor{m, next, current, lower, upper, forward} = cursor
281 View{m, lower, upper, Bool.not(forward)}
282
283def 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>>:
284 (m, next) = r
285 (Cursor{m, next, id, lower, upper, forward}, Some{entry})
286
287def 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>:
288 match r:
289 case Tuple{m, Some{old}}:
290 (Cursor{m, next, current, lower, upper, forward}, Done{old})
291 case Tuple{m, None{}}:
292 (Cursor{m, next, current, lower, upper, forward}, Fail{NoCurrent{}})
293
294def 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>:
295 (m, Search{id, p, on_left}) = r
296 (Cursor{m, id, 0n, lower, upper, forward}, removed)
297
298def 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>:
299 match r:
300 case Tuple{cursor, None{}}:
301 (cursor, None{})
302 case Tuple{cursor, Some{Entry{k, v}}}:
303 (cursor, Some{k})
304
305def 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>:
306 match r:
307 case Tuple{cursor, None{}}:
308 (cursor, None{})
309 case Tuple{cursor, Some{Entry{k, v}}}:
310 (cursor, Some{v})
311
312def changed_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Bool:
313 match r:
314 case Tuple{m, None{}}:
315 (m, False{})
316 case Tuple{m, Some{old}}:
317 (m, True{})
318
319def view_contains_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: View<K, V, cmp> & Maybe<&2, V>) -> View<K, V, cmp> & Bool:
320 match r:
321 case Tuple{view, None{}}:
322 (view, False{})
323 case Tuple{view, Some{x}}:
324 (view, True{})
325
326def 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>>:
327 match valid:
328 case True{}:
329 (View{m, lower, upper, descending}, Some{entry})
330 case False{}:
331 (View{m, lower, upper, descending}, None{})
332
333def child(~K: Data, +n: Node<K>, forward: Bool) -> Nat:
334 pick(Nat, forward, node_right(~K, n), node_left(~K, n))
335
336# All links reference live slots. Free slots contain no key and no value.
337
338def read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Node<K>:
339 match m id:
340 case mm 0n:
341 (mm, Free{0n})
342 case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
343 read_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, D.get_at(~Node<K>, nodes, i))
344
345def write(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:
346 match m id:
347 case mm 0n:
348 mm
349 case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
350 write_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, D.set_at(~Node<K>, nodes, i, node))
351
352def 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>:
353 match m id:
354 case mm 0n:
355 (mm, None{})
356 case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
357 exchange_finish(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, D.swap_at(~Maybe<&2, V>, payloads, i, value))
358
359def append_values(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: D.DynArray<&2, Node<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>:
360 match r:
361 case Tuple{payloads, Done{u}}:
362 (TM{n, root, lo, hi, free, nodes, payloads}, Done{id})
363 case Tuple{payloads, Fail{e}}:
364 append_rollback(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, D.pop_at(~Node<K>, nodes))
365
366def 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>:
367 TM{+n, root, +lo, +hi, free, nodes, payloads} = m
368 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}
369
370def get_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
371 match m id:
372 case mm 0n:
373 (mm, None{})
374 case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
375 get_id_finish(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, D.get_at(~Maybe<&2, V>, payloads, i))
376
377def 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:
378 match r:
379 case Tuple{m, Free{next}}:
380 (m, Ascend{0n, 0n, True{}})
381 case Tuple{m, N{c, l, r, q, key}}:
382 (m, ascend_choice(p, p, q, Nat.is_eq(x, pick(Nat, forward, l, r))))
383
384def node_slot_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: Array<Maybe<&2, Node<K>>>, +i: Nat, +valid: Bool) -> Array<Maybe<&2, Node<K>>> & Node<K>:
385 match valid:
386 case False{}:
387 (nodes, Free{0n})
388 case True{}:
389 node_slot_done(~K, ~V, ~cmp, Array.get(Maybe<&2, Node<K>>, nodes, U32.from_nat(i)))
390
391def ascend_slots_step(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +forward: Bool, r: Array<Maybe<&2, Node<K>>> & Node<K>) -> Array<Maybe<&2, Node<K>>> & Ascend:
392 match r:
393 case Tuple{nodes, Free{next}}:
394 (nodes, Ascend{0n, 0n, True{}})
395 case Tuple{nodes, N{c, l, r, q, key}}:
396 (nodes, ascend_choice(p, p, q, Nat.is_eq(x, pick(Nat, forward, l, r))))
397
398def refresh_ends_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo: Nat, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
399 (m3, +hi) = pair_result
400 set_ends(~K, ~V, ~cmp, m3, lo, hi)
401
402def is_empty(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Bool:
403 is_empty_1(~K, ~V, ~cmp, size(~K, ~V, ~cmp, m))
404
405def key_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
406 (m, node) = r
407 (m, node_key(~K, node))
408
409def above_lower(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, bound: Bound<K>) -> Bool:
410 match bound:
411 case Unbounded{}:
412 True{}
413 case Inclusive{lo}:
414 ordering_ok(cmp(lo, k), True{})
415 case Exclusive{lo}:
416 ordering_ok(cmp(lo, k), False{})
417
418def below_upper(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, bound: Bound<K>) -> Bool:
419 match bound:
420 case Unbounded{}:
421 True{}
422 case Inclusive{hi}:
423 ordering_ok(cmp(k, hi), True{})
424 case Exclusive{hi}:
425 ordering_ok(cmp(k, hi), False{})
426
427def bounds_valid(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: Bound<K>, upper: Bound<K>) -> Bool:
428 match lower upper:
429 case Unbounded{} _:
430 True{}
431 case _ Unbounded{}:
432 True{}
433 case Inclusive{lo} Inclusive{hi}:
434 ordering_ok(cmp(lo, hi), True{})
435 case Inclusive{lo} Exclusive{hi}:
436 ordering_ok(cmp(lo, hi), True{})
437 case Exclusive{lo} Inclusive{hi}:
438 ordering_ok(cmp(lo, hi), True{})
439 case Exclusive{lo} Exclusive{hi}:
440 ordering_ok(cmp(lo, hi), True{})
441
442def range_unbounded(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
443 match forward:
444 case True{}:
445 first_id(~K, ~V, ~cmp, m)
446 case False{}:
447 last_id(~K, ~V, ~cmp, m)
448
449def iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
450 cursor_started(~K, ~V, ~cmp, Unbounded{}, Unbounded{}, True{}, first_id(~K, ~V, ~cmp, m))
451
452def descending_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
453 cursor_started(~K, ~V, ~cmp, Unbounded{}, Unbounded{}, False{}, last_id(~K, ~V, ~cmp, m))
454
455def set_left_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:
456 match node:
457 case Free{next}:
458 m
459 case N{c, l, r, p, k}:
460 write(~K, ~V, ~cmp, m, id, N{c, v, r, p, k})
461
462def set_right_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:
463 match node:
464 case Free{next}:
465 m
466 case N{c, l, r, p, k}:
467 write(~K, ~V, ~cmp, m, id, N{c, l, v, p, k})
468
469def set_parent_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:
470 match node:
471 case Free{next}:
472 m
473 case N{c, l, r, p, k}:
474 write(~K, ~V, ~cmp, m, id, N{c, l, r, v, k})
475
476def set_red_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Bool, +node: Node<K>) -> TreeMap<K, V, cmp>:
477 match node:
478 case Free{next}:
479 m
480 case N{c, l, r, p, k}:
481 write(~K, ~V, ~cmp, m, id, N{v, l, r, p, k})
482
483def 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):
484 probe_node(~K, ~V, ~cmp, id, k, read(~K, ~V, ~cmp, m, id))
485
486def 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: D.DynArray<&2, Node<K>> & Result<&2, &2, DE.Error, Unit>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
487 match r:
488 case Tuple{nodes, Done{u}}:
489 append_values(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, k, v, id, D.push_at(~Maybe<&2, V>, payloads, Some{v}))
490 case Tuple{nodes, Fail{e}}:
491 (TM{n, root, lo, hi, free, nodes, payloads}, Fail{Rejected{CapacityExceeded{}, k, v}})
492
493def 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>:
494 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}))
495
496def get_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
497 (m, Search{id, p, on_left}) = r
498 get_id(~K, ~V, ~cmp, m, id)
499
500def extreme_probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Nat:
501 (m, node) = r
502 (m, child(~K, node, forward))
503
504def 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:
505 match fuel st:
506 case 0n Tuple{m, state}:
507 (m, 0n)
508 case 1n+f Tuple{m, Ascend{x, p, True{}}}:
509 (m, p)
510 case 1n+f Tuple{m, Ascend{+x, +p, False{}}}:
511 ascend_loop(~K, ~V, ~cmp, f, forward, ascend_step_node(~K, ~V, ~cmp, x, p, forward, read(~K, ~V, ~cmp, m, p)))
512
513def node_slot(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: Array<Maybe<&2, Node<K>>>, +used: Nat, +id: Nat) -> Array<Maybe<&2, Node<K>>> & Node<K>:
514 match id:
515 case 0n:
516 (nodes, Free{0n})
517 case 1n+ +i:
518 node_slot_checked(~K, ~V, ~cmp, nodes, i, Nat.is_lt(i, used))
519
520def extreme_slots_probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, r: Array<Maybe<&2, Node<K>>> & Node<K>) -> Array<Maybe<&2, Node<K>>> & Nat:
521 (nodes, node) = r
522 (nodes, child(~K, node, forward))
523
524def 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>:
525 match node:
526 case Free{next}:
527 m
528 case N{c, l, r, p, old}:
529 write(~K, ~V, ~cmp, m, id, N{c, l, r, p, k})
530
531def recycle(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>:
532 TM{n, root, lo, hi, +free, nodes, payloads} = m
533 release_header(~K, ~V, ~cmp, write(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, id, Free{free}), id)
534
535def key_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
536 (m, id) = r
537 key_finish(~K, ~V, ~cmp, read(~K, ~V, ~cmp, m, id))
538
539def entry_snapshot_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, id: Nat, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
540 (m, node) = r
541 entry_value(~K, ~V, ~cmp, node_key(~K, node), get_id(~K, ~V, ~cmp, m, id))
542
543def 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>:
544 match r:
545 case Tuple{m, Search{0n, p, on_left}}:
546 (m, None{})
547 case Tuple{m, Search{1n+i, p, on_left}}:
548 exchange(~K, ~V, ~cmp, m, 1n+i, Some{v})
549
550def in_range(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, lower: Bound<K>, upper: Bound<K>) -> Bool:
551 Bool.and(above_lower(~K, ~V, ~cmp, k, lower), below_upper(~K, ~V, ~cmp, k, upper))
552
553def 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>>:
554 view_checked(~K, ~V, ~cmp, m, lower, upper, False{}, bounds_valid(~K, ~V, ~cmp, lower, upper))
555
556def 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>:
557 match cursor:
558 case Cursor{m, next, 0n, lower, upper, forward}:
559 (Cursor{m, next, 0n, lower, upper, forward}, Fail{NoCurrent{}})
560 case Cursor{m, next, 1n+ +id, lower, upper, forward}:
561 iterator_set_done(~K, ~V, ~cmp, next, 1n+id, lower, upper, forward, exchange(~K, ~V, ~cmp, m, 1n+id, Some{v}))
562
563def entry_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
564 iterator(~K, ~V, ~cmp, m)
565
566def key_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
567 iterator(~K, ~V, ~cmp, m)
568
569def values(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
570 iterator(~K, ~V, ~cmp, m)
571
572def 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:
573 match equal:
574 case False{}:
575 (m, False{})
576 case True{}:
577 changed_value(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, m, id, Some{replacement}))
578
579def set_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
580 (m1, +node) = pair_result
581 set_left_node(~K, ~V, ~cmp, m1, id, v, node)
582
583def set_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
584 (m1, +node) = pair_result
585 set_right_node(~K, ~V, ~cmp, m1, id, v, node)
586
587def set_parent_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
588 (m1, +node) = pair_result
589 set_parent_node(~K, ~V, ~cmp, m1, id, v, node)
590
591def set_red_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Bool, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
592 (m1, +node) = pair_result
593 set_red_node(~K, ~V, ~cmp, m1, id, v, node)
594
595def 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:
596 match fuel st:
597 case 0n Tuple{m, node}:
598 (m, Search{0n, p, on_left})
599 case 1n+f Tuple{m, Tuple{Free{next}, order}}:
600 (m, Search{0n, p, on_left})
601 case 1n+f Tuple{m, Tuple{N{c, +l, r, p0, key}, LT{}}}:
602 search_loop(~K, ~V, ~cmp, f, k, l, id, True{}, probe(~K, ~V, ~cmp, m, l, k))
603 case 1n+f Tuple{m, Tuple{N{c, l, +r, p0, key}, GT{}}}:
604 search_loop(~K, ~V, ~cmp, f, k, r, id, False{}, probe(~K, ~V, ~cmp, m, r, k))
605 case 1n+f Tuple{m, Tuple{N{c, l, r, p0, key}, EQ{}}}:
606 (m, Search{id, p, on_left})
607
608def 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: D.DynArray<&2, Node<K>> & Nat) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
609 (nodes, +used) = r
610 append_nodes(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, 1n+used, D.push_at(~Node<K>, nodes, N{True{}, 0n, 0n, p, k}))
611
612def 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>:
613 match r:
614 case Tuple{m, Free{next}}:
615 reuse_slot(~K, ~V, ~cmp, m, id, next, p, k, v)
616 case Tuple{m, N{c, l, r, q, oldk}}:
617 (m, Fail{Rejected{CapacityExceeded{}, k, v}})
618
619def extreme_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, +id: Nat, st: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Nat:
620 match fuel st:
621 case 0n Tuple{m, next}:
622 (m, id)
623 case 1n+p Tuple{m, 0n}:
624 (m, id)
625 case 1n+p Tuple{m, 1n+ +j}:
626 extreme_loop(~K, ~V, ~cmp, p, forward, 1n+j, extreme_probe(~K, ~V, ~cmp, forward, read(~K, ~V, ~cmp, m, 1n+j)))
627
628def ascend_slots_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +used: Nat, +forward: Bool, st: Array<Maybe<&2, Node<K>>> & Ascend) -> Array<Maybe<&2, Node<K>>> & Nat:
629 match fuel st:
630 case 0n Tuple{nodes, state}:
631 (nodes, 0n)
632 case 1n+f Tuple{nodes, Ascend{x, p, True{}}}:
633 (nodes, p)
634 case 1n+f Tuple{nodes, Ascend{+x, +p, False{}}}:
635 ascend_slots_loop(~K, ~V, ~cmp, f, used, forward, ascend_slots_step(~K, ~V, ~cmp, x, p, forward, node_slot(~K, ~V, ~cmp, nodes, used, p)))
636
637def extreme_slots_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +used: Nat, +forward: Bool, +id: Nat, st: Array<Maybe<&2, Node<K>>> & Nat) -> Array<Maybe<&2, Node<K>>> & Nat:
638 match fuel st:
639 case 0n Tuple{nodes, next}:
640 (nodes, id)
641 case 1n+f Tuple{nodes, 0n}:
642 (nodes, id)
643 case 1n+f Tuple{nodes, 1n+ +j}:
644 extreme_slots_loop(~K, ~V, ~cmp, f, used, forward, 1n+j, extreme_slots_probe(~K, ~V, ~cmp, forward, node_slot(~K, ~V, ~cmp, nodes, used, 1n+j)))
645
646def 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>:
647 (m1, +node) = pair_result
648 set_key_node(~K, ~V, ~cmp, m1, id, k, node)
649
650def first_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
651 key_id(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))
652
653def last_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
654 key_id(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))
655
656def 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>>:
657 (m, +id) = r
658 entry_snapshot_value(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))
659
660def 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:
661 match r:
662 case Tuple{m, None{}}:
663 (m, False{})
664 case Tuple{m, Some{old}}:
665 replace_if_apply(~K, ~V, ~cmp, m, id, replacement, eq(old, expected))
666
667def 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:
668 match r:
669 case Tuple{m, Free{free}}:
670 (Cursor{m, next, current, lower, upper, forward}, False{})
671 case Tuple{m, N{c, l, rr, p, key}}:
672 (Cursor{m, next, current, lower, upper, forward}, in_range(~K, ~V, ~cmp, key, lower, upper))
673
674def 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>>:
675 match r:
676 case Tuple{m, None{}}:
677 (View{m, lower, upper, descending}, None{})
678 case Tuple{m, Some{Entry{+k, v}}}:
679 view_entry_checked(~K, ~V, ~cmp, m, lower, upper, descending, Entry{k, v}, in_range(~K, ~V, ~cmp, k, lower, upper))
680
681def set_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:
682 set_left_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))
683
684def set_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:
685 set_right_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))
686
687def set_parent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:
688 set_parent_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))
689
690def set_red(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Bool) -> TreeMap<K, V, cmp>:
691 set_red_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))
692
693def search(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Search:
694 TM{+n, +root, lo, hi, free, nodes, payloads} = m
695 search_loop(~K, ~V, ~cmp, 1n+n, k, root, 0n, False{}, probe(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, root, k))
696
697def 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>:
698 TM{n, root, lo, hi, free, nodes, payloads} = m
699 append_count(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, p, D.length(Node<K>, nodes))
700
701def extreme(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
702 TM{+n, root, lo, hi, free, nodes, payloads} = m
703 extreme_loop(~K, ~V, ~cmp, 1n+n, forward, id, extreme_probe(~K, ~V, ~cmp, forward, read(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, id)))
704
705
706def neighbor_slots(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: Array<Maybe<&2, Node<K>>>, +n: Nat, +used: Nat, +id: Nat, +p: Nat, +forward: Bool, +c: Nat) -> Array<Maybe<&2, Node<K>>> & Nat:
707 match c:
708 case 0n:
709 ascend_slots_loop(~K, ~V, ~cmp, 1n+n, used, forward, (nodes, Ascend{id, p, False{}}))
710 case 1n+ +j:
711 extreme_slots_loop(~K, ~V, ~cmp, 1n+n, used, Bool.not(forward), 1n+j, extreme_slots_probe(~K, ~V, ~cmp, Bool.not(forward), node_slot(~K, ~V, ~cmp, nodes, used, 1n+j)))
712
713def set_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +k: K) -> TreeMap<K, V, cmp>:
714 set_key_1(~K, ~V, ~cmp, id, k, read(~K, ~V, ~cmp, m, id))
715
716def first_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
717 entry_snapshot(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))
718
719def last_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
720 entry_snapshot(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))
721
722def 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:
723 (m, Search{+id, p, on_left}) = r
724 replace_if_value(~K, ~V, ~cmp, ~eq, id, expected, replacement, get_id(~K, ~V, ~cmp, m, id))
725
726def iterator_has_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Bool:
727 Cursor{m, +next, current, lower, upper, forward} = cursor
728 iterator_has_checked(~K, ~V, ~cmp, next, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))
729
730def 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>:
731 match p on_left:
732 case 0n _:
733 set_root(~K, ~V, ~cmp, m, x)
734 case 1n+q True{}:
735 set_left(~K, ~V, ~cmp, m, 1n+q, x)
736 case 1n+q False{}:
737 set_right(~K, ~V, ~cmp, m, 1n+q, x)
738
739def black_root_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
740 (m1, +r) = pair_result
741 set_red(~K, ~V, ~cmp, m1, r, False{})
742
743def 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>:
744 TM{n, root, lo, hi, free, nodes, payloads} = m
745 match free:
746 case 0n:
747 append(~K, ~V, ~cmp, TM{n, root, lo, hi, 0n, nodes, payloads}, k, v, p)
748 case 1n+ +f:
749 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))
750
751def get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
752 get_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))
753
754def contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Bool:
755 contains_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))
756
757def 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:
758 (TM{+n, root, lo, hi, free, D.DA{limit, depth, cap, +used, nodes}, payloads}, +node) = r
759 neighbor_slots_finish(~K, ~V, ~cmp, n, root, lo, hi, free, limit, depth, cap, used, payloads, neighbor_slots(~K, ~V, ~cmp, nodes, n, used, id, node_parent(~K, node), forward, child(~K, node, forward)))
760
761def copy_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +target: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:
762 match node:
763 case Free{next}:
764 m
765 case N{c, l, r, p, k}:
766 set_key(~K, ~V, ~cmp, m, target, k)
767
768def refresh_ends_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +r: Nat, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
769 (m2, +lo) = pair_result
770 refresh_ends_3(~K, ~V, ~cmp, lo, extreme(~K, ~V, ~cmp, m2, r, True{}))
771
772def 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>:
773 replace_found(~K, ~V, ~cmp, v, search(~K, ~V, ~cmp, m, k))
774
775def 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>:
776 match k r:
777 case None{} Tuple{m, removed}:
778 (Cursor{m, 0n, 0n, lower, upper, forward}, removed)
779 case Some{key} Tuple{m, removed}:
780 iterator_relocated(~K, ~V, ~cmp, lower, upper, forward, removed, search(~K, ~V, ~cmp, m, key))
781
782def 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:
783 replace_if_found(~K, ~V, ~cmp, ~eq, expected, replacement, search(~K, ~V, ~cmp, m, k))
784
785def 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>:
786 set_parent(~K, ~V, ~cmp, attach_side(~K, ~V, ~cmp, m, p, x, on_left), x, p)
787
788def black_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>:
789 black_root_1(~K, ~V, ~cmp, root_id(~K, ~V, ~cmp, m))
790
791
792def neighbor(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
793 neighbor_node(~K, ~V, ~cmp, id, forward, read(~K, ~V, ~cmp, m, id))
794
795def 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:
796 (m2, value) = pair_result
797 move_successor_3(~K, ~V, ~cmp, source, exchange(~K, ~V, ~cmp, copy_key(~K, ~V, ~cmp, m2, target, source_node), target, value))
798
799def refresh_ends_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
800 (m1, +r) = pair_result
801 refresh_ends_2(~K, ~V, ~cmp, r, extreme(~K, ~V, ~cmp, m1, r, False{}))
802
803def 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:
804 default_value(~K, ~V, ~cmp, fallback, get(~K, ~V, ~cmp, m, k))
805
806
807def 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>:
808 match valid:
809 case True{}:
810 view_value(~K, ~V, ~cmp, lower, upper, descending, get(~K, ~V, ~cmp, m, k))
811 case False{}:
812 (View{m, lower, upper, descending}, None{})
813
814def 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>:
815 (m3, +pn) = pair_result
816 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))
817
818def 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>:
819 (m3, +pn) = pair_result
820 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))
821
822def 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:
823 (m1, +source_node) = pair_result
824 move_successor_2(~K, ~V, ~cmp, target, source, source_node, exchange(~K, ~V, ~cmp, m1, source, None{}))
825
826def refresh_ends(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>:
827 refresh_ends_1(~K, ~V, ~cmp, root_id(~K, ~V, ~cmp, m))
828
829def 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:
830 match inclusive:
831 case True{}:
832 (m, id)
833 case False{}:
834 neighbor(~K, ~V, ~cmp, m, id, higher)
835
836def view_get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, V>:
837 View{m, +lower, +upper, descending} = view
838 view_get_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))
839
840def iterator_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: 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>>:
841 match valid:
842 case True{}:
843 iterator_yield(~K, ~V, ~cmp, id, lower, upper, forward, entry, neighbor(~K, ~V, ~cmp, m, id, forward))
844 case False{}:
845 (Cursor{m, 0n, current, lower, upper, forward}, None{})
846
847def 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>:
848 (m2, +yn) = pair_result
849 rotate_left_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, node_parent(~K, xn)))
850
851def 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>:
852 (m2, +yn) = pair_result
853 rotate_right_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, node_parent(~K, xn)))
854
855def move_successor(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +target: Nat, +source: Nat) -> TreeMap<K, V, cmp> & Nat:
856 move_successor_1(~K, ~V, ~cmp, target, source, read(~K, ~V, ~cmp, m, source))
857
858def 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:
859 match fuel st:
860 case 0n Tuple{m, node}:
861 (m, best)
862 case 1n+f Tuple{m, Tuple{Free{next}, order}}:
863 (m, best)
864 case 1n+f Tuple{m, Tuple{N{c, +l, r, p, key}, LT{}}}:
865 nav_loop(~K, ~V, ~cmp, f, k, higher, inclusive, l, pick(Nat, higher, id, best), probe(~K, ~V, ~cmp, m, l, k))
866 case 1n+f Tuple{m, Tuple{N{c, l, +r, p, key}, GT{}}}:
867 nav_loop(~K, ~V, ~cmp, f, k, higher, inclusive, r, pick(Nat, higher, best, id), probe(~K, ~V, ~cmp, m, r, k))
868 case 1n+f Tuple{m, Tuple{node, EQ{}}}:
869 nav_equal(~K, ~V, ~cmp, m, id, higher, inclusive)
870
871def iterator_read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +current: Nat, +lower: Bound<K>, +upper: Bound<K>, +forward: Bool, r: TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
872 match r:
873 case Tuple{m, None{}}:
874 (Cursor{m, 0n, current, lower, upper, forward}, None{})
875 case Tuple{m, Some{Entry{+k, v}}}:
876 iterator_checked(~K, ~V, ~cmp, m, id, current, lower, upper, forward, Entry{k, v}, in_range(~K, ~V, ~cmp, k, lower, upper))
877
878def view_contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Bool:
879 view_contains_value(~K, ~V, ~cmp, view_get(~K, ~V, ~cmp, view, k))
880
881def 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>:
882 (m1, +xn) = pair_result
883 rotate_left_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, node_right(~K, xn)))
884
885def 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>:
886 (m1, +xn) = pair_result
887 rotate_right_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, node_left(~K, xn)))
888
889def successor_ready(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Nat:
890 (m, source) = r
891 move_successor(~K, ~V, ~cmp, m, target, source)
892
893def 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:
894 TM{+n, +root, lo, hi, free, nodes, payloads} = m
895 nav_loop(~K, ~V, ~cmp, 1n+n, k, higher, inclusive, root, 0n, probe(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, root, k))
896
897def iterator_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
898 Cursor{m, +next, current, lower, upper, forward} = cursor
899 iterator_read(~K, ~V, ~cmp, next, current, lower, upper, forward, entry_snapshot(~K, ~V, ~cmp, (m, next)))
900
901def rotate_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat) -> TreeMap<K, V, cmp>:
902 rotate_left_1(~K, ~V, ~cmp, x, read(~K, ~V, ~cmp, m, x))
903
904def rotate_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat) -> TreeMap<K, V, cmp>:
905 rotate_right_1(~K, ~V, ~cmp, x, read(~K, ~V, ~cmp, m, x))
906
907def delete_target(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Nat:
908 match r:
909 case Tuple{m, N{c, 1n+l, 1n+r, p, k}}:
910 successor_ready(~K, ~V, ~cmp, id, extreme(~K, ~V, ~cmp, m, 1n+r, False{}))
911 case Tuple{m, node}:
912 (m, id)
913
914
915def lower_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
916 key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, False{}))
917
918def floor_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
919 key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, True{}))
920
921def ceiling_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
922 key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, True{}))
923
924def higher_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
925 key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, False{}))
926
927def 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>>:
928 entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, False{}))
929
930def 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>>:
931 entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, True{}))
932
933def 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>>:
934 entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, True{}))
935
936def 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>>:
937 entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, False{}))
938
939def 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:
940 match bound:
941 case Unbounded{}:
942 range_unbounded(~K, ~V, ~cmp, m, forward)
943 case Inclusive{k}:
944 navigate(~K, ~V, ~cmp, m, k, forward, True{})
945 case Exclusive{k}:
946 navigate(~K, ~V, ~cmp, m, k, forward, False{})
947
948def iterator_next_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, K>:
949 iterator_key_result(~K, ~V, ~cmp, iterator_next(~K, ~V, ~cmp, cursor))
950
951def iterator_next_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, V>:
952 iterator_value_result(~K, ~V, ~cmp, iterator_next(~K, ~V, ~cmp, cursor))
953
954def 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:
955 match fuel found st:
956 case _ True{} Tuple{cursor, item}:
957 (iterator_finish(~K, ~V, ~cmp, cursor), True{})
958 case 0n False{} Tuple{cursor, item}:
959 (iterator_finish(~K, ~V, ~cmp, cursor), False{})
960 case 1n+f False{} Tuple{cursor, None{}}:
961 (iterator_finish(~K, ~V, ~cmp, cursor), False{})
962 case 1n+f False{} Tuple{cursor, Some{Entry{k, v}}}:
963 contains_value_loop(~K, ~V, ~cmp, ~eq, f, wanted, eq(v, wanted), iterator_next(~K, ~V, ~cmp, cursor))
964
965def 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:
966 match fuel st:
967 case 0n Tuple{cursor, item}:
968 (iterator_view(~K, ~V, ~cmp, cursor), count)
969 case 1n+f Tuple{cursor, None{}}:
970 (iterator_view(~K, ~V, ~cmp, cursor), count)
971 case 1n+f Tuple{cursor, Some{item}}:
972 view_count_loop(~K, ~V, ~cmp, f, 1n+count, iterator_next(~K, ~V, ~cmp, cursor))
973
974def 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>>:
975 (cursor, removed) = r
976 iterator_next(~K, ~V, ~cmp, cursor)
977
978def 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:
979 match triangle:
980 case True{}:
981 (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{}})
982 case False{}:
983 (rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), g, True{}), g), Fix{0n, False{}})
984
985def 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:
986 match triangle:
987 case True{}:
988 (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{}})
989 case False{}:
990 (rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), g, True{}), g), Fix{0n, False{}})
991
992def 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:
993 (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{}})
994
995def 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:
996 (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{}})
997
998def view_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> Cursor<K, V, cmp>:
999 View{m, +lower, +upper, +descending} = view
1000 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)))
1001
1002def 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:
1003 (m, n) = r
1004 contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+n, wanted, False{}, iterator_next(~K, ~V, ~cmp, iterator(~K, ~V, ~cmp, m)))
1005
1006def 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:
1007 match within:
1008 case True{}:
1009 navigate(~K, ~V, ~cmp, m, k, higher, inclusive)
1010 case False{}:
1011 range_start(~K, ~V, ~cmp, m, pick(Bound<K>, higher, lower, upper), higher)
1012
1013def 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>>:
1014 View{m, +lower, +upper, +descending} = view
1015 +up = pick(Bool, descending, Bool.not(first), first)
1016 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)))
1017
1018def 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:
1019 match uncle:
1020 case N{True{}, l, r, gp, k}:
1021 (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{}})
1022 case _:
1023 insert_black_left(~K, ~V, ~cmp, m, z, p, g, triangle)
1024
1025def 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:
1026 match uncle:
1027 case N{True{}, l, r, gp, k}:
1028 (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{}})
1029 case _:
1030 insert_black_right(~K, ~V, ~cmp, m, z, p, g, triangle)
1031
1032def 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:
1033 (m2, +wn) = pair_result
1034 delete_borrow_left(~K, ~V, ~cmp, m2, p, node_right(~K, pn), pn, wn)
1035
1036def 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:
1037 (m2, +wn) = pair_result
1038 delete_borrow_right(~K, ~V, ~cmp, m2, p, node_left(~K, pn), pn, wn)
1039
1040def 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:
1041 contains_value_start(~K, ~V, ~cmp, ~eq, wanted, size(~K, ~V, ~cmp, m))
1042
1043def 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>>:
1044 View{m, +lower, +upper, +descending} = view
1045 +up = pick(Bool, descending, Bool.not(higher), higher)
1046 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)))))
1047
1048def 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>>:
1049 view_extreme(~K, ~V, ~cmp, view, True{})
1050
1051def 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>>:
1052 view_extreme(~K, ~V, ~cmp, view, False{})
1053
1054def view_size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp> & Nat:
1055 View{TM{+n, root, lo, hi, free, nodes, payloads}, lower, upper, descending} = view
1056 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})))
1057
1058def 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:
1059 (m1, +un) = pair_result
1060 insert_uncle_left(~K, ~V, ~cmp, m1, z, p, g, node_right(~K, gn), Nat.is_eq(z, node_right(~K, pn)), un)
1061
1062def 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:
1063 (m1, +un) = pair_result
1064 insert_uncle_right(~K, ~V, ~cmp, m1, z, p, g, node_left(~K, gn), Nat.is_eq(z, node_left(~K, pn)), un)
1065
1066def 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:
1067 (m1, +pn) = pair_result
1068 delete_borrow_read_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_right(~K, pn)))
1069
1070def 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:
1071 (m1, +pn) = pair_result
1072 delete_borrow_read_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_left(~K, pn)))
1073
1074def 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>>:
1075 view_nav(~K, ~V, ~cmp, view, k, False{}, False{})
1076
1077def 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>>:
1078 view_nav(~K, ~V, ~cmp, view, k, False{}, True{})
1079
1080def 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>>:
1081 view_nav(~K, ~V, ~cmp, view, k, True{}, True{})
1082
1083def 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>>:
1084 view_nav(~K, ~V, ~cmp, view, k, True{}, False{})
1085
1086def 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:
1087 insert_side_left_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, node_right(~K, gn)))
1088
1089def 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:
1090 insert_side_right_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, node_left(~K, gn)))
1091
1092def delete_borrow_read_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
1093 delete_borrow_read_left_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1094
1095def delete_borrow_read_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
1096 delete_borrow_read_right_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1097
1098def 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:
1099 match on_left:
1100 case True{}:
1101 insert_side_left(~K, ~V, ~cmp, m, z, p, g, pn, gn)
1102 case False{}:
1103 insert_side_right(~K, ~V, ~cmp, m, z, p, g, pn, gn)
1104
1105def 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:
1106 match far_red:
1107 case True{}:
1108 delete_borrow_left(~K, ~V, ~cmp, m, p, w, pn, wn)
1109 case False{}:
1110 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)
1111
1112def 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:
1113 match far_red:
1114 case True{}:
1115 delete_borrow_right(~K, ~V, ~cmp, m, p, w, pn, wn)
1116 case False{}:
1117 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)
1118
1119def 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:
1120 (m1, +gn) = pair_result
1121 insert_side(~K, ~V, ~cmp, m1, z, p, node_parent(~K, pn), pn, gn, Nat.is_eq(p, node_left(~K, gn)))
1122
1123def 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:
1124 match near_red far_red:
1125 case False{} False{}:
1126 (set_red(~K, ~V, ~cmp, m, w, True{}), DF{p, node_parent(~K, pn), True{}})
1127 case _ _:
1128 delete_far_left(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)
1129
1130def 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:
1131 match near_red far_red:
1132 case False{} False{}:
1133 (set_red(~K, ~V, ~cmp, m, w, True{}), DF{p, node_parent(~K, pn), True{}})
1134 case _ _:
1135 delete_far_right(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)
1136
1137def 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:
1138 insert_grand_1(~K, ~V, ~cmp, z, p, pn, read(~K, ~V, ~cmp, m, node_parent(~K, pn)))
1139
1140def 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:
1141 (m4, +far_node) = pair_result
1142 delete_children_left(~K, ~V, ~cmp, m4, p, node_right(~K, pn), pn, wn, node_red(~K, near_node), node_red(~K, far_node))
1143
1144def 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:
1145 (m4, +far_node) = pair_result
1146 delete_children_right(~K, ~V, ~cmp, m4, p, node_left(~K, pn), pn, wn, node_red(~K, near_node), node_red(~K, far_node))
1147
1148def 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:
1149 match is_red:
1150 case False{}:
1151 (m, Fix{0n, False{}})
1152 case True{}:
1153 insert_grand(~K, ~V, ~cmp, m, z, p, pn)
1154
1155def 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:
1156 (m3, +near_node) = pair_result
1157 delete_sibling_left_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, node_right(~K, wn)))
1158
1159def 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:
1160 (m3, +near_node) = pair_result
1161 delete_sibling_right_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, node_left(~K, wn)))
1162
1163def 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:
1164 (m2, +pn) = pair_result
1165 insert_parent(~K, ~V, ~cmp, m2, z, node_parent(~K, zn), pn, node_red(~K, pn))
1166
1167def 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:
1168 (m2, +wn) = pair_result
1169 delete_sibling_left_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, node_left(~K, wn)))
1170
1171def 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:
1172 (m2, +wn) = pair_result
1173 delete_sibling_right_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, node_right(~K, wn)))
1174
1175def 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:
1176 (m1, +zn) = pair_result
1177 insert_fix_step_2(~K, ~V, ~cmp, z, zn, read(~K, ~V, ~cmp, m1, node_parent(~K, zn)))
1178
1179def 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:
1180 (m1, +pn) = pair_result
1181 delete_sibling_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_right(~K, pn)))
1182
1183def 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:
1184 (m1, +pn) = pair_result
1185 delete_sibling_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_left(~K, pn)))
1186
1187def insert_fix_step(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat) -> TreeMap<K, V, cmp> & Fix:
1188 insert_fix_step_1(~K, ~V, ~cmp, z, read(~K, ~V, ~cmp, m, z))
1189
1190def delete_sibling_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
1191 delete_sibling_left_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1192
1193def delete_sibling_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
1194 delete_sibling_right_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1195
1196def insert_fix_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: TreeMap<K, V, cmp> & Fix) -> TreeMap<K, V, cmp>:
1197 match fuel st:
1198 case 0n Tuple{m, f}:
1199 black_root(~K, ~V, ~cmp, m)
1200 case 1n+p Tuple{m, Fix{z, False{}}}:
1201 black_root(~K, ~V, ~cmp, m)
1202 case 1n+p Tuple{m, Fix{z, True{}}}:
1203 insert_fix_loop(~K, ~V, ~cmp, p, insert_fix_step(~K, ~V, ~cmp, m, z))
1204
1205def 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:
1206 match red_sibling:
1207 case True{}:
1208 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)
1209 case False{}:
1210 delete_sibling_left(~K, ~V, ~cmp, m, p)
1211
1212def 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:
1213 match red_sibling:
1214 case True{}:
1215 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)
1216 case False{}:
1217 delete_sibling_right(~K, ~V, ~cmp, m, p)
1218
1219def insert_fixed(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
1220 (m, n) = r
1221 insert_fix_loop(~K, ~V, ~cmp, 1n+n, (m, Fix{id, True{}}))
1222
1223def 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:
1224 (m1, +wn) = pair_result
1225 delete_red_sibling_left(~K, ~V, ~cmp, m1, p, node_right(~K, pn), node_red(~K, wn))
1226
1227def 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:
1228 (m1, +wn) = pair_result
1229 delete_red_sibling_right(~K, ~V, ~cmp, m1, p, node_left(~K, pn), node_red(~K, wn))
1230
1231def 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>>:
1232 match r:
1233 case Tuple{m, Done{+id}}:
1234 (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{}})
1235 case Tuple{m, Fail{e}}:
1236 (m, Fail{e})
1237
1238def 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:
1239 delete_side_left_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, node_right(~K, pn)))
1240
1241def 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:
1242 delete_side_right_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, node_left(~K, pn)))
1243
1244def 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>>:
1245 match r:
1246 case Tuple{m, Search{0n, +p, +on_left}}:
1247 put_allocated(~K, ~V, ~cmp, p, on_left, allocate(~K, ~V, ~cmp, m, p, k, v))
1248 case Tuple{m, Search{1n+i, p, on_left}}:
1249 put_replaced(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, m, 1n+i, Some{v}))
1250
1251def 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:
1252 match on_left:
1253 case True{}:
1254 delete_side_left(~K, ~V, ~cmp, m, p, pn)
1255 case False{}:
1256 delete_side_right(~K, ~V, ~cmp, m, p, pn)
1257
1258def 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>>:
1259 match r:
1260 case Tuple{m, Search{0n, +p, +on_left}}:
1261 put_allocated(~K, ~V, ~cmp, p, on_left, allocate(~K, ~V, ~cmp, m, p, k, v))
1262 case Tuple{m, Search{1n+i, p, on_left}}:
1263 put_replaced(~K, ~V, ~cmp, get_id(~K, ~V, ~cmp, m, 1n+i))
1264
1265def 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>>:
1266 put_found(~K, ~V, ~cmp, k, v, search(~K, ~V, ~cmp, m, k))
1267
1268def 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:
1269 match stop:
1270 case True{}:
1271 (set_red(~K, ~V, ~cmp, m, x, False{}), DF{0n, 0n, False{}})
1272 case False{}:
1273 delete_side(~K, ~V, ~cmp, m, x, p, pn, Nat.is_eq(x, node_left(~K, pn)))
1274
1275def 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>>:
1276 put_absent_found(~K, ~V, ~cmp, k, v, search(~K, ~V, ~cmp, m, k))
1277
1278def 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:
1279 (m3, +pn) = pair_result
1280 delete_stop(~K, ~V, ~cmp, m3, x, p, pn, Bool.or(Nat.is_eq(x, root_node), node_red(~K, xn)))
1281
1282def 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>>:
1283 match valid:
1284 case True{}:
1285 view_put_finish(~K, ~V, ~cmp, lower, upper, descending, put(~K, ~V, ~cmp, m, k, v))
1286 case False{}:
1287 (View{m, lower, upper, descending}, Fail{Rejected{OutOfRange{}, k, v}})
1288
1289def 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:
1290 (m2, +xn) = pair_result
1291 delete_fix_step_3(~K, ~V, ~cmp, x, p, root_node, xn, read(~K, ~V, ~cmp, m2, p))
1292
1293def 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>>:
1294 View{m, +lower, +upper, descending} = view
1295 view_put_checked(~K, ~V, ~cmp, m, k, v, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))
1296
1297def 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:
1298 (m1, +root_node) = pair_result
1299 delete_fix_step_2(~K, ~V, ~cmp, x, p, root_node, read(~K, ~V, ~cmp, m1, x))
1300
1301def 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:
1302 delete_fix_step_1(~K, ~V, ~cmp, x, p, root_id(~K, ~V, ~cmp, m))
1303
1304def delete_fix_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: TreeMap<K, V, cmp> & DeleteFix) -> TreeMap<K, V, cmp>:
1305 match fuel st:
1306 case 0n Tuple{m, fix}:
1307 black_root(~K, ~V, ~cmp, m)
1308 case 1n+f Tuple{m, DF{x, p, False{}}}:
1309 black_root(~K, ~V, ~cmp, m)
1310 case 1n+f Tuple{m, DF{x, p, True{}}}:
1311 delete_fix_loop(~K, ~V, ~cmp, f, delete_fix_step(~K, ~V, ~cmp, m, x, p))
1312
1313def 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>:
1314 TM{+n, root, lo, hi, free, nodes, payloads} = m
1315 delete_fix_loop(~K, ~V, ~cmp, 1n+n, (TM{n, root, lo, hi, free, nodes, payloads}, DF{x, p, Bool.not(was_red)}))
1316
1317def 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>:
1318 (m2, +pn) = pair_result
1319 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))
1320
1321def unlink_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
1322 (m1, +node) = pair_result
1323 unlink_2(~K, ~V, ~cmp, id, node, read(~K, ~V, ~cmp, m1, node_parent(~K, node)))
1324
1325def unlink(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>:
1326 unlink_1(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))
1327
1328def unlink_target(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
1329 (m, id) = r
1330 refresh_ends(~K, ~V, ~cmp, unlink(~K, ~V, ~cmp, m, id))
1331
1332def 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>:
1333 (m1, value) = pair_result
1334 (unlink_target(~K, ~V, ~cmp, delete_target(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m1, id))), value)
1335
1336def remove_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
1337 remove_present_1(~K, ~V, ~cmp, id, exchange(~K, ~V, ~cmp, m, id, None{}))
1338
1339def remove_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
1340 match id:
1341 case 0n:
1342 (m, None{})
1343 case 1n+i:
1344 remove_present(~K, ~V, ~cmp, m, 1n+i)
1345
1346def remove_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
1347 (m, Search{id, p, on_left}) = r
1348 remove_id(~K, ~V, ~cmp, m, id)
1349
1350def 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>>:
1351 (m1, +node) = pair_result
1352 entry_value(~K, ~V, ~cmp, node_key(~K, node), remove_id(~K, ~V, ~cmp, m1, id))
1353
1354def 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>:
1355 (m1, +node) = pair_result
1356 iterator_reseek(~K, ~V, ~cmp, node_key(~K, node), lower, upper, forward, remove_id(~K, ~V, ~cmp, m1, current))
1357
1358def 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:
1359 match equal:
1360 case False{}:
1361 (m, False{})
1362 case True{}:
1363 changed_value(~K, ~V, ~cmp, remove_id(~K, ~V, ~cmp, m, id))
1364
1365def remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
1366 remove_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))
1367
1368def 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>>:
1369 remove_entry_id_1(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))
1370
1371def 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>:
1372 iterator_delete_1(~K, ~V, ~cmp, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))
1373
1374def 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:
1375 match r:
1376 case Tuple{m, None{}}:
1377 (m, False{})
1378 case Tuple{m, Some{old}}:
1379 remove_if_apply(~K, ~V, ~cmp, m, id, replacement, eq(old, expected))
1380
1381def 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>>:
1382 (m, id) = r
1383 remove_entry_id(~K, ~V, ~cmp, m, id)
1384
1385def 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>:
1386 match valid:
1387 case True{}:
1388 view_value(~K, ~V, ~cmp, lower, upper, descending, remove(~K, ~V, ~cmp, m, k))
1389 case False{}:
1390 (View{m, lower, upper, descending}, None{})
1391
1392def iterator_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, V>:
1393 Cursor{m, next, current, lower, upper, forward} = cursor
1394 iterator_delete(~K, ~V, ~cmp, m, next, current, lower, upper, forward)
1395
1396def 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:
1397 (m, Search{+id, p, on_left}) = r
1398 remove_if_value(~K, ~V, ~cmp, ~eq, id, expected, replacement, get_id(~K, ~V, ~cmp, m, id))
1399
1400def 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>>:
1401 poll_ready(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))
1402
1403def 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>>:
1404 poll_ready(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))
1405
1406def view_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, V>:
1407 View{m, +lower, +upper, descending} = view
1408 view_remove_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))
1409
1410def 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:
1411 remove_if_found(~K, ~V, ~cmp, ~eq, expected, expected, search(~K, ~V, ~cmp, m, k))
1412
1413def 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>:
1414 match fuel st:
1415 case 0n Tuple{cursor, item}:
1416 iterator_view(~K, ~V, ~cmp, cursor)
1417 case 1n+f Tuple{cursor, None{}}:
1418 iterator_view(~K, ~V, ~cmp, cursor)
1419 case 1n+f Tuple{cursor, Some{item}}:
1420 view_clear_loop(~K, ~V, ~cmp, f, view_clear_next(~K, ~V, ~cmp, iterator_remove(~K, ~V, ~cmp, cursor)))
1421
1422def view_clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp>:
1423 View{TM{+n, root, lo, hi, free, nodes, payloads}, lower, upper, descending} = view
1424 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})))