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	
12	import Base
13	
14	# A hexadecimal digit has exactly these sixteen values, H0 to Hf, in value
15	# order. Encoding is lowercase.
16	type 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'.
35	def 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.
71	def 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.
107	def 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).
144	def 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).
181	def 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.
217	def 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.
253	def 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.
289	def 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.
325	def 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.
331	def 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.
341	def Digit.from_char(char: Char) -> Maybe<&2, Digit>:
342	  Digit.from_char.find(Digit.all(), char)