src/hex.bend
bend-trace-context@0.1.2.0 · 342 lines · 0 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)