src/Keys.bend checks

raw source on the hub · import mylsm-lsm-store@0.4.0.0/src/Keys.bend as Keys

3 imports

import Base
import bend-mathlib@0.7.0.0/string.bend as MString
import bend-mathlib@0.7.0.0/bool.bend as MBool

Definitions

def unpack source · line 8 · raw

@pair:Pair(Pair(String, String), Cmp) -> Cmp

Total-order comparison for keys. Base's String.cmp hands the strings back beside the verdict ((s1, s2), c); we take reusable copies and unpack via a helper (a match cannot scrutinize the computed call directly).

def cmp source · line 14 · raw

@+s1:String -> @+s2:String -> Cmp

Handle cmp in the key ordering and comparison.

def eq source · line 18 · raw

@+s1:String -> @+s2:String -> Bool

Handle eq in the key ordering and comparison.

def cmp_is_lt source · line 22 · raw

@ord:Cmp -> Bool

Small, coherent views of Cmp used by key-order laws and sorted-run code.

def cmp_is_eq source · line 26 · raw

@ord:Cmp -> Bool

Compare whether is eq holds for the key ordering and comparison.

def cmp_is_gt source · line 30 · raw

@ord:Cmp -> Bool

Compare whether is gt holds for the key ordering and comparison.

def cmp_is_le source · line 34 · raw

@ord:Cmp -> Bool

Compare whether is le holds for the key ordering and comparison.

def lt source · line 38 · raw

@+s1:String -> @+s2:String -> Bool

Handle lt in the key ordering and comparison.

def le source · line 42 · raw

@+s1:String -> @+s2:String -> Bool

Handle le in the key ordering and comparison.

def cmp_reverse source · line 46 · raw

@ord:Cmp -> Cmp

Compare whether reverse holds for the key ordering and comparison.

def implies source · line 56 · raw

@s1:Bool -> @s2:Bool -> Bool

Handle implies in the key ordering and comparison.

def iff source · line 64 · raw

@+s1:Bool -> @+s2:Bool -> Bool

Select f for the key ordering and comparison.

def one_hot3 source · line 68 · raw

@first:Bool -> @second:Bool -> @third:Bool -> Bool

True exactly when one of three arbitrary predicates is true.

def cmp_one_hot source · line 80 · raw

@+ord:Cmp -> Bool

Cmp is intrinsically one-hot; this predicate gives K6 a reusable statement.

def cmp_one_hot_proof source · line 84 · raw

@+ord:Cmp -> {cmp_one_hot(ord) == True{} : Bool}

Compare whether one hot proof holds for the key ordering and comparison.

def cmp_eq_pair source · line 96 · raw

@pair:Pair(Pair(String, String), Cmp) -> {cmp_is_eq(unpack(pair)) == Cmp.is_eq(Pair.snd(Pair(String, String), Cmp, pair)) : Bool}

String.eq is defined by the EQ projection of String.cmp (Cmp.is_eq of Pair.snd since bend 2.0.33); matching the handed-back comparison pair exposes that definitional correspondence.

def cmp_eq_bridge source · line 110 · raw

@+s1:String -> @+s2:String -> {cmp_is_eq(cmp(s1, s2)) == eq(s1, s2) : Bool}

Compare whether eq bridge holds for the key ordering and comparison.

def bool_refl source · line 120 · raw

@+flag:Bool -> {Bool.cmp(flag, flag) == EQ{} : Cmp}

Evaluate refl for the key ordering and comparison.

def word_refl source · line 124 · raw

@width:Nat -> @+word:Word(width) -> {Word.cmp(width, word, word) == EQ{} : Cmp}

Handle word refl in the key ordering and comparison.

def u32_refl source · line 138 · raw

@+val:U32 -> {U32.cmp(val, val) == EQ{} : Cmp}

Encode or decode a 32-bit word for refl for the key ordering and comparison.

def char_refl source · line 142 · raw

@+ch:Char -> {Char.cmp(ch, ch) == ((ch, ch), EQ{}) : Pair(Pair(Char, Char), Cmp)}

Handle char refl in the key ordering and comparison.

def s_cmp_pair_refl source · line 146 · raw

@+str:String -> {String.cmp(str, str) == ((str, str), EQ{}) : Pair(Pair(String, String), Cmp)}

Handle s cmp pair refl in the key ordering and comparison.

def str_refl source · line 150 · raw

@+str:String -> {cmp(str, str) == EQ{} : Cmp}

Handle str refl in the key ordering and comparison.

def str_eq_refl source · line 155 · raw

@+str:String -> {eq(str, str) == True{} : Bool}

Handle str eq refl in the key ordering and comparison.