~/jendhub

src/containers/hash_table.bend

bend-collections-laws-crypto@1.0.0.0 · 587 lines · 103 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/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
31type 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
34def 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
40def tag() -> U32:
41  2147483648
42
43def bnext(+i: U32, +mask: U32) -> U32:
44  U32.and(U32.inc(i), mask)
45
46def link(+s: U32) -> U32:
47  U32.inc(s)
48
49def slot(+l: U32) -> U32:
50  U32.sub(l, 1)
51
52def short_word(+c: U32) -> U32:
53  U32.or(c, tag())
54
55def long_word(+h: U32) -> U32:
56  U32.or(U32.and(h, 2147483647), 1)
57
58def is_short(+w: U32) -> Bool:
59  U32.is_ge(w, tag())
60
61def 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
68def 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
75def 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.
87def eq(a: String, b: String) -> (String & String) & Bool:
88  eq_acc(a, b, SNil{}, SNil{}, True{})
89
90def 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).
98def str_copy(s: String) -> String & String:
99  copy_acc(s, SNil{}, SNil{})
100
101def lw_fin(r: String & U32) -> String & U32:
102  (k, +h) = r
103  (k, long_word(h))
104
105def key_long(key: String) -> String & U32:
106  lw_fin(hash_acc(key, 0, SNil{}))
107
108# ---- probing ----
109
110type 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.
114type 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
119def 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
126def 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
130def 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
134def 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
141def 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
145def 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
152def 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
156def 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
159def 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
175def 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
179def 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.
183type QStep is Type:
184  QEnd{tab: Array<U32>}
185  QHit{tab: Array<U32>, l: U32}
186  QNext{tab: Array<U32>}
187
188def qs_l(r: Array<U32> & U32) -> QStep:
189  (tab, +l) = r
190  QHit{tab, l}
191
192def 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
199def 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
206def 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
210def qstep(tab: Array<U32>, +i: U32, +w: U32) -> QStep:
211  qs_w(i, w, Array.get(U32, tab, U32.shl(i)))
212
213type QFound is Type:
214  QF{tab: Array<U32>, at: U32, link: U32}
215
216def 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
232def 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
236def 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
243def 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.
252def 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
261def 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
264type RStep is Type:
265  REmpty{tab: Array<U32>}
266  RFull{tab: Array<U32>}
267
268def rs_if(tab: Array<U32>, e: Bool) -> RStep:
269  match e:
270    case True{}:
271      REmpty{tab}
272    case False{}:
273      RFull{tab}
274
275def rs_w(r: Array<U32> & U32) -> RStep:
276  (tab, +x) = r
277  rs_if(tab, U32.is_eq(x, 0))
278
279def rstep(tab: Array<U32>, +i: U32) -> RStep:
280  rs_w(Array.get(U32, tab, U32.shl(i)))
281
282def 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.
295def 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
298type Mv is Type:
299  MV{old: Array<U32>, nt: Array<U32>}
300
301def 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
305def 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
312def 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
316def 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
320def 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
327def mv_fin(m: Mv) -> Array<U32>:
328  MV{old, nt} = m
329  nt
330
331def clear_bucket(tab: Array<U32>, +i: U32) -> Array<U32>:
332  put_bucket(tab, i, 0, 0)
333
334type Sh is Type:
335  HEnd{tab: Array<U32>}
336  HMove{tab: Array<U32>, w: U32, l: U32}
337  HSkip{tab: Array<U32>}
338
339def 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
346def 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
350def 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
357def 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
361def 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
364def 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.
382def 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).
388def 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
395def 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.
401def 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
404type Arena<a, -V: Kind(a)> is Type:
405  AR{ks: Array<String>, vs: Array<Maybe<a, V>>}
406
407def 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
410def 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).
415def 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
422def 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
426def 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
433def 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
440def 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
447def 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.
453def 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
459def 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
467def 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
471def 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
478def 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).
484def 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
488def 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
493def 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
499def 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
506def 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
510def 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
517def 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.
523def 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
527def del_drop(a, -V: Kind(a), r: HashMap<a, V> & Maybe<a, V>) -> HashMap<a, V>:
528  (m, v) = r
529  m
530
531def 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
536type Walk is Type:
537  WK{tab: Array<U32>, ks: Array<String>, acc: List<&2, String>}
538
539def 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
543def 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
547def 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
551def 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
558def 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
565def 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
569def 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
573def 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
580def 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.
585def 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{}}))