1	import Base
2	import ../../lib/nat.bend as N
3	import ../../../spec/lib/common.bend as SC
4	import ../../lib/u32div.bend as UD
5	import ../../../src/containers/hash_table.bend as H
6	import ./buckets.bend as B
7	import ../../lib/words32.bend as W32
8	
9	# Reading the implementation's arrays as a bucket list.
10	#   tab   (check word, link) pairs: bucket i is (tab[2i], tab[2i+1])
11	#   ks    the slot arena's stored keys: a long key's String, "" for a
12	#         one-character key (its word is the key)
13	
14	
15	def nths(ks: List<&2, String>, +i: Nat) -> String:
16	  match ks i:
17	    case Nil{} _:
18	      SNil{}
19	    case Con{x, t} 0n:
20	      x
21	    case Con{x, t} 1n+p:
22	      nths(t, p)
23	
24	# the key of a full bucket with word w and stored string s
25	def keyof_c(+w: U32, s: String, short: Bool) -> String:
26	  match short:
27	    case True{}:
28	      SCon{Chr{U32.and(w, 2147483647)}, SNil{}}
29	    case False{}:
30	      s
31	
32	def keyof(+w: U32, s: String) -> String:
33	  keyof_c(w, s, H.is_short(w))
34	
35	def dec_c(+w: U32, +l: U32, +ks: List<&2, String>, empty: Bool) -> B.Bk:
36	  match empty:
37	    case True{}:
38	      B.BE{}
39	    case False{}:
40	      B.BF{w, l, keyof(w, nths(ks, UD.v(H.slot(l))))}
41	
42	# bucket i of the arrays
43	def dec(+tb: List<&2, U32>, +ks: List<&2, String>, +i: Nat) -> B.Bk:
44	  dec_c(W32.nth0(tb, Nat.double(i)), W32.nth0(tb, 1n+Nat.double(i)), ks, U32.is_eq(W32.nth0(tb, Nat.double(i)), 0))
45	
46	# buckets i .. i + m - 1
47	def dlist(+tb: List<&2, U32>, +ks: List<&2, String>, +m: Nat, +i: Nat) -> List<&2, B.Bk>:
48	  match m:
49	    case 0n:
50	      Nil{}
51	    case 1n+p:
52	      Con{dec(tb, ks, i), dlist(tb, ks, p, 1n+i)}
53	
54	def at_dlist(+tb: List<&2, U32>, +ks: List<&2, String>, +m: Nat, +i: Nat, +j: Nat, +hj: {Nat.is_lt(j, m) == True{} : Bool}) -> {B.at(dlist(tb, ks, m, i), j) == dec(tb, ks, Nat.add(i, j)) : B.Bk}:
55	  match m j:
56	    case 0n _:
57	      Empty.absurd({B.at(dlist(tb, ks, 0n, i), j) == dec(tb, ks, Nat.add(i, j)) : B.Bk}, N.lt_zero_absurd(j, hj))
58	    case 1n+p 0n:
59	      Equal.cong(Nat, B.Bk, z => dec(tb, ks, z), i, Nat.add(i, 0n), Equal.sym(Nat, Nat.add(i, 0n), i, N.add_zero(i)))
60	    case 1n+p 1n+q:
61	      Equal.trans(B.Bk, B.at(dlist(tb, ks, p, 1n+i), q), dec(tb, ks, Nat.add(1n+i, q)), dec(tb, ks, Nat.add(i, 1n+q)), at_dlist(tb, ks, p, 1n+i, q, hj), Equal.cong(Nat, B.Bk, z => dec(tb, ks, z), 1n+Nat.add(i, q), Nat.add(i, 1n+q), Equal.sym(Nat, Nat.add(i, 1n+q), 1n+Nat.add(i, q), N.add_succ(i, q))))
62	
63	# the bucket list of a table of n buckets
64	def buckets(+tb: List<&2, U32>, +ks: List<&2, String>, +n: Nat) -> List<&2, B.Bk>:
65	  dlist(tb, ks, n, 0n)
66	
67	def at_buckets(+tb: List<&2, U32>, +ks: List<&2, String>, +n: Nat, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}) -> {B.at(buckets(tb, ks, n), j) == dec(tb, ks, j) : B.Bk}:
68	  at_dlist(tb, ks, n, 0n, j, hj)
69	
70	# a list index below the length reads its element
71	
72	def nths_some(+ks: List<&2, String>, +i: Nat, +h: {Nat.is_lt(i, SC.length(String, ks)) == True{} : Bool}) -> {SC.nth(String, ks, i) == Some{nths(ks, i)} : Maybe<&2, String>}:
73	  match ks i:
74	    case Nil{} _:
75	      Empty.absurd({SC.nth(String, Nil{}, i) == Some{nths(Nil{}, i)} : Maybe<&2, String>}, N.lt_zero_absurd(i, h))
76	    case Con{x, t} 0n:
77	      {==}
78	    case Con{x, t} 1n+p:
79	      nths_some(t, p, h)
80	
81	def upd_upd(+xs: List<&2, String>, +i: Nat, +a: String, +b: String) -> {SC.update(String, SC.update(String, xs, i, a), i, b) == SC.update(String, xs, i, b) : List<&2, String>}:
82	  match xs i:
83	    case Nil{} _:
84	      {==}
85	    case Con{h, t} 0n:
86	      {==}
87	    case Con{h, t} 1n+p:
88	      Equal.cong(List<&2, String>, List<&2, String>, r => Con{h, r}, SC.update(String, SC.update(String, t, p, a), p, b), SC.update(String, t, p, b), upd_upd(t, p, a, b))
89	
90	def upd_self(+xs: List<&2, String>, +i: Nat) -> {SC.update(String, xs, i, nths(xs, i)) == xs : List<&2, String>}:
91	  match xs i:
92	    case Nil{} _:
93	      {==}
94	    case Con{h, t} 0n:
95	      {==}
96	    case Con{h, t} 1n+p:
97	      Equal.cong(List<&2, String>, List<&2, String>, r => Con{h, r}, SC.update(String, t, p, nths(t, p)), t, upd_self(t, p))