1	# Purpose: pure command definitions, validation, and text rendering for Bend CLIs.
2	# Expected output: ALL PROOFS CHECK.
3	# Run: bend cli.bend --check-only
4	
5	import Base
6	
7	type Style is Data:
8	  Bold{}
9	  Dim{}
10	  Under{}
11	  Red{}
12	  Green{}
13	  Yellow{}
14	  Blue{}
15	  Magenta{}
16	  Cyan{}
17	
18	type Segment is Data:
19	  Segment{text: String, styles: List<&2, Style>}
20	
21	def style_code(style: Style) -> String:
22	  match style:
23	    case Bold{}: "1"
24	    case Dim{}: "2"
25	    case Under{}: "4"
26	    case Red{}: "31"
27	    case Green{}: "32"
28	    case Yellow{}: "33"
29	    case Blue{}: "34"
30	    case Magenta{}: "35"
31	    case Cyan{}: "36"
32	
33	def style_codes_tail(styles: List<&2, Style>) -> String:
34	  match styles:
35	    case Nil{}: ""
36	    case h <> t:
37	      String.append(";", String.append(style_code(h), style_codes_tail(t)))
38	
39	def style_codes(styles: List<&2, Style>) -> String:
40	  match styles:
41	    case Nil{}: ""
42	    case h <> t:
43	      String.append(style_code(h), style_codes_tail(t))
44	
45	def paint(on: Bool, styles: List<&2, Style>, text: String) -> String:
46	  match on styles:
47	    case False{} _:
48	      text
49	    case True{} Nil{}:
50	      text
51	    case True{} h <> t:
52	      String.append("\u{1B}[",
53	        String.append(style_codes(h <> t),
54	          String.append("m", String.append(text, "\u{1B}[0m"))))
55	
56	def emit_go(segments: List<&2, Segment>, +on: Bool) -> String:
57	  match segments:
58	    case Nil{}:
59	      ""
60	    case h <> t:
61	      match h:
62	        case Segment{text, styles}:
63	          String.append(paint(on, styles, text), emit_go(t, on))
64	
65	def emit(on: Bool, segments: List<&2, Segment>) -> String:
66	  emit_go(segments, on)
67	
68	def sgr_body_char(+c: Char) -> Bool:
69	  Bool.or(Char.is_digit(c), Char.is_eq(c, ';'))
70	
71	type StripState is Data:
72	  StripPlain{}
73	  StripEsc{}
74	  StripBody{pending: String}
75	
76	def strip_go(s: String, state: StripState) -> String:
77	  match s:
78	    case SNil{}:
79	      match state:
80	        case StripPlain{}: ""
81	        case StripEsc{}: "\u{1B}"
82	        case StripBody{pending}: pending
83	    case SCon{+h, t}:
84	      match state:
85	        case StripPlain{}:
86	          +esc = Char.is_eq(h, '\u{1B}')
87	          String.append(Bool.pick(String, esc, "", Char.show(h)),
88	            strip_go(t, Bool.pick(StripState, esc, StripEsc{}, StripPlain{})))
89	        case StripEsc{}:
90	          +bracket = Char.is_eq(h, '[')
91	          +esc = Char.is_eq(h, '\u{1B}')
92	          +prefix = Bool.pick(String, bracket, "",
93	            Bool.pick(String, esc, "\u{1B}",
94	              String.append("\u{1B}", Char.show(h))))
95	          +next = Bool.pick(StripState, bracket, StripBody{"\u{1B}["},
96	            Bool.pick(StripState, esc, StripEsc{}, StripPlain{}))
97	          String.append(prefix, strip_go(t, next))
98	        case StripBody{+pending}:
99	          +end = Char.is_eq(h, 'm')
100	          +esc = Char.is_eq(h, '\u{1B}')
101	          +ok = sgr_body_char(h)
102	          +grown = String.append(pending, Char.show(h))
103	          +prefix = Bool.pick(String, end, "",
104	            Bool.pick(String, esc, pending,
105	              Bool.pick(String, ok, "", grown)))
106	          +next = Bool.pick(StripState, end, StripPlain{},
107	            Bool.pick(StripState, esc, StripEsc{},
108	              Bool.pick(StripState, ok, StripBody{grown}, StripPlain{})))
109	          String.append(prefix, strip_go(t, next))
110	
111	def strip(s: String) -> String:
112	  strip_go(s, StripPlain{})
113	
114	type CodeRange is Data:
115	  CodeRange{lo: U32, hi: U32}
116	
117	def contains_range(ranges: List<&2, CodeRange>, +code: U32) -> Bool:
118	  match ranges:
119	    case Nil{}:
120	      False{}
121	    case CodeRange{lo, hi} <> tail:
122	      Bool.or(Bool.and(U32.is_ge(code, lo), U32.is_le(code, hi)),
123	        contains_range(tail, code))
124	
125	# Unicode 15.1 East Asian Wide and Fullwidth ranges, including reserved ranges.
126	# Source: https://www.unicode.org/Public/15.1.0/ucd/EastAsianWidth.txt
127	def unicode_is_wide(code: U32) -> Bool:
128	  contains_range([
129	    CodeRange{4352, 4447},
130	    CodeRange{8986, 8987},
131	    CodeRange{9001, 9002},
132	    CodeRange{9193, 9196},
133	    CodeRange{9200, 9200},
134	    CodeRange{9203, 9203},
135	    CodeRange{9725, 9726},
136	    CodeRange{9748, 9749},
137	    CodeRange{9800, 9811},
138	    CodeRange{9855, 9855},
139	    CodeRange{9875, 9875},
140	    CodeRange{9889, 9889},
141	    CodeRange{9898, 9899},
142	    CodeRange{9917, 9918},
143	    CodeRange{9924, 9925},
144	    CodeRange{9934, 9934},
145	    CodeRange{9940, 9940},
146	    CodeRange{9962, 9962},
147	    CodeRange{9970, 9971},
148	    CodeRange{9973, 9973},
149	    CodeRange{9978, 9978},
150	    CodeRange{9981, 9981},
151	    CodeRange{9989, 9989},
152	    CodeRange{9994, 9995},
153	    CodeRange{10024, 10024},
154	    CodeRange{10060, 10060},
155	    CodeRange{10062, 10062},
156	    CodeRange{10067, 10069},
157	    CodeRange{10071, 10071},
158	    CodeRange{10133, 10135},
159	    CodeRange{10160, 10160},
160	    CodeRange{10175, 10175},
161	    CodeRange{11035, 11036},
162	    CodeRange{11088, 11088},
163	    CodeRange{11093, 11093},
164	    CodeRange{11904, 11929},
165	    CodeRange{11931, 12019},
166	    CodeRange{12032, 12245},
167	    CodeRange{12272, 12350},
168	    CodeRange{12353, 12438},
169	    CodeRange{12441, 12543},
170	    CodeRange{12549, 12591},
171	    CodeRange{12593, 12686},
172	    CodeRange{12688, 12771},
173	    CodeRange{12783, 12830},
174	    CodeRange{12832, 12871},
175	    CodeRange{12880, 19903},
176	    CodeRange{19968, 42124},
177	    CodeRange{42128, 42182},
178	    CodeRange{43360, 43388},
179	    CodeRange{44032, 55203},
180	    CodeRange{63744, 64255},
181	    CodeRange{65040, 65049},
182	    CodeRange{65072, 65106},
183	    CodeRange{65108, 65126},
184	    CodeRange{65128, 65131},
185	    CodeRange{65281, 65376},
186	    CodeRange{65504, 65510},
187	    CodeRange{94176, 94180},
188	    CodeRange{94192, 94193},
189	    CodeRange{94208, 100343},
190	    CodeRange{100352, 101589},
191	    CodeRange{101632, 101640},
192	    CodeRange{110576, 110579},
193	    CodeRange{110581, 110587},
194	    CodeRange{110589, 110590},
195	    CodeRange{110592, 110882},
196	    CodeRange{110898, 110898},
197	    CodeRange{110928, 110930},
198	    CodeRange{110933, 110933},
199	    CodeRange{110948, 110951},
200	    CodeRange{110960, 111355},
201	    CodeRange{126980, 126980},
202	    CodeRange{127183, 127183},
203	    CodeRange{127374, 127374},
204	    CodeRange{127377, 127386},
205	    CodeRange{127488, 127490},
206	    CodeRange{127504, 127547},
207	    CodeRange{127552, 127560},
208	    CodeRange{127568, 127569},
209	    CodeRange{127584, 127589},
210	    CodeRange{127744, 127776},
211	    CodeRange{127789, 127797},
212	    CodeRange{127799, 127868},
213	    CodeRange{127870, 127891},
214	    CodeRange{127904, 127946},
215	    CodeRange{127951, 127955},
216	    CodeRange{127968, 127984},
217	    CodeRange{127988, 127988},
218	    CodeRange{127992, 128062},
219	    CodeRange{128064, 128064},
220	    CodeRange{128066, 128252},
221	    CodeRange{128255, 128317},
222	    CodeRange{128331, 128334},
223	    CodeRange{128336, 128359},
224	    CodeRange{128378, 128378},
225	    CodeRange{128405, 128406},
226	    CodeRange{128420, 128420},
227	    CodeRange{128507, 128591},
228	    CodeRange{128640, 128709},
229	    CodeRange{128716, 128716},
230	    CodeRange{128720, 128722},
231	    CodeRange{128725, 128727},
232	    CodeRange{128732, 128735},
233	    CodeRange{128747, 128748},
234	    CodeRange{128756, 128764},
235	    CodeRange{128992, 129003},
236	    CodeRange{129008, 129008},
237	    CodeRange{129292, 129338},
238	    CodeRange{129340, 129349},
239	    CodeRange{129351, 129535},
240	    CodeRange{129648, 129660},
241	    CodeRange{129664, 129672},
242	    CodeRange{129680, 129725},
243	    CodeRange{129727, 129733},
244	    CodeRange{129742, 129755},
245	    CodeRange{129760, 129768},
246	    CodeRange{129776, 129784},
247	    CodeRange{131072, 196605},
248	    CodeRange{196608, 262141},
249	  ], code)
250	
251	# Unicode 15.1 nonspacing and enclosing mark ranges (Mn and Me).
252	# Source: https://www.unicode.org/Public/15.1.0/ucd/UnicodeData.txt
253	def unicode_is_zero_mark(code: U32) -> Bool:
254	  contains_range([
255	    CodeRange{768, 879},
256	    CodeRange{1155, 1161},
257	    CodeRange{1425, 1469},
258	    CodeRange{1471, 1471},
259	    CodeRange{1473, 1474},
260	    CodeRange{1476, 1477},
261	    CodeRange{1479, 1479},
262	    CodeRange{1552, 1562},
263	    CodeRange{1611, 1631},
264	    CodeRange{1648, 1648},
265	    CodeRange{1750, 1756},
266	    CodeRange{1759, 1764},
267	    CodeRange{1767, 1768},
268	    CodeRange{1770, 1773},
269	    CodeRange{1809, 1809},
270	    CodeRange{1840, 1866},
271	    CodeRange{1958, 1968},
272	    CodeRange{2027, 2035},
273	    CodeRange{2045, 2045},
274	    CodeRange{2070, 2073},
275	    CodeRange{2075, 2083},
276	    CodeRange{2085, 2087},
277	    CodeRange{2089, 2093},
278	    CodeRange{2137, 2139},
279	    CodeRange{2200, 2207},
280	    CodeRange{2250, 2273},
281	    CodeRange{2275, 2306},
282	    CodeRange{2362, 2362},
283	    CodeRange{2364, 2364},
284	    CodeRange{2369, 2376},
285	    CodeRange{2381, 2381},
286	    CodeRange{2385, 2391},
287	    CodeRange{2402, 2403},
288	    CodeRange{2433, 2433},
289	    CodeRange{2492, 2492},
290	    CodeRange{2497, 2500},
291	    CodeRange{2509, 2509},
292	    CodeRange{2530, 2531},
293	    CodeRange{2558, 2558},
294	    CodeRange{2561, 2562},
295	    CodeRange{2620, 2620},
296	    CodeRange{2625, 2626},
297	    CodeRange{2631, 2632},
298	    CodeRange{2635, 2637},
299	    CodeRange{2641, 2641},
300	    CodeRange{2672, 2673},
301	    CodeRange{2677, 2677},
302	    CodeRange{2689, 2690},
303	    CodeRange{2748, 2748},
304	    CodeRange{2753, 2757},
305	    CodeRange{2759, 2760},
306	    CodeRange{2765, 2765},
307	    CodeRange{2786, 2787},
308	    CodeRange{2810, 2815},
309	    CodeRange{2817, 2817},
310	    CodeRange{2876, 2876},
311	    CodeRange{2879, 2879},
312	    CodeRange{2881, 2884},
313	    CodeRange{2893, 2893},
314	    CodeRange{2901, 2902},
315	    CodeRange{2914, 2915},
316	    CodeRange{2946, 2946},
317	    CodeRange{3008, 3008},
318	    CodeRange{3021, 3021},
319	    CodeRange{3072, 3072},
320	    CodeRange{3076, 3076},
321	    CodeRange{3132, 3132},
322	    CodeRange{3134, 3136},
323	    CodeRange{3142, 3144},
324	    CodeRange{3146, 3149},
325	    CodeRange{3157, 3158},
326	    CodeRange{3170, 3171},
327	    CodeRange{3201, 3201},
328	    CodeRange{3260, 3260},
329	    CodeRange{3263, 3263},
330	    CodeRange{3270, 3270},
331	    CodeRange{3276, 3277},
332	    CodeRange{3298, 3299},
333	    CodeRange{3328, 3329},
334	    CodeRange{3387, 3388},
335	    CodeRange{3393, 3396},
336	    CodeRange{3405, 3405},
337	    CodeRange{3426, 3427},
338	    CodeRange{3457, 3457},
339	    CodeRange{3530, 3530},
340	    CodeRange{3538, 3540},
341	    CodeRange{3542, 3542},
342	    CodeRange{3633, 3633},
343	    CodeRange{3636, 3642},
344	    CodeRange{3655, 3662},
345	    CodeRange{3761, 3761},
346	    CodeRange{3764, 3772},
347	    CodeRange{3784, 3790},
348	    CodeRange{3864, 3865},
349	    CodeRange{3893, 3893},
350	    CodeRange{3895, 3895},
351	    CodeRange{3897, 3897},
352	    CodeRange{3953, 3966},
353	    CodeRange{3968, 3972},
354	    CodeRange{3974, 3975},
355	    CodeRange{3981, 3991},
356	    CodeRange{3993, 4028},
357	    CodeRange{4038, 4038},
358	    CodeRange{4141, 4144},
359	    CodeRange{4146, 4151},
360	    CodeRange{4153, 4154},
361	    CodeRange{4157, 4158},
362	    CodeRange{4184, 4185},
363	    CodeRange{4190, 4192},
364	    CodeRange{4209, 4212},
365	    CodeRange{4226, 4226},
366	    CodeRange{4229, 4230},
367	    CodeRange{4237, 4237},
368	    CodeRange{4253, 4253},
369	    CodeRange{4957, 4959},
370	    CodeRange{5906, 5908},
371	    CodeRange{5938, 5939},
372	    CodeRange{5970, 5971},
373	    CodeRange{6002, 6003},
374	    CodeRange{6068, 6069},
375	    CodeRange{6071, 6077},
376	    CodeRange{6086, 6086},
377	    CodeRange{6089, 6099},
378	    CodeRange{6109, 6109},
379	    CodeRange{6155, 6157},
380	    CodeRange{6159, 6159},
381	    CodeRange{6277, 6278},
382	    CodeRange{6313, 6313},
383	    CodeRange{6432, 6434},
384	    CodeRange{6439, 6440},
385	    CodeRange{6450, 6450},
386	    CodeRange{6457, 6459},
387	    CodeRange{6679, 6680},
388	    CodeRange{6683, 6683},
389	    CodeRange{6742, 6742},
390	    CodeRange{6744, 6750},
391	    CodeRange{6752, 6752},
392	    CodeRange{6754, 6754},
393	    CodeRange{6757, 6764},
394	    CodeRange{6771, 6780},
395	    CodeRange{6783, 6783},
396	    CodeRange{6832, 6862},
397	    CodeRange{6912, 6915},
398	    CodeRange{6964, 6964},
399	    CodeRange{6966, 6970},
400	    CodeRange{6972, 6972},
401	    CodeRange{6978, 6978},
402	    CodeRange{7019, 7027},
403	    CodeRange{7040, 7041},
404	    CodeRange{7074, 7077},
405	    CodeRange{7080, 7081},
406	    CodeRange{7083, 7085},
407	    CodeRange{7142, 7142},
408	    CodeRange{7144, 7145},
409	    CodeRange{7149, 7149},
410	    CodeRange{7151, 7153},
411	    CodeRange{7212, 7219},
412	    CodeRange{7222, 7223},
413	    CodeRange{7376, 7378},
414	    CodeRange{7380, 7392},
415	    CodeRange{7394, 7400},
416	    CodeRange{7405, 7405},
417	    CodeRange{7412, 7412},
418	    CodeRange{7416, 7417},
419	    CodeRange{7616, 7679},
420	    CodeRange{8400, 8432},
421	    CodeRange{11503, 11505},
422	    CodeRange{11647, 11647},
423	    CodeRange{11744, 11775},
424	    CodeRange{12330, 12333},
425	    CodeRange{12441, 12442},
426	    CodeRange{42607, 42610},
427	    CodeRange{42612, 42621},
428	    CodeRange{42654, 42655},
429	    CodeRange{42736, 42737},
430	    CodeRange{43010, 43010},
431	    CodeRange{43014, 43014},
432	    CodeRange{43019, 43019},
433	    CodeRange{43045, 43046},
434	    CodeRange{43052, 43052},
435	    CodeRange{43204, 43205},
436	    CodeRange{43232, 43249},
437	    CodeRange{43263, 43263},
438	    CodeRange{43302, 43309},
439	    CodeRange{43335, 43345},
440	    CodeRange{43392, 43394},
441	    CodeRange{43443, 43443},
442	    CodeRange{43446, 43449},
443	    CodeRange{43452, 43453},
444	    CodeRange{43493, 43493},
445	    CodeRange{43561, 43566},
446	    CodeRange{43569, 43570},
447	    CodeRange{43573, 43574},
448	    CodeRange{43587, 43587},
449	    CodeRange{43596, 43596},
450	    CodeRange{43644, 43644},
451	    CodeRange{43696, 43696},
452	    CodeRange{43698, 43700},
453	    CodeRange{43703, 43704},
454	    CodeRange{43710, 43711},
455	    CodeRange{43713, 43713},
456	    CodeRange{43756, 43757},
457	    CodeRange{43766, 43766},
458	    CodeRange{44005, 44005},
459	    CodeRange{44008, 44008},
460	    CodeRange{44013, 44013},
461	    CodeRange{64286, 64286},
462	    CodeRange{65024, 65039},
463	    CodeRange{65056, 65071},
464	    CodeRange{66045, 66045},
465	    CodeRange{66272, 66272},
466	    CodeRange{66422, 66426},
467	    CodeRange{68097, 68099},
468	    CodeRange{68101, 68102},
469	    CodeRange{68108, 68111},
470	    CodeRange{68152, 68154},
471	    CodeRange{68159, 68159},
472	    CodeRange{68325, 68326},
473	    CodeRange{68900, 68903},
474	    CodeRange{69291, 69292},
475	    CodeRange{69373, 69375},
476	    CodeRange{69446, 69456},
477	    CodeRange{69506, 69509},
478	    CodeRange{69633, 69633},
479	    CodeRange{69688, 69702},
480	    CodeRange{69744, 69744},
481	    CodeRange{69747, 69748},
482	    CodeRange{69759, 69761},
483	    CodeRange{69811, 69814},
484	    CodeRange{69817, 69818},
485	    CodeRange{69826, 69826},
486	    CodeRange{69888, 69890},
487	    CodeRange{69927, 69931},
488	    CodeRange{69933, 69940},
489	    CodeRange{70003, 70003},
490	    CodeRange{70016, 70017},
491	    CodeRange{70070, 70078},
492	    CodeRange{70089, 70092},
493	    CodeRange{70095, 70095},
494	    CodeRange{70191, 70193},
495	    CodeRange{70196, 70196},
496	    CodeRange{70198, 70199},
497	    CodeRange{70206, 70206},
498	    CodeRange{70209, 70209},
499	    CodeRange{70367, 70367},
500	    CodeRange{70371, 70378},
501	    CodeRange{70400, 70401},
502	    CodeRange{70459, 70460},
503	    CodeRange{70464, 70464},
504	    CodeRange{70502, 70508},
505	    CodeRange{70512, 70516},
506	    CodeRange{70712, 70719},
507	    CodeRange{70722, 70724},
508	    CodeRange{70726, 70726},
509	    CodeRange{70750, 70750},
510	    CodeRange{70835, 70840},
511	    CodeRange{70842, 70842},
512	    CodeRange{70847, 70848},
513	    CodeRange{70850, 70851},
514	    CodeRange{71090, 71093},
515	    CodeRange{71100, 71101},
516	    CodeRange{71103, 71104},
517	    CodeRange{71132, 71133},
518	    CodeRange{71219, 71226},
519	    CodeRange{71229, 71229},
520	    CodeRange{71231, 71232},
521	    CodeRange{71339, 71339},
522	    CodeRange{71341, 71341},
523	    CodeRange{71344, 71349},
524	    CodeRange{71351, 71351},
525	    CodeRange{71453, 71455},
526	    CodeRange{71458, 71461},
527	    CodeRange{71463, 71467},
528	    CodeRange{71727, 71735},
529	    CodeRange{71737, 71738},
530	    CodeRange{71995, 71996},
531	    CodeRange{71998, 71998},
532	    CodeRange{72003, 72003},
533	    CodeRange{72148, 72151},
534	    CodeRange{72154, 72155},
535	    CodeRange{72160, 72160},
536	    CodeRange{72193, 72202},
537	    CodeRange{72243, 72248},
538	    CodeRange{72251, 72254},
539	    CodeRange{72263, 72263},
540	    CodeRange{72273, 72278},
541	    CodeRange{72281, 72283},
542	    CodeRange{72330, 72342},
543	    CodeRange{72344, 72345},
544	    CodeRange{72752, 72758},
545	    CodeRange{72760, 72765},
546	    CodeRange{72767, 72767},
547	    CodeRange{72850, 72871},
548	    CodeRange{72874, 72880},
549	    CodeRange{72882, 72883},
550	    CodeRange{72885, 72886},
551	    CodeRange{73009, 73014},
552	    CodeRange{73018, 73018},
553	    CodeRange{73020, 73021},
554	    CodeRange{73023, 73029},
555	    CodeRange{73031, 73031},
556	    CodeRange{73104, 73105},
557	    CodeRange{73109, 73109},
558	    CodeRange{73111, 73111},
559	    CodeRange{73459, 73460},
560	    CodeRange{73472, 73473},
561	    CodeRange{73526, 73530},
562	    CodeRange{73536, 73536},
563	    CodeRange{73538, 73538},
564	    CodeRange{78912, 78912},
565	    CodeRange{78919, 78933},
566	    CodeRange{92912, 92916},
567	    CodeRange{92976, 92982},
568	    CodeRange{94031, 94031},
569	    CodeRange{94095, 94098},
570	    CodeRange{94180, 94180},
571	    CodeRange{113821, 113822},
572	    CodeRange{118528, 118573},
573	    CodeRange{118576, 118598},
574	    CodeRange{119143, 119145},
575	    CodeRange{119163, 119170},
576	    CodeRange{119173, 119179},
577	    CodeRange{119210, 119213},
578	    CodeRange{119362, 119364},
579	    CodeRange{121344, 121398},
580	    CodeRange{121403, 121452},
581	    CodeRange{121461, 121461},
582	    CodeRange{121476, 121476},
583	    CodeRange{121499, 121503},
584	    CodeRange{121505, 121519},
585	    CodeRange{122880, 122886},
586	    CodeRange{122888, 122904},
587	    CodeRange{122907, 122913},
588	    CodeRange{122915, 122916},
589	    CodeRange{122918, 122922},
590	    CodeRange{123023, 123023},
591	    CodeRange{123184, 123190},
592	    CodeRange{123566, 123566},
593	    CodeRange{123628, 123631},
594	    CodeRange{124140, 124143},
595	    CodeRange{125136, 125142},
596	    CodeRange{125252, 125258},
597	    CodeRange{917760, 917999},
598	  ], code)
599	
600	# Unicode 15.1 Extended_Pictographic ranges, including reserved ranges.
601	# Source: https://www.unicode.org/Public/15.1.0/ucd/emoji/emoji-data.txt
602	def unicode_is_pictographic(code: U32) -> Bool:
603	  contains_range([
604	    CodeRange{169, 169},
605	    CodeRange{174, 174},
606	    CodeRange{8252, 8252},
607	    CodeRange{8265, 8265},
608	    CodeRange{8482, 8482},
609	    CodeRange{8505, 8505},
610	    CodeRange{8596, 8601},
611	    CodeRange{8617, 8618},
612	    CodeRange{8986, 8987},
613	    CodeRange{9000, 9000},
614	    CodeRange{9096, 9096},
615	    CodeRange{9167, 9167},
616	    CodeRange{9193, 9203},
617	    CodeRange{9208, 9210},
618	    CodeRange{9410, 9410},
619	    CodeRange{9642, 9643},
620	    CodeRange{9654, 9654},
621	    CodeRange{9664, 9664},
622	    CodeRange{9723, 9726},
623	    CodeRange{9728, 9733},
624	    CodeRange{9735, 9746},
625	    CodeRange{9748, 9861},
626	    CodeRange{9872, 9989},
627	    CodeRange{9992, 10002},
628	    CodeRange{10004, 10004},
629	    CodeRange{10006, 10006},
630	    CodeRange{10013, 10013},
631	    CodeRange{10017, 10017},
632	    CodeRange{10024, 10024},
633	    CodeRange{10035, 10036},
634	    CodeRange{10052, 10052},
635	    CodeRange{10055, 10055},
636	    CodeRange{10060, 10060},
637	    CodeRange{10062, 10062},
638	    CodeRange{10067, 10069},
639	    CodeRange{10071, 10071},
640	    CodeRange{10083, 10087},
641	    CodeRange{10133, 10135},
642	    CodeRange{10145, 10145},
643	    CodeRange{10160, 10160},
644	    CodeRange{10175, 10175},
645	    CodeRange{10548, 10549},
646	    CodeRange{11013, 11015},
647	    CodeRange{11035, 11036},
648	    CodeRange{11088, 11088},
649	    CodeRange{11093, 11093},
650	    CodeRange{12336, 12336},
651	    CodeRange{12349, 12349},
652	    CodeRange{12951, 12951},
653	    CodeRange{12953, 12953},
654	    CodeRange{126976, 127231},
655	    CodeRange{127245, 127247},
656	    CodeRange{127279, 127279},
657	    CodeRange{127340, 127345},
658	    CodeRange{127358, 127359},
659	    CodeRange{127374, 127374},
660	    CodeRange{127377, 127386},
661	    CodeRange{127405, 127461},
662	    CodeRange{127489, 127503},
663	    CodeRange{127514, 127514},
664	    CodeRange{127535, 127535},
665	    CodeRange{127538, 127546},
666	    CodeRange{127548, 127551},
667	    CodeRange{127561, 127994},
668	    CodeRange{128000, 128317},
669	    CodeRange{128326, 128591},
670	    CodeRange{128640, 128767},
671	    CodeRange{128884, 128895},
672	    CodeRange{128981, 129023},
673	    CodeRange{129036, 129039},
674	    CodeRange{129096, 129103},
675	    CodeRange{129114, 129119},
676	    CodeRange{129160, 129167},
677	    CodeRange{129198, 129279},
678	    CodeRange{129292, 129338},
679	    CodeRange{129340, 129349},
680	    CodeRange{129351, 129791},
681	    CodeRange{130048, 131069},
682	  ], code)
683	
684	# Unicode 15.1 Emoji_Modifier_Base ranges: the emoji a skin tone modifies.
685	# Source: https://www.unicode.org/Public/15.1.0/ucd/emoji/emoji-data.txt
686	def unicode_takes_tone(code: U32) -> Bool:
687	  contains_range([
688	    CodeRange{9757, 9757},
689	    CodeRange{9977, 9977},
690	    CodeRange{9994, 9997},
691	    CodeRange{127877, 127877},
692	    CodeRange{127938, 127940},
693	    CodeRange{127943, 127943},
694	    CodeRange{127946, 127948},
695	    CodeRange{128066, 128067},
696	    CodeRange{128070, 128080},
697	    CodeRange{128102, 128120},
698	    CodeRange{128124, 128124},
699	    CodeRange{128129, 128131},
700	    CodeRange{128133, 128135},
701	    CodeRange{128143, 128143},
702	    CodeRange{128145, 128145},
703	    CodeRange{128170, 128170},
704	    CodeRange{128372, 128373},
705	    CodeRange{128378, 128378},
706	    CodeRange{128400, 128400},
707	    CodeRange{128405, 128406},
708	    CodeRange{128581, 128583},
709	    CodeRange{128587, 128591},
710	    CodeRange{128675, 128675},
711	    CodeRange{128692, 128694},
712	    CodeRange{128704, 128704},
713	    CodeRange{128716, 128716},
714	    CodeRange{129292, 129292},
715	    CodeRange{129295, 129295},
716	    CodeRange{129304, 129311},
717	    CodeRange{129318, 129318},
718	    CodeRange{129328, 129337},
719	    CodeRange{129340, 129342},
720	    CodeRange{129399, 129399},
721	    CodeRange{129461, 129462},
722	    CodeRange{129464, 129465},
723	    CodeRange{129467, 129467},
724	    CodeRange{129485, 129487},
725	    CodeRange{129489, 129501},
726	    CodeRange{129731, 129733},
727	    CodeRange{129776, 129784},
728	  ], code)
729	
730	# Unicode 15.1 code points with an emoji presentation sequence (VS16) that
731	# are not East Asian Wide or Fullwidth, so VS16 widens them to 2.
732	# Sources: https://www.unicode.org/Public/15.1.0/ucd/emoji/emoji-variation-sequences.txt
733	# and https://www.unicode.org/Public/15.1.0/ucd/EastAsianWidth.txt
734	def unicode_widens_with_vs16(code: U32) -> Bool:
735	  contains_range([
736	    CodeRange{35, 35},
737	    CodeRange{42, 42},
738	    CodeRange{48, 57},
739	    CodeRange{169, 169},
740	    CodeRange{174, 174},
741	    CodeRange{8252, 8252},
742	    CodeRange{8265, 8265},
743	    CodeRange{8482, 8482},
744	    CodeRange{8505, 8505},
745	    CodeRange{8596, 8601},
746	    CodeRange{8617, 8618},
747	    CodeRange{9000, 9000},
748	    CodeRange{9167, 9167},
749	    CodeRange{9197, 9199},
750	    CodeRange{9201, 9202},
751	    CodeRange{9208, 9210},
752	    CodeRange{9410, 9410},
753	    CodeRange{9642, 9643},
754	    CodeRange{9654, 9654},
755	    CodeRange{9664, 9664},
756	    CodeRange{9723, 9724},
757	    CodeRange{9728, 9732},
758	    CodeRange{9742, 9742},
759	    CodeRange{9745, 9745},
760	    CodeRange{9752, 9752},
761	    CodeRange{9757, 9757},
762	    CodeRange{9760, 9760},
763	    CodeRange{9762, 9763},
764	    CodeRange{9766, 9766},
765	    CodeRange{9770, 9770},
766	    CodeRange{9774, 9775},
767	    CodeRange{9784, 9786},
768	    CodeRange{9792, 9792},
769	    CodeRange{9794, 9794},
770	    CodeRange{9823, 9824},
771	    CodeRange{9827, 9827},
772	    CodeRange{9829, 9830},
773	    CodeRange{9832, 9832},
774	    CodeRange{9851, 9851},
775	    CodeRange{9854, 9854},
776	    CodeRange{9874, 9874},
777	    CodeRange{9876, 9879},
778	    CodeRange{9881, 9881},
779	    CodeRange{9883, 9884},
780	    CodeRange{9888, 9888},
781	    CodeRange{9895, 9895},
782	    CodeRange{9904, 9905},
783	    CodeRange{9928, 9928},
784	    CodeRange{9935, 9935},
785	    CodeRange{9937, 9937},
786	    CodeRange{9939, 9939},
787	    CodeRange{9961, 9961},
788	    CodeRange{9968, 9969},
789	    CodeRange{9972, 9972},
790	    CodeRange{9975, 9977},
791	    CodeRange{9986, 9986},
792	    CodeRange{9992, 9993},
793	    CodeRange{9996, 9997},
794	    CodeRange{9999, 9999},
795	    CodeRange{10002, 10002},
796	    CodeRange{10004, 10004},
797	    CodeRange{10006, 10006},
798	    CodeRange{10013, 10013},
799	    CodeRange{10017, 10017},
800	    CodeRange{10035, 10036},
801	    CodeRange{10052, 10052},
802	    CodeRange{10055, 10055},
803	    CodeRange{10083, 10084},
804	    CodeRange{10145, 10145},
805	    CodeRange{10548, 10549},
806	    CodeRange{11013, 11015},
807	    CodeRange{127344, 127345},
808	    CodeRange{127358, 127359},
809	    CodeRange{127777, 127777},
810	    CodeRange{127780, 127788},
811	    CodeRange{127798, 127798},
812	    CodeRange{127869, 127869},
813	    CodeRange{127894, 127895},
814	    CodeRange{127897, 127899},
815	    CodeRange{127902, 127903},
816	    CodeRange{127947, 127950},
817	    CodeRange{127956, 127967},
818	    CodeRange{127987, 127987},
819	    CodeRange{127989, 127989},
820	    CodeRange{127991, 127991},
821	    CodeRange{128063, 128063},
822	    CodeRange{128065, 128065},
823	    CodeRange{128253, 128253},
824	    CodeRange{128329, 128330},
825	    CodeRange{128367, 128368},
826	    CodeRange{128371, 128377},
827	    CodeRange{128391, 128391},
828	    CodeRange{128394, 128397},
829	    CodeRange{128400, 128400},
830	    CodeRange{128421, 128421},
831	    CodeRange{128424, 128424},
832	    CodeRange{128433, 128434},
833	    CodeRange{128444, 128444},
834	    CodeRange{128450, 128452},
835	    CodeRange{128465, 128467},
836	    CodeRange{128476, 128478},
837	    CodeRange{128481, 128481},
838	    CodeRange{128483, 128483},
839	    CodeRange{128488, 128488},
840	    CodeRange{128495, 128495},
841	    CodeRange{128499, 128499},
842	    CodeRange{128506, 128506},
843	    CodeRange{128715, 128715},
844	    CodeRange{128717, 128719},
845	    CodeRange{128736, 128741},
846	    CodeRange{128745, 128745},
847	    CodeRange{128752, 128752},
848	    CodeRange{128755, 128755},
849	  ], code)
850	
851	# A code point's own width: controls, marks, 200B-200F and tag characters
852	# (E0000-E007F) are 0, East Asian Wide and Fullwidth are 2, the rest 1.
853	def code_width_by(small: Bool, +code: U32) -> Nat:
854	  match small:
855	    case True{}:
856	      Bool.pick(Nat, Bool.or(U32.is_le(code, 31),
857	        Bool.and(U32.is_ge(code, 127), U32.is_le(code, 159))), 0n, 1n)
858	    case False{}:
859	      Bool.pick(Nat, Bool.or(unicode_is_zero_mark(code),
860	        Bool.or(Bool.and(U32.is_ge(code, 8203), U32.is_le(code, 8207)),
861	          Bool.and(U32.is_ge(code, 917504), U32.is_le(code, 917631)))), 0n,
862	        Bool.pick(Nat, unicode_is_wide(code), 2n, 1n))
863	
864	def code_width(+code: U32) -> Nat:
865	  code_width_by(U32.is_lt(code, 768), code)
866	
867	# What a code point can do in an emoji sequence (UTS #51): start a keycap
868	# (#, * and 0-9), be a pictograph, a skin tone, a ZWJ or VS16, or none.
869	type CodeClass is Data:
870	  PlainCode{}
871	  KeycapCode{}
872	  PictoCode{}
873	  ToneCode{}
874	  JoinerCode{}
875	  Vs16Code{}
876	
877	# Where width stands in an emoji sequence: outside one; after an emoji, with
878	# the code a skin tone or VS16 applies to, whether it counts 1 so far, and
879	# whether a ZWJ may join it; after such a ZWJ; or after a pictograph that a
880	# ZWJ joined, which adds nothing.
881	type EmojiRun is Data:
882	  EmojiNone{}
883	  EmojiBase{code: U32, narrow: Bool, join: Bool}
884	  EmojiJoiner{}
885	  EmojiJoined{code: U32}
886	
887	type WidthStep is Data:
888	  WidthStep{width: Nat, run: EmojiRun}
889	
890	def keycap_base(+code: U32) -> Bool:
891	  Bool.or(Bool.or(U32.is_eq(code, 35), U32.is_eq(code, 42)),
892	    Bool.and(U32.is_ge(code, 48), U32.is_le(code, 57)))
893	
894	# may: whether code is in 203C-3299 or from 1F000, which hold every
895	# pictograph from 768 on.
896	def picto_class(may: Bool, +code: U32) -> CodeClass:
897	  match may:
898	    case True{}:
899	      Bool.pick(CodeClass, unicode_is_pictographic(code), PictoCode{},
900	        PlainCode{})
901	    case False{}: PlainCode{}
902	
903	def code_class_by(small: Bool, +code: U32) -> CodeClass:
904	  match small:
905	    case True{}:
906	      Bool.pick(CodeClass, keycap_base(code), KeycapCode{},
907	        Bool.pick(CodeClass, Bool.or(U32.is_eq(code, 169),
908	          U32.is_eq(code, 174)), PictoCode{}, PlainCode{}))
909	    case False{}:
910	      Bool.pick(CodeClass, U32.is_eq(code, 65039), Vs16Code{},
911	        Bool.pick(CodeClass, U32.is_eq(code, 8205), JoinerCode{},
912	          Bool.pick(CodeClass, Bool.and(U32.is_ge(code, 127995),
913	            U32.is_le(code, 127999)), ToneCode{},
914	            picto_class(Bool.or(Bool.and(U32.is_ge(code, 8252),
915	              U32.is_le(code, 12953)), U32.is_ge(code, 126976)), code))))
916	
917	def code_class(+code: U32) -> CodeClass:
918	  code_class_by(U32.is_lt(code, 768), code)
919	
920	def picto_alone(+wide: Bool, code: U32) -> WidthStep:
921	  WidthStep{Bool.pick(Nat, wide, 2n, 1n),
922	    EmojiBase{code, Bool.not(wide), True{}}}
923	
924	# A pictograph after a ZWJ joins the sequence; any other starts an emoji.
925	def picto_step(run: EmojiRun, +code: U32) -> WidthStep:
926	  match run:
927	    case EmojiNone{}: picto_alone(unicode_is_wide(code), code)
928	    case EmojiBase{base, narrow, join}:
929	      picto_alone(unicode_is_wide(code), code)
930	    case EmojiJoiner{}: WidthStep{0n, EmojiJoined{code}}
931	    case EmojiJoined{base}: picto_alone(unicode_is_wide(code), code)
932	
933	# A skin tone after an emoji that takes one widens it to 2; any other is
934	# 2 wide alone, as East Asian Wide.
935	def tone_on(takes: Bool, narrow: Bool, join: Bool, code: U32) ->
936	    WidthStep:
937	  match takes:
938	    case True{}:
939	      WidthStep{Bool.pick(Nat, narrow, 1n, 0n), EmojiBase{code, False{}, join}}
940	    case False{}: WidthStep{2n, EmojiNone{}}
941	
942	def tone_on_joined(takes: Bool, code: U32) -> WidthStep:
943	  match takes:
944	    case True{}: WidthStep{0n, EmojiJoined{code}}
945	    case False{}: WidthStep{2n, EmojiNone{}}
946	
947	def tone_step(run: EmojiRun, code: U32) -> WidthStep:
948	  match run:
949	    case EmojiNone{}: WidthStep{2n, EmojiNone{}}
950	    case EmojiBase{base, narrow, join}:
951	      tone_on(unicode_takes_tone(base), narrow, join, code)
952	    case EmojiJoiner{}: WidthStep{2n, EmojiNone{}}
953	    case EmojiJoined{base}: tone_on_joined(unicode_takes_tone(base), code)
954	
955	# A ZWJ after an emoji that may join, or after a joined pictograph, waits
956	# for the next pictograph.
957	def joiner_run(run: EmojiRun) -> EmojiRun:
958	  match run:
959	    case EmojiNone{}: EmojiNone{}
960	    case EmojiBase{code, narrow, join}:
961	      Bool.pick(EmojiRun, join, EmojiJoiner{}, EmojiNone{})
962	    case EmojiJoiner{}: EmojiNone{}
963	    case EmojiJoined{code}: EmojiJoiner{}
964	
965	def vs16_widen(widens: Bool, code: U32, join: Bool) -> WidthStep:
966	  match widens:
967	    case True{}: WidthStep{1n, EmojiBase{code, False{}, join}}
968	    case False{}: WidthStep{0n, EmojiBase{code, True{}, join}}
969	
970	def vs16_on(narrow: Bool, +code: U32, join: Bool) -> WidthStep:
971	  match narrow:
972	    case True{}: vs16_widen(unicode_widens_with_vs16(code), code, join)
973	    case False{}: WidthStep{0n, EmojiBase{code, False{}, join}}
974	
975	# VS16 widens a 1-wide emoji with an emoji presentation to 2, once.
976	def vs16_step(run: EmojiRun) -> WidthStep:
977	  match run:
978	    case EmojiNone{}: WidthStep{0n, EmojiNone{}}
979	    case EmojiBase{code, narrow, join}: vs16_on(narrow, code, join)
980	    case EmojiJoiner{}: WidthStep{0n, EmojiNone{}}
981	    case EmojiJoined{code}: WidthStep{0n, EmojiJoined{code}}
982	
983	def code_step(cls: CodeClass, run: EmojiRun, code: U32) -> WidthStep:
984	  match cls:
985	    case PlainCode{}: WidthStep{code_width(code), EmojiNone{}}
986	    case KeycapCode{}: WidthStep{1n, EmojiBase{code, True{}, False{}}}
987	    case PictoCode{}: picto_step(run, code)
988	    case ToneCode{}: tone_step(run, code)
989	    case JoinerCode{}: WidthStep{0n, joiner_run(run)}
990	    case Vs16Code{}: vs16_step(run)
991	
992	# acc, plus the width of step, the last code point's, and of s after it.
993	def width_go(s: String, step: WidthStep, acc: Nat) -> Nat:
994	  match s step:
995	    case SNil{} WidthStep{w, run}: Nat.add(w, acc)
996	    case SCon{head, tail} WidthStep{w, run}:
997	      +code = Char.to_u32(head)
998	      width_go(tail, code_step(code_class(code), run, code), Nat.add(w, acc))
999	
1000	# Display columns, as Rust's unicode-width 0.2 counts them: each code point's
1001	# own width, except that an emoji sequence is one cell 2 wide. A pictograph
1002	# that a ZWJ joins, a skin tone after an emoji that takes one, and tag
1003	# characters add nothing; VS16 widens a 1-wide emoji to 2.
1004	def width(s: String) -> Nat:
1005	  width_go(s, WidthStep{0n, EmojiNone{}}, 0n)
1006	
1007	def leading_indent(s: String) -> String:
1008	  match s:
1009	    case SNil{}:
1010	      ""
1011	    case SCon{+head, tail}:
1012	      Bool.pick(String, Char.is_eq(head, ' '),
1013	        SCon{head, leading_indent(tail)}, "")
1014	
1015	type WrapState is Data:
1016	  WrapState{indent: String, cols: Nat, line: String,
1017	    started: Bool, done: List<&2, String>}
1018	
1019	def wrap_words(words: List<&2, String>, state: WrapState) -> String:
1020	  match words state:
1021	    case Nil{} WrapState{indent, cols, line, started, done}:
1022	      Bool.pick(String, started,
1023	        String.join(List.reverse(&2, String, line <> done), "\n"), "")
1024	    case +word <> rest WrapState{+indent, +cols, +line, +started, +done}:
1025	      +candidate = Bool.pick(String, started,
1026	        String.append(line, String.append(" ", word)),
1027	        String.append(indent, word))
1028	      fits = Bool.or(Bool.not(started), Nat.is_le(width(strip(candidate)), cols))
1029	      next = Bool.pick(WrapState, fits,
1030	        WrapState{indent, cols, candidate, True{}, done},
1031	        WrapState{indent, cols, String.append(indent, word), True{}, line <> done})
1032	      wrap_words(rest, next)
1033	
1034	def words(s: String) -> List<&2, String>:
1035	  List.filter(~String, ~(w => Bool.not(String.is_empty(w))),
1036	    String.split(s, ' '))
1037	
1038	def wrap_line(+line: String, cols: Nat) -> String:
1039	  +indent = leading_indent(line)
1040	  body = String.drop(line, String.length(indent))
1041	  parts = words(body)
1042	  wrap_words(parts, WrapState{indent, cols, indent, False{}, Nil{}})
1043	
1044	def wrap_lines(lines: List<&2, String>, +cols: Nat) -> List<&2, String>:
1045	  match lines:
1046	    case Nil{}:
1047	      Nil{}
1048	    case head <> tail:
1049	      wrap_line(head, cols) <> wrap_lines(tail, cols)
1050	
1051	def wrap(text: String, cols: Nat) -> String:
1052	  String.join(wrap_lines(String.lines(text), cols), "\n")
1053	
1054	type ValueType is Data:
1055	  TNat{}
1056	  TU32{}
1057	  TF32{}
1058	  TBool{}
1059	  TFile{}
1060	  TDir{}
1061	
1062	def type_name(t: ValueType) -> String:
1063	  match t:
1064	    case TNat{}: "as_nat"
1065	    case TU32{}: "as_u32"
1066	    case TF32{}: "as_f32"
1067	    case TBool{}: "as_bool"
1068	    case TFile{}: "as_file"
1069	    case TDir{}: "as_dir"
1070	
1071	type Item is Data:
1072	  Arg{usage: String, help: String, items: List<&2, Item>}
1073	  Sub{name: String, about: String, items: List<&2, Item>}
1074	  Version{value: String}
1075	  Alias{name: String}
1076	  Hidden{}
1077	  Example{line: String, what: String}
1078	  After{text: String}
1079	  SubOptional{}
1080	  External{}
1081	  Exclusive{group: String}
1082	  NeedOne{group: String}
1083	  Id{value: String}
1084	  Required{}
1085	  AttrDefault{value: String}
1086	  AttrEnv{name: String}
1087	  Global{}
1088	  Heading{title: String}
1089	  As{t: ValueType}
1090	  OneOf{values: List<&2, String>}
1091	  Delim{sep: Char}
1092	  Hyphen{}
1093	  Rest{}
1094	  Bare{value: String}
1095	  Conflicts{id: String}
1096	  Requires{id: String}
1097	  Group{name: String}
1098	  Builtin{}
1099	
1100	type Cmd is Data:
1101	  Cmd{name: String, about: String, items: List<&2, Item>}
1102	
1103	type Problem is Data:
1104	  BadUsage{at: String, usage: String, col: Nat}
1105	  BadName{at: String, name: String}
1106	  Dup{at: String, name: String}
1107	  Reserved{at: String, name: String}
1108	  Misplaced{at: String, attr: String}
1109	  NoHelp{at: String, what: String}
1110	  BadDefault{at: String, id: String, value: String}
1111	  BadRef{at: String, id: String}
1112	  BadPositional{at: String, id: String, why: String}
1113	  Mixed{at: String}
1114	  BadChoices{at: String, id: String}
1115	  BadChoice{at: String, id: String, value: String}
1116	  NeedBare{at: String, id: String}
1117	  DecodeBug{at: String, msg: String}
1118	
1119	def cmd(name: String, about: String, items: List<&2, Item>) -> Cmd:
1120	  Cmd{name, about, items}
1121	
1122	def sub(name: String, about: String, items: List<&2, Item>) -> Item:
1123	  Sub{name, about, items}
1124	
1125	def arg(usage: String, help: String, items: List<&2, Item>) -> Item:
1126	  Arg{usage, help, items}
1127	
1128	def version(value: String) -> Item:
1129	  Version{value}
1130	
1131	def alias(name: String) -> Item:
1132	  Alias{name}
1133	
1134	def hidden() -> Item:
1135	  Hidden{}
1136	
1137	def example(line: String, what: String) -> Item:
1138	  Example{line, what}
1139	
1140	def after(text: String) -> Item:
1141	  After{text}
1142	
1143	def sub_optional() -> Item:
1144	  SubOptional{}
1145	
1146	def external() -> Item:
1147	  External{}
1148	
1149	def exclusive(group: String) -> Item:
1150	  Exclusive{group}
1151	
1152	def need_one(group: String) -> Item:
1153	  NeedOne{group}
1154	
1155	def id(value: String) -> Item:
1156	  Id{value}
1157	
1158	def required() -> Item:
1159	  Required{}
1160	
1161	def default(value: String) -> Item:
1162	  AttrDefault{value}
1163	
1164	def env(name: String) -> Item:
1165	  AttrEnv{name}
1166	
1167	def global() -> Item:
1168	  Global{}
1169	
1170	def heading(title: String) -> Item:
1171	  Heading{title}
1172	
1173	def as_nat() -> Item:
1174	  As{TNat{}}
1175	
1176	def as_u32() -> Item:
1177	  As{TU32{}}
1178	
1179	def as_f32() -> Item:
1180	  As{TF32{}}
1181	
1182	def as_bool() -> Item:
1183	  As{TBool{}}
1184	
1185	def as_file() -> Item:
1186	  As{TFile{}}
1187	
1188	def as_dir() -> Item:
1189	  As{TDir{}}
1190	
1191	def one_of(values: List<&2, String>) -> Item:
1192	  OneOf{values}
1193	
1194	def delim(sep: Char) -> Item:
1195	  Delim{sep}
1196	
1197	def hyphen() -> Item:
1198	  Hyphen{}
1199	
1200	def rest() -> Item:
1201	  Rest{}
1202	
1203	def bare(value: String) -> Item:
1204	  Bare{value}
1205	
1206	def conflicts(target: String) -> Item:
1207	  Conflicts{target}
1208	
1209	def requires(target: String) -> Item:
1210	  Requires{target}
1211	
1212	def group(name: String) -> Item:
1213	  Group{name}
1214	
1215	def color() -> Item:
1216	  arg("--color <WHEN>", "When to use color", [one_of(["auto", "always", "never"]), default("auto"), global()])
1217	
1218	# Builtin{} marks the subcommands that only eval acts on (§6.4).
1219	def completions() -> Item:
1220	  sub("completions", "Print a shell completion script", [Builtin{}, arg("<SHELL>", "Shell to generate for", [one_of(["bash", "zsh", "fish"])])])
1221	
1222	def man() -> Item:
1223	  sub("man", "Print the man page", [Builtin{}, hidden(), arg("[COMMAND]...", "Subcommand path", [])])
1224	
1225	type UsageKind is Data:
1226	  FlagKind{}
1227	  CountKind{}
1228	  NegatableKind{}
1229	  OptionKind{many: Bool}
1230	  BareOptionKind{}
1231	  PosKind{required: Bool, many: Bool}
1232	
1233	type Usage is Data:
1234	  Parsed{id: String, short: String, long: String, kind: UsageKind}
1235	  Invalid{col: Nat}
1236	
1237	type NameScan is Data:
1238	  NameOK{name: String, rest: String, next: Nat}
1239	  NameBad{col: Nat}
1240	
1241	# PhOK's name is reversed: only a positional's name is read.
1242	type PhScan is Data:
1243	  PhOK{rev: String, rest: String, next: Nat}
1244	  PhBad{col: Nat}
1245	
1246	def name_start(+c: Char) -> Bool:
1247	  Bool.or(Char.is_alpha(c), Char.is_digit(c))
1248	
1249	def name_char(+c: Char) -> Bool:
1250	  Bool.or(name_start(c), Bool.or(Char.is_eq(c, '-'),
1251	    Bool.or(Char.is_eq(c, '_'), Char.is_eq(c, '.'))))
1252	
1253	# rev is the name so far, reversed.
1254	def finish_name(rev: String, rest: String, +pos: Nat,
1255	    +first: Bool, +dot_start: Nat) -> NameScan:
1256	  Bool.pick(NameScan, Bool.or(first, Nat.is_lt(dot_start, pos)),
1257	    NameBad{Bool.pick(Nat, first, pos, dot_start)},
1258	    NameOK{String.reverse(rev), rest, pos})
1259	
1260	def scan_name(s: String, +pos: Nat, rev: String,
1261	    +first: Bool, dot_start: Nat) -> NameScan:
1262	  match s:
1263	    case SNil{}:
1264	      finish_name(rev, SNil{}, pos, first, dot_start)
1265	    case SCon{Chr{32}, tail}:
1266	      finish_name(rev, SCon{Char.from_u32(32), tail}, pos, first, dot_start)
1267	    case SCon{Chr{91}, tail}:
1268	      finish_name(rev, SCon{Char.from_u32(91), tail}, pos, first, dot_start)
1269	    case SCon{+h, tail}:
1270	      valid = Bool.pick(Bool, first, name_start(h), name_char(h))
1271	      next_dot = Bool.pick(Nat, Char.is_eq(h, '.'), dot_start, Nat.add(pos, 1n))
1272	      Bool.pick(NameScan, valid,
1273	        scan_name(tail, Nat.add(pos, 1n), SCon{h, rev}, False{}, next_dot),
1274	        NameBad{pos})
1275	
1276	# A placeholder ends at a character no name holds: at close after a name,
1277	# else with an error there.
1278	def ph_stop(at_close: Bool, rev: String, rest: String, +pos: Nat) -> PhScan:
1279	  match at_close rev:
1280	    case True{} SCon{h, t}: PhOK{SCon{h, t}, rest, Nat.add(pos, 1n)}
1281	    case _ _: PhBad{pos}
1282	
1283	# The placeholder name in s up to close, reversed in rev. A name holds no
1284	# space, '<', '>', '[', ']' or '=', and close is one of them.
1285	def scan_ph(s: String, +pos: Nat, rev: String, +close: Char) -> PhScan:
1286	  match s:
1287	    case SNil{}: PhBad{pos}
1288	    case SCon{Chr{32}, tail}: ph_stop(Char.is_eq(' ', close), rev, tail, pos)
1289	    case SCon{Chr{60}, tail}: ph_stop(Char.is_eq('<', close), rev, tail, pos)
1290	    case SCon{Chr{62}, tail}: ph_stop(Char.is_eq('>', close), rev, tail, pos)
1291	    case SCon{Chr{91}, tail}: ph_stop(Char.is_eq('[', close), rev, tail, pos)
1292	    case SCon{Chr{93}, tail}: ph_stop(Char.is_eq(']', close), rev, tail, pos)
1293	    case SCon{Chr{61}, tail}: ph_stop(Char.is_eq('=', close), rev, tail, pos)
1294	    case SCon{h, tail}: scan_ph(tail, Nat.add(pos, 1n), SCon{h, rev}, close)
1295	
1296	def finish_pos(found: PhScan, kind: UsageKind) -> Usage:
1297	  match found:
1298	    case PhBad{col}:
1299	      Invalid{col}
1300	    case PhOK{rev, SNil{}, next}:
1301	      Parsed{String.to_lower(String.reverse(rev)), "", "", kind}
1302	    case PhOK{rev, rest, next}:
1303	      Invalid{next}
1304	
1305	def parse_pos(s: String, +repeat: Bool) -> Usage:
1306	  match s:
1307	    case SCon{Chr{60}, tail}:
1308	      finish_pos(scan_ph(tail, 1n, "", '>'),
1309	        PosKind{True{}, repeat})
1310	    case SCon{Chr{91}, tail}:
1311	      finish_pos(scan_ph(tail, 1n, "", ']'),
1312	        PosKind{False{}, repeat})
1313	    case _:
1314	      Invalid{0n}
1315	
1316	def finish_required_value(found: PhScan, id: String, short: String,
1317	    long: String, kind: UsageKind) -> Usage:
1318	  match found:
1319	    case PhBad{col}:
1320	      Invalid{col}
1321	    case PhOK{rev, SNil{}, next}:
1322	      Parsed{id, short, long, kind}
1323	    case PhOK{rev, rest, next}:
1324	      Invalid{next}
1325	
1326	def finish_optional_value(found: PhScan, id: String, short: String,
1327	    long: String) -> Usage:
1328	  match found:
1329	    case PhBad{col}:
1330	      Invalid{col}
1331	    case PhOK{rev, SCon{Chr{93}, SNil{}}, next}:
1332	      Parsed{id, short, long, BareOptionKind{}}
1333	    case PhOK{rev, rest, next}:
1334	      Invalid{next}
1335	
1336	def finish_long(found: NameScan, short: String,
1337	    +repeat: Bool, +negatable: Bool) -> Usage:
1338	  match found:
1339	    case NameBad{col}:
1340	      Invalid{col}
1341	    case NameOK{+name, SNil{}, next}:
1342	      Parsed{name, short, String.append("--", name),
1343	        Bool.pick(UsageKind, negatable, NegatableKind{},
1344	          Bool.pick(UsageKind, repeat, CountKind{}, FlagKind{}))}
1345	    case NameOK{+name, SCon{Chr{32}, SCon{Chr{60}, tail}}, +next}:
1346	      Bool.pick(Usage, negatable, Invalid{next},
1347	        finish_required_value(scan_ph(tail, Nat.add(next, 2n), "", '>'),
1348	          name, short, String.append("--", name),
1349	          OptionKind{repeat}))
1350	    case NameOK{+name, SCon{Chr{91}, SCon{Chr{61}, SCon{Chr{60}, tail}}}, +next}:
1351	      Bool.pick(Usage, Bool.or(negatable, repeat), Invalid{next},
1352	        finish_optional_value(scan_ph(tail, Nat.add(next, 3n), "", '>'),
1353	          name, short, String.append("--", name)))
1354	    case NameOK{name, rest, next}:
1355	      Invalid{next}
1356	
1357	# A long name after "--[no-]" or "--", at column start.
1358	def parse_long_prefixed(s: String, short: String,
1359	    repeat: Bool, +start: Nat) -> Usage:
1360	  match s:
1361	    case SCon{Chr{45}, SCon{Chr{45}, SCon{Chr{91}, SCon{Chr{110},
1362	        SCon{Chr{111}, SCon{Chr{45}, SCon{Chr{93}, rest}}}}}}}:
1363	      finish_long(scan_name(rest, Nat.add(start, 7n), "", True{},
1364	        Nat.add(start, 7n)), short, repeat, True{})
1365	    case SCon{Chr{45}, SCon{Chr{45}, rest}}:
1366	      finish_long(scan_name(rest, Nat.add(start, 2n), "", True{},
1367	        Nat.add(start, 2n)), short, repeat, False{})
1368	    case _:
1369	      Invalid{start}
1370	
1371	def parse_short_tail(tail: String, +short: String, +repeat: Bool) -> Usage:
1372	  match tail:
1373	    case SNil{}:
1374	      Parsed{String.drop(short, 1n), short, "",
1375	        Bool.pick(UsageKind, repeat, CountKind{}, FlagKind{})}
1376	    case SCon{Chr{44}, SCon{Chr{32}, long_rest}}:
1377	      parse_long_prefixed(long_rest, short, repeat, 4n)
1378	    case SCon{Chr{32}, SCon{Chr{60}, ph_rest}}:
1379	      finish_required_value(scan_ph(ph_rest, 4n, "", '>'),
1380	        String.drop(short, 1n), short, "",
1381	        OptionKind{repeat})
1382	    case SCon{Chr{91}, SCon{Chr{61}, SCon{Chr{60}, ph_rest}}}:
1383	      finish_optional_value(scan_ph(ph_rest, 5n, "", '>'),
1384	        String.drop(short, 1n), short, "")
1385	    case _:
1386	      Invalid{2n}
1387	
1388	def parse_short(s: String, repeat: Bool) -> Usage:
1389	  match s:
1390	    case SCon{Chr{45}, SCon{+h, tail}}:
1391	      Bool.pick(Usage, name_start(h),
1392	        parse_short_tail(tail, String.append("-", Char.show(h)), repeat),
1393	        Invalid{1n})
1394	    case _:
1395	      Invalid{1n}
1396	
1397	def parse_usage_body(s: String, +repeat: Bool) -> Usage:
1398	  match s:
1399	    case SCon{Chr{60}, tail}:
1400	      parse_pos(SCon{Char.from_u32(60), tail}, repeat)
1401	    case SCon{Chr{91}, tail}:
1402	      parse_pos(SCon{Char.from_u32(91), tail}, repeat)
1403	    case SCon{Chr{45}, SCon{Chr{45}, tail}}:
1404	      parse_long_prefixed(String.append("--", tail), "", repeat, 0n)
1405	    case SCon{Chr{45}, tail}:
1406	      parse_short(SCon{Char.from_u32(45), tail}, repeat)
1407	    case _:
1408	      Invalid{0n}
1409	
1410	# Whether s ends in "...": run counts the dots just before s.
1411	def ends_in_ellipsis(s: String, run: Nat) -> Bool:
1412	  match s:
1413	    case SNil{}: Nat.is_lt(2n, run)
1414	    case SCon{h, t}:
1415	      ends_in_ellipsis(t, Bool.pick(Nat, Char.is_eq(h, '.'), Nat.add(run, 1n), 0n))
1416	
1417	def parse_usage_repeated(repeated: Bool, +usage: String) -> Usage:
1418	  match repeated:
1419	    case False{}: parse_usage_body(usage, False{})
1420	    case True{}:
1421	      parse_usage_body(String.take(usage, Nat.sub(String.length(usage), 3n)),
1422	        True{})
1423	
1424	def parse_usage(+usage: String) -> Usage:
1425	  parse_usage_repeated(ends_in_ellipsis(usage, 0n), usage)
1426	
1427	def alias_valid_result(parsed: Usage, +raw: String) -> Bool:
1428	  match parsed:
1429	    case Parsed{id, short, long, FlagKind{}}:
1430	      Bool.or(String.eq(raw, short), String.eq(raw, long))
1431	    case _: False{}
1432	
1433	def valid_arg_alias(+raw: String) -> Bool:
1434	  alias_valid_result(parse_usage(raw), raw)
1435	
1436	def kind_pos(kind: UsageKind) -> Bool:
1437	  match kind:
1438	    case PosKind{required, many}: True{}
1439	    case _: False{}
1440	
1441	def kind_optional_pos(kind: UsageKind) -> Bool:
1442	  match kind:
1443	    case PosKind{required, many}: Bool.not(required)
1444	    case _: False{}
1445	
1446	def kind_variadic_pos(kind: UsageKind) -> Bool:
1447	  match kind:
1448	    case PosKind{required, many}: many
1449	    case _: False{}
1450	
1451	def kind_required_pos(kind: UsageKind) -> Bool:
1452	  match kind:
1453	    case PosKind{required, many}: required
1454	    case _: False{}
1455	
1456	def kind_valued(kind: UsageKind) -> Bool:
1457	  match kind:
1458	    case OptionKind{many}: True{}
1459	    case BareOptionKind{}: True{}
1460	    case PosKind{required, many}: True{}
1461	    case _: False{}
1462	
1463	def kind_bare(kind: UsageKind) -> Bool:
1464	  match kind:
1465	    case BareOptionKind{}: True{}
1466	    case _: False{}
1467	
1468	def kind_default_allowed(kind: UsageKind) -> Bool:
1469	  match kind:
1470	    case OptionKind{many}: True{}
1471	    case BareOptionKind{}: True{}
1472	    case PosKind{required, many}: Bool.not(required)
1473	    case NegatableKind{}: True{}
1474	    case _: False{}
1475	
1476	def kind_required_allowed(kind: UsageKind) -> Bool:
1477	  match kind:
1478	    case OptionKind{many}: True{}
1479	    case _: False{}
1480	
1481	def kind_delim_allowed(kind: UsageKind) -> Bool:
1482	  match kind:
1483	    case OptionKind{many}: many
1484	    case PosKind{required, many}: many
1485	    case _: False{}
1486	
1487	def bad_attr(cond: Bool, name: String) -> Maybe<&2, String>:
1488	  Bool.pick(Maybe<&2, String>, cond, Some{name}, None{})
1489	
1490	def misplaced_attr_name(attr: Item, +kind: UsageKind) ->
1491	    Maybe<&2, String>:
1492	  match attr:
1493	    case Global{}: bad_attr(kind_pos(kind), "global")
1494	    case Rest{}: bad_attr(Bool.not(kind_variadic_pos(kind)), "rest")
1495	    case AttrDefault{value}:
1496	      bad_attr(Bool.not(kind_default_allowed(kind)), "default")
1497	    case Required{}:
1498	      bad_attr(Bool.not(kind_required_allowed(kind)), "required")
1499	    case Heading{title}: bad_attr(kind_pos(kind), "heading")
1500	    case Alias{name}: bad_attr(kind_pos(kind), "alias")
1501	    case As{t}: bad_attr(Bool.not(kind_valued(kind)), type_name(t))
1502	    case OneOf{values}:
1503	      bad_attr(Bool.not(kind_valued(kind)), "one_of")
1504	    case Delim{sep}: bad_attr(Bool.not(kind_delim_allowed(kind)), "delim")
1505	    case Hyphen{}: bad_attr(Bool.not(kind_valued(kind)), "hyphen")
1506	    case Arg{usage, help, items}: Some{"arg"}
1507	    case Sub{name, about, items}: Some{"sub"}
1508	    case Version{value}: Some{"version"}
1509	    case Example{line, what}: Some{"example"}
1510	    case After{text}: Some{"after"}
1511	    case SubOptional{}: Some{"sub_optional"}
1512	    case External{}: Some{"external"}
1513	    case Exclusive{group}: Some{"exclusive"}
1514	    case NeedOne{group}: Some{"need_one"}
1515	    case _: None{}
1516	
1517	def maybe_misplaced(found: Maybe<&2, String>, at: String) ->
1518	    List<&2, Problem>:
1519	  match found:
1520	    case None{}: Nil{}
1521	    case Some{name}: [Misplaced{at, name}]
1522	
1523	def placement_issues(attrs: List<&2, Item>, +kind: UsageKind,
1524	    +at: String) -> List<&2, Problem>:
1525	  match attrs:
1526	    case Nil{}: Nil{}
1527	    case head <> tail:
1528	      List.append(&2, Problem,
1529	        maybe_misplaced(misplaced_attr_name(head, kind), at),
1530	        placement_issues(tail, kind, at))
1531	
1532	def value_type_names(attrs: List<&2, Item>) -> List<&2, String>:
1533	  match attrs:
1534	    case Nil{}: Nil{}
1535	    case As{t} <> tail: type_name(t) <> value_type_names(tail)
1536	    case head <> tail: value_type_names(tail)
1537	
1538	def extra_type_issues(names: List<&2, String>, +at: String) ->
1539	    List<&2, Problem>:
1540	  match names:
1541	    case Nil{}: Nil{}
1542	    case name <> tail:
1543	      Misplaced{at, name} <> extra_type_issues(tail, at)
1544	
1545	def duplicate_type_issues(names: List<&2, String>, at: String) ->
1546	    List<&2, Problem>:
1547	  match names:
1548	    case Nil{}: Nil{}
1549	    case head <> tail: extra_type_issues(tail, at)
1550	
1551	def command_attr_name(attr: Item, root: Bool) -> Maybe<&2, String>:
1552	  match attr:
1553	    case Arg{usage, help, attrs}: None{}
1554	    case Sub{name, about, children}: None{}
1555	    case Version{value}: bad_attr(Bool.not(root), "version")
1556	    case Alias{name}: bad_attr(root, "alias")
1557	    case Hidden{}: bad_attr(root, "hidden")
1558	    case Example{line, what}: None{}
1559	    case After{text}: None{}
1560	    case SubOptional{}: None{}
1561	    case External{}: None{}
1562	    case Exclusive{group}: None{}
1563	    case NeedOne{group}: None{}
1564	    case Id{value}: Some{"id"}
1565	    case Required{}: Some{"required"}
1566	    case AttrDefault{value}: Some{"default"}
1567	    case AttrEnv{name}: Some{"env"}
1568	    case Global{}: Some{"global"}
1569	    case Heading{title}: Some{"heading"}
1570	    case As{t}: Some{type_name(t)}
1571	    case OneOf{values}: Some{"one_of"}
1572	    case Delim{sep}: Some{"delim"}
1573	    case Hyphen{}: Some{"hyphen"}
1574	    case Rest{}: Some{"rest"}
1575	    case Bare{value}: Some{"bare"}
1576	    case Conflicts{id}: Some{"conflicts"}
1577	    case Requires{id}: Some{"requires"}
1578	    case Group{name}: Some{"group"}
1579	    case Builtin{}: None{}
1580	
1581	def has_rest(items: List<&2, Item>) -> Bool:
1582	  match items:
1583	    case Nil{}: False{}
1584	    case Rest{} <> tail: True{}
1585	    case head <> tail: has_rest(tail)
1586	
1587	def has_hidden(items: List<&2, Item>) -> Bool:
1588	  match items:
1589	    case Nil{}: False{}
1590	    case Hidden{} <> tail: True{}
1591	    case head <> tail: has_hidden(tail)
1592	
1593	def has_builtin(items: List<&2, Item>) -> Bool:
1594	  match items:
1595	    case Nil{}: False{}
1596	    case Builtin{} <> tail: True{}
1597	    case head <> tail: has_builtin(tail)
1598	
1599	def has_bare(items: List<&2, Item>) -> Bool:
1600	  match items:
1601	    case Nil{}: False{}
1602	    case Bare{value} <> tail: True{}
1603	    case head <> tail: has_bare(tail)
1604	
1605	def has_required(items: List<&2, Item>) -> Bool:
1606	  match items:
1607	    case Nil{}: False{}
1608	    case Required{} <> tail: True{}
1609	    case head <> tail: has_required(tail)
1610	
1611	def duplicate_strings(xs: List<&2, String>) -> Bool:
1612	  match xs:
1613	    case Nil{}: False{}
1614	    case +head <> +tail:
1615	      Bool.or(List.contains(~String, ~String.eq, tail, head),
1616	        duplicate_strings(tail))
1617	
1618	def bad_choices(items: List<&2, Item>) -> Bool:
1619	  match items:
1620	    case Nil{}: False{}
1621	    case OneOf{+values} <> tail:
1622	      Bool.or(Bool.or(List.is_empty(&2, String, values),
1623	        duplicate_strings(values)), bad_choices(tail))
1624	    case head <> tail: bad_choices(tail)
1625	
1626	def find_default(items: List<&2, Item>) -> Maybe<&2, String>:
1627	  match items:
1628	    case Nil{}: None{}
1629	    case AttrDefault{value} <> tail: Some{value}
1630	    case head <> tail: find_default(tail)
1631	
1632	def find_delim(attrs: List<&2, Item>) -> Maybe<&2, Char>:
1633	  match attrs:
1634	    case Nil{}: None{}
1635	    case Delim{sep} <> tail: Some{sep}
1636	    case head <> tail: find_delim(tail)
1637	
1638	def split_each(values: List<&2, String>, +sep: Char) ->
1639	    List<&2, String>:
1640	  match values:
1641	    case Nil{}: Nil{}
1642	    case head <> tail:
1643	      List.append(&2, String, String.split(head, sep),
1644	        split_each(tail, sep))
1645	
1646	def apply_delim(found: Maybe<&2, Char>,
1647	    values: List<&2, String>) -> List<&2, String>:
1648	  match found:
1649	    case None{}: values
1650	    case Some{sep}: split_each(values, sep)
1651	
1652	def find_id(items: List<&2, Item>) -> Maybe<&2, String>:
1653	  match items:
1654	    case Nil{}: None{}
1655	    case Id{value} <> tail: Some{value}
1656	    case head <> tail: find_id(tail)
1657	
1658	def find_requires(items: List<&2, Item>) -> List<&2, String>:
1659	  match items:
1660	    case Nil{}: Nil{}
1661	    case Requires{target} <> tail: target <> find_requires(tail)
1662	    case head <> tail: find_requires(tail)
1663	
1664	def find_conflicts(items: List<&2, Item>) -> List<&2, String>:
1665	  match items:
1666	    case Nil{}: Nil{}
1667	    case Conflicts{target} <> tail: target <> find_conflicts(tail)
1668	    case head <> tail: find_conflicts(tail)
1669	
1670	def find_group_attrs(items: List<&2, Item>) -> List<&2, String>:
1671	  match items:
1672	    case Nil{}: Nil{}
1673	    case Group{name} <> tail: name <> find_group_attrs(tail)
1674	    case head <> tail: find_group_attrs(tail)
1675	
1676	def find_aliases(items: List<&2, Item>) -> List<&2, String>:
1677	  match items:
1678	    case Nil{}: Nil{}
1679	    case Alias{name} <> tail: name <> find_aliases(tail)
1680	    case head <> tail: find_aliases(tail)
1681	
1682	def scope_groups(items: List<&2, Item>) -> List<&2, String>:
1683	  match items:
1684	    case Nil{}: Nil{}
1685	    case Arg{usage, help, attrs} <> tail:
1686	      List.append(&2, String, find_group_attrs(attrs), scope_groups(tail))
1687	    case head <> tail: scope_groups(tail)
1688	
1689	def scope_group_rules(items: List<&2, Item>) -> List<&2, String>:
1690	  match items:
1691	    case Nil{}: Nil{}
1692	    case Exclusive{group} <> tail: group <> scope_group_rules(tail)
1693	    case NeedOne{group} <> tail: group <> scope_group_rules(tail)
1694	    case head <> tail: scope_group_rules(tail)
1695	
1696	def usage_kind(~f: UsageKind -> Bool, parsed: Usage) -> Bool:
1697	  match parsed:
1698	    case Parsed{id, short, long, kind}: f(kind)
1699	    case Invalid{col}: False{}
1700	
1701	# An item as lint walks it: an Arg with its usage parsed once, a Sub with
1702	# its children's too.
1703	type LintItem is Data:
1704	  LintArg{usage: String, help: String, attrs: List<&2, Item>, parsed: Usage}
1705	  LintSub{name: String, about: String, children: List<&2, Item>,
1706	    items: List<&2, LintItem>}
1707	  LintOther{item: Item}
1708	
1709	def lint_items(items: List<&2, Item>) -> List<&2, LintItem>:
1710	  match items:
1711	    case Nil{}: Nil{}
1712	    case Arg{+usage, help, attrs} <> tail:
1713	      LintArg{usage, help, attrs, parse_usage(usage)} <> lint_items(tail)
1714	    case Sub{name, about, +children} <> tail:
1715	      LintSub{name, about, children, lint_items(children)} <> lint_items(tail)
1716	    case head <> tail: LintOther{head} <> lint_items(tail)
1717	
1718	def has_pos_item(items: List<&2, LintItem>) -> Bool:
1719	  match items:
1720	    case Nil{}: False{}
1721	    case LintArg{usage, help, attrs, parsed} <> tail:
1722	      Bool.or(usage_kind(~kind_pos, parsed), has_pos_item(tail))
1723	    case head <> tail: has_pos_item(tail)
1724	
1725	def has_sub_item(items: List<&2, Item>) -> Bool:
1726	  match items:
1727	    case Nil{}: False{}
1728	    case Sub{name, about, children} <> tail: True{}
1729	    case head <> tail: has_sub_item(tail)
1730	
1731	def has_version_item(items: List<&2, Item>) -> Bool:
1732	  match items:
1733	    case Nil{}: False{}
1734	    case Version{value} <> tail: True{}
1735	    case head <> tail: has_version_item(tail)
1736	
1737	def name_scan_valid(result: NameScan) -> Bool:
1738	  match result:
1739	    case NameOK{name, SNil{}, next}: True{}
1740	    case _: False{}
1741	
1742	def valid_command_name(s: String) -> Bool:
1743	  name_scan_valid(scan_name(s, 0n, "", True{}, 0n))
1744	
1745	def use_id(found: Maybe<&2, String>, derived: String) -> String:
1746	  match found:
1747	    case None{}: derived
1748	    case Some{explicit}: explicit
1749	
1750	def usage_id(parsed: Usage, attrs: List<&2, Item>) -> String:
1751	  match parsed:
1752	    case Parsed{derived, short, long, kind}:
1753	      use_id(find_id(attrs), derived)
1754	    case Invalid{col}:
1755	      ""
1756	
1757	def scope_ids(items: List<&2, LintItem>) -> List<&2, String>:
1758	  match items:
1759	    case Nil{}:
1760	      Nil{}
1761	    case LintArg{usage, help, attrs, parsed} <> tail:
1762	      +name = usage_id(parsed, attrs)
1763	      +rest = scope_ids(tail)
1764	      Bool.pick(List<&2, String>, String.is_empty(name),
1765	        rest, name <> rest)
1766	    case head <> tail:
1767	      scope_ids(tail)
1768	
1769	type Seen is Data:
1770	  SeenArg{id: String, short: String, long: String}
1771	  SeenSub{name: String}
1772	  SeenArgAlias{name: String}
1773	  SeenSubAlias{name: String}
1774	
1775	# String.eq, without rebuilding both strings to hand them back; the walk
1776	# stops at the first difference.
1777	def same_go(a: String, b: String, same: Bool) -> Bool:
1778	  match a b same:
1779	    case SNil{} SNil{} done: done
1780	    case SCon{x, xt} SCon{y, yt} True{}: same_go(xt, yt, Char.is_eq(x, y))
1781	    case _ _ _: False{}
1782	
1783	def same_text(a: String, b: String) -> Bool:
1784	  same_go(a, b, True{})
1785	
1786	def same_nonempty(+a: String, b: String) -> Bool:
1787	  Bool.and(Bool.not(String.is_empty(a)), same_text(a, b))
1788	
1789	def arg_collision(seen: List<&2, Seen>, +id: String,
1790	    +short: String, +long: String) -> Maybe<&2, String>:
1791	  match seen:
1792	    case Nil{}:
1793	      None{}
1794	    case SeenArg{old_id, old_short, old_long} <> tail:
1795	      here = Bool.pick(Maybe<&2, String>, same_nonempty(short, old_short),
1796	        Some{short}, Bool.pick(Maybe<&2, String>,
1797	          same_nonempty(long, old_long), Some{long},
1798	          Bool.pick(Maybe<&2, String>, same_text(id, old_id), Some{id}, None{})))
1799	      Maybe.or(&2, String, here, arg_collision(tail, id, short, long))
1800	    case SeenArgAlias{+old} <> tail:
1801	      Bool.pick(Maybe<&2, String>, same_nonempty(short, old),
1802	        Some{short}, Bool.pick(Maybe<&2, String>,
1803	          same_nonempty(long, old), Some{long},
1804	          arg_collision(tail, id, short, long)))
1805	    case head <> tail:
1806	      arg_collision(tail, id, short, long)
1807	
1808	def sub_collision(seen: List<&2, Seen>, +name: String) -> Bool:
1809	  match seen:
1810	    case Nil{}:
1811	      False{}
1812	    case SeenSub{old} <> tail:
1813	      Bool.or(same_text(name, old), sub_collision(tail, name))
1814	    case SeenSubAlias{old} <> tail:
1815	      Bool.or(same_text(name, old), sub_collision(tail, name))
1816	    case head <> tail:
1817	      sub_collision(tail, name)
1818	
1819	def arg_alias_collision(seen: List<&2, Seen>, +name: String) -> Bool:
1820	  match seen:
1821	    case Nil{}: False{}
1822	    case SeenArg{id, short, long} <> tail:
1823	      Bool.or(Bool.or(same_nonempty(name, short),
1824	        same_nonempty(name, long)), arg_alias_collision(tail, name))
1825	    case SeenArgAlias{old} <> tail:
1826	      Bool.or(same_text(name, old), arg_alias_collision(tail, name))
1827	    case head <> tail:
1828	      arg_alias_collision(tail, name)
1829	
1830	def maybe_dup(found: Maybe<&2, String>, at: String) -> List<&2, Problem>:
1831	  match found:
1832	    case None{}: Nil{}
1833	    case Some{name}: [Dup{at, name}]
1834	
1835	def when_problem(cond: Bool, problem: Problem) -> List<&2, Problem>:
1836	  Bool.pick(List<&2, Problem>, cond, [problem], Nil{})
1837	
1838	def arg_alias_issue(+name: String, +at: String,
1839	    seen: List<&2, Seen>, version: Bool) -> List<&2, Problem>:
1840	  Bool.pick(List<&2, Problem>, valid_arg_alias(name),
1841	    Bool.pick(List<&2, Problem>, Bool.or(String.eq(name, "--help"),
1842	      Bool.and(version, String.eq(name, "--version"))),
1843	      [Reserved{at, name}],
1844	      when_problem(arg_alias_collision(seen, name), Dup{at, name})),
1845	    [BadName{at, name}])
1846	
1847	def arg_alias_issues(aliases: List<&2, String>, +at: String,
1848	    +seen: List<&2, Seen>, +version: Bool) -> List<&2, Problem>:
1849	  match aliases:
1850	    case Nil{}: Nil{}
1851	    case +name <> tail:
1852	      List.append(&2, Problem,
1853	        arg_alias_issue(name, at, seen, version),
1854	        arg_alias_issues(tail, at, SeenArgAlias{name} <> seen, version))
1855	
1856	def arg_alias_entries(aliases: List<&2, String>) -> List<&2, Seen>:
1857	  match aliases:
1858	    case Nil{}: Nil{}
1859	    case name <> tail:
1860	      SeenArgAlias{name} <> arg_alias_entries(tail)
1861	
1862	def arg_entries(parsed: Usage, +attrs: List<&2, Item>) -> List<&2, Seen>:
1863	  match parsed:
1864	    case Parsed{derived, short, long, kind}:
1865	      SeenArg{use_id(find_id(attrs), derived), short, long} <>
1866	        arg_alias_entries(find_aliases(attrs))
1867	    case Invalid{col}:
1868	      Nil{}
1869	
1870	def has_global(items: List<&2, Item>) -> Bool:
1871	  match items:
1872	    case Nil{}: False{}
1873	    case Global{} <> tail: True{}
1874	    case head <> tail: has_global(tail)
1875	
1876	def global_entries(items: List<&2, LintItem>) -> List<&2, Seen>:
1877	  match items:
1878	    case Nil{}: Nil{}
1879	    case LintArg{usage, help, +attrs, parsed} <> tail:
1880	      List.append(&2, Seen,
1881	        Bool.pick(List<&2, Seen>, has_global(attrs),
1882	          arg_entries(parsed, attrs), Nil{}),
1883	        global_entries(tail))
1884	    case head <> tail: global_entries(tail)
1885	
1886	def sub_alias_issue(+name: String, +at: String,
1887	    seen: List<&2, Seen>) -> List<&2, Problem>:
1888	  Bool.pick(List<&2, Problem>, valid_command_name(name),
1889	    Bool.pick(List<&2, Problem>, String.eq(name, "help"),
1890	      [Reserved{at, name}],
1891	      when_problem(sub_collision(seen, name), Dup{at, name})),
1892	    [BadName{at, name}])
1893	
1894	def sub_alias_issues(aliases: List<&2, String>, +at: String,
1895	    +seen: List<&2, Seen>) -> List<&2, Problem>:
1896	  match aliases:
1897	    case Nil{}: Nil{}
1898	    case +name <> tail:
1899	      List.append(&2, Problem,
1900	        sub_alias_issue(name, at, seen),
1901	        sub_alias_issues(tail, at, SeenSubAlias{name} <> seen))
1902	
1903	def sub_alias_entries(aliases: List<&2, String>) -> List<&2, Seen>:
1904	  match aliases:
1905	    case Nil{}: Nil{}
1906	    case name <> tail:
1907	      SeenSubAlias{name} <> sub_alias_entries(tail)
1908	
1909	def missing_refs(targets: List<&2, String>, +ids: List<&2, String>,
1910	    +at: String) -> List<&2, Problem>:
1911	  match targets:
1912	    case Nil{}:
1913	      Nil{}
1914	    case +target <> tail:
1915	      List.append(&2, Problem,
1916	        when_problem(Bool.not(List.contains(~String, ~String.eq, ids, target)),
1917	          BadRef{at, target}), missing_refs(tail, ids, at))
1918	
1919	# A U32 value is what U32.read reads (P22).
1920	def valid_u32(s: String) -> Bool:
1921	  Maybe.is_some(&2, U32, U32.read(s))
1922	
1923	# Decimal digits by Nat.read's own test, which Char.is_digit agrees with.
1924	def decimal_digits(s: String) -> Bool:
1925	  match s:
1926	    case SNil{}: True{}
1927	    case SCon{Chr{x}, tail}:
1928	      Bool.and(U32.is_lt(U32.sub(x, 48), 10), decimal_digits(tail))
1929	
1930	# A Nat value is what Nat.read reads (P22): digits that, less leading
1931	# zeroes, fit under its cap of 2^48-1.
1932	def valid_nat(+s: String) -> Bool:
1933	  Bool.and(Bool.not(String.is_empty(s)),
1934	    Bool.and(decimal_digits(s), Nat.read.fits(Nat.read.trim(s))))
1935	
1936	def valid_bool(s: String) -> Bool:
1937	  List.contains(~String, ~String.eq,
1938	    ["true", "false", "yes", "no", "on", "off", "1", "0"],
1939	    String.to_lower(s))
1940	
1941	type DecimalState is Data:
1942	  DecStart{}
1943	  DecAfterMinus{}
1944	  DecInt{}
1945	  DecDotFirst{}
1946	  DecDotAfterInt{}
1947	  DecFrac{}
1948	  DecExpStart{}
1949	  DecExpSign{}
1950	  DecExpDigits{}
1951	  DecInvalid{}
1952	
1953	def is_exponent(+c: Char) -> Bool:
1954	  Bool.or(Char.is_eq(c, 'e'), Char.is_eq(c, 'E'))
1955	
1956	def is_sign(+c: Char) -> Bool:
1957	  Bool.or(Char.is_eq(c, '+'), Char.is_eq(c, '-'))
1958	
1959	def decimal_step(state: DecimalState, +c: Char) -> DecimalState:
1960	  match state:
1961	    case DecStart{}:
1962	      Bool.pick(DecimalState, Char.is_eq(c, '-'), DecAfterMinus{},
1963	        Bool.pick(DecimalState, Char.is_digit(c), DecInt{},
1964	          Bool.pick(DecimalState, Char.is_eq(c, '.'), DecDotFirst{}, DecInvalid{})))
1965	    case DecAfterMinus{}:
1966	      Bool.pick(DecimalState, Char.is_digit(c), DecInt{},
1967	        Bool.pick(DecimalState, Char.is_eq(c, '.'), DecDotFirst{}, DecInvalid{}))
1968	    case DecInt{}:
1969	      Bool.pick(DecimalState, Char.is_digit(c), DecInt{},
1970	        Bool.pick(DecimalState, Char.is_eq(c, '.'), DecDotAfterInt{},
1971	          Bool.pick(DecimalState, is_exponent(c), DecExpStart{}, DecInvalid{})))
1972	    case DecDotFirst{}:
1973	      Bool.pick(DecimalState, Char.is_digit(c), DecFrac{}, DecInvalid{})
1974	    case DecDotAfterInt{}:
1975	      Bool.pick(DecimalState, Char.is_digit(c), DecFrac{},
1976	        Bool.pick(DecimalState, is_exponent(c), DecExpStart{}, DecInvalid{}))
1977	    case DecFrac{}:
1978	      Bool.pick(DecimalState, Char.is_digit(c), DecFrac{},
1979	        Bool.pick(DecimalState, is_exponent(c), DecExpStart{}, DecInvalid{}))
1980	    case DecExpStart{}:
1981	      Bool.pick(DecimalState, is_sign(c), DecExpSign{},
1982	        Bool.pick(DecimalState, Char.is_digit(c), DecExpDigits{}, DecInvalid{}))
1983	    case DecExpSign{}:
1984	      Bool.pick(DecimalState, Char.is_digit(c), DecExpDigits{}, DecInvalid{})
1985	    case DecExpDigits{}:
1986	      Bool.pick(DecimalState, Char.is_digit(c), DecExpDigits{}, DecInvalid{})
1987	    case DecInvalid{}:
1988	      DecInvalid{}
1989	
1990	def decimal_accept(state: DecimalState) -> Bool:
1991	  match state:
1992	    case DecInt{}: True{}
1993	    case DecDotAfterInt{}: True{}
1994	    case DecFrac{}: True{}
1995	    case DecExpDigits{}: True{}
1996	    case _: False{}
1997	
1998	def decimal_scan(s: String, state: DecimalState) -> Bool:
1999	  match s:
2000	    case SNil{}: decimal_accept(state)
Lines 1-2000 of 8031. More: https://jend.leeeet.dev/read.txt?path=cli@0.2.0.0/cli.bend&start_line=2001