proofs/containers/balanced_search_tree/mirror.bend

bend-collections-laws-containers@1.0.0.0 · 1,412 lines · 0 definitions

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