src/hex.bend source
src/hex.bend on the hub · documented module
# Hexadecimal digits# ==================## The sixteen lowercase hexadecimal digits as a closed type, with their# characters, values and bits. The codec reads identifiers and flags into this# type, so anything other than a lowercase hexadecimal digit (W3C 3.2.2,# HEXDIGLC) cannot appear in a parsed value. This module is internal: callers# handle identifiers as text through trace_context.bend. proofs/hex.bend proves# that decoding inverts encoding: every digit's character decodes back to it,# and an accepted character is exactly the encoding of the digit returned.import Base# A hexadecimal digit has exactly these sixteen values, H0 to Hf, in value# order. Encoding is lowercase.type Digit is Data: H0{} H1{} H2{} H3{} H4{} H5{} H6{} H7{} H8{} H9{} Ha{} Hb{} Hc{} Hd{} He{} Hf{}# The lowercase character of a digit: '0' to '9', then 'a' to 'f'.def Digit.to_char(digit: Digit) -> Char: match digit: case H0{}: '0' case H1{}: '1' case H2{}: '2' case H3{}: '3' case H4{}: '4' case H5{}: '5' case H6{}: '6' case H7{}: '7' case H8{}: '8' case H9{}: '9' case Ha{}: 'a' case Hb{}: 'b' case Hc{}: 'c' case Hd{}: 'd' case He{}: 'e' case Hf{}: 'f'# The value of a digit, 0 to 15.def Digit.to_u32(digit: Digit) -> U32: match digit: case H0{}: 0 case H1{}: 1 case H2{}: 2 case H3{}: 3 case H4{}: 4 case H5{}: 5 case H6{}: 6 case H7{}: 7 case H8{}: 8 case H9{}: 9 case Ha{}: 10 case Hb{}: 11 case Hc{}: 12 case Hd{}: 13 case He{}: 14 case Hf{}: 15# Whether the digit is 0. An identifier is all zero when every digit is.def Digit.is_zero(digit: Digit) -> Bool: match digit: case H0{}: True{} case H1{}: False{} case H2{}: False{} case H3{}: False{} case H4{}: False{} case H5{}: False{} case H6{}: False{} case H7{}: False{} case H8{}: False{} case H9{}: False{} case Ha{}: False{} case Hb{}: False{} case Hc{}: False{} case Hd{}: False{} case He{}: False{} case Hf{}: False{}# Whether bit 0 (value 1) of the digit is set. In the last digit of the flags# this is the sampled flag (W3C 3.2.2.5.1).def Digit.is_odd(digit: Digit) -> Bool: match digit: case H0{}: False{} case H1{}: True{} case H2{}: False{} case H3{}: True{} case H4{}: False{} case H5{}: True{} case H6{}: False{} case H7{}: True{} case H8{}: False{} case H9{}: True{} case Ha{}: False{} case Hb{}: True{} case Hc{}: False{} case Hd{}: True{} case He{}: False{} case Hf{}: True{}# Whether bit 1 (value 2) of the digit is set. In the last digit of the flags# this is the random-trace-id flag (W3C 3.2.2.5.2).def Digit.has_bit1(digit: Digit) -> Bool: match digit: case H0{}: False{} case H1{}: False{} case H2{}: True{} case H3{}: True{} case H4{}: False{} case H5{}: False{} case H6{}: True{} case H7{}: True{} case H8{}: False{} case H9{}: False{} case Ha{}: True{} case Hb{}: True{} case Hc{}: False{} case Hd{}: False{} case He{}: True{} case Hf{}: True{}# Whether bit 2 (value 4) of the digit is set.def Digit.has_bit2(digit: Digit) -> Bool: match digit: case H0{}: False{} case H1{}: False{} case H2{}: False{} case H3{}: False{} case H4{}: True{} case H5{}: True{} case H6{}: True{} case H7{}: True{} case H8{}: False{} case H9{}: False{} case Ha{}: False{} case Hb{}: False{} case Hc{}: True{} case Hd{}: True{} case He{}: True{} case Hf{}: True{}# Whether bit 3 (value 8) of the digit is set.def Digit.has_bit3(digit: Digit) -> Bool: match digit: case H0{}: False{} case H1{}: False{} case H2{}: False{} case H3{}: False{} case H4{}: False{} case H5{}: False{} case H6{}: False{} case H7{}: False{} case H8{}: True{} case H9{}: True{} case Ha{}: True{} case Hb{}: True{} case Hc{}: True{} case Hd{}: True{} case He{}: True{} case Hf{}: True{}# The digit whose value is bit0 + 2 * bit1 + 4 * bit2 + 8 * bit3.def Digit.from_bits(bit0: Bool, bit1: Bool, bit2: Bool, bit3: Bool) -> Digit: match bit0 bit1 bit2 bit3: case False{} False{} False{} False{}: H0{} case True{} False{} False{} False{}: H1{} case False{} True{} False{} False{}: H2{} case True{} True{} False{} False{}: H3{} case False{} False{} True{} False{}: H4{} case True{} False{} True{} False{}: H5{} case False{} True{} True{} False{}: H6{} case True{} True{} True{} False{}: H7{} case False{} False{} False{} True{}: H8{} case True{} False{} False{} True{}: H9{} case False{} True{} False{} True{}: Ha{} case True{} True{} False{} True{}: Hb{} case False{} False{} True{} True{}: Hc{} case True{} False{} True{} True{}: Hd{} case False{} True{} True{} True{}: He{} case True{} True{} True{} True{}: Hf{}# Every digit, in encoding order.def Digit.all() -> List<&2, Digit>: [H0{}, H1{}, H2{}, H3{}, H4{}, H5{}, H6{}, H7{}, H8{}, H9{}, Ha{}, Hb{}, Hc{}, Hd{}, He{}, Hf{}]# Search the encoder's own alphabet, so an accepted character is exactly the# encoding of the digit returned for it.def Digit.from_char.find(digits: List<&2, Digit>, +char: Char) -> Maybe<&2, Digit>: match digits: case Nil{}: None{} case Con{+digit, tail}: Bool.pick(Maybe<&2, Digit>, Char.is_eq(char, Digit.to_char(digit)), Some{digit}, Digit.from_char.find(tail, char))# The digit a character encodes. Uppercase and every non-hexadecimal character# are rejected with None.def Digit.from_char(char: Char) -> Maybe<&2, Digit>: Digit.from_char.find(Digit.all(), char)