1	import Base
2	import ../math/hash.bend as HS
3	
4	# A String-keyed hash table with Base.Map's shape of API:
5	#
6	#   new(a, V)                   -> HashMap<a, V>
7	#   set(a, V, m, key, x)        -> HashMap<a, V>              insert or replace
8	#   get(V, d, m, key)           -> HashMap<&2, V> & V         d when absent (V: Data)
9	#   has(a, V, m, key)           -> HashMap<a, V> & Bool
10	#   pop(a, V, m, key)           -> HashMap<a, V> & Maybe<a, V>
11	#   del(a, V, m, key)           -> HashMap<a, V>
12	#   size(a, V, m)               -> HashMap<a, V> & U32
13	#   keys(a, V, m)               -> HashMap<a, V> & List<&2, String>   (bucket order)
14	#
15	# The table owns arrays, so it is a Type and is threaded through every call.
16	#
17	# Layout:
18	#   - buckets: one packed Array<U32> of (check word, slot link) pairs; open
19	#     addressing with linear probing over a power-of-two number of buckets,
20	#     load <= 1/2, backward-shift deletion (no tombstones);
21	#   - entries: a dense slot arena (key `ks`, value `vs`), with a free list of
22	#     removed slots chained through `nx`. Growing the buckets rehashes U32
23	#     pairs only; keys and values never move.
24	# A one-character key (code < 2^31) has check word code | 2^31: equal words
25	# mean equal keys, so its String is never hashed, compared or stored (its
26	# `ks` cell holds SNil and `keys` rebuilds it). Any other key has check word
27	# (hash & (2^31 - 1)) | 1, confirmed by a String comparison. Links are
28	# slot + 1 (0 = none). Every String walk is a tail loop, and nothing boxed is
29	# shared with `+`.
30	
31	type HashMap<a, -V: Kind(a)> is Type:
32	  HM{n: U32, mask: U32, td: U32, fresh: U32, ssz: U32, sd: U32, free: U32, tab: Array<U32>, ks: Array<String>, vs: Array<Maybe<a, V>>, nx: Array<U32>}
33	
34	def size(a, -V: Kind(a), m: HashMap<a, V>) -> HashMap<a, V> & U32:
35	  HM{+n, mask, td, fresh, sz, sd, free, tab, ks, vs, nx} = m
36	  (HM{n, mask, td, fresh, sz, sd, free, tab, ks, vs, nx}, n)
37	
38	# ---- words, hashing, equality ----
39	
40	def tag() -> U32:
41	  2147483648
42	
43	def bnext(+i: U32, +mask: U32) -> U32:
44	  U32.and(U32.inc(i), mask)
45	
46	def link(+s: U32) -> U32:
47	  U32.inc(s)
48	
49	def slot(+l: U32) -> U32:
50	  U32.sub(l, 1)
51	
52	def short_word(+c: U32) -> U32:
53	  U32.or(c, tag())
54	
55	def long_word(+h: U32) -> U32:
56	  U32.or(U32.and(h, 2147483647), 1)
57	
58	def is_short(+w: U32) -> Bool:
59	  U32.is_ge(w, tag())
60	
61	def rev_onto(s: String, acc: String) -> String:
62	  match s:
63	    case SNil{}:
64	      acc
65	    case SCon{h, t}:
66	      rev_onto(t, SCon{h, acc})
67	
68	def hash_acc(s: String, +h: U32, acc: String) -> String & U32:
69	  match s:
70	    case SNil{}:
71	      (rev_onto(acc, SNil{}), h)
72	    case SCon{Chr{+c}, t}:
73	      hash_acc(t, HS.mix(h, c), SCon{Chr{c}, acc})
74	
75	def eq_acc(a: String, b: String, ra: String, rb: String, +e: Bool) -> (String & String) & Bool:
76	  match a b:
77	    case SNil{} SNil{}:
78	      ((rev_onto(ra, SNil{}), rev_onto(rb, SNil{})), e)
79	    case SNil{} SCon{h, t}:
80	      ((rev_onto(ra, SNil{}), rev_onto(rb, SCon{h, t})), False{})
81	    case SCon{h, t} SNil{}:
82	      ((rev_onto(ra, SCon{h, t}), rev_onto(rb, SNil{})), False{})
83	    case SCon{Chr{+x}, ta} SCon{Chr{+y}, tb}:
84	      eq_acc(ta, tb, SCon{Chr{x}, ra}, SCon{Chr{y}, rb}, Bool.and(e, U32.is_eq(x, y)))
85	
86	# String equality, handing both strings back.
87	def eq(a: String, b: String) -> (String & String) & Bool:
88	  eq_acc(a, b, SNil{}, SNil{}, True{})
89	
90	def copy_acc(s: String, ra: String, rb: String) -> String & String:
91	  match s:
92	    case SNil{}:
93	      (rev_onto(ra, SNil{}), rev_onto(rb, SNil{}))
94	    case SCon{Chr{+c}, t}:
95	      copy_acc(t, SCon{Chr{c}, ra}, SCon{Chr{c}, rb})
96	
97	# A deep copy (sharing a String with `+` would refcount every String).
98	def str_copy(s: String) -> String & String:
99	  copy_acc(s, SNil{}, SNil{})
100	
101	def lw_fin(r: String & U32) -> String & U32:
102	  (k, +h) = r
103	  (k, long_word(h))
104	
105	def key_long(key: String) -> String & U32:
106	  lw_fin(hash_acc(key, 0, SNil{}))
107	
108	# ---- probing ----
109	
110	type Found is Type:
111	  FD{tab: Array<U32>, ks: Array<String>, key: String, at: U32, link: U32}
112	
113	# Long keys: a matching word is confirmed against the slot's stored String.
114	type Step is Type:
115	  SEnd{tab: Array<U32>, ks: Array<String>, key: String}
116	  SHit{tab: Array<U32>, ks: Array<String>, key: String, l: U32}
117	  SNext{tab: Array<U32>, ks: Array<String>, key: String}
118	
119	def sk_pick(tab: Array<U32>, +l: U32, ks: Array<String>, key: String, e: Bool) -> Step:
120	  match e:
121	    case True{}:
122	      SHit{tab, ks, key, l}
123	    case False{}:
124	      SNext{tab, ks, key}
125	
126	def sk_fin(tab: Array<U32>, +l: U32, ks: Array<String>, r: (String & String) & Bool) -> Step:
127	  ((key, k), e) = r
128	  sk_pick(tab, l, Array.set(String, ks, slot(l), k), key, e)
129	
130	def sk_cmp(tab: Array<U32>, +l: U32, key: String, r: Array<String> & String) -> Step:
131	  (ks, k) = r
132	  sk_fin(tab, l, ks, eq(key, k))
133	
134	def sk_same(tab: Array<U32>, ks: Array<String>, +l: U32, key: String, same: Bool) -> Step:
135	  match same:
136	    case False{}:
137	      SNext{tab, ks, key}
138	    case True{}:
139	      sk_cmp(tab, l, key, Array.swap(String, ks, slot(l), SNil{}))
140	
141	def sk_l(ks: Array<String>, key: String, +x: U32, +w: U32, r: Array<U32> & U32) -> Step:
142	  (tab, +l) = r
143	  sk_same(tab, ks, l, key, U32.is_eq(x, w))
144	
145	def sk_empty(tab: Array<U32>, ks: Array<String>, +i: U32, key: String, +w: U32, +x: U32, e: Bool) -> Step:
146	  match e:
147	    case True{}:
148	      SEnd{tab, ks, key}
149	    case False{}:
150	      sk_l(ks, key, x, w, Array.get(U32, tab, U32.inc(U32.shl(i))))
151	
152	def sk_w(ks: Array<String>, +i: U32, key: String, +w: U32, r: Array<U32> & U32) -> Step:
153	  (tab, +x) = r
154	  sk_empty(tab, ks, i, key, w, x, U32.is_eq(x, 0))
155	
156	def step(tab: Array<U32>, ks: Array<String>, +i: U32, key: String, +w: U32) -> Step:
157	  sk_w(ks, i, key, w, Array.get(U32, tab, U32.shl(i)))
158	
159	def find(fuel: Nat, s: Step, +mask: U32, +w: U32, +i: U32) -> Found:
160	  match fuel s:
161	    case 0n SEnd{tab, ks, key}:
162	      FD{tab, ks, key, i, 0}
163	    case 0n SHit{tab, ks, key, +l}:
164	      FD{tab, ks, key, i, l}
165	    case 0n SNext{tab, ks, key}:
166	      FD{tab, ks, key, i, 0}
167	    case 1n+p SEnd{tab, ks, key}:
168	      FD{tab, ks, key, i, 0}
169	    case 1n+p SHit{tab, ks, key, +l}:
170	      FD{tab, ks, key, i, l}
171	    case 1n+p SNext{tab, ks, key}:
172	      +j = bnext(i, mask)
173	      find(p, step(tab, ks, j, key, w), mask, w, j)
174	
175	def probe_lw(tab: Array<U32>, ks: Array<String>, +mask: U32, r: String & U32) -> Found & U32:
176	  (key, +w) = r
177	  (find(U32.to_nat(U32.inc(mask)), step(tab, ks, HS.bucket(w, mask), key, w), mask, w, HS.bucket(w, mask)), w)
178	
179	def probe_long(tab: Array<U32>, ks: Array<String>, +mask: U32, key: String) -> Found & U32:
180	  probe_lw(tab, ks, mask, key_long(key))
181	
182	# One-character keys: the bucket words alone decide.
183	type QStep is Type:
184	  QEnd{tab: Array<U32>}
185	  QHit{tab: Array<U32>, l: U32}
186	  QNext{tab: Array<U32>}
187	
188	def qs_l(r: Array<U32> & U32) -> QStep:
189	  (tab, +l) = r
190	  QHit{tab, l}
191	
192	def qs_same(tab: Array<U32>, +i: U32, same: Bool) -> QStep:
193	  match same:
194	    case True{}:
195	      qs_l(Array.get(U32, tab, U32.inc(U32.shl(i))))
196	    case False{}:
197	      QNext{tab}
198	
199	def qs_if(tab: Array<U32>, +i: U32, +w: U32, +x: U32, e: Bool) -> QStep:
200	  match e:
201	    case True{}:
202	      QEnd{tab}
203	    case False{}:
204	      qs_same(tab, i, U32.is_eq(x, w))
205	
206	def qs_w(+i: U32, +w: U32, r: Array<U32> & U32) -> QStep:
207	  (tab, +x) = r
208	  qs_if(tab, i, w, x, U32.is_eq(x, 0))
209	
210	def qstep(tab: Array<U32>, +i: U32, +w: U32) -> QStep:
211	  qs_w(i, w, Array.get(U32, tab, U32.shl(i)))
212	
213	type QFound is Type:
214	  QF{tab: Array<U32>, at: U32, link: U32}
215	
216	def qfind(fuel: Nat, s: QStep, +mask: U32, +w: U32, +i: U32) -> QFound:
217	  match fuel s:
218	    case 0n QEnd{tab}:
219	      QF{tab, i, 0}
220	    case 0n QHit{tab, +l}:
221	      QF{tab, i, l}
222	    case 0n QNext{tab}:
223	      QF{tab, i, 0}
224	    case 1n+p QEnd{tab}:
225	      QF{tab, i, 0}
226	    case 1n+p QHit{tab, +l}:
227	      QF{tab, i, l}
228	    case 1n+p QNext{tab}:
229	      +j = bnext(i, mask)
230	      qfind(p, qstep(tab, j, w), mask, w, j)
231	
232	def q_fin(ks: Array<String>, +w: U32, r: QFound) -> Found & U32:
233	  QF{tab, +at, +l} = r
234	  (FD{tab, ks, SNil{}, at, l}, w)
235	
236	def probe_short(tab: Array<U32>, ks: Array<String>, +mask: U32, +c: U32, ok: Bool) -> Found & U32:
237	  match ok:
238	    case True{}:
239	      q_fin(ks, short_word(c), qfind(U32.to_nat(U32.inc(mask)), qstep(tab, HS.bucket(short_word(c), mask), short_word(c)), mask, short_word(c), HS.bucket(short_word(c), mask)))
240	    case False{}:
241	      probe_long(tab, ks, mask, SCon{Chr{c}, SNil{}})
242	
243	def probe_c(tab: Array<U32>, ks: Array<String>, +mask: U32, +c: U32, t: String) -> Found & U32:
244	  match t:
245	    case SNil{}:
246	      probe_short(tab, ks, mask, c, U32.is_lt(c, tag()))
247	    case SCon{d, t2}:
248	      probe_long(tab, ks, mask, SCon{Chr{c}, SCon{d, t2}})
249	
250	# The bucket holding key (link != 0) or the empty bucket ending its probe,
251	# the key as it would be stored (SNil for a one-character key), and its word.
252	def probe(tab: Array<U32>, ks: Array<String>, +mask: U32, key: String) -> Found & U32:
253	  match key:
254	    case SNil{}:
255	      probe_long(tab, ks, mask, SNil{})
256	    case SCon{Chr{+c}, t}:
257	      probe_c(tab, ks, mask, c, t)
258	
259	# ---- buckets: placement without comparison, growth, backward shift ----
260	
261	def put_bucket(tab: Array<U32>, +i: U32, +w: U32, +l: U32) -> Array<U32>:
262	  Array.set(U32, Array.set(U32, tab, U32.shl(i), w), U32.inc(U32.shl(i)), l)
263	
264	type RStep is Type:
265	  REmpty{tab: Array<U32>}
266	  RFull{tab: Array<U32>}
267	
268	def rs_if(tab: Array<U32>, e: Bool) -> RStep:
269	  match e:
270	    case True{}:
271	      REmpty{tab}
272	    case False{}:
273	      RFull{tab}
274	
275	def rs_w(r: Array<U32> & U32) -> RStep:
276	  (tab, +x) = r
277	  rs_if(tab, U32.is_eq(x, 0))
278	
279	def rstep(tab: Array<U32>, +i: U32) -> RStep:
280	  rs_w(Array.get(U32, tab, U32.shl(i)))
281	
282	def ins_go(fuel: Nat, s: RStep, +mask: U32, +i: U32, +w: U32, +l: U32) -> Array<U32>:
283	  match fuel s:
284	    case 0n REmpty{tab}:
285	      tab
286	    case 0n RFull{tab}:
287	      tab
288	    case 1n+p REmpty{tab}:
289	      put_bucket(tab, i, w, l)
290	    case 1n+p RFull{tab}:
291	      +j = bnext(i, mask)
292	      ins_go(p, rstep(tab, j), mask, j, w, l)
293	
294	# Put (w, l) in the first empty bucket of w's probe.
295	def ins_raw(tab: Array<U32>, +mask: U32, +w: U32, +l: U32) -> Array<U32>:
296	  ins_go(U32.to_nat(U32.inc(mask)), rstep(tab, HS.bucket(w, mask)), mask, HS.bucket(w, mask), w, l)
297	
298	type Mv is Type:
299	  MV{old: Array<U32>, nt: Array<U32>}
300	
301	def mv_l(+w: U32, nt: Array<U32>, +nmask: U32, r: Array<U32> & U32) -> Mv:
302	  (old, +l) = r
303	  MV{old, ins_raw(nt, nmask, w, l)}
304	
305	def mv_if(+k: U32, old: Array<U32>, nt: Array<U32>, +nmask: U32, +w: U32, e: Bool) -> Mv:
306	  match e:
307	    case True{}:
308	      MV{old, nt}
309	    case False{}:
310	      mv_l(w, nt, nmask, Array.get(U32, old, U32.inc(U32.shl(k))))
311	
312	def mv_w(+k: U32, nt: Array<U32>, +nmask: U32, r: Array<U32> & U32) -> Mv:
313	  (old, +w) = r
314	  mv_if(k, old, nt, nmask, w, U32.is_eq(w, 0))
315	
316	def mv_step(+k: U32, +nmask: U32, m: Mv) -> Mv:
317	  MV{old, nt} = m
318	  mv_w(k, nt, nmask, Array.get(U32, old, U32.shl(k)))
319	
320	def mv_go(fuel: Nat, +k: U32, +nmask: U32, m: Mv) -> Mv:
321	  match fuel:
322	    case 0n:
323	      m
324	    case 1n+p:
325	      mv_go(p, U32.inc(k), nmask, mv_step(k, nmask, m))
326	
327	def mv_fin(m: Mv) -> Array<U32>:
328	  MV{old, nt} = m
329	  nt
330	
331	def clear_bucket(tab: Array<U32>, +i: U32) -> Array<U32>:
332	  put_bucket(tab, i, 0, 0)
333	
334	type Sh is Type:
335	  HEnd{tab: Array<U32>}
336	  HMove{tab: Array<U32>, w: U32, l: U32}
337	  HSkip{tab: Array<U32>}
338	
339	def sh_mv(tab: Array<U32>, +w: U32, +l: U32, mv: Bool) -> Sh:
340	  match mv:
341	    case True{}:
342	      HMove{tab, w, l}
343	    case False{}:
344	      HSkip{tab}
345	
346	def sh_l(+w: U32, +mask: U32, +i: U32, +k: U32, r: Array<U32> & U32) -> Sh:
347	  (tab, +l) = r
348	  sh_mv(tab, w, l, U32.is_ge(U32.and(U32.sub(k, HS.bucket(w, mask)), mask), U32.and(U32.sub(k, i), mask)))
349	
350	def sh_if(tab: Array<U32>, +mask: U32, +i: U32, +k: U32, +w: U32, e: Bool) -> Sh:
351	  match e:
352	    case True{}:
353	      HEnd{tab}
354	    case False{}:
355	      sh_l(w, mask, i, k, Array.get(U32, tab, U32.inc(U32.shl(k))))
356	
357	def sh_w(+mask: U32, +i: U32, +k: U32, r: Array<U32> & U32) -> Sh:
358	  (tab, +w) = r
359	  sh_if(tab, mask, i, k, w, U32.is_eq(w, 0))
360	
361	def sh_step(tab: Array<U32>, +mask: U32, +i: U32, +k: U32) -> Sh:
362	  sh_w(mask, i, k, Array.get(U32, tab, U32.shl(k)))
363	
364	def shift(fuel: Nat, s: Sh, +mask: U32, +i: U32, +k: U32) -> Array<U32>:
365	  match fuel s:
366	    case 0n HEnd{tab}:
367	      clear_bucket(tab, i)
368	    case 0n HMove{tab, w, l}:
369	      clear_bucket(tab, i)
370	    case 0n HSkip{tab}:
371	      clear_bucket(tab, i)
372	    case 1n+p HEnd{tab}:
373	      clear_bucket(tab, i)
374	    case 1n+p HMove{tab, +w, +l}:
375	      +k2 = bnext(k, mask)
376	      shift(p, sh_step(put_bucket(tab, i, w, l), mask, k, k2), mask, k, k2)
377	    case 1n+p HSkip{tab}:
378	      +k2 = bnext(k, mask)
379	      shift(p, sh_step(tab, mask, i, k2), mask, i, k2)
380	
381	# Empty bucket i, closing the gap behind it.
382	def del_at(tab: Array<U32>, +mask: U32, +i: U32) -> Array<U32>:
383	  shift(U32.to_nat(U32.inc(mask)), sh_step(tab, mask, i, bnext(i, mask)), mask, i, bnext(i, mask))
384	
385	# ---- the slot arena ----
386	
387	# A value array of 2^d vacant cells (Array.new needs Data values).
388	def vac(a, -V: Kind(a), d: Nat) -> Array<Maybe<a, V>>:
389	  match d:
390	    case 0n:
391	      ALeaf{None{}}
392	    case 1n+ +p:
393	      ANode{vac(a, V, p), vac(a, V, p)}
394	
395	def new(a, -V: Kind(a)) -> HashMap<a, V>:
396	  HM{0, 1, 2, 0, 1, 0, 0, Array.new(U32, 2n, 0), Array.new(String, 0n, ""), ALeaf{None{}}, Array.new(U32, 0n, 0)}
397	
398	# ---- set ----
399	
400	# Twice the buckets, every (word, link) pair re-placed.
401	def grow_tab(+mask: U32, +td: U32, tab: Array<U32>) -> Array<U32>:
402	  mv_fin(mv_go(U32.to_nat(U32.inc(mask)), 0, U32.inc(U32.shl(mask)), MV{tab, Array.new(U32, U32.to_nat(U32.inc(td)), 0)}))
403	
404	type Arena<a, -V: Kind(a)> is Type:
405	  AR{ks: Array<String>, vs: Array<Maybe<a, V>>}
406	
407	def store(a, -V: Kind(a), ks: Array<String>, vs: Array<Maybe<a, V>>, +s: U32, key: String, x: V) -> Arena<a, V>:
408	  AR{Array.set(String, ks, s, key), Array.set(Maybe<a, V>, vs, s, Some{x})}
409	
410	def ins_fin(a, -V: Kind(a), +n: U32, +mask: U32, +td: U32, +fresh: U32, +sz: U32, +sd: U32, +free: U32, tab: Array<U32>, nx: Array<U32>, r: Arena<a, V>) -> HashMap<a, V>:
411	  AR{ks, vs} = r
412	  HM{U32.inc(n), mask, td, fresh, sz, sd, free, tab, ks, vs, nx}
413	
414	# The new entry's slot s is chosen; its bucket is at (or, after growth, found anew).
415	def ins_slot(a, -V: Kind(a), +n: U32, +mask: U32, +td: U32, +fresh: U32, +sz: U32, +sd: U32, +free: U32, tab: Array<U32>, ks: Array<String>, vs: Array<Maybe<a, V>>, nx: Array<U32>, +s: U32, +at: U32, +w: U32, key: String, x: V, over: Bool) -> HashMap<a, V>:
416	  match over:
417	    case False{}:
418	      ins_fin(a, V, n, mask, td, fresh, sz, sd, free, put_bucket(tab, at, w, link(s)), nx, store(a, V, ks, vs, s, key, x))
419	    case True{}:
420	      ins_fin(a, V, n, U32.inc(U32.shl(mask)), U32.inc(td), fresh, sz, sd, free, ins_raw(grow_tab(mask, td, tab), U32.inc(U32.shl(mask)), w, link(s)), nx, store(a, V, ks, vs, s, key, x))
421	
422	def ins_free(a, -V: Kind(a), +n: U32, +mask: U32, +td: U32, +fresh: U32, +sz: U32, +sd: U32, tab: Array<U32>, ks: Array<String>, vs: Array<Maybe<a, V>>, +s: U32, +at: U32, +w: U32, key: String, x: V, r: Array<U32> & U32) -> HashMap<a, V>:
423	  (nx, +nf) = r
424	  ins_slot(a, V, n, mask, td, fresh, sz, sd, nf, tab, ks, vs, nx, s, at, w, key, x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(mask)))
425	
426	def ins_fresh(a, -V: Kind(a), +n: U32, +mask: U32, +td: U32, +fresh: U32, +sz: U32, +sd: U32, tab: Array<U32>, ks: Array<String>, vs: Array<Maybe<a, V>>, nx: Array<U32>, +at: U32, +w: U32, key: String, x: V, room: Bool) -> HashMap<a, V>:
427	  match room:
428	    case True{}:
429	      ins_slot(a, V, n, mask, td, U32.inc(fresh), sz, sd, 0, tab, ks, vs, nx, fresh, at, w, key, x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(mask)))
430	    case False{}:
431	      ins_slot(a, V, n, mask, td, U32.inc(fresh), U32.shl(sz), U32.inc(sd), 0, tab, ANode{ks, Array.new(String, U32.to_nat(sd), "")}, ANode{vs, vac(a, V, U32.to_nat(sd))}, ANode{nx, Array.new(U32, U32.to_nat(sd), 0)}, fresh, at, w, key, x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(mask)))
432	
433	def ins_new(a, -V: Kind(a), +n: U32, +mask: U32, +td: U32, +fresh: U32, +sz: U32, +sd: U32, +free: U32, tab: Array<U32>, ks: Array<String>, vs: Array<Maybe<a, V>>, nx: Array<U32>, +at: U32, +w: U32, key: String, x: V, none: Bool) -> HashMap<a, V>:
434	  match none:
435	    case True{}:
436	      ins_fresh(a, V, n, mask, td, fresh, sz, sd, tab, ks, vs, nx, at, w, key, x, U32.is_lt(fresh, sz))
437	    case False{}:
438	      ins_free(a, V, n, mask, td, fresh, sz, sd, tab, ks, vs, slot(free), at, w, key, x, Array.get(U32, nx, slot(free)))
439	
440	def set_hit(a, -V: Kind(a), +n: U32, +mask: U32, +td: U32, +fresh: U32, +sz: U32, +sd: U32, +free: U32, tab: Array<U32>, ks: Array<String>, vs: Array<Maybe<a, V>>, nx: Array<U32>, +at: U32, +l: U32, +w: U32, key: String, x: V, absent: Bool) -> HashMap<a, V>:
441	  match absent:
442	    case False{}:
443	      HM{n, mask, td, fresh, sz, sd, free, tab, ks, Array.set(Maybe<a, V>, vs, slot(l), Some{x}), nx}
444	    case True{}:
445	      ins_new(a, V, n, mask, td, fresh, sz, sd, free, tab, ks, vs, nx, at, w, key, x, U32.is_eq(free, 0))
446	
447	def set_f(a, -V: Kind(a), +n: U32, +mask: U32, +td: U32, +fresh: U32, +sz: U32, +sd: U32, +free: U32, vs: Array<Maybe<a, V>>, nx: Array<U32>, x: V, r: Found & U32) -> HashMap<a, V>:
448	  (fd, +w) = r
449	  FD{tab, ks, key, +at, +l} = fd
450	  set_hit(a, V, n, mask, td, fresh, sz, sd, free, tab, ks, vs, nx, at, l, w, key, x, U32.is_eq(l, 0))
451	
452	# Insert key -> x, replacing any value already stored under key.
453	def set(a, -V: Kind(a), m: HashMap<a, V>, key: String, x: V) -> HashMap<a, V>:
454	  HM{+n, +mask, +td, +fresh, +sz, +sd, +free, tab, ks, vs, nx} = m
455	  set_f(a, V, n, mask, td, fresh, sz, sd, free, vs, nx, x, probe(tab, ks, mask, key))
456	
457	# ---- get / has ----
458	
459	def get_v(-V: Data, dflt: V, r: Array<Maybe<&2, V>> & Maybe<&2, V>) -> Array<Maybe<&2, V>> & V:
460	  (vs, mv) = r
461	  match mv:
462	    case None{}:
463	      (vs, dflt)
464	    case Some{v}:
465	      (vs, v)
466	
467	def get_fin(-V: Data, +n: U32, +mask: U32, +td: U32, +fresh: U32, +sz: U32, +sd: U32, +free: U32, tab: Array<U32>, ks: Array<String>, nx: Array<U32>, r: Array<Maybe<&2, V>> & V) -> HashMap<&2, V> & V:
468	  (vs, v) = r
469	  (HM{n, mask, td, fresh, sz, sd, free, tab, ks, vs, nx}, v)
470	
471	def get_hit(-V: Data, +n: U32, +mask: U32, +td: U32, +fresh: U32, +sz: U32, +sd: U32, +free: U32, tab: Array<U32>, ks: Array<String>, vs: Array<Maybe<&2, V>>, nx: Array<U32>, dflt: V, +l: U32, absent: Bool) -> HashMap<&2, V> & V:
472	  match absent:
473	    case True{}:
474	      (HM{n, mask, td, fresh, sz, sd, free, tab, ks, vs, nx}, dflt)
475	    case False{}:
476	      get_fin(V, n, mask, td, fresh, sz, sd, free, tab, ks, nx, get_v(V, dflt, Array.get(Maybe<&2, V>, vs, slot(l))))
477	
478	def get_f(-V: Data, +n: U32, +mask: U32, +td: U32, +fresh: U32, +sz: U32, +sd: U32, +free: U32, vs: Array<Maybe<&2, V>>, nx: Array<U32>, dflt: V, r: Found & U32) -> HashMap<&2, V> & V:
479	  (fd, w) = r
480	  FD{tab, ks, key, at, +l} = fd
481	  get_hit(V, n, mask, td, fresh, sz, sd, free, tab, ks, vs, nx, dflt, l, U32.is_eq(l, 0))
482	
483	# The value stored under key, or dflt (values are copied out, so V: Data).
484	def get(-V: Data, dflt: V, m: HashMap<&2, V>, key: String) -> HashMap<&2, V> & V:
485	  HM{+n, +mask, +td, +fresh, +sz, +sd, +free, tab, ks, vs, nx} = m
486	  get_f(V, n, mask, td, fresh, sz, sd, free, vs, nx, dflt, probe(tab, ks, mask, key))
487	
488	def has_f(a, -V: Kind(a), +n: U32, +mask: U32, +td: U32, +fresh: U32, +sz: U32, +sd: U32, +free: U32, vs: Array<Maybe<a, V>>, nx: Array<U32>, r: Found & U32) -> HashMap<a, V> & Bool:
489	  (fd, w) = r
490	  FD{tab, ks, key, at, +l} = fd
491	  (HM{n, mask, td, fresh, sz, sd, free, tab, ks, vs, nx}, U32.is_ne(l, 0))
492	
493	def has(a, -V: Kind(a), m: HashMap<a, V>, key: String) -> HashMap<a, V> & Bool:
494	  HM{+n, +mask, +td, +fresh, +sz, +sd, +free, tab, ks, vs, nx} = m
495	  has_f(a, V, n, mask, td, fresh, sz, sd, free, vs, nx, probe(tab, ks, mask, key))
496	
497	# ---- pop / del ----
498	
499	def drop_key(ks: Array<String>, +s: U32, short: Bool) -> Array<String>:
500	  match short:
501	    case True{}:
502	      ks
503	    case False{}:
504	      Array.set(String, ks, s, "")
505	
506	def pop_v(a, -V: Kind(a), +n: U32, +mask: U32, +td: U32, +fresh: U32, +sz: U32, +sd: U32, +free: U32, tab: Array<U32>, ks: Array<String>, nx: Array<U32>, +at: U32, +s: U32, +w: U32, r: Array<Maybe<a, V>> & Maybe<a, V>) -> HashMap<a, V> & Maybe<a, V>:
507	  (vs, v) = r
508	  (HM{U32.sub(n, 1), mask, td, fresh, sz, sd, link(s), del_at(tab, mask, at), drop_key(ks, s, is_short(w)), vs, Array.set(U32, nx, s, free)}, v)
509	
510	def pop_hit(a, -V: Kind(a), +n: U32, +mask: U32, +td: U32, +fresh: U32, +sz: U32, +sd: U32, +free: U32, tab: Array<U32>, ks: Array<String>, vs: Array<Maybe<a, V>>, nx: Array<U32>, +at: U32, +l: U32, +w: U32, absent: Bool) -> HashMap<a, V> & Maybe<a, V>:
511	  match absent:
512	    case True{}:
513	      (HM{n, mask, td, fresh, sz, sd, free, tab, ks, vs, nx}, None{})
514	    case False{}:
515	      pop_v(a, V, n, mask, td, fresh, sz, sd, free, tab, ks, nx, at, slot(l), w, Array.swap(Maybe<a, V>, vs, slot(l), None{}))
516	
517	def pop_f(a, -V: Kind(a), +n: U32, +mask: U32, +td: U32, +fresh: U32, +sz: U32, +sd: U32, +free: U32, vs: Array<Maybe<a, V>>, nx: Array<U32>, r: Found & U32) -> HashMap<a, V> & Maybe<a, V>:
518	  (fd, +w) = r
519	  FD{tab, ks, key, +at, +l} = fd
520	  pop_hit(a, V, n, mask, td, fresh, sz, sd, free, tab, ks, vs, nx, at, l, w, U32.is_eq(l, 0))
521	
522	# Remove key, answering its value.
523	def pop(a, -V: Kind(a), m: HashMap<a, V>, key: String) -> HashMap<a, V> & Maybe<a, V>:
524	  HM{+n, +mask, +td, +fresh, +sz, +sd, +free, tab, ks, vs, nx} = m
525	  pop_f(a, V, n, mask, td, fresh, sz, sd, free, vs, nx, probe(tab, ks, mask, key))
526	
527	def del_drop(a, -V: Kind(a), r: HashMap<a, V> & Maybe<a, V>) -> HashMap<a, V>:
528	  (m, v) = r
529	  m
530	
531	def del(a, -V: Kind(a), m: HashMap<a, V>, key: String) -> HashMap<a, V>:
532	  del_drop(a, V, pop(a, V, m, key))
533	
534	# ---- keys ----
535	
536	type Walk is Type:
537	  WK{tab: Array<U32>, ks: Array<String>, acc: List<&2, String>}
538	
539	def wk_long(tab: Array<U32>, +s: U32, acc: List<&2, String>, ks: Array<String>, kk: String & String) -> Walk:
540	  (k1, k2) = kk
541	  WK{tab, Array.set(String, ks, s, k1), Con{k2, acc}}
542	
543	def wk_copy(tab: Array<U32>, +s: U32, acc: List<&2, String>, r: Array<String> & String) -> Walk:
544	  (ks, key) = r
545	  wk_long(tab, s, acc, ks, str_copy(key))
546	
547	def wk_ll(ks: Array<String>, acc: List<&2, String>, r: Array<U32> & U32) -> Walk:
548	  (tab, +l) = r
549	  wk_copy(tab, slot(l), acc, Array.swap(String, ks, slot(l), SNil{}))
550	
551	def wk_kind(tab: Array<U32>, ks: Array<String>, +k: U32, acc: List<&2, String>, +w: U32, short: Bool) -> Walk:
552	  match short:
553	    case True{}:
554	      WK{tab, ks, Con{SCon{Chr{U32.and(w, 2147483647)}, SNil{}}, acc}}
555	    case False{}:
556	      wk_ll(ks, acc, Array.get(U32, tab, U32.inc(U32.shl(k))))
557	
558	def wk_if(tab: Array<U32>, ks: Array<String>, +k: U32, acc: List<&2, String>, +w: U32, e: Bool) -> Walk:
559	  match e:
560	    case True{}:
561	      WK{tab, ks, acc}
562	    case False{}:
563	      wk_kind(tab, ks, k, acc, w, is_short(w))
564	
565	def wk_w(ks: Array<String>, +k: U32, acc: List<&2, String>, r: Array<U32> & U32) -> Walk:
566	  (tab, +w) = r
567	  wk_if(tab, ks, k, acc, w, U32.is_eq(w, 0))
568	
569	def wk_step(+k: U32, w: Walk) -> Walk:
570	  WK{tab, ks, acc} = w
571	  wk_w(ks, k, acc, Array.get(U32, tab, U32.shl(k)))
572	
573	def wk_go(fuel: Nat, +k: U32, w: Walk) -> Walk:
574	  match fuel:
575	    case 0n:
576	      w
577	    case 1n+p:
578	      wk_go(p, U32.sub(k, 1), wk_step(k, w))
579	
580	def keys_fin(a, -V: Kind(a), +n: U32, +mask: U32, +td: U32, +fresh: U32, +sz: U32, +sd: U32, +free: U32, vs: Array<Maybe<a, V>>, nx: Array<U32>, w: Walk) -> HashMap<a, V> & List<&2, String>:
581	  WK{tab, ks, acc} = w
582	  (HM{n, mask, td, fresh, sz, sd, free, tab, ks, vs, nx}, acc)
583	
584	# Every key, in bucket order.
585	def keys(a, -V: Kind(a), m: HashMap<a, V>) -> HashMap<a, V> & List<&2, String>:
586	  HM{+n, +mask, +td, +fresh, +sz, +sd, +free, tab, ks, vs, nx} = m
587	  keys_fin(a, V, n, mask, td, fresh, sz, sd, free, vs, nx, wk_go(U32.to_nat(U32.inc(mask)), mask, WK{tab, ks, Nil{}}))