spec/containers/balanced_search_tree/main.bend
bend-collections-laws-containers@1.0.0.0 · 765 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
4import bend-collections-laws-containers@1.0.0.0/spec/lib/order.bend as SO
5
6# Independent model of the indexed TreeMap: a limit exponent (at most
7# 2^limit entries) and the entries in key order under the comparator ~cmp.
8# Cursors name their next and current entries by key; views are the map with
9# a range and a direction. Nothing here refers to nodes, colours, links,
10# slots or the free list; only the neutral datatypes of the implementation
11# module (M.Entry, M.Rejected, M.Error, M.Bound) are used.
12
13type Model<-K: Data, -V: Data> is Data:
14 TM{limit: Nat, es: List<&2, M.Entry<K, V>>}
15
16type Cursor<-K: Data, -V: Data> is Data:
17 CR{map: Model<K, V>, next: Maybe<&2, K>, current: Maybe<&2, K>, lower: M.Bound<K>, upper: M.Bound<K>, forward: Bool}
18
19type View<-K: Data, -V: Data> is Data:
20 VW{map: Model<K, V>, lower: M.Bound<K>, upper: M.Bound<K>, descending: Bool}
21
22type InvalidView<-K: Data, -V: Data> is Data:
23 IV{map: Model<K, V>, error: M.Error}
24
25def pick(-T: Type, +b: Bool, x: T, y: T) -> T:
26 match b:
27 case True{}:
28 x
29 case False{}:
30 y
31
32def new(-K: Data, -V: Data) -> Model<K, V>:
33 TM{31n, Nil{}}
34
35def with_limit(-K: Data, -V: Data, +k: Nat) -> Model<K, V>:
36 TM{pick(Nat, Nat.is_lt(k, 31n), k, 31n), Nil{}}
37
38def key(-K: Data, -V: Data, e: M.Entry<K, V>) -> K:
39 match e:
40 case M.Entry{k, v}:
41 k
42
43def val(-K: Data, -V: Data, e: M.Entry<K, V>) -> V:
44 match e:
45 case M.Entry{k, v}:
46 v
47
48def keys(-K: Data, -V: Data, es: List<&2, M.Entry<K, V>>) -> List<&2, K>:
49 match es:
50 case Nil{}:
51 Nil{}
52 case Con{e, t}:
53 Con{key(K, V, e), keys(K, V, t)}
54
55def is_eq(c: Cmp) -> Bool:
56 match c:
57 case EQ{}:
58 True{}
59 case _:
60 False{}
61
62# ---- the entry of a key ----
63
64# the first entry whose key is equal to k
65def find_e(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, es: List<&2, M.Entry<K, V>>) -> Maybe<&2, M.Entry<K, V>>:
66 match es:
67 case Nil{}:
68 None{}
69 case Con{+e, +t}:
70 pick(Maybe<&2, M.Entry<K, V>>, is_eq(cmp(k, key(K, V, e))), Some{e}, find_e(~K, ~V, ~cmp, k, t))
71
72def val_m(-K: Data, -V: Data, m: Maybe<&2, M.Entry<K, V>>) -> Maybe<&2, V>:
73 match m:
74 case None{}:
75 None{}
76 case Some{e}:
77 Some{val(K, V, e)}
78
79def key_m(-K: Data, -V: Data, m: Maybe<&2, M.Entry<K, V>>) -> Maybe<&2, K>:
80 match m:
81 case None{}:
82 None{}
83 case Some{e}:
84 Some{key(K, V, e)}
85
86def find(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, es: List<&2, M.Entry<K, V>>) -> Maybe<&2, V>:
87 val_m(K, V, find_e(~K, ~V, ~cmp, k, es))
88
89def is_some(-X: Data, m: Maybe<&2, X>) -> Bool:
90 match m:
91 case None{}:
92 False{}
93 case Some{x}:
94 True{}
95
96# ---- changes ----
97
98# k, absent, inserted before the first entry with a greater key
99def ins(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, es: List<&2, M.Entry<K, V>>) -> List<&2, M.Entry<K, V>>:
100 match es:
101 case Nil{}:
102 Con{M.Entry{k, v}, Nil{}}
103 case Con{+e, +t}:
104 pick(List<&2, M.Entry<K, V>>, Cmp.is_lt(cmp(k, key(K, V, e))), Con{M.Entry{k, v}, Con{e, t}}, Con{e, ins(~K, ~V, ~cmp, k, v, t)})
105
106# the value of the first entry equal to k replaced (its key is kept)
107def set_val(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, es: List<&2, M.Entry<K, V>>) -> List<&2, M.Entry<K, V>>:
108 match es:
109 case Nil{}:
110 Nil{}
111 case Con{+e, +t}:
112 pick(List<&2, M.Entry<K, V>>, is_eq(cmp(k, key(K, V, e))), Con{M.Entry{key(K, V, e), v}, t}, Con{e, set_val(~K, ~V, ~cmp, k, v, t)})
113
114# the first entry equal to k removed
115def del(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, es: List<&2, M.Entry<K, V>>) -> List<&2, M.Entry<K, V>>:
116 match es:
117 case Nil{}:
118 Nil{}
119 case Con{+e, +t}:
120 pick(List<&2, M.Entry<K, V>>, is_eq(cmp(k, key(K, V, e))), t, Con{e, del(~K, ~V, ~cmp, k, t)})
121
122# ---- ranges ----
123
124def ordering_ok(c: Cmp, inclusive: Bool) -> Bool:
125 match c:
126 case LT{}:
127 True{}
128 case EQ{}:
129 inclusive
130 case GT{}:
131 False{}
132
133def above_lower(~K: Data, ~cmp: K -> K -> Cmp, +k: K, b: M.Bound<K>) -> Bool:
134 match b:
135 case M.Unbounded{}:
136 True{}
137 case M.Inclusive{lo}:
138 ordering_ok(cmp(lo, k), True{})
139 case M.Exclusive{lo}:
140 ordering_ok(cmp(lo, k), False{})
141
142def below_upper(~K: Data, ~cmp: K -> K -> Cmp, +k: K, b: M.Bound<K>) -> Bool:
143 match b:
144 case M.Unbounded{}:
145 True{}
146 case M.Inclusive{hi}:
147 ordering_ok(cmp(k, hi), True{})
148 case M.Exclusive{hi}:
149 ordering_ok(cmp(k, hi), False{})
150
151def in_range(~K: Data, ~cmp: K -> K -> Cmp, +k: K, lo: M.Bound<K>, hi: M.Bound<K>) -> Bool:
152 Bool.and(above_lower(~K, ~cmp, k, lo), below_upper(~K, ~cmp, k, hi))
153
154# a view's bounds are valid when neither is past the other
155def bounds_valid(~K: Data, ~cmp: K -> K -> Cmp, lo: M.Bound<K>, hi: M.Bound<K>) -> Bool:
156 match lo hi:
157 case M.Unbounded{} _:
158 True{}
159 case _ M.Unbounded{}:
160 True{}
161 case M.Inclusive{a} M.Inclusive{b}:
162 ordering_ok(cmp(a, b), True{})
163 case M.Inclusive{a} M.Exclusive{b}:
164 ordering_ok(cmp(a, b), True{})
165 case M.Exclusive{a} M.Inclusive{b}:
166 ordering_ok(cmp(a, b), True{})
167 case M.Exclusive{a} M.Exclusive{b}:
168 ordering_ok(cmp(a, b), True{})
169
170def within(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo: M.Bound<K>, +hi: M.Bound<K>, es: List<&2, M.Entry<K, V>>) -> List<&2, M.Entry<K, V>>:
171 match es:
172 case Nil{}:
173 Nil{}
174 case Con{+e, +t}:
175 pick(List<&2, M.Entry<K, V>>, in_range(~K, ~cmp, key(K, V, e), lo, hi), Con{e, within(~K, ~V, ~cmp, lo, hi, t)}, within(~K, ~V, ~cmp, lo, hi, t))
176
177def outside(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo: M.Bound<K>, +hi: M.Bound<K>, es: List<&2, M.Entry<K, V>>) -> List<&2, M.Entry<K, V>>:
178 match es:
179 case Nil{}:
180 Nil{}
181 case Con{+e, +t}:
182 pick(List<&2, M.Entry<K, V>>, in_range(~K, ~cmp, key(K, V, e), lo, hi), outside(~K, ~V, ~cmp, lo, hi, t), Con{e, outside(~K, ~V, ~cmp, lo, hi, t)})
183
184# ---- order queries ----
185
186# the first entry e with keep(cmp(k, e.key))
187def first_where(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +inclusive: Bool, es: List<&2, M.Entry<K, V>>) -> Maybe<&2, M.Entry<K, V>>:
188 match es:
189 case Nil{}:
190 None{}
191 case Con{+e, +t}:
192 pick(Maybe<&2, M.Entry<K, V>>, ordering_ok(cmp(k, key(K, V, e)), inclusive), Some{e}, first_where(~K, ~V, ~cmp, k, inclusive, t))
193
194# the last entry e below k (or equal, when inclusive)
195def last_where(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +inclusive: Bool, es: List<&2, M.Entry<K, V>>, +best: Maybe<&2, M.Entry<K, V>>) -> Maybe<&2, M.Entry<K, V>>:
196 match es:
197 case Nil{}:
198 best
199 case Con{+e, t}:
200 last_where(~K, ~V, ~cmp, k, inclusive, t, pick(Maybe<&2, M.Entry<K, V>>, ordering_ok(cmp(key(K, V, e), k), inclusive), Some{e}, best))
201
202def head(-X: Data, xs: List<&2, X>) -> Maybe<&2, X>:
203 match xs:
204 case Nil{}:
205 None{}
206 case Con{x, t}:
207 Some{x}
208
209def last(-X: Data, xs: List<&2, X>) -> Maybe<&2, X>:
210 C.last(X, xs)
211
212# ceiling (higher: strict) when up, floor (lower: strict) otherwise
213def nav(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +up: Bool, +inclusive: Bool, es: List<&2, M.Entry<K, V>>) -> Maybe<&2, M.Entry<K, V>>:
214 match up:
215 case True{}:
216 first_where(~K, ~V, ~cmp, k, inclusive, es)
217 case False{}:
218 last_where(~K, ~V, ~cmp, k, inclusive, es, None{})
219
220# the key after (forward) or before k
221def succ(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +forward: Bool, es: List<&2, M.Entry<K, V>>) -> Maybe<&2, K>:
222 key_m(K, V, nav(~K, ~V, ~cmp, k, forward, False{}, es))
223
224# the first entry past a bound, in a direction
225def start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, b: M.Bound<K>, +forward: Bool, es: List<&2, M.Entry<K, V>>) -> Maybe<&2, K>:
226 match b forward:
227 case M.Unbounded{} True{}:
228 key_m(K, V, head(M.Entry<K, V>, es))
229 case M.Unbounded{} False{}:
230 key_m(K, V, last(M.Entry<K, V>, es))
231 case M.Inclusive{+x} _:
232 key_m(K, V, nav(~K, ~V, ~cmp, x, forward, True{}, es))
233 case M.Exclusive{+x} _:
234 key_m(K, V, nav(~K, ~V, ~cmp, x, forward, False{}, es))
235
236# ---- the map ----
237
238
239def size(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Nat:
240 match m:
241 case TM{+l, +es}:
242 (TM{l, es}, C.length(M.Entry<K, V>, es))
243
244def is_empty(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Bool:
245 match m:
246 case TM{+l, +es}:
247 (TM{l, es}, Nat.is_eq(C.length(M.Entry<K, V>, es), 0n))
248
249def put_new(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V) -> Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
250 pick(Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, Nat.is_lt(C.length(M.Entry<K, V>, es), C.pow2(l)), (TM{l, ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}), (TM{l, es}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}}))
251
252def put_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, old: Maybe<&2, V>) -> Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
253 match old:
254 case Some{+o}:
255 (TM{l, set_val(~K, ~V, ~cmp, k, v, es)}, Done{Some{o}})
256 case None{}:
257 put_new(~K, ~V, ~cmp, l, es, k, v)
258
259# k mapped to v: replaced when present, inserted when there is room
260def put(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, +v: V) -> Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
261 match m:
262 case TM{+l, +es}:
263 put_at(~K, ~V, ~cmp, l, es, k, v, find(~K, ~V, ~cmp, k, es))
264
265def absent_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, old: Maybe<&2, V>) -> Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
266 match old:
267 case Some{+o}:
268 (TM{l, es}, Done{Some{o}})
269 case None{}:
270 put_new(~K, ~V, ~cmp, l, es, k, v)
271
272def put_if_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, +v: V) -> Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
273 match m:
274 case TM{+l, +es}:
275 absent_at(~K, ~V, ~cmp, l, es, k, v, find(~K, ~V, ~cmp, k, es))
276
277def get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K) -> Model<K, V> & Maybe<&2, V>:
278 match m:
279 case TM{+l, +es}:
280 (TM{l, es}, find(~K, ~V, ~cmp, k, es))
281
282def or_default(-V: Data, m: Maybe<&2, V>, fallback: V) -> V:
283 match m:
284 case None{}:
285 fallback
286 case Some{v}:
287 v
288
289def get_or_default(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, fallback: V) -> Model<K, V> & V:
290 match m:
291 case TM{+l, +es}:
292 (TM{l, es}, or_default(V, find(~K, ~V, ~cmp, k, es), fallback))
293
294def contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K) -> Model<K, V> & Bool:
295 match m:
296 case TM{+l, +es}:
297 (TM{l, es}, is_some(V, find(~K, ~V, ~cmp, k, es)))
298
299def remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K) -> Model<K, V> & Maybe<&2, V>:
300 match m:
301 case TM{+l, +es}:
302 (TM{l, del(~K, ~V, ~cmp, k, es)}, find(~K, ~V, ~cmp, k, es))
303
304def replace_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, old: Maybe<&2, V>) -> Model<K, V> & Maybe<&2, V>:
305 match old:
306 case Some{+o}:
307 (TM{l, set_val(~K, ~V, ~cmp, k, v, es)}, Some{o})
308 case None{}:
309 (TM{l, es}, None{})
310
311def replace(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, +v: V) -> Model<K, V> & Maybe<&2, V>:
312 match m:
313 case TM{+l, +es}:
314 replace_at(~K, ~V, ~cmp, l, es, k, v, find(~K, ~V, ~cmp, k, es))
315
316def any_value(~K: Data, ~V: Data, ~eq: V -> V -> Bool, +w: V, es: List<&2, M.Entry<K, V>>) -> Bool:
317 match es:
318 case Nil{}:
319 False{}
320 case Con{e, t}:
321 Bool.or(eq(val(K, V, e), w), any_value(~K, ~V, ~eq, w, t))
322
323def contains_value(~K: Data, ~V: Data, ~eq: V -> V -> Bool, m: Model<K, V>, +w: V) -> Model<K, V> & Bool:
324 match m:
325 case TM{+l, +es}:
326 (TM{l, es}, any_value(~K, ~V, ~eq, w, es))
327
328def remove_if_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +expected: V, old: Maybe<&2, V>) -> Model<K, V> & Bool:
329 match old:
330 case None{}:
331 (TM{l, es}, False{})
332 case Some{o}:
333 pick(Model<K, V> & Bool, eq(o, expected), (TM{l, del(~K, ~V, ~cmp, k, es)}, True{}), (TM{l, es}, False{}))
334
335def remove_if_equal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, m: Model<K, V>, +k: K, +expected: V) -> Model<K, V> & Bool:
336 match m:
337 case TM{+l, +es}:
338 remove_if_at(~K, ~V, ~cmp, ~eq, l, es, k, expected, find(~K, ~V, ~cmp, k, es))
339
340def replace_if_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +expected: V, +replacement: V, old: Maybe<&2, V>) -> Model<K, V> & Bool:
341 match old:
342 case None{}:
343 (TM{l, es}, False{})
344 case Some{o}:
345 pick(Model<K, V> & Bool, eq(o, expected), (TM{l, set_val(~K, ~V, ~cmp, k, replacement, es)}, True{}), (TM{l, es}, False{}))
346
347def replace_if_equal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, m: Model<K, V>, +k: K, +expected: V, +replacement: V) -> Model<K, V> & Bool:
348 match m:
349 case TM{+l, +es}:
350 replace_if_at(~K, ~V, ~cmp, ~eq, l, es, k, expected, replacement, find(~K, ~V, ~cmp, k, es))
351
352def clear(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V>:
353 match m:
354 case TM{+l, es}:
355 TM{l, Nil{}}
356
357def first_entry(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Maybe<&2, M.Entry<K, V>>:
358 match m:
359 case TM{+l, +es}:
360 (TM{l, es}, head(M.Entry<K, V>, es))
361
362def last_entry(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Maybe<&2, M.Entry<K, V>>:
363 match m:
364 case TM{+l, +es}:
365 (TM{l, es}, last(M.Entry<K, V>, es))
366
367def first_key(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Maybe<&2, K>:
368 match m:
369 case TM{+l, +es}:
370 (TM{l, es}, key_m(K, V, head(M.Entry<K, V>, es)))
371
372def last_key(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Maybe<&2, K>:
373 match m:
374 case TM{+l, +es}:
375 (TM{l, es}, key_m(K, V, last(M.Entry<K, V>, es)))
376
377# lower/floor (up False) and ceiling/higher (up True) entries
378def nav_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, +up: Bool, +inclusive: Bool) -> Model<K, V> & Maybe<&2, M.Entry<K, V>>:
379 match m:
380 case TM{+l, +es}:
381 (TM{l, es}, nav(~K, ~V, ~cmp, k, up, inclusive, es))
382
383def nav_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, +up: Bool, +inclusive: Bool) -> Model<K, V> & Maybe<&2, K>:
384 match m:
385 case TM{+l, +es}:
386 (TM{l, es}, key_m(K, V, nav(~K, ~V, ~cmp, k, up, inclusive, es)))
387
388def poll_first_entry(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Maybe<&2, M.Entry<K, V>>:
389 match m:
390 case TM{+l, es}:
391 match es:
392 case Nil{}:
393 (TM{l, Nil{}}, None{})
394 case Con{e, t}:
395 (TM{l, t}, Some{e})
396
397def poll_last_entry(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Maybe<&2, M.Entry<K, V>>:
398 match m:
399 case TM{+l, +es}:
400 (TM{l, C.init(M.Entry<K, V>, es)}, last(M.Entry<K, V>, es))
401
402# ---- cursors ----
403
404
405def iterator(-K: Data, -V: Data, m: Model<K, V>) -> Cursor<K, V>:
406 match m:
407 case TM{+l, +es}:
408 CR{TM{l, es}, key_m(K, V, head(M.Entry<K, V>, es)), None{}, M.Unbounded{}, M.Unbounded{}, True{}}
409
410def descending_iterator(-K: Data, -V: Data, m: Model<K, V>) -> Cursor<K, V>:
411 match m:
412 case TM{+l, +es}:
413 CR{TM{l, es}, key_m(K, V, last(M.Entry<K, V>, es)), None{}, M.Unbounded{}, M.Unbounded{}, False{}}
414
415def next_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +current: Maybe<&2, K>, +lo: M.Bound<K>, +hi: M.Bound<K>, +forward: Bool, found: Maybe<&2, M.Entry<K, V>>) -> Cursor<K, V> & Maybe<&2, M.Entry<K, V>>:
416 match found:
417 case None{}:
418 (CR{TM{l, es}, None{}, current, lo, hi, forward}, None{})
419 case Some{M.Entry{+k, +v}}:
420 pick(Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, in_range(~K, ~cmp, k, lo, hi), (CR{TM{l, es}, succ(~K, ~V, ~cmp, k, forward, es), Some{k}, lo, hi, forward}, Some{M.Entry{k, v}}), (CR{TM{l, es}, None{}, current, lo, hi, forward}, None{}))
421
422def iterator_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, c: Cursor<K, V>) -> Cursor<K, V> & Maybe<&2, M.Entry<K, V>>:
423 match c:
424 case CR{TM{+l, +es}, next, +current, +lo, +hi, +forward}:
425 match next:
426 case None{}:
427 (CR{TM{l, es}, None{}, current, lo, hi, forward}, None{})
428 case Some{+k}:
429 next_at(~K, ~V, ~cmp, l, es, current, lo, hi, forward, find_e(~K, ~V, ~cmp, k, es))
430
431def iterator_has_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, c: Cursor<K, V>) -> Cursor<K, V> & Bool:
432 match c:
433 case CR{m, next, current, +lo, +hi, forward}:
434 match next:
435 case None{}:
436 (CR{m, None{}, current, lo, hi, forward}, False{})
437 case Some{+k}:
438 (CR{m, Some{k}, current, lo, hi, forward}, in_range(~K, ~cmp, k, lo, hi))
439
440def set_value_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, next: Maybe<&2, K>, +k: K, lo: M.Bound<K>, hi: M.Bound<K>, +forward: Bool, +v: V, old: Maybe<&2, V>) -> Cursor<K, V> & Result<&2, &2, M.Error, V>:
441 match old:
442 case None{}:
443 (CR{TM{l, es}, next, Some{k}, lo, hi, forward}, Fail{M.NoCurrent{}})
444 case Some{o}:
445 (CR{TM{l, set_val(~K, ~V, ~cmp, k, v, es)}, next, Some{k}, lo, hi, forward}, Done{o})
446
447def iterator_set_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, c: Cursor<K, V>, +v: V) -> Cursor<K, V> & Result<&2, &2, M.Error, V>:
448 match c:
449 case CR{TM{+l, +es}, next, current, lo, hi, +forward}:
450 match current:
451 case None{}:
452 (CR{TM{l, es}, next, None{}, lo, hi, forward}, Fail{M.NoCurrent{}})
453 case Some{+k}:
454 set_value_at(~K, ~V, ~cmp, l, es, next, k, lo, hi, forward, v, find(~K, ~V, ~cmp, k, es))
455
456def iterator_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, c: Cursor<K, V>) -> Cursor<K, V> & Maybe<&2, V>:
457 match c:
458 case CR{TM{+l, +es}, next, current, lo, hi, forward}:
459 match current:
460 case None{}:
461 (CR{TM{l, es}, next, None{}, lo, hi, forward}, None{})
462 case Some{+k}:
463 (CR{TM{l, del(~K, ~V, ~cmp, k, es)}, next, None{}, lo, hi, forward}, find(~K, ~V, ~cmp, k, es))
464
465def iterator_finish(-K: Data, -V: Data, c: Cursor<K, V>) -> Model<K, V>:
466 match c:
467 case CR{m, next, current, lo, hi, forward}:
468 m
469
470def key_result(-K: Data, -V: Data, r: Cursor<K, V> & Maybe<&2, M.Entry<K, V>>) -> Cursor<K, V> & Maybe<&2, K>:
471 match r:
472 case Tuple{c2, m}:
473 (c2, key_m(K, V, m))
474
475def value_result(-K: Data, -V: Data, r: Cursor<K, V> & Maybe<&2, M.Entry<K, V>>) -> Cursor<K, V> & Maybe<&2, V>:
476 match r:
477 case Tuple{c2, m}:
478 (c2, val_m(K, V, m))
479
480def iterator_next_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, c: Cursor<K, V>) -> Cursor<K, V> & Maybe<&2, K>:
481 key_result(K, V, iterator_next(~K, ~V, ~cmp, c))
482
483def iterator_next_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, c: Cursor<K, V>) -> Cursor<K, V> & Maybe<&2, V>:
484 value_result(K, V, iterator_next(~K, ~V, ~cmp, c))
485
486# ---- views ----
487
488
489def view_checked(-K: Data, -V: Data, m: Model<K, V>, lo: M.Bound<K>, hi: M.Bound<K>, valid: Bool) -> Result<&1, &1, InvalidView<K, V>, View<K, V>>:
490 match valid:
491 case True{}:
492 Done{VW{m, lo, hi, False{}}}
493 case False{}:
494 Fail{IV{m, M.InvalidBounds{}}}
495
496def sub_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +lo: M.Bound<K>, +hi: M.Bound<K>) -> Result<&1, &1, InvalidView<K, V>, View<K, V>>:
497 view_checked(K, V, m, lo, hi, bounds_valid(~K, ~cmp, lo, hi))
498
499def head_map(-K: Data, -V: Data, m: Model<K, V>, hi: M.Bound<K>) -> View<K, V>:
500 VW{m, M.Unbounded{}, hi, False{}}
501
502def tail_map(-K: Data, -V: Data, m: Model<K, V>, lo: M.Bound<K>) -> View<K, V>:
503 VW{m, lo, M.Unbounded{}, False{}}
504
505def descending_map(-K: Data, -V: Data, m: Model<K, V>) -> View<K, V>:
506 VW{m, M.Unbounded{}, M.Unbounded{}, True{}}
507
508def view_reverse(-K: Data, -V: Data, w: View<K, V>) -> View<K, V>:
509 match w:
510 case VW{m, lo, hi, +d}:
511 VW{m, lo, hi, Bool.not(d)}
512
513def view_finish(-K: Data, -V: Data, w: View<K, V>) -> Model<K, V>:
514 match w:
515 case VW{m, lo, hi, d}:
516 m
517
518def view_get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>, +k: K) -> View<K, V> & Maybe<&2, V>:
519 match w:
520 case VW{TM{+l, +es}, +lo, +hi, +d}:
521 (VW{TM{l, es}, lo, hi, d}, pick(Maybe<&2, V>, in_range(~K, ~cmp, k, lo, hi), find(~K, ~V, ~cmp, k, es), None{}))
522
523def contained(-K: Data, -V: Data, r: View<K, V> & Maybe<&2, V>) -> View<K, V> & Bool:
524 match r:
525 case Tuple{w2, m}:
526 (w2, is_some(V, m))
527
528def view_contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>, +k: K) -> View<K, V> & Bool:
529 contained(K, V, view_get(~K, ~V, ~cmp, w, k))
530
531def rewrap_put(-K: Data, -V: Data, lo: M.Bound<K>, hi: M.Bound<K>, +d: Bool, r: Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>) -> View<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
532 match r:
533 case Tuple{m2, x}:
534 (VW{m2, lo, hi, d}, x)
535
536def view_put_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, +v: V, lo: M.Bound<K>, hi: M.Bound<K>, +d: Bool, valid: Bool) -> View<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
537 match valid:
538 case True{}:
539 rewrap_put(K, V, lo, hi, d, put(~K, ~V, ~cmp, m, k, v))
540 case False{}:
541 (VW{m, lo, hi, d}, Fail{M.Rejected{M.OutOfRange{}, k, v}})
542
543def view_put(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>, +k: K, +v: V) -> View<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
544 match w:
545 case VW{m, +lo, +hi, +d}:
546 view_put_at(~K, ~V, ~cmp, m, k, v, lo, hi, d, in_range(~K, ~cmp, k, lo, hi))
547
548def rewrap_val(-K: Data, -V: Data, lo: M.Bound<K>, hi: M.Bound<K>, +d: Bool, r: Model<K, V> & Maybe<&2, V>) -> View<K, V> & Maybe<&2, V>:
549 match r:
550 case Tuple{m2, x}:
551 (VW{m2, lo, hi, d}, x)
552
553def view_remove_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, lo: M.Bound<K>, hi: M.Bound<K>, +d: Bool, valid: Bool) -> View<K, V> & Maybe<&2, V>:
554 match valid:
555 case True{}:
556 rewrap_val(K, V, lo, hi, d, remove(~K, ~V, ~cmp, m, k))
557 case False{}:
558 (VW{m, lo, hi, d}, None{})
559
560def view_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>, +k: K) -> View<K, V> & Maybe<&2, V>:
561 match w:
562 case VW{m, +lo, +hi, +d}:
563 view_remove_at(~K, ~V, ~cmp, m, k, lo, hi, d, in_range(~K, ~cmp, k, lo, hi))
564
565def view_size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>) -> View<K, V> & Nat:
566 match w:
567 case VW{TM{+l, +es}, +lo, +hi, +d}:
568 (VW{TM{l, es}, lo, hi, d}, C.length(M.Entry<K, V>, within(~K, ~V, ~cmp, lo, hi, es)))
569
570def view_clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>) -> View<K, V>:
571 match w:
572 case VW{TM{+l, +es}, +lo, +hi, +d}:
573 VW{TM{l, outside(~K, ~V, ~cmp, lo, hi, es)}, lo, hi, d}
574
575# the view's first (or last) entry in its own direction
576def view_extreme(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>, +first: Bool) -> View<K, V> & Maybe<&2, M.Entry<K, V>>:
577 match w:
578 case VW{TM{+l, +es}, +lo, +hi, +d}:
579 (VW{TM{l, es}, lo, hi, d}, pick(Maybe<&2, M.Entry<K, V>>, pick(Bool, d, Bool.not(first), first), head(M.Entry<K, V>, within(~K, ~V, ~cmp, lo, hi, es)), last(M.Entry<K, V>, within(~K, ~V, ~cmp, lo, hi, es))))
580
581def view_first_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>) -> View<K, V> & Maybe<&2, M.Entry<K, V>>:
582 view_extreme(~K, ~V, ~cmp, w, True{})
583
584def view_last_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>) -> View<K, V> & Maybe<&2, M.Entry<K, V>>:
585 view_extreme(~K, ~V, ~cmp, w, False{})
586
587# the view's lower/floor (higher False) or ceiling/higher (higher True)
588# entry, in the view's own direction
589def view_nav(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>, +k: K, +higher: Bool, +inclusive: Bool) -> View<K, V> & Maybe<&2, M.Entry<K, V>>:
590 match w:
591 case VW{TM{+l, +es}, +lo, +hi, +d}:
592 (VW{TM{l, es}, lo, hi, d}, nav(~K, ~V, ~cmp, k, pick(Bool, d, Bool.not(higher), higher), inclusive, within(~K, ~V, ~cmp, lo, hi, es)))
593
594def view_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>) -> Cursor<K, V>:
595 match w:
596 case VW{TM{+l, +es}, +lo, +hi, +d}:
597 CR{TM{l, es}, start(~K, ~V, ~cmp, pick(M.Bound<K>, d, hi, lo), Bool.not(d), es), None{}, lo, hi, Bool.not(d)}
598
599# the map's invariant: consecutive keys strictly increasing (SPARK's ordered
600# maps keep Keys (Container) sorted; Formal_Ordered_Maps, Formal_Model.K)
601def ordered(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, es: List<&2, M.Entry<K, V>>) -> Bool:
602 match es:
603 case Nil{}:
604 True{}
605 case Con{e, t}:
606 match t:
607 case Nil{}:
608 True{}
609 case Con{+e2, +u}:
610 Bool.and(Cmp.is_lt(cmp(key(K, V, e), key(K, V, e2))), ordered(~K, ~V, ~cmp, Con{e2, u}))
611
612# ---- contract (SPARK formal containers) ----
613# Each `<Subprogram>.<clause>` definition below states one Post clause of
614# that SPARK subprogram, as a proposition on this model; the table names the
615# clauses. proofs/containers/balanced_search_tree/ proves every clause under its clause name,
616# and its `impl` lemma carries them to the implementation.
617#
618# Contracts of the TreeMap in the style of SPARK's formal ordered maps
619# (SPARKlib src/full/spark-containers-formal-ordered_maps.ads, AdaCore/
620# SPARKlib master), stated on the independent model (this file: a limit and
621# the entries in key order). The refinement proof (proof.bend, api/capi/
622# vapi) shows the implementation returns exactly the model's result for
623# every operation, so each clause holds of the implementation.
624# Model (K) = S.find (K, es); keys are compared by ~cmp, a total order
625# (O.Order: flip, antisymmetry, transitivity); the entries are ordered
626# (ST.ordered), which is the model's invariant.
627#
628# SPARK subprogram (.ads line) ours clauses
629# Empty_Map (101) new new_empty
630# Length (114), Is_Empty (425) size, is_empty size_value, is_empty_value
631# Clear (433) clear clear_empty
632# Element (Key) (1283), Find (1257) get, get_or_default get_value, get_or_default_value
633# Contains (1332) contains_key contains_value
634# Include (754) put put_present, put_absent, put_full,
635# put_found_present, put_found_absent,
636# find_set_other, find_ins_other (others unchanged),
637# set_length, ins_length
638# Insert (612/697, keeps a present key) put_if_absent put_if_absent_present, put_if_absent_absent
639# Replace (846) replace replace_present, replace_absent,
640# find_set_same, find_set_other
641# Exclude (884) / Delete (937) remove remove_present, remove_absent,
642# find_del_same (gone), find_del_other, del_length
643# First/First_Element/First_Key (1116-1137) first_value
644# Last/Last_Element/Last_Key (1148-1171) last_value
645# Floor (1291), Ceiling (1312) floor/ceiling/lower/higher (key, entry) nav_value
646# Delete_First (1037), Delete_Last (1077) poll_first/last_entry (model: S.poll_*; refinement: proof.bend)
647# Not in this API: "=", Assign/Copy/Move, Reference, Replace_Element and
648# Key/Element/Next/Previous by cursor (the map's cursors are its iterators,
649# whose steps the refinement proof relates to S.succ), Has_Element.
650
651# Include (754)
652def Include.find_ins_other(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +q: K, +hq: {is_eq(cmp(q, k)) == False{} : Bool}, +es: List<&2, M.Entry<K, V>>) -> Type:
653 {find_e(~K, ~V, ~cmp, q, ins(~K, ~V, ~cmp, k, v, es)) == find_e(~K, ~V, ~cmp, q, es) : Maybe<&2, M.Entry<K, V>>}
654
655# Include (754)
656def Include.ins_length(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +es: List<&2, M.Entry<K, V>>) -> Type:
657 {C.length(M.Entry<K, V>, ins(~K, ~V, ~cmp, k, v, es)) == 1n+C.length(M.Entry<K, V>, es) : Nat}
658
659# Replace (846)
660def Replace.find_set_same(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +e0: M.Entry<K, V>, +es: List<&2, M.Entry<K, V>>, +hp: {find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> Type:
661 {find(~K, ~V, ~cmp, k, set_val(~K, ~V, ~cmp, k, v, es)) == Some{v} : Maybe<&2, V>}
662
663# Include (754)
664def Include.find_set_other(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +v: V, +q: K, +hq: {is_eq(cmp(q, k)) == False{} : Bool}, +es: List<&2, M.Entry<K, V>>) -> Type:
665 {find_e(~K, ~V, ~cmp, q, set_val(~K, ~V, ~cmp, k, v, es)) == find_e(~K, ~V, ~cmp, q, es) : Maybe<&2, M.Entry<K, V>>}
666
667# Include (754)
668def Include.set_length(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +es: List<&2, M.Entry<K, V>>) -> Type:
669 {C.length(M.Entry<K, V>, set_val(~K, ~V, ~cmp, k, v, es)) == C.length(M.Entry<K, V>, es) : Nat}
670
671# Exclude (884) / Delete (937)
672def Exclude.find_del_other(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +q: K, +hq: {is_eq(cmp(q, k)) == False{} : Bool}, +es: List<&2, M.Entry<K, V>>) -> Type:
673 {find_e(~K, ~V, ~cmp, q, del(~K, ~V, ~cmp, k, es)) == find_e(~K, ~V, ~cmp, q, es) : Maybe<&2, M.Entry<K, V>>}
674
675# Exclude (884) / Delete (937)
676def Exclude.find_del_same(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +es: List<&2, M.Entry<K, V>>, +hord: {ordered(~K, ~V, ~cmp, es) == True{} : Bool}) -> Type:
677 {find_e(~K, ~V, ~cmp, k, del(~K, ~V, ~cmp, k, es)) == None{} : Maybe<&2, M.Entry<K, V>>}
678
679# Exclude (884) / Delete (937)
680def Exclude.del_length(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +e0: M.Entry<K, V>, +es: List<&2, M.Entry<K, V>>, +hp: {find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> Type:
681 {1n+C.length(M.Entry<K, V>, del(~K, ~V, ~cmp, k, es)) == C.length(M.Entry<K, V>, es) : Nat}
682
683# Empty_Map (101)
684def Empty_Map.new_empty(-K: Data, -V: Data) -> Type:
685 {new(K, V) == TM{31n, Nil{}} : Model<K, V>}
686
687# Length (114), Is_Empty (425)
688def Length.size_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> Type:
689 {size(K, V, TM{l, es}) == (TM{l, es}, C.length(M.Entry<K, V>, es)) : Model<K, V> & Nat}
690
691# Length (114), Is_Empty (425)
692def Length.is_empty_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> Type:
693 {is_empty(K, V, TM{l, es}) == (TM{l, es}, Nat.is_eq(C.length(M.Entry<K, V>, es), 0n)) : Model<K, V> & Bool}
694
695# Clear (433)
696def Clear.clear_empty(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> Type:
697 {clear(K, V, TM{l, es}) == TM{l, Nil{}} : Model<K, V>}
698
699# Element (Key) (1283), Find (1257)
700def Element.get_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K) -> Type:
701 {get(~K, ~V, ~cmp, TM{l, es}, k) == (TM{l, es}, find(~K, ~V, ~cmp, k, es)) : Model<K, V> & Maybe<&2, V>}
702
703# Element (Key) (1283), Find (1257)
704def Element.get_or_default_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +d: V) -> Type:
705 {get_or_default(~K, ~V, ~cmp, TM{l, es}, k, d) == (TM{l, es}, or_default(V, find(~K, ~V, ~cmp, k, es), d)) : Model<K, V> & V}
706
707# Contains (1332)
708def Contains.contains_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K) -> Type:
709 {contains_key(~K, ~V, ~cmp, TM{l, es}, k) == (TM{l, es}, is_some(V, find(~K, ~V, ~cmp, k, es))) : Model<K, V> & Bool}
710
711# Include (754)
712def Include.put_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +e0: M.Entry<K, V>, +hp: {find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> Type:
713 {put(~K, ~V, ~cmp, TM{l, es}, k, v) == (TM{l, set_val(~K, ~V, ~cmp, k, v, es)}, Done{Some{val(K, V, e0)}}) : Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
714
715# Include (754)
716def Include.put_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +ha: {find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}, +hr: {Nat.is_lt(C.length(M.Entry<K, V>, es), C.pow2(l)) == True{} : Bool}) -> Type:
717 {put(~K, ~V, ~cmp, TM{l, es}, k, v) == (TM{l, ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}) : Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
718
719# Include (754)
720def Include.put_full(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +ha: {find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}, +hr: {Nat.is_lt(C.length(M.Entry<K, V>, es), C.pow2(l)) == False{} : Bool}) -> Type:
721 {put(~K, ~V, ~cmp, TM{l, es}, k, v) == (TM{l, es}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}}) : Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
722
723# Include (754)
724def Include.put_found_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +e0: M.Entry<K, V>, +hp: {find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> Type:
725 {find(~K, ~V, ~cmp, k, set_val(~K, ~V, ~cmp, k, v, es)) == Some{v} : Maybe<&2, V>}
726
727# Include (754)
728def Include.put_found_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +ha: {find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}) -> Type:
729 {find(~K, ~V, ~cmp, k, ins(~K, ~V, ~cmp, k, v, es)) == Some{v} : Maybe<&2, V>}
730
731# Insert (612/697, keeps a present key) put_if_absent
732def Insert.put_if_absent_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +e0: M.Entry<K, V>, +hp: {find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> Type:
733 {put_if_absent(~K, ~V, ~cmp, TM{l, es}, k, v) == (TM{l, es}, Done{Some{val(K, V, e0)}}) : Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
734
735# Insert (612/697, keeps a present key) put_if_absent
736def Insert.put_if_absent_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +ha: {find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}, +hr: {Nat.is_lt(C.length(M.Entry<K, V>, es), C.pow2(l)) == True{} : Bool}) -> Type:
737 {put_if_absent(~K, ~V, ~cmp, TM{l, es}, k, v) == (TM{l, ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}) : Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
738
739# Replace (846)
740def Replace.replace_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +e0: M.Entry<K, V>, +hp: {find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> Type:
741 {replace(~K, ~V, ~cmp, TM{l, es}, k, v) == (TM{l, set_val(~K, ~V, ~cmp, k, v, es)}, Some{val(K, V, e0)}) : Model<K, V> & Maybe<&2, V>}
742
743# Replace (846)
744def Replace.replace_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +ha: {find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}) -> Type:
745 {replace(~K, ~V, ~cmp, TM{l, es}, k, v) == (TM{l, es}, None{}) : Model<K, V> & Maybe<&2, V>}
746
747# Exclude (884) / Delete (937)
748def Exclude.remove_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +e0: M.Entry<K, V>, +hp: {find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> Type:
749 {remove(~K, ~V, ~cmp, TM{l, es}, k) == (TM{l, del(~K, ~V, ~cmp, k, es)}, Some{val(K, V, e0)}) : Model<K, V> & Maybe<&2, V>}
750
751# Exclude (884) / Delete (937)
752def Exclude.remove_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +ha: {find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}) -> Type:
753 {remove(~K, ~V, ~cmp, TM{l, es}, k) == (TM{l, es}, None{}) : Model<K, V> & Maybe<&2, V>}
754
755# First/First_Element/First_Key (1116-1137)
756def First.first_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> Type:
757 {first_entry(K, V, TM{l, es}) == (TM{l, es}, head(M.Entry<K, V>, es)) : Model<K, V> & Maybe<&2, M.Entry<K, V>>}
758
759# Last/Last_Element/Last_Key (1148-1171)
760def Last.last_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> Type:
761 {last_entry(K, V, TM{l, es}) == (TM{l, es}, last(M.Entry<K, V>, es)) : Model<K, V> & Maybe<&2, M.Entry<K, V>>}
762
763# Floor (1291), Ceiling (1312)
764def Floor.nav_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +up: Bool, +inclusive: Bool) -> Type:
765 {nav_entry(~K, ~V, ~cmp, TM{l, es}, k, up, inclusive) == (TM{l, es}, nav(~K, ~V, ~cmp, k, up, inclusive, es)) : Model<K, V> & Maybe<&2, M.Entry<K, V>>}