src/Keys.bend
mylsm-lsm-store@0.3.1.0 · 153 lines · 0 definitions
1import Base
2
3# Total-order comparison for keys. Base's String.cmp hands the strings back
4# beside the verdict ((s1, s2), c); we take reusable copies and unpack via a
5# helper (a match cannot scrutinize the computed call directly).
6def unpack(pair: (String & String) & Cmp) -> Cmp:
7 match pair:
8 case ((_, _), c):
9 c
10
11def cmp(+s1: String, +s2: String) -> Cmp:
12 unpack(String.cmp(s1, s2))
13
14def eq(+s1: String, +s2: String) -> Bool:
15 String.eq(s1, s2)
16
17# Small, coherent views of Cmp used by key-order laws and sorted-run code.
18def cmp_is_lt(ord: Cmp) -> Bool:
19 Cmp.is_lt(ord)
20
21def cmp_is_eq(ord: Cmp) -> Bool:
22 Cmp.is_eq(ord)
23
24def cmp_is_gt(ord: Cmp) -> Bool:
25 Cmp.is_gt(ord)
26
27def cmp_is_le(ord: Cmp) -> Bool:
28 Cmp.is_le(ord)
29
30def lt(+s1: String, +s2: String) -> Bool:
31 cmp_is_lt(cmp(s1, s2))
32
33def le(+s1: String, +s2: String) -> Bool:
34 cmp_is_le(cmp(s1, s2))
35
36def cmp_reverse(ord: Cmp) -> Cmp:
37 match ord:
38 case LT{}:
39 GT{}
40 case EQ{}:
41 EQ{}
42 case GT{}:
43 LT{}
44
45def implies(s1: Bool, s2: Bool) -> Bool:
46 match s1:
47 case False{}:
48 True{}
49 case True{}:
50 s2
51
52def iff(+s1: Bool, +s2: Bool) -> Bool:
53 Bool.and(implies(s1, s2), implies(s2, s1))
54
55# True exactly when one of three arbitrary predicates is true.
56def one_hot3(first: Bool, second: Bool, third: Bool) -> Bool:
57 match first second third:
58 case True{} False{} False{}:
59 True{}
60 case False{} True{} False{}:
61 True{}
62 case False{} False{} True{}:
63 True{}
64 case _ _ _:
65 False{}
66
67# Cmp is intrinsically one-hot; this predicate gives K6 a reusable statement.
68def cmp_one_hot(+ord: Cmp) -> Bool:
69 one_hot3(cmp_is_lt(ord), cmp_is_eq(ord), cmp_is_gt(ord))
70
71def cmp_one_hot_proof(+ord: Cmp) -> {cmp_one_hot(ord) == True{} : Bool}:
72 match ord:
73 case LT{}:
74 {==}
75 case EQ{}:
76 {==}
77 case GT{}:
78 {==}
79
80# `String.eq` is defined by the EQ projection of `String.cmp`; matching the
81# handed-back comparison pair exposes that definitional correspondence.
82def cmp_eq_pair(pair: (String & String) & Cmp) -> {cmp_is_eq(unpack(pair)) == String.eq.fin(pair) : Bool}:
83 match pair:
84 case ((a, b), c):
85 match c:
86 case LT{}:
87 {==}
88 case EQ{}:
89 {==}
90 case GT{}:
91 {==}
92
93def cmp_eq_bridge(+s1: String, +s2: String) -> {cmp_is_eq(cmp(s1, s2)) == eq(s1, s2) : Bool}:
94 cmp_eq_pair(String.cmp(s1, s2))
95
96# Reflexivity chain for open keys. Every product law about keyed lookup
97# rewrites with str_eq_refl; it rests on the layers below, down to bits.
98# (Proving Base's own primitives is the one exception to the trust-root
99# rule: without open-key comparison facts, NO keyed law is provable.)
100
101def bool_refl(+flag: Bool) -> {Bool.cmp(flag, flag) == EQ{} : Cmp}:
102 match flag:
103 case False{}:
104 {==}
105 case True{}:
106 {==}
107
108def word_refl(width: Nat, +word: Word(width)) -> {Word.cmp(width, word, word) == EQ{} : Cmp}:
109 match width word:
110 case 0n WNil{}:
111 {==}
112 case 1n+p WCon{ab, at}:
113 match ab:
114 case False{}:
115 %Equal.sym(Cmp, Word.cmp(p, at, at), EQ{}, word_refl(p, at)) : {Word.cmp.fin(False{}, False{}, _) == EQ{} : Cmp}
116 {==}
117 case True{}:
118 %Equal.sym(Cmp, Word.cmp(p, at, at), EQ{}, word_refl(p, at)) : {Word.cmp.fin(True{}, True{}, _) == EQ{} : Cmp}
119 {==}
120
121def u32_refl(+val: U32) -> {U32.cmp(val, val) == EQ{} : Cmp}:
122 match val:
123 case U32{w}:
124 %Equal.sym(Cmp, Word.cmp(32n, w, w), EQ{}, word_refl(32n, w)) : {_ == EQ{} : Cmp}
125 {==}
126
127def char_refl(+ch: Char) -> {Char.cmp(ch, ch) == ((ch, ch), EQ{}) : (Char & Char) & Cmp}:
128 match ch:
129 case Chr{x}:
130 %Equal.sym(Cmp, U32.cmp(x, x), EQ{}, u32_refl(x)) : {((Chr{x}, Chr{x}), _) == ((Chr{x}, Chr{x}), EQ{}) : (Char & Char) & Cmp}
131 {==}
132
133def s_cmp_pair_refl(+str: String) -> {String.cmp(str, str) == ((str, str), EQ{}) : (String & String) & Cmp}:
134 match str:
135 case SNil{}:
136 {==}
137 case SCon{h, t}:
138 %Equal.sym((Char & Char) & Cmp, Char.cmp(h, h), ((h, h), EQ{}), char_refl(h)) : {String.cmp.fin(t, t, _) == ((SCon{h, t}, SCon{h, t}), EQ{}) : (String & String) & Cmp}
139 %Equal.sym((String & String) & Cmp, String.cmp(t, t), ((t, t), EQ{}), s_cmp_pair_refl(t)) : {String.cmp.rec(h, h, _) == ((SCon{h, t}, SCon{h, t}), EQ{}) : (String & String) & Cmp}
140 {==}
141
142def str_refl(+str: String) -> {cmp(str, str) == EQ{} : Cmp}:
143 %Equal.sym((String & String) & Cmp, String.cmp(str, str), ((str, str), EQ{}), s_cmp_pair_refl(str)) : {unpack(_) == EQ{} : Cmp}
144 {==}
145
146def str_eq_refl(+str: String) -> {eq(str, str) == True{} : Bool}:
147 match str:
148 case SNil{}:
149 {==}
150 case SCon{h, t}:
151 %Equal.sym((Char & Char) & Cmp, Char.cmp(h, h), ((h, h), EQ{}), char_refl(h)) : {String.eq.fin(String.cmp.fin(t, t, _)) == True{} : Bool}
152 %Equal.sym((String & String) & Cmp, String.cmp(t, t), ((t, t), EQ{}), s_cmp_pair_refl(t)) : {String.eq.fin(String.cmp.rec(h, h, _)) == True{} : Bool}
153 {==}