src/hex.bend

bend-trace-context@0.2.0.0 · 342 lines · 12 definitions

1# Hexadecimal digits
2# ==================
3#
4# The sixteen lowercase hexadecimal digits as a closed type, with their
5# characters, values and bits. The codec reads identifiers and flags into this
6# type, so anything other than a lowercase hexadecimal digit (W3C 3.2.2,
7# HEXDIGLC) cannot appear in a parsed value. This module is internal: callers
8# handle identifiers as text through trace_context.bend. proofs/hex.bend proves
9# that decoding inverts encoding: every digit's character decodes back to it,
10# and an accepted character is exactly the encoding of the digit returned.
11
12import Base
13
14# A hexadecimal digit has exactly these sixteen values, H0 to Hf, in value
15# order. Encoding is lowercase.
16type Digit is Data:
17  H0{}
18  H1{}
19  H2{}
20  H3{}
21  H4{}
22  H5{}
23  H6{}
24  H7{}
25  H8{}
26  H9{}
27  Ha{}
28  Hb{}
29  Hc{}
30  Hd{}
31  He{}
32  Hf{}
33
34# The lowercase character of a digit: '0' to '9', then 'a' to 'f'.
35def Digit.to_char(digit: Digit) -> Char:
36  match digit:
37    case H0{}:
38      '0'
39    case H1{}:
40      '1'
41    case H2{}:
42      '2'
43    case H3{}:
44      '3'
45    case H4{}:
46      '4'
47    case H5{}:
48      '5'
49    case H6{}:
50      '6'
51    case H7{}:
52      '7'
53    case H8{}:
54      '8'
55    case H9{}:
56      '9'
57    case Ha{}:
58      'a'
59    case Hb{}:
60      'b'
61    case Hc{}:
62      'c'
63    case Hd{}:
64      'd'
65    case He{}:
66      'e'
67    case Hf{}:
68      'f'
69
70# The value of a digit, 0 to 15.
71def Digit.to_u32(digit: Digit) -> U32:
72  match digit:
73    case H0{}:
74      0
75    case H1{}:
76      1
77    case H2{}:
78      2
79    case H3{}:
80      3
81    case H4{}:
82      4
83    case H5{}:
84      5
85    case H6{}:
86      6
87    case H7{}:
88      7
89    case H8{}:
90      8
91    case H9{}:
92      9
93    case Ha{}:
94      10
95    case Hb{}:
96      11
97    case Hc{}:
98      12
99    case Hd{}:
100      13
101    case He{}:
102      14
103    case Hf{}:
104      15
105
106# Whether the digit is 0. An identifier is all zero when every digit is.
107def Digit.is_zero(digit: Digit) -> Bool:
108  match digit:
109    case H0{}:
110      True{}
111    case H1{}:
112      False{}
113    case H2{}:
114      False{}
115    case H3{}:
116      False{}
117    case H4{}:
118      False{}
119    case H5{}:
120      False{}
121    case H6{}:
122      False{}
123    case H7{}:
124      False{}
125    case H8{}:
126      False{}
127    case H9{}:
128      False{}
129    case Ha{}:
130      False{}
131    case Hb{}:
132      False{}
133    case Hc{}:
134      False{}
135    case Hd{}:
136      False{}
137    case He{}:
138      False{}
139    case Hf{}:
140      False{}
141
142# Whether bit 0 (value 1) of the digit is set. In the last digit of the flags
143# this is the sampled flag (W3C 3.2.2.5.1).
144def Digit.is_odd(digit: Digit) -> Bool:
145  match digit:
146    case H0{}:
147      False{}
148    case H1{}:
149      True{}
150    case H2{}:
151      False{}
152    case H3{}:
153      True{}
154    case H4{}:
155      False{}
156    case H5{}:
157      True{}
158    case H6{}:
159      False{}
160    case H7{}:
161      True{}
162    case H8{}:
163      False{}
164    case H9{}:
165      True{}
166    case Ha{}:
167      False{}
168    case Hb{}:
169      True{}
170    case Hc{}:
171      False{}
172    case Hd{}:
173      True{}
174    case He{}:
175      False{}
176    case Hf{}:
177      True{}
178
179# Whether bit 1 (value 2) of the digit is set. In the last digit of the flags
180# this is the random-trace-id flag (W3C 3.2.2.5.2).
181def Digit.has_bit1(digit: Digit) -> Bool:
182  match digit:
183    case H0{}:
184      False{}
185    case H1{}:
186      False{}
187    case H2{}:
188      True{}
189    case H3{}:
190      True{}
191    case H4{}:
192      False{}
193    case H5{}:
194      False{}
195    case H6{}:
196      True{}
197    case H7{}:
198      True{}
199    case H8{}:
200      False{}
201    case H9{}:
202      False{}
203    case Ha{}:
204      True{}
205    case Hb{}:
206      True{}
207    case Hc{}:
208      False{}
209    case Hd{}:
210      False{}
211    case He{}:
212      True{}
213    case Hf{}:
214      True{}
215
216# Whether bit 2 (value 4) of the digit is set.
217def Digit.has_bit2(digit: Digit) -> Bool:
218  match digit:
219    case H0{}:
220      False{}
221    case H1{}:
222      False{}
223    case H2{}:
224      False{}
225    case H3{}:
226      False{}
227    case H4{}:
228      True{}
229    case H5{}:
230      True{}
231    case H6{}:
232      True{}
233    case H7{}:
234      True{}
235    case H8{}:
236      False{}
237    case H9{}:
238      False{}
239    case Ha{}:
240      False{}
241    case Hb{}:
242      False{}
243    case Hc{}:
244      True{}
245    case Hd{}:
246      True{}
247    case He{}:
248      True{}
249    case Hf{}:
250      True{}
251
252# Whether bit 3 (value 8) of the digit is set.
253def Digit.has_bit3(digit: Digit) -> Bool:
254  match digit:
255    case H0{}:
256      False{}
257    case H1{}:
258      False{}
259    case H2{}:
260      False{}
261    case H3{}:
262      False{}
263    case H4{}:
264      False{}
265    case H5{}:
266      False{}
267    case H6{}:
268      False{}
269    case H7{}:
270      False{}
271    case H8{}:
272      True{}
273    case H9{}:
274      True{}
275    case Ha{}:
276      True{}
277    case Hb{}:
278      True{}
279    case Hc{}:
280      True{}
281    case Hd{}:
282      True{}
283    case He{}:
284      True{}
285    case Hf{}:
286      True{}
287
288# The digit whose value is bit0 + 2 * bit1 + 4 * bit2 + 8 * bit3.
289def Digit.from_bits(bit0: Bool, bit1: Bool, bit2: Bool, bit3: Bool) -> Digit:
290  match bit0 bit1 bit2 bit3:
291    case False{} False{} False{} False{}:
292      H0{}
293    case True{} False{} False{} False{}:
294      H1{}
295    case False{} True{} False{} False{}:
296      H2{}
297    case True{} True{} False{} False{}:
298      H3{}
299    case False{} False{} True{} False{}:
300      H4{}
301    case True{} False{} True{} False{}:
302      H5{}
303    case False{} True{} True{} False{}:
304      H6{}
305    case True{} True{} True{} False{}:
306      H7{}
307    case False{} False{} False{} True{}:
308      H8{}
309    case True{} False{} False{} True{}:
310      H9{}
311    case False{} True{} False{} True{}:
312      Ha{}
313    case True{} True{} False{} True{}:
314      Hb{}
315    case False{} False{} True{} True{}:
316      Hc{}
317    case True{} False{} True{} True{}:
318      Hd{}
319    case False{} True{} True{} True{}:
320      He{}
321    case True{} True{} True{} True{}:
322      Hf{}
323
324# Every digit, in encoding order.
325def Digit.all() -> List<&2, Digit>:
326  [H0{}, H1{}, H2{}, H3{}, H4{}, H5{}, H6{}, H7{},
327   H8{}, H9{}, Ha{}, Hb{}, Hc{}, Hd{}, He{}, Hf{}]
328
329# Search the encoder's own alphabet, so an accepted character is exactly the
330# encoding of the digit returned for it.
331def Digit.from_char.find(digits: List<&2, Digit>, +char: Char) -> Maybe<&2, Digit>:
332  match digits:
333    case Nil{}:
334      None{}
335    case Con{+digit, tail}:
336      Bool.pick(Maybe<&2, Digit>, Char.is_eq(char, Digit.to_char(digit)),
337        Some{digit}, Digit.from_char.find(tail, char))
338
339# The digit a character encodes. Uppercase and every non-hexadecimal character
340# are rejected with None.
341def Digit.from_char(char: Char) -> Maybe<&2, Digit>:
342  Digit.from_char.find(Digit.all(), char)