1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/u32alg.bend as A
4	import ../../../spec/containers/hash_table.bend as S
5	import ../../../src/containers/hash_table.bend as H
6	import ./strings.bend as STR
7	import ../../lib/u32.bend as UW
8	
9	# Key identity: structural String equality is an equivalence, and every key
10	# has one check word (a one-character key below 2^31 its short word, any
11	# other key its long hash word).
12	
13	
14	def chr_refl(+c: Char) -> {S.chr_eq(c, c) == True{} : Bool}:
15	  match c:
16	    case Chr{+x}:
17	      UW.u32_eq_refl(x)
18	
19	def str_refl(+s: String) -> {S.str_eq(s, s) == True{} : Bool}:
20	  match s:
21	    case SNil{}:
22	      {==}
23	    case SCon{+c, +t}:
24	      L.and_intro(S.chr_eq(c, c), S.str_eq(t, t), chr_refl(c), str_refl(t))
25	
26	def chr_eq_of(+a: Char, +b: Char, +h: {S.chr_eq(a, b) == True{} : Bool}) -> {a == b : Char}:
27	  match a b:
28	    case Chr{+x} Chr{+y}:
29	      Equal.cong(U32, Char, z => Chr{z}, x, y, A.eq_of(x, y, h))
30	
31	# equal by str_eq means equal
32	def str_eq_of(+a: String, +b: String, +h: {S.str_eq(a, b) == True{} : Bool}) -> {a == b : String}:
33	  match a b:
34	    case SNil{} SNil{}:
35	      {==}
36	    case SNil{} SCon{c, t}:
37	      Empty.absurd({SNil{} == SCon{c, t} : String}, L.false_true(h))
38	    case SCon{c, t} SNil{}:
39	      Empty.absurd({SCon{c, t} == SNil{} : String}, L.false_true(h))
40	    case SCon{+x, +s} SCon{+y, +t}:
41	      +ex = chr_eq_of(x, y, L.and_left(S.chr_eq(x, y), S.str_eq(s, t), h))
42	      +es = str_eq_of(s, t, L.and_right(S.chr_eq(x, y), S.str_eq(s, t), h))
43	      Equal.trans(String, SCon{x, s}, SCon{y, s}, SCon{y, t}, Equal.cong(Char, String, z => SCon{z, s}, x, y, ex), Equal.cong(String, String, z => SCon{y, z}, s, t, es))
44	
45	def str_eq_true(+a: String, +b: String, +e: {a == b : String}) -> {S.str_eq(a, b) == True{} : Bool}:
46	  L.subst(String, z => {S.str_eq(a, z) == True{} : Bool}, a, b, e, str_refl(a))
47	
48	def sym_c(+a: String, +b: String, +c: Bool, +hc: {S.str_eq(a, b) == c : Bool}, +d: Bool, +hd: {S.str_eq(b, a) == d : Bool}) -> {c == d : Bool}:
49	  match c d:
50	    case True{} True{}:
51	      {==}
52	    case False{} False{}:
53	      {==}
54	    case True{} False{}:
55	      Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, S.str_eq(b, a), False{}, Equal.sym(Bool, S.str_eq(b, a), True{}, str_eq_true(b, a, Equal.sym(String, a, b, str_eq_of(a, b, hc)))), hd)))
56	    case False{} True{}:
57	      Empty.absurd({False{} == True{} : Bool}, L.true_false(Equal.trans(Bool, True{}, S.str_eq(a, b), False{}, Equal.sym(Bool, S.str_eq(a, b), True{}, str_eq_true(a, b, Equal.sym(String, b, a, str_eq_of(b, a, hd)))), hc)))
58	
59	def str_sym(+a: String, +b: String) -> {S.str_eq(a, b) == S.str_eq(b, a) : Bool}:
60	  sym_c(a, b, S.str_eq(a, b), {==}, S.str_eq(b, a), {==})
61	
62	# ---- the check word of a key ----
63	
64	# a one-character key whose code is below 2^31 (stored by its word alone)
65	def short_c(+c: U32, t: String) -> Bool:
66	  match t:
67	    case SNil{}:
68	      U32.is_lt(c, H.tag())
69	    case SCon{d, r}:
70	      False{}
71	
72	def shortk(key: String) -> Bool:
73	  match key:
74	    case SNil{}:
75	      False{}
76	    case SCon{Chr{+c}, +t}:
77	      short_c(c, t)
78	
79	def kw_c(+c: U32, +t: String, sh: Bool) -> U32:
80	  match sh:
81	    case True{}:
82	      H.short_word(c)
83	    case False{}:
84	      STR.lword(SCon{Chr{c}, t})
85	
86	def kword(key: String) -> U32:
87	  match key:
88	    case SNil{}:
89	      STR.lword(SNil{})
90	    case SCon{Chr{+c}, +t}:
91	      kw_c(c, t, short_c(c, t))
92	
93	def kword_long(+key: String, +hk: {shortk(key) == False{} : Bool}) -> {kword(key) == STR.lword(key) : U32}:
94	  match key:
95	    case SNil{}:
96	      {==}
97	    case SCon{Chr{+c}, +t}:
98	      L.subst(Bool, b => {kw_c(c, t, b) == STR.lword(SCon{Chr{c}, t}) : U32}, False{}, short_c(c, t), Equal.sym(Bool, short_c(c, t), False{}, hk), {==})
99	
100	def kword_short(+c: U32, +hc: {U32.is_lt(c, H.tag()) == True{} : Bool}) -> {kword(SCon{Chr{c}, SNil{}}) == H.short_word(c) : U32}:
101	  L.subst(Bool, b => {kw_c(c, SNil{}, b) == H.short_word(c) : U32}, True{}, U32.is_lt(c, H.tag()), Equal.sym(Bool, U32.is_lt(c, H.tag()), True{}, hc), {==})
102	
103	def not_true_eq(+b: Bool, +h: {Bool.not(b) == True{} : Bool}) -> {b == False{} : Bool}:
104	  match b:
105	    case True{}:
106	      Empty.absurd({True{} == False{} : Bool}, L.false_true(h))
107	    case False{}:
108	      {==}
109	
110	def not_true_eq2(+b: Bool, +h: {Bool.not(b) == False{} : Bool}) -> {b == True{} : Bool}:
111	  match b:
112	    case True{}:
113	      {==}
114	    case False{}:
115	      Empty.absurd({False{} == True{} : Bool}, L.true_false(h))