1	import Base
2	import ../../lib/common.bend as C
3	import ../../../src/containers/balanced_search_tree.bend as M
4	import ../../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	
13	type Model<-K: Data, -V: Data> is Data:
14	  TM{limit: Nat, es: List<&2, M.Entry<K, V>>}
15	
16	type 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	
19	type View<-K: Data, -V: Data> is Data:
20	  VW{map: Model<K, V>, lower: M.Bound<K>, upper: M.Bound<K>, descending: Bool}
21	
22	type InvalidView<-K: Data, -V: Data> is Data:
23	  IV{map: Model<K, V>, error: M.Error}
24	
25	def pick(-T: Type, +b: Bool, x: T, y: T) -> T:
26	  match b:
27	    case True{}:
28	      x
29	    case False{}:
30	      y
31	
32	def new(-K: Data, -V: Data) -> Model<K, V>:
33	  TM{31n, Nil{}}
34	
35	def with_limit(-K: Data, -V: Data, +k: Nat) -> Model<K, V>:
36	  TM{pick(Nat, Nat.is_lt(k, 31n), k, 31n), Nil{}}
37	
38	def key(-K: Data, -V: Data, e: M.Entry<K, V>) -> K:
39	  match e:
40	    case M.Entry{k, v}:
41	      k
42	
43	def val(-K: Data, -V: Data, e: M.Entry<K, V>) -> V:
44	  match e:
45	    case M.Entry{k, v}:
46	      v
47	
48	def 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	
55	def 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
65	def 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	
72	def 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	
79	def 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	
86	def 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	
89	def 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
99	def 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)
107	def 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
115	def 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	
124	def 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	
133	def 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	
142	def 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	
151	def 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
155	def 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	
170	def 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	
177	def 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))
187	def 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)
195	def 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	
202	def 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	
209	def 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
213	def 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
221	def 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
225	def 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	
239	def 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	
244	def 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	
249	def 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	
252	def 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
260	def 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	
265	def 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	
272	def 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	
277	def 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	
282	def 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	
289	def 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	
294	def 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	
299	def 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	
304	def 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	
311	def 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	
316	def 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	
323	def 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	
328	def 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	
335	def 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	
340	def 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	
347	def 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	
352	def 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	
357	def 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	
362	def 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	
367	def 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	
372	def 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
378	def 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	
383	def 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	
388	def 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	
397	def 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	
405	def 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	
410	def 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	
415	def 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	
422	def 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	
431	def 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	
440	def 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	
447	def 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	
456	def 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	
465	def 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	
470	def 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	
475	def 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	
480	def 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	
483	def 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	
489	def 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	
496	def 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	
499	def 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	
502	def 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	
505	def descending_map(-K: Data, -V: Data, m: Model<K, V>) -> View<K, V>:
506	  VW{m, M.Unbounded{}, M.Unbounded{}, True{}}
507	
508	def 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	
513	def 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	
518	def 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	
523	def 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	
528	def 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	
531	def 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	
536	def 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	
543	def 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	
548	def 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	
553	def 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	
560	def 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	
565	def 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	
570	def 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
576	def 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	
581	def 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	
584	def 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
589	def 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	
594	def 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)
601	def 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)
652	def 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)
656	def 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)
660	def 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)
664	def 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)
668	def 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)
672	def 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)
676	def 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)
680	def 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)
684	def 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)
688	def 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)
692	def 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)
696	def 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)
700	def 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)
704	def 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)
708	def 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)
712	def 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)
716	def 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)
720	def 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)
724	def 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)
728	def 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
732	def 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
736	def 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)
740	def 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)
744	def 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)
748	def 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)
752	def 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)
756	def 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)
760	def 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)
764	def 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>>}