1	import Base
2	import ../../../spec/containers/hash_table.bend as S
3	import ../../../src/math/hash.bend as HS
4	import ../../../src/containers/hash_table.bend as H
5	
6	# The hash map's String walks: hashing hands the key back and folds the
7	# multiply-xor mix over its characters; equality is the spec's structural
8	# equality and hands both strings back; copying makes two equal strings.
9	
10	def rr(+s: String, +acc: String) -> {H.rev_onto(H.rev_onto(s, acc), SNil{}) == H.rev_onto(acc, s) : String}:
11	  match s:
12	    case SNil{}:
13	      {==}
14	    case SCon{h, t}:
15	      rr(t, SCon{h, acc})
16	
17	def rev2(+s: String) -> {H.rev_onto(H.rev_onto(s, SNil{}), SNil{}) == s : String}:
18	  rr(s, SNil{})
19	
20	# the hash of a key: the mix folded over its character codes
21	def fold(s: String, +h: U32) -> U32:
22	  match s:
23	    case SNil{}:
24	      h
25	    case SCon{Chr{+c}, t}:
26	      fold(t, HS.mix(h, c))
27	
28	def hash_acc(+s: String, +h: U32, +acc: String) -> {H.hash_acc(s, h, acc) == (H.rev_onto(acc, s), fold(s, h)) : String & U32}:
29	  match s:
30	    case SNil{}:
31	      {==}
32	    case SCon{Chr{+c}, t}:
33	      hash_acc(t, HS.mix(h, c), SCon{Chr{c}, acc})
34	
35	# a key's long check word
36	def lword(+s: String) -> U32:
37	  H.long_word(fold(s, 0))
38	
39	def key_long(+s: String) -> {H.key_long(s) == (s, lword(s)) : String & U32}:
40	  Equal.cong(String & U32, String & U32, r => H.lw_fin(r), H.hash_acc(s, 0, SNil{}), (s, fold(s, 0)), hash_acc(s, 0, SNil{}))
41	
42	def and_true(+e: Bool) -> {Bool.and(e, True{}) == e : Bool}:
43	  match e:
44	    case True{}:
45	      {==}
46	    case False{}:
47	      {==}
48	
49	def and_false(+e: Bool) -> {Bool.and(e, False{}) == False{} : Bool}:
50	  match e:
51	    case True{}:
52	      {==}
53	    case False{}:
54	      {==}
55	
56	def and_assoc(+e: Bool, +p: Bool, +q: Bool) -> {Bool.and(Bool.and(e, p), q) == Bool.and(e, Bool.and(p, q)) : Bool}:
57	  match e:
58	    case True{}:
59	      {==}
60	    case False{}:
61	      {==}
62	
63	def eq_acc(+a: String, +b: String, +ra: String, +rb: String, +e: Bool) -> {H.eq_acc(a, b, ra, rb, e) == ((H.rev_onto(ra, a), H.rev_onto(rb, b)), Bool.and(e, S.str_eq(a, b))) : (String & String) & Bool}:
64	  match a b:
65	    case SNil{} SNil{}:
66	      Equal.cong(Bool, (String & String) & Bool, z => ((H.rev_onto(ra, SNil{}), H.rev_onto(rb, SNil{})), z), e, Bool.and(e, True{}), Equal.sym(Bool, Bool.and(e, True{}), e, and_true(e)))
67	    case SNil{} SCon{h, t}:
68	      Equal.cong(Bool, (String & String) & Bool, z => ((H.rev_onto(ra, SNil{}), H.rev_onto(rb, SCon{h, t})), z), False{}, Bool.and(e, False{}), Equal.sym(Bool, Bool.and(e, False{}), False{}, and_false(e)))
69	    case SCon{Chr{c}, t} SNil{}:
70	      Equal.cong(Bool, (String & String) & Bool, z => ((H.rev_onto(ra, SCon{Chr{c}, t}), H.rev_onto(rb, SNil{})), z), False{}, Bool.and(e, False{}), Equal.sym(Bool, Bool.and(e, False{}), False{}, and_false(e)))
71	    case SCon{Chr{+x}, +ta} SCon{Chr{+y}, +tb}:
72	      Equal.trans((String & String) & Bool, H.eq_acc(ta, tb, SCon{Chr{x}, ra}, SCon{Chr{y}, rb}, Bool.and(e, U32.is_eq(x, y))), ((H.rev_onto(ra, SCon{Chr{x}, ta}), H.rev_onto(rb, SCon{Chr{y}, tb})), Bool.and(Bool.and(e, U32.is_eq(x, y)), S.str_eq(ta, tb))), ((H.rev_onto(ra, SCon{Chr{x}, ta}), H.rev_onto(rb, SCon{Chr{y}, tb})), Bool.and(e, S.str_eq(SCon{Chr{x}, ta}, SCon{Chr{y}, tb}))),
73	        eq_acc(ta, tb, SCon{Chr{x}, ra}, SCon{Chr{y}, rb}, Bool.and(e, U32.is_eq(x, y))),
74	        Equal.cong(Bool, (String & String) & Bool, z => ((H.rev_onto(ra, SCon{Chr{x}, ta}), H.rev_onto(rb, SCon{Chr{y}, tb})), z), Bool.and(Bool.and(e, U32.is_eq(x, y)), S.str_eq(ta, tb)), Bool.and(e, Bool.and(U32.is_eq(x, y), S.str_eq(ta, tb))), and_assoc(e, U32.is_eq(x, y), S.str_eq(ta, tb))))
75	
76	# THEOREM: eq is String equality, handing both strings back.
77	def eq(+a: String, +b: String) -> {H.eq(a, b) == ((a, b), S.str_eq(a, b)) : (String & String) & Bool}:
78	  eq_acc(a, b, SNil{}, SNil{}, True{})
79	
80	def copy_acc(+s: String, +ra: String, +rb: String) -> {H.copy_acc(s, ra, rb) == (H.rev_onto(ra, s), H.rev_onto(rb, s)) : String & String}:
81	  match s:
82	    case SNil{}:
83	      {==}
84	    case SCon{Chr{+c}, t}:
85	      copy_acc(t, SCon{Chr{c}, ra}, SCon{Chr{c}, rb})
86	
87	def str_copy(+s: String) -> {H.str_copy(s) == (s, s) : String & String}:
88	  copy_acc(s, SNil{}, SNil{})