1	# eztoml: TOML for Bend 2, a proven parser and renderer for TOML documents.
2	#
3	# eztoml reads and writes TOML documents. Values are strings, integers, floats,
4	# booleans, datetimes, arrays, inline tables, tables, and arrays of tables.
5	# Comments and blank lines are passed over.
6	#
7	# parse, render, get, at, root, bad, string, digits, flag
8	# str, integer, float, boolean, array, inline, table, pair
9	# key, wf
10	import Base
11	
12	# the sign of an integer, a float, or a zone offset
13	type Sign is Data:
14	  Plus{}
15	  Minus{}
16	
17	# a calendar date: year, month, day
18	type Date is Data:
19	  Date{y: U32, mo: U32, d: U32}
20	
21	# a time of day. frac is the fractional second, empty when there is none
22	type Clock is Data:
23	  Clock{h: U32, mi: U32, s: U32, frac: String}
24	
25	# a zone offset: Z, or a numeric offset
26	type Zone is Data:
27	  Zulu{}
28	  Shift{sign: Sign, h: U32, mi: U32}
29	
30	# the four TOML datetime forms
31	type When is Data:
32	  WOff{date: Date, clock: Clock, zone: Zone}
33	  WLocal{date: Date, clock: Clock}
34	  WDate{date: Date}
35	  WTime{clock: Clock}
36	
37	# one TOML value. Tables remember the dotted path they were opened under.
38	# An inline table is VInl. An array of tables is VAots, and each element is
39	# VAot. VPair is a key in a table. VSpan is a plain string: the first n
40	# characters of a source suffix.
41	type Val is Data:
42	  VStr{text: String}
43	  VSpan{src: String, n: U32}
44	  VInt{sign: Sign, digits: String}
45	  VFlo{sign: Sign, text: String}
46	  VBool{bit: Bool}
47	  VWhen{when: When}
48	  VArr{items: List<&2, Val>}
49	  VInl{rows: List<&2, Val>}
50	  VHead{path: String, rows: List<&2, Val>}
51	  VAot{path: String, rows: List<&2, Val>}
52	  VAots{path: String, elems: List<&2, Val>}
53	  VPair{name: String, val: Val}
54	
55	# a key found in a table, or not
56	type Hit is Data:
57	  Found{val: Val}
58	  Miss{}
59	
60	# a parsed document: the first error, and the root table in order
61	type Doc is Data:
62	  Doc{bad: String, rows: List<&2, Val>}
63	
64	# a value read from a bare word, or the reason it is not one
65	type Got is Data:
66	  GotVal{val: Val}
67	  GotBad{why: String}
68	
69	# digits taken from the front of a character list
70	type Dig is Data:
71	  DigOk{n: U32, cs: List<&2, Char>}
72	  DigBad{}
73	
74	# what a datetime scan produced
75	type WhenOut is Data:
76	  WSome{when: When}
77	  WFail{why: String}
78	  WSkip{}
79	
80	# a decimal numeral being built, least-significant digit first
81	type NK is Data:
82	  NLead{}
83	  NSign{}
84	  NZero{}
85	  NDig{}
86	  NBase{}
87	  NFrac{}
88	  NExp{}
89	  NEDig{}
90	  NBad{}
91	
92	# the numeral scan
93	type Num is Data:
94	  Num{nk: NK, sign: Sign, base: U32, ds: List<&2, U32>, us: Bool, saw: Bool,
95	    why: String}
96	
97	# how a basic-string character is written
98	type BK is Data:
99	  BKCh{}
100	  BKHex{}
101	  BKEsc{mark: Char}
102	
103	# where the scanner is in a document
104	type Lex is Data:
105	  LTop{}
106	  LLine{}
107	  LKey{}
108	  LKeyDot{}
109	  LAfter{}
110	  LKeyQ{}
111	  LKeyE{}
112	  LKeyU{}
113	  LVal{}
114	  LQ{}
115	  LQ2{}
116	  LStr{}
117	  LEsc{}
118	  LUni{}
119	  LFold{}
120	  LMq{}
121	  LMqEnd{}
122	  LTrim{}
123	  LTrim2{}
124	  LBare{}
125	  LDate{}
126	  LCom{}
127	  LHead{}
128	  LHeadGap{}
129	  LHeadDot{}
130	  LHeadQ{}
131	  LHeadE{}
132	  LHeadU{}
133	  LHeadR{}
134	  LArr{}
135	  LArrC{}
136	  LInl{}
137	  LInlK{}
138	  LInlC{}
139	  LSink{}
140	
141	# which quotes a string is using
142	type QKind is Data:
143	  QBasic{}
144	  QLit{}
145	  QMulti{}
146	  QMultiLit{}
147	
148	# one character to read again
149	type Hold is Data:
150	  HNone{}
151	  HChar{c: Char}
152	
153	# an open array or inline table
154	type Ctx is Data:
155	  CArr{items: List<&2, Val>, parts: List<&2, String>, here: List<&2, String>}
156	  CInl{rows: List<&2, Val>, parts: List<&2, String>, here: List<&2, String>}
157	
158	# the scanner
159	type St is Data:
160	  St{bad: String, rows: List<&2, Val>, heads: List<&2, String>,
161	    here: List<&2, String>, parts: List<&2, String>, buf: List<&2, Char>,
162	    lex: Lex, back: Lex, qkind: QKind, stack: List<&2, Ctx>, hold: Hold,
163	    uni: U32, left: U32, arrtab: Bool, lead: Bool}
164	
165	# an escape in a basic string
166	type Esc is Data:
167	  EChar{c: Char}
168	  EUni{n: U32}
169	  EFold{saw: Bool}
170	  EBad{}
171	
172	# a character a bare key may hold
173	def bare.at(+cc: Char) -> Bool:
174	  Bool.or(Char.is_alpha(cc), Bool.or(Char.is_digit(cc),
175	    Bool.or(Char.is_eq(cc, '_'), Char.is_eq(cc, '-'))))
176	
177	# one step of the bare-key walk, with the head's answer in hand
178	def bare.all.step(here: Bool, rest: Unit -> Bool) -> Bool:
179	  match here:
180	    case True{}:
181	      rest(Unit{})
182	    case False{}:
183	      False{}
184	
185	# whether every character of a key is one a bare key may hold
186	def bare.all(cs: List<&2, Char>) -> Bool:
187	  match cs:
188	    case []:
189	      True{}
190	    case +h <> t:
191	      bare.all.step(bare.at(h), _u => bare.all(t))
192	
193	# whether a key can be written without quotes
194	def bare(+ss: String) -> Bool:
195	  Bool.and(Bool.not(String.is_empty(ss)), bare.all(String.to_list(ss)))
196	
197	# one hex nibble as a character
198	def hex.char.go(dec: Bool, nn: U32) -> Char:
199	  match dec:
200	    case True{}:
201	      Chr{U32.add(48, nn)}
202	    case False{}:
203	      Chr{U32.add(87, nn)}
204	
205	# one hex nibble as a character
206	def hex.char(+nn: U32) -> Char:
207	  hex.char.go(U32.is_lt(nn, 10), nn)
208	
209	# four lowercase hex digits of a code point, then the \u introducer, reversed
210	def basic.hex(+uu: U32, out: List<&2, Char>) -> List<&2, Char>:
211	  hex.char(U32.mod(uu, 16)) <> (hex.char(U32.mod(U32.shrn(uu, 4n), 16)) <>
212	    (hex.char(U32.mod(U32.shrn(uu, 8n), 16)) <>
213	      (hex.char(U32.mod(U32.shrn(uu, 12n), 16)) <> ('u' <> ('\\' <> out)))))
214	
215	# an escape mark reversed onto the output: the mark, then the backslash
216	def basic.esc(mark: Char, out: List<&2, Char>) -> List<&2, Char>:
217	  mark <> ('\\' <> out)
218	
219	# other controls are \u escapes; the rest are themselves
220	def basic.cls.hex(hit: Bool) -> BK:
221	  match hit:
222	    case True{}:
223	      BKHex{}
224	    case False{}:
225	      BKCh{}
226	
227	# backslash
228	def basic.cls.bslash(hit: Bool, +uu: U32) -> BK:
229	  match hit:
230	    case True{}:
231	      BKEsc{'\\'}
232	    case False{}:
233	      basic.cls.hex(Bool.or(U32.is_lt(uu, 32), U32.is_eq(uu, 127)))
234	
235	# quotation mark
236	def basic.cls.quote(hit: Bool, +uu: U32) -> BK:
237	  match hit:
238	    case True{}:
239	      BKEsc{'"'}
240	    case False{}:
241	      basic.cls.bslash(U32.is_eq(uu, 92), uu)
242	
243	# carriage return
244	def basic.cls.cr(hit: Bool, +uu: U32) -> BK:
245	  match hit:
246	    case True{}:
247	      BKEsc{'r'}
248	    case False{}:
249	      basic.cls.quote(U32.is_eq(uu, 34), uu)
250	
251	# form feed
252	def basic.cls.ff(hit: Bool, +uu: U32) -> BK:
253	  match hit:
254	    case True{}:
255	      BKEsc{'f'}
256	    case False{}:
257	      basic.cls.cr(U32.is_eq(uu, 13), uu)
258	
259	# line feed
260	def basic.cls.lf(hit: Bool, +uu: U32) -> BK:
261	  match hit:
262	    case True{}:
263	      BKEsc{'n'}
264	    case False{}:
265	      basic.cls.ff(U32.is_eq(uu, 12), uu)
266	
267	# tab
268	def basic.cls.tab(hit: Bool, +uu: U32) -> BK:
269	  match hit:
270	    case True{}:
271	      BKEsc{'t'}
272	    case False{}:
273	      basic.cls.lf(U32.is_eq(uu, 10), uu)
274	
275	# backspace, then the rest
276	def basic.cls.bs(hit: Bool, +uu: U32) -> BK:
277	  match hit:
278	    case True{}:
279	      BKEsc{'b'}
280	    case False{}:
281	      basic.cls.tab(U32.is_eq(uu, 9), uu)
282	
283	# the class of a code point in a basic string
284	def basic.cls(+uu: U32) -> BK:
285	  basic.cls.bs(U32.is_eq(uu, 8), uu)
286	
287	# one character of a basic string, reversed onto the output
288	def basic.disp(kk: BK, cc: Char, uu: U32, out: List<&2, Char>) -> List<&2, Char>:
289	  match kk:
290	    case BKCh{}:
291	      cc <> out
292	    case BKEsc{mark}:
293	      basic.esc(mark, out)
294	    case BKHex{}:
295	      basic.hex(uu, out)
296	
297	# one character of a basic string
298	def basic.one(+cc: Char, out: List<&2, Char>) -> List<&2, Char>:
299	  +u = Char.to_u32(cc)
300	  basic.disp(basic.cls(u), cc, u, out)
301	
302	# the escaped characters of a basic string, reversed
303	def basic.go(cs: List<&2, Char>, out: List<&2, Char>) -> List<&2, Char>:
304	  match cs:
305	    case []:
306	      out
307	    case +h <> t:
308	      basic.go(t, basic.one(h, out))
309	
310	# a basic string: quotes, with controls and quotes escaped
311	def key.basic(+ss: String) -> String:
312	  "\"" ++ String.from_list(List.reverse(&2, Char,
313	    basic.go(String.to_list(ss), []))) ++ "\""
314	
315	# bare when the name allows it, otherwise a basic string
316	def key.go(ok: Bool, +ss: String) -> String:
317	  match ok:
318	    case True{}:
319	      ss
320	    case False{}:
321	      key.basic(ss)
322	
323	# a key as TOML writes it
324	def key(+ss: String) -> String:
325	  key.go(bare(ss), ss)
326	
327	# the overflow of a decimal step, least-significant digit first
328	def dec.carry.c0(zz: Bool, cc: U32) -> List<&2, U32>:
329	  match zz:
330	    case True{}:
331	      []
332	    case False{}:
333	      [U32.mod(cc, 10)]
334	
335	# the overflow of a decimal step
336	def dec.carry.c(+cc: U32) -> List<&2, U32>:
337	  dec.carry.c0(U32.is_zero(cc), cc)
338	
339	# the next digit of an overflow
340	def dec.carry.b0(zz: Bool, +cc: U32) -> List<&2, U32>:
341	  match zz:
342	    case True{}:
343	      []
344	    case False{}:
345	      U32.mod(cc, 10) <> dec.carry.c(U32.div(cc, 10))
346	
347	# the next digit of an overflow
348	def dec.carry.b(+cc: U32) -> List<&2, U32>:
349	  dec.carry.b0(U32.is_zero(cc), cc)
350	
351	# the first digit of an overflow
352	def dec.carry.a(zz: Bool, +cc: U32) -> List<&2, U32>:
353	  match zz:
354	    case True{}:
355	      []
356	    case False{}:
357	      U32.mod(cc, 10) <> dec.carry.b(U32.div(cc, 10))
358	
359	# the digits of a leftover carry
360	def dec.carry(+cc: U32) -> List<&2, U32>:
361	  dec.carry.a(U32.is_zero(cc), cc)
362	
363	# multiply a decimal numeral by a radix and add a digit
364	def dec.go(ds: List<&2, U32>, +radix: U32, +carry: U32) -> List<&2, U32>:
365	  match ds:
366	    case []:
367	      dec.carry(carry)
368	    case +d <> t:
369	      U32.mod(U32.add(U32.mul(d, radix), carry), 10) <> dec.go(t, radix,
370	        U32.div(U32.add(U32.mul(d, radix), carry), 10))
371	
372	# a digit character
373	def dec.ch(dd: U32) -> Char:
374	  Chr{U32.add(48, dd)}
375	
376	# digits as characters, in the order given
377	def dec.chars(ds: List<&2, U32>) -> List<&2, Char>:
378	  match ds:
379	    case []:
380	      []
381	    case d <> t:
382	      dec.ch(d) <> dec.chars(t)
383	
384	# whether a leading zero is still being skipped
385	def dec.drop.lead(lead: Bool, +hh: Char) -> Bool:
386	  match lead:
387	    case False{}:
388	      False{}
389	    case True{}:
390	      Char.is_eq(hh, '0')
391	
392	# a leading zero is skipped; any other character is kept
393	def dec.drop.outz(zz: Bool, hh: Char, out: List<&2, Char>) -> List<&2, Char>:
394	  match zz:
395	    case True{}:
396	      out
397	    case False{}:
398	      hh <> out
399	
400	# the output after one character, reversed
401	def dec.drop.out(lead: Bool, +hh: Char, out: List<&2, Char>) -> List<&2, Char>:
402	  match lead:
403	    case False{}:
404	      hh <> out
405	    case True{}:
406	      dec.drop.outz(Char.is_eq(hh, '0'), hh, out)
407	
408	# the numeral, or 0 when every digit was zero
409	def dec.drop.end(lead: Bool, out: List<&2, Char>) -> String:
410	  match lead:
411	    case True{}:
412	      "0"
413	    case False{}:
414	      String.from_list(List.reverse(&2, Char, out))
415	
416	# drop leading zeros from a most-significant-first digit list
417	def dec.drop(cs: List<&2, Char>, +lead: Bool, out: List<&2, Char>) -> String:
418	  match cs:
419	    case []:
420	      dec.drop.end(lead, out)
421	    case +h <> t:
422	      dec.drop(t, dec.drop.lead(lead, h), dec.drop.out(lead, h, out))
423	
424	# a decimal numeral. The digit list is least-significant first
425	def dec.text(ds: List<&2, U32>) -> String:
426	  dec.drop(dec.chars(List.reverse(&2, U32, ds)), True{}, [])
427	
428	# a code point's digit value, or 99 when the character is not a digit
429	def dig.up(ok: Bool, uu: U32) -> U32:
430	  match ok:
431	    case True{}:
432	      U32.sub(uu, 55)
433	    case False{}:
434	      99
435	
436	# a lowercase hex digit, otherwise an uppercase one
437	def dig.low(ok: Bool, +uu: U32) -> U32:
438	  match ok:
439	    case True{}:
440	      U32.sub(uu, 87)
441	    case False{}:
442	      dig.up(Bool.and(U32.is_ge(uu, 65), U32.is_le(uu, 70)), uu)
443	
444	# a decimal digit, otherwise a hex letter
445	def dig.dec(ok: Bool, +uu: U32) -> U32:
446	  match ok:
447	    case True{}:
448	      U32.sub(uu, 48)
449	    case False{}:
450	      dig.low(Bool.and(U32.is_ge(uu, 97), U32.is_le(uu, 102)), uu)
451	
452	# the value of a digit character, or 99
453	def dig.val(+cc: Char) -> U32:
454	  +u = Char.to_u32(cc)
455	  dig.dec(Bool.and(U32.is_ge(u, 48), U32.is_le(u, 57)), u)
456	
457	# whether a digit value fits a base
458	def dig.ok(dd: U32, base: U32) -> Bool:
459	  U32.is_lt(dd, base)
460	
461	# exactly k digits, or DigBad
462	def take.acc.d(digit: Bool, nn: U32, +cc: Char) -> U32:
463	  match digit:
464	    case False{}:
465	      nn
466	    case True{}:
467	      U32.add(U32.mul(nn, 10), U32.sub(Char.to_u32(cc), 48))
468	
469	# the accumulator after one character
470	def take.acc(ok: Bool, nn: U32, +cc: Char) -> U32:
471	  match ok:
472	    case False{}:
473	      nn
474	    case True{}:
475	      take.acc.d(Char.is_digit(cc), nn, cc)
476	
477	# the scan stays well only while every character is a digit
478	def take.ok(ok: Bool, +cc: Char) -> Bool:
479	  match ok:
480	    case False{}:
481	      False{}
482	    case True{}:
483	      Char.is_digit(cc)
484	
485	# the finished take
486	def take.fin(ok: Bool, nn: U32, cs: List<&2, Char>) -> Dig:
487	  match ok:
488	    case True{}:
489	      DigOk{nn, cs}
490	    case False{}:
491	      DigBad{}
492	
493	# exactly k digits from the front of a list
494	def take.n(kk: Nat, cs: List<&2, Char>, nn: U32, +ok: Bool) -> Dig:
495	  match kk:
496	    case 0n:
497	      take.fin(ok, nn, cs)
498	    case 1n+p:
499	      match cs:
500	        case []:
501	          DigBad{}
502	        case +h <> t:
503	          take.n(p, t, take.acc(ok, nn, h), take.ok(ok, h))
504	
505	# a number is inside the inclusive bounds
506	def bound.rng(+nn: U32, lo: U32, hi: U32) -> Bool:
507	  Bool.and(U32.is_ge(nn, lo), U32.is_le(nn, hi))
508	
509	# two digits, zero padded
510	def pad2.go(small: Bool, nn: U32) -> String:
511	  match small:
512	    case True{}:
513	      "0" ++ U32.show(nn)
514	    case False{}:
515	      U32.show(nn)
516	
517	# two digits, zero padded
518	def text.pad2(+nn: U32) -> String:
519	  pad2.go(U32.is_lt(nn, 10), nn)
520	
521	# the one-zero pad, or the digits themselves
522	def pad4.big(nn: U32, big: Bool) -> String:
523	  match big:
524	    case True{}:
525	      "0" ++ U32.show(nn)
526	    case False{}:
527	      U32.show(nn)
528	
529	# the three-digit and two-digit pads
530	def pad4.mid(nn: U32, mid: Bool, big: Bool) -> String:
531	  match mid:
532	    case True{}:
533	      "00" ++ U32.show(nn)
534	    case False{}:
535	      pad4.big(nn, big)
536	
537	# four digits, zero padded
538	def pad4.go(nn: U32, small: Bool, mid: Bool, big: Bool) -> String:
539	  match small:
540	    case True{}:
541	      "000" ++ U32.show(nn)
542	    case False{}:
543	      pad4.mid(nn, mid, big)
544	
545	# four digits, zero padded
546	def text.pad4(+nn: U32) -> String:
547	  pad4.go(nn, U32.is_lt(nn, 10), U32.is_lt(nn, 100), U32.is_lt(nn, 1000))
548	
549	# the sign of a zone offset
550	def zone.mark(sign: Sign) -> String:
551	  match sign:
552	    case Plus{}:
553	      "+"
554	    case Minus{}:
555	      "-"
556	
557	# a numeric zone offset
558	def zone.shift(sign: Sign, hh: U32, mi: U32) -> String:
559	  zone.mark(sign) ++ text.pad2(hh) ++ ":" ++ text.pad2(mi)
560	
561	# a zone suffix
562	def zone.text(zz: Zone) -> String:
563	  match zz:
564	    case Zulu{}:
565	      "Z"
566	    case Shift{sign, h, mi}:
567	      zone.shift(sign, h, mi)
568	
569	# the fractional second, or nothing
570	def clock.frac.go(empty: Bool, frac: String) -> String:
571	  match empty:
572	    case True{}:
573	      ""
574	    case False{}:
575	      "." ++ frac
576	
577	# the fractional second, or nothing
578	def clock.frac(+frac: String) -> String:
579	  clock.frac.go(String.is_empty(frac), frac)
580	
581	# a clock, with a fractional second when it has one
582	def clock.text(cc: Clock) -> String:
583	  Clock{h, mi, s, frac} = cc
584	  text.pad2(h) ++ ":" ++ text.pad2(mi) ++ ":" ++ text.pad2(s) ++ clock.frac(frac)
585	
586	# a date
587	def date.text(dd: Date) -> String:
588	  Date{y, mo, day} = dd
589	  text.pad4(y) ++ "-" ++ text.pad2(mo) ++ "-" ++ text.pad2(day)
590	
591	# a datetime in TOML spelling
592	def when.text(ww: When) -> String:
593	  match ww:
594	    case WOff{date, clock, zone}:
595	      date.text(date) ++ "T" ++ clock.text(clock) ++ zone.text(zone)
596	    case WLocal{date, clock}:
597	      date.text(date) ++ "T" ++ clock.text(clock)
598	    case WDate{date}:
599	      date.text(date)
600	    case WTime{clock}:
601	      clock.text(clock)
602	
603	# the sign of an integer or a float, empty when it is positive
604	def sign.text(sign: Sign) -> String:
605	  match sign:
606	    case Plus{}:
607	      ""
608	    case Minus{}:
609	      "-"
610	
611	# whether the list still has a character
612	def cs.some(cs: List<&2, Char>) -> Bool:
613	  match cs:
614	    case []:
615	      False{}
616	    case _ <> _:
617	      True{}
618	
619	# one character, when the list has one
620	def cs.head(cs: List<&2, Char>) -> Char:
621	  match cs:
622	    case []:
623	      ' '
624	    case h <> _:
625	      h
626	
627	# the tail of a list
628	def cs.tail(cs: List<&2, Char>) -> List<&2, Char>:
629	  match cs:
630	    case []:
631	      []
632	    case _ <> t:
633	      t
634	
635	# a clock with its fraction filled in
636	def clock.with(cc: Clock, frac: String) -> Clock:
637	  Clock{h, mi, s, _f} = cc
638	  Clock{h, mi, s, frac}
639	
640	# a finished local datetime, or one with a zone still to read
641	def when.done(_date: Date, _clock: Clock, ww: When) -> WhenOut:
642	  WSome{ww}
643	
644	# Z ends the token
645	def when.zone.z(tt: List<&2, Char>, clock: Clock, date: Date) -> WhenOut:
646	  match tt:
647	    case []:
648	      WSome{WOff{date, clock, Zulu{}}}
649	    case _ <> _:
650	      WFail{"invalid zone"}
651	
652	# the offset minute is in range
653	def when.zone.mm.ok2(mi_ok: Bool, sign: Sign, hh: U32, mi: U32, clock: Clock, date: Date) -> WhenOut:
654	  match mi_ok:
655	    case False{}:
656	      WFail{"zone minute is out of range"}
657	    case True{}:
658	      WSome{WOff{date, clock, Shift{sign, hh, mi}}}
659	
660	# the offset fields are in range
661	def when.zone.mm.ok(h_ok: Bool, mi_ok: Bool, sign: Sign, hh: U32, mi: U32, clock: Clock, date: Date) -> WhenOut:
662	  match h_ok:
663	    case False{}:
664	      WFail{"zone hour is out of range"}
665	    case True{}:
666	      when.zone.mm.ok2(mi_ok, sign, hh, mi, clock, date)
667	
668	# nothing follows an offset, and its fields are in range
669	def when.zone.mm.end(
670	  cs: List<&2, Char>,
671	  h_ok: Bool,
672	  mi_ok: Bool,
673	  sign: Sign,
674	  hh: U32,
675	  mi: U32,
676	  clock: Clock,
677	  date: Date
678	) -> WhenOut:
679	  match cs:
680	    case []:
681	      when.zone.mm.ok(h_ok, mi_ok, sign, hh, mi, clock, date)
682	    case _ <> _:
683	      WFail{"invalid zone"}
684	
685	# the offset minute is in range
686	def when.zone.mm.go(dd: Dig, sign: Sign, +hh: U32, clock: Clock, date: Date) -> WhenOut:
687	  match dd:
688	    case DigBad{}:
689	      WFail{"invalid zone"}
690	    case DigOk{+n, cs}:
691	      when.zone.mm.end(cs, bound.rng(hh, 0, 23), bound.rng(n, 0, 59), sign, hh, n, clock, date)
692	
693	# the offset minute
694	def when.zone.mm(hit: Bool, dd: Dig, sign: Sign, hh: U32, clock: Clock, date: Date) -> WhenOut:
695	  match hit:
696	    case False{}:
697	      WFail{"invalid zone"}
698	    case True{}:
699	      when.zone.mm.go(dd, sign, hh, clock, date)
700	
701	# the colon in an offset
702	def when.zone.hh.colon(cs: List<&2, Char>, sign: Sign, hh: U32, clock: Clock, date: Date) -> WhenOut:
703	  match cs:
704	    case []:
705	      WFail{"invalid zone"}
706	    case +c <> t:
707	      when.zone.mm(Char.is_eq(c, ':'), take.n(2n, t, 0, True{}), sign, hh, clock, date)
708	
709	# the offset hour
710	def when.zone.hh(dd: Dig, sign: Sign, clock: Clock, date: Date) -> WhenOut:
711	  match dd:
712	    case DigBad{}:
713	      WFail{"invalid zone"}
714	    case DigOk{n, cs}:
715	      when.zone.hh.colon(cs, sign, n, clock, date)
716	
717	# HH:MM of a numeric offset
718	def when.zone.off(sign: Sign, tt: List<&2, Char>, clock: Clock, date: Date) -> WhenOut:
719	  when.zone.hh(take.n(2n, tt, 0, True{}), sign, clock, date)
720	
721	# a minus starts a numeric offset
722	def when.zone.minus(minus: Bool, tt: List<&2, Char>, clock: Clock, date: Date) -> WhenOut:
723	  match minus:
724	    case True{}:
725	      when.zone.off(Minus{}, tt, clock, date)
726	    case False{}:
727	      WFail{"invalid zone"}
728	
729	# a plus or a minus starts a numeric offset
730	def when.zone.sign(plus: Bool, minus: Bool, tt: List<&2, Char>, clock: Clock, date: Date) -> WhenOut:
731	  match plus:
732	    case True{}:
733	      when.zone.off(Plus{}, tt, clock, date)
734	    case False{}:
735	      when.zone.minus(minus, tt, clock, date)
736	
737	# Z, or a signed numeric offset
738	def when.zone.go(zee: Bool, plus: Bool, minus: Bool, tt: List<&2, Char>, clock: Clock, date: Date) -> WhenOut:
739	  match zee:
740	    case True{}:
741	      when.zone.z(tt, clock, date)
742	    case False{}:
743	      when.zone.sign(plus, minus, tt, clock, date)
744	
745	# a zone, or the end of a local datetime
746	def when.zone(cs: List<&2, Char>, clock: Clock, date: Date) -> WhenOut:
747	  match cs:
748	    case []:
749	      WSome{WLocal{date, clock}}
750	    case +c <> t:
751	      when.zone.go(Bool.or(Char.is_eq(c, 'Z'), Char.is_eq(c, 'z')),
752	        Char.is_eq(c, '+'), Char.is_eq(c, '-'), t, clock, date)
753	
754	# the fraction must hold a digit
755	def when.frac.end.go(some: Bool, rev: List<&2, Char>, clock: Clock, date: Date, rest: List<&2, Char>) -> WhenOut:
756	  match some:
757	    case False{}:
758	      WFail{"invalid fraction"}
759	    case True{}:
760	      when.zone(rest, clock.with(clock, String.from_list(List.reverse(&2, Char, rev))),
761	        date)
762	
763	# the fraction must hold a digit
764	def when.frac.end(+rev: List<&2, Char>, clock: Clock, date: Date, rest: List<&2, Char>) -> WhenOut:
765	  when.frac.end.go(cs.some(rev), rev, clock, date, rest)
766	
767	# one fractional digit, or the end of the fraction
768	def when.frac.digit(
769	  digit: Bool,
770	  +cc: Char,
771	  tt: List<&2, Char>,
772	  rev: List<&2, Char>,
773	  clock: Clock,
774	  date: Date,
775	  more: Unit -> WhenOut
776	) -> WhenOut:
777	  match digit:
778	    case True{}:
779	      more(Unit{})
780	    case False{}:
781	      when.frac.end(rev, clock, date, cc <> tt)
782	
783	# fractional digits
784	def when.frac.digits(cs: List<&2, Char>, +rev: List<&2, Char>, +clock: Clock, +date: Date) -> WhenOut:
785	  match cs:
786	    case []:
787	      when.frac.end(rev, clock, date, [])
788	    case +c <> +t:
789	      when.frac.digit(Char.is_digit(c), c, t, rev, clock, date,
790	        _u => when.frac.digits(t, c <> rev, clock, date))
791	
792	# a dot starts a fraction; anything else is a zone
793	def when.frac.go(dot: Bool, tt: List<&2, Char>, clock: Clock, date: Date, +cc: Char) -> WhenOut:
794	  match dot:
795	    case True{}:
796	      when.frac.digits(tt, [], clock, date)
797	    case False{}:
798	      when.zone(cc <> tt, clock, date)
799	
800	# an optional fractional second
801	def when.frac(cs: List<&2, Char>, +clock: Clock, +date: Date) -> WhenOut:
802	  match cs:
803	    case []:
804	      when.done(date, clock, WLocal{date, clock})
805	    case +c <> t:
806	      when.frac.go(Char.is_eq(c, '.'), t, clock, date, c)
807	
808	# the second is in range, then the fraction and the zone
809	def when.clock.range.s(s_ok: Bool, hh: U32, mi: U32, ss: U32, cs: List<&2, Char>, date: Date) -> WhenOut:
810	  match s_ok:
811	    case False{}:
812	      WFail{"second is out of range"}
813	    case True{}:
814	      when.frac(cs, Clock{hh, mi, ss, ""}, date)
815	
816	# minute and second are in range
817	def when.clock.range.m(mi_ok: Bool, s_ok: Bool, hh: U32, mi: U32, ss: U32, cs: List<&2, Char>, date: Date) -> WhenOut:
818	  match mi_ok:
819	    case False{}:
820	      WFail{"minute is out of range"}
821	    case True{}:
822	      when.clock.range.s(s_ok, hh, mi, ss, cs, date)
823	
824	# hour, minute, and second are in range
825	def when.clock.range(
826	  h_ok: Bool,
827	  mi_ok: Bool,
828	  s_ok: Bool,
829	  hh: U32,
830	  mi: U32,
831	  ss: U32,
832	  cs: List<&2, Char>,
833	  date: Date
834	) -> WhenOut:
835	  match h_ok:
836	    case False{}:
837	      WFail{"hour is out of range"}
838	    case True{}:
839	      when.clock.range.m(mi_ok, s_ok, hh, mi, ss, cs, date)
840	
841	# seconds, then an optional fraction and zone
842	def when.clock.ss.go(dd: Dig, +hh: U32, +mi: U32, date: Date) -> WhenOut:
843	  match dd:
844	    case DigBad{}:
845	      WFail{"invalid time"}
846	    case DigOk{+n, cs}:
847	      when.clock.range(bound.rng(hh, 0, 23), bound.rng(mi, 0, 59), bound.rng(n, 0, 60), hh, mi, n,
848	        cs, date)
849	
850	# seconds after the colon
851	def when.clock.ss(hit: Bool, dd: Dig, hh: U32, mi: U32, date: Date) -> WhenOut:
852	  match hit:
853	    case False{}:
854	      WFail{"invalid time"}
855	    case True{}:
856	      when.clock.ss.go(dd, hh, mi, date)
857	
858	# the colon after the minutes
859	def when.clock.mm.colon(cs: List<&2, Char>, hh: U32, mi: U32, date: Date) -> WhenOut:
860	  match cs:
861	    case []:
862	      WFail{"invalid time"}
863	    case +c <> t:
864	      when.clock.ss(Char.is_eq(c, ':'), take.n(2n, t, 0, True{}), hh, mi, date)
865	
866	# minutes, then seconds
867	def when.clock.mm(dd: Dig, hh: U32, date: Date) -> WhenOut:
868	  match dd:
869	    case DigBad{}:
870	      WFail{"invalid time"}
871	    case DigOk{n, cs}:
872	      when.clock.mm.colon(cs, hh, n, date)
873	
874	# the colon after the hour
875	def when.clock.colon.go(hit: Bool, hh: U32, tt: List<&2, Char>, date: Date) -> WhenOut:
876	  match hit:
877	    case False{}:
878	      WFail{"invalid time"}
879	    case True{}:
880	      when.clock.mm(take.n(2n, tt, 0, True{}), hh, date)
881	
882	# the colon after the hour
883	def when.clock.colon(cs: List<&2, Char>, hh: U32, date: Date) -> WhenOut:
884	  match cs:
885	    case []:
886	      WFail{"invalid time"}
887	    case +c <> t:
888	      when.clock.colon.go(Char.is_eq(c, ':'), hh, t, date)
889	
890	# a clock following a date
891	def when.clock.of(dd: Dig, date: Date) -> WhenOut:
892	  match dd:
893	    case DigBad{}:
894	      WFail{"invalid time"}
895	    case DigOk{n, cs}:
896	      when.clock.colon(cs, n, date)
897	
898	# a space separates a date from a time
899	def when.after.sp(sp: Bool, date: Date, tt: List<&2, Char>) -> WhenOut:
900	  match sp:
901	    case True{}:
902	      when.clock.of(take.n(2n, tt, 0, True{}), date)
903	    case False{}:
904	      WFail{"invalid datetime"}
905	
906	# T or a space separates a date from a time
907	def when.after.sep(tee: Bool, sp: Bool, date: Date, tt: List<&2, Char>) -> WhenOut:
908	  match tee:
909	    case True{}:
910	      when.clock.of(take.n(2n, tt, 0, True{}), date)
911	    case False{}:
912	      when.after.sp(sp, date, tt)
913	
914	# the character after a date: nothing, T, or a space, and then a time
915	def when.after.date(date: Date, cs: List<&2, Char>) -> WhenOut:
916	  match cs:
917	    case []:
918	      WSome{WDate{date}}
919	    case +c <> t:
920	      when.after.sep(Bool.or(Char.is_eq(c, 'T'), Char.is_eq(c, 't')),
921	        Char.is_eq(c, ' '), date, t)
922	
923	# the day is in range, then the rest of the token is a time or nothing
924	def when.date.ok.d(d_ok: Bool, yy: U32, mo: U32, dd: U32, cs: List<&2, Char>) -> WhenOut:
925	  match d_ok:
926	    case False{}:
927	      WFail{"day is out of range"}
928	    case True{}:
929	      when.after.date(Date{yy, mo, dd}, cs)
930	
931	# a date whose fields are in range
932	def when.date.ok.go(mo_ok: Bool, d_ok: Bool, yy: U32, mo: U32, dd: U32, cs: List<&2, Char>) -> WhenOut:
933	  match mo_ok:
934	    case False{}:
935	      WFail{"month is out of range"}
936	    case True{}:
937	      when.date.ok.d(d_ok, yy, mo, dd, cs)
938	
939	# February in a year divisible by 4 and by 100: 29 days only when the year
940	# is also divisible by 400
941	def when.feb.quad(four_hundred: Bool) -> U32:
942	  match four_hundred:
943	    case True{}:
944	      29
945	    case False{}:
946	      28
947	
948	# February in a year divisible by 4: 29 days unless the year is a century
949	def when.feb.cent(hundred: Bool, four_hundred: Bool) -> U32:
950	  match hundred:
951	    case False{}:
952	      29
953	    case True{}:
954	      when.feb.quad(four_hundred)
955	
956	# February: 29 days in a leap year and 28 otherwise. A leap year is divisible
957	# by 4, except by 100 unless also by 400 (RFC 3339, Appendix C)
958	def when.feb.go(four: Bool, hundred: Bool, four_hundred: Bool) -> U32:
959	  match four:
960	    case False{}:
961	      28
962	    case True{}:
963	      when.feb.cent(hundred, four_hundred)
964	
965	# the days of February in a year
966	def when.feb(+yy: U32) -> U32:
967	  when.feb.go(U32.is_eq(U32.mod(yy, 4), 0), U32.is_eq(U32.mod(yy, 100), 0),
968	    U32.is_eq(U32.mod(yy, 400), 0))
969	
970	# April, June, September and November have 30 days
971	def when.short(+mo: U32) -> Bool:
972	  Bool.or(Bool.or(U32.is_eq(mo, 4), U32.is_eq(mo, 6)),
973	    Bool.or(U32.is_eq(mo, 9), U32.is_eq(mo, 11)))
974	
975	# 30 days in a short month and 31 in the others
976	def when.days.short(short: Bool) -> U32:
977	  match short:
978	    case True{}:
979	      30
980	    case False{}:
981	      31
982	
983	# the days of a month, by whether it is February or a short month
984	def when.days.go(feb: Bool, short: Bool, +yy: U32) -> U32:
985	  match feb:
986	    case True{}:
987	      when.feb(yy)
988	    case False{}:
989	      when.days.short(short)
990	
991	# the days of month mo in year yy
992	def when.days(+yy: U32, +mo: U32) -> U32:
993	  when.days.go(U32.is_eq(mo, 2), when.short(mo), yy)
994	
995	# a date whose fields are in range: the day within its month in that year
996	def when.date.ok(+yy: U32, +mo: U32, +dd: U32, cs: List<&2, Char>) -> WhenOut:
997	  when.date.ok.go(bound.rng(mo, 1, 12), bound.rng(dd, 1, when.days(yy, mo)), yy, mo, dd, cs)
998	
999	# a local time: HH:MM:SS, with the hour already taken
1000	def when.time.rest(tt: List<&2, Char>, hh: U32) -> WhenOut:
1001	  when.clock.mm(take.n(2n, tt, 0, True{}), hh, Date{0, 1, 1})
1002	
1003	# a local time uses a dummy date and then keeps only the clock
1004	def when.time.only(ww: WhenOut) -> WhenOut:
1005	  match ww:
1006	    case WSome{WLocal{_date, clock}}:
1007	      WSome{WTime{clock}}
1008	    case WSome{WOff{_date, clock, zone}}:
1009	      WFail{"invalid time"}
1010	    case WSome{other}:
1011	      WFail{"invalid time"}
1012	    case WFail{why}:
1013	      WFail{why}
1014	    case WSkip{}:
1015	      WFail{"invalid time"}
1016	
1017	# a complete date, then whatever follows it
1018	def when.day.end(dd: Dig, yy: U32, mo: U32) -> WhenOut:
1019	  match dd:
1020	    case DigBad{}:
1021	      WFail{"invalid date"}
1022	    case DigOk{n, cs}:
1023	      when.date.ok(yy, mo, n, cs)
1024	
1025	# the day is two digits
1026	def when.day.go(hit: Bool, dd: Dig, yy: U32, mo: U32) -> WhenOut:
1027	  match hit:
1028	    case False{}:
1029	      WFail{"invalid date"}
1030	    case True{}:
1031	      when.day.end(dd, yy, mo)
1032	
1033	# the day
1034	def when.day(cs: List<&2, Char>, yy: U32, mo: U32) -> WhenOut:
1035	  match cs:
1036	    case []:
1037	      WFail{"invalid date"}
1038	    case +c <> t:
1039	      when.day.go(Char.is_eq(c, '-'), take.n(2n, t, 0, True{}), yy, mo)
1040	
1041	# the dash after the month
1042	def when.month.go(dd: Dig, yy: U32) -> WhenOut:
1043	  match dd:
1044	    case DigBad{}:
1045	      WFail{"invalid date"}
1046	    case DigOk{n, cs}:
1047	      when.day(cs, yy, n)
1048	
1049	# the month
1050	def when.month(hit: Bool, dd: Dig, yy: U32) -> WhenOut:
1051	  match hit:
1052	    case False{}:
1053	      WFail{"invalid date"}
1054	    case True{}:
1055	      when.month.go(dd, yy)
1056	
1057	# the dash after the year
1058	def when.year.dash(cs: List<&2, Char>, yy: U32) -> WhenOut:
1059	  match cs:
1060	    case []:
1061	      WFail{"invalid date"}
1062	    case +c <> t:
1063	      when.month(Char.is_eq(c, '-'), take.n(2n, t, 0, True{}), yy)
1064	
1065	# the fourth year digit, then the month
1066	def when.year4(dd: Dig) -> WhenOut:
1067	  match dd:
1068	    case DigBad{}:
1069	      WFail{"invalid date"}
1070	    case DigOk{n, cs}:
1071	      when.year.dash(cs, n)
1072	
1073	# two more year digits, then a dash
1074	def when.year.more(digit: Bool, nn: U32, +cc: Char, tt: List<&2, Char>) -> WhenOut:
1075	  match digit:
1076	    case False{}:
1077	      WFail{"invalid datetime"}
1078	    case True{}:
1079	      when.year4(take.n(1n, tt, U32.add(U32.mul(nn, 10), dig.val(cc)), True{}))
1080	
1081	# a colon means a local time; another digit continues a year
1082	def when.branch(colon: Bool, digit: Bool, nn: U32, +cc: Char, tt: List<&2, Char>) -> WhenOut:
1083	  match colon:
1084	    case True{}:
1085	      when.time.only(when.time.rest(tt, nn))
1086	    case False{}:
1087	      when.year.more(digit, nn, cc, tt)
1088	
1089	# two digits decide a time or a date
1090	def when.after2.go(cs: List<&2, Char>, nn: U32) -> WhenOut:
1091	  match cs:
1092	    case []:
1093	      WFail{"invalid datetime"}
1094	    case +c <> t:
1095	      when.branch(Char.is_eq(c, ':'), Char.is_digit(c), nn, c, t)
1096	
1097	# two digits decide a time (HH:) or a date (YYYY-)
1098	def when.after2(dd: Dig) -> WhenOut:
1099	  match dd:
1100	    case DigBad{}:
1101	      WFail{"invalid datetime"}
1102	    case DigOk{n, cs}:
1103	      when.after2.go(cs, n)
1104	
1105	# a datetime token
1106	def when.read(cs: List<&2, Char>) -> WhenOut:
1107	  when.after2(take.n(2n, cs, 0, True{}))
1108	
1109	# a dash after the first character
1110	def word.dash.hit(first: Bool, +cc: Char) -> Bool:
1111	  match first:
1112	    case True{}:
1113	      False{}
1114	    case False{}:
1115	      Char.is_eq(cc, '-')
1116	
1117	# either flag
1118	def word.or(aa: Bool, bb: Bool) -> Bool:
1119	  match aa:
1120	    case True{}:
1121	      True{}
1122	    case False{}:
1123	      bb
1124	
1125	# a colon anywhere in the token
1126	def word.colon(cs: List<&2, Char>) -> Bool:
1127	  match cs:
1128	    case []:
1129	      False{}
1130	    case +c <> t:
1131	      word.or(Char.is_eq(c, ':'), word.colon(t))
1132	
1133	# e or E: an exponent, so the token is a numeral rather than a datetime
1134	def word.ee.hit(+cc: Char) -> Bool:
1135	  Bool.or(Char.is_eq(cc, 'e'), Char.is_eq(cc, 'E'))
1136	
1137	# whether the token holds an exponent marker
1138	def word.ee(cs: List<&2, Char>) -> Bool:
1139	  match cs:
1140	    case []:
1141	      False{}
1142	    case +c <> t:
1143	      word.or(word.ee.hit(c), word.ee(t))
1144	
1145	# a datetime scan only when the token is not an exponent numeral
1146	def word.as_date(date: Bool, exp: Bool) -> Bool:
1147	  match exp:
1148	    case True{}:
1149	      False{}
1150	    case False{}:
1151	      date
1152	
1153	# a dash after the first character
1154	def word.dash(cs: List<&2, Char>, first: Bool) -> Bool:
1155	  match cs:
1156	    case []:
1157	      False{}
1158	    case +c <> t:
1159	      word.or(word.dash.hit(first, c), word.dash(t, False{}))
1160	
1161	# a negative nan, or not a special
1162	def word.spec.nan3(cc: Bool) -> Got:
1163	  match cc:
1164	    case True{}:
1165	      GotVal{VFlo{Minus{}, "nan"}}
1166	    case False{}:
1167	      GotBad{""}
1168	
1169	# a signed nan
1170	def word.spec.nan2(bb: Bool, cc: Bool) -> Got:
1171	  match bb:
1172	    case True{}:
1173	      GotVal{VFlo{Plus{}, "nan"}}
1174	    case False{}:
1175	      word.spec.nan3(cc)
1176	
1177	# nan
1178	def word.spec.nan(aa: Bool, bb: Bool, cc: Bool) -> Got:
1179	  match aa:
1180	    case True{}:
1181	      GotVal{VFlo{Plus{}, "nan"}}
1182	    case False{}:
1183	      word.spec.nan2(bb, cc)
1184	
1185	# character-for-character equality. a mismatch drops the rest and stops
1186	def str.eq.step(aa: String, bb: String, same: Bool) -> Bool:
1187	  match aa bb same:
1188	    case SNil{} SNil{} True{}:
1189	      True{}
1190	    case SCon{x, xt} SCon{y, yt} True{}:
1191	      str.eq.step(xt, yt, Char.is_eq(x, y))
1192	    case _a _b _s:
1193	      False{}
1194	
1195	# the search only needs the bool, not a rebuilt copy of either string
1196	def str.eq(aa: String, bb: String) -> Bool:
1197	  str.eq.step(aa, bb, True{})
1198	
1199	# a negative inf, or nan
1200	def word.spec.inf3(cc: Bool, +ss: String) -> Got:
1201	  match cc:
1202	    case True{}:
1203	      GotVal{VFlo{Minus{}, "inf"}}
1204	    case False{}:
1205	      word.spec.nan(str.eq(ss, "nan"), str.eq(ss, "+nan"), str.eq(ss, "-nan"))
1206	
1207	# a signed inf, or nan
1208	def word.spec.inf2(bb: Bool, cc: Bool, +ss: String) -> Got:
1209	  match bb:
1210	    case True{}:
1211	      GotVal{VFlo{Plus{}, "inf"}}
1212	    case False{}:
1213	      word.spec.inf3(cc, ss)
1214	
1215	# inf, or nan
1216	def word.spec.inf(aa: Bool, bb: Bool, cc: Bool, +ss: String) -> Got:
1217	  match aa:
1218	    case True{}:
1219	      GotVal{VFlo{Plus{}, "inf"}}
1220	    case False{}:
1221	      word.spec.inf2(bb, cc, ss)
1222	
1223	# false, or the rest of the specials
1224	def word.spec.f(hit: Bool, +ss: String) -> Got:
1225	  match hit:
1226	    case True{}:
1227	      GotVal{VBool{False{}}}
1228	    case False{}:
1229	      word.spec.inf(str.eq(ss, "inf"), str.eq(ss, "+inf"), str.eq(ss, "-inf"), ss)
1230	
1231	# true, or the rest of the specials
1232	def word.spec.t(hit: Bool, other: Bool, +ss: String) -> Got:
1233	  match hit:
1234	    case True{}:
1235	      GotVal{VBool{True{}}}
1236	    case False{}:
1237	      word.spec.f(other, ss)
1238	
1239	# true, false, inf, and nan, including a sign on inf and nan
1240	def word.spec(+ss: String) -> Got:
1241	  word.spec.t(str.eq(ss, "true"), str.eq(ss, "false"), ss)
1242	
1243	# a datetime result as a value
1244	def word.from.when(ww: WhenOut) -> Got:
1245	  match ww:
1246	    case WSome{when}:
1247	      GotVal{VWhen{when}}
1248	    case WFail{why}:
1249	      GotBad{why}
1250	    case WSkip{}:
1251	      GotBad{"invalid datetime"}
1252	
1253	# the spelling of a numeral with the leading sign and underscores removed
1254	def word.body.put.sign(is_sign: Bool, cc: Char, out: List<&2, Char>) -> List<&2, Char>:
1255	  match is_sign:
1256	    case True{}:
1257	      out
1258	    case False{}:
1259	      cc <> out
1260	
1261	# an underscore is dropped; every other character is kept
1262	def word.body.put.us(is_us: Bool, cc: Char, out: List<&2, Char>) -> List<&2, Char>:
1263	  match is_us:
1264	    case True{}:
1265	      out
1266	    case False{}:
1267	      cc <> out
1268	
1269	# one character of a numeral spelling
1270	def word.body.put(lead: Bool, +cc: Char, out: List<&2, Char>) -> List<&2, Char>:
1271	  match lead:
1272	    case True{}:
1273	      word.body.put.sign(Bool.or(Char.is_eq(cc, '+'), Char.is_eq(cc, '-')), cc, out)
1274	    case False{}:
1275	      word.body.put.us(Char.is_eq(cc, '_'), cc, out)
1276	
1277	# the spelling, reversed, then put back in order at the end
1278	def word.body.go(cs: List<&2, Char>, lead: Bool, out: List<&2, Char>) -> List<&2, Char>:
1279	  match cs:
1280	    case []:
1281	      List.reverse(&2, Char, out)
1282	    case +c <> t:
1283	      word.body.go(t, False{}, word.body.put(lead, c, out))
1284	
1285	# the spelling of a numeral with the leading sign and underscores removed
1286	def word.body(cs: List<&2, Char>) -> String:
1287	  String.from_list(word.body.go(cs, True{}, []))
1288	
1289	# a fresh numeral scan
1290	def num.start() -> Num:
1291	  Num{NLead{}, Plus{}, 10, [], False{}, False{}, ""}
1292	
1293	# a scan that has failed
1294	def num.bad(_st: Num, why: String) -> Num:
1295	  Num{NBad{}, Plus{}, 10, [], False{}, False{}, why}
1296	
1297	# set the sign and wait for a digit
1298	def num.sign(_st: Num, sign: Sign) -> Num:
1299	  Num{NSign{}, sign, 10, [], False{}, False{}, ""}
1300	
1301	# a digit that fits the base
1302	def num.digit.ok(ok: Bool, +cc: Char, nk: NK, sign: Sign, +base: U32, ds: List<&2, U32>) -> Num:
1303	  match ok:
1304	    case False{}:
1305	      num.bad(Num{NLead{}, Plus{}, 10, [], False{}, False{}, ""}, "invalid digit")
1306	    case True{}:
1307	      Num{nk, sign, base, dec.go(ds, base, dig.val(cc)), False{}, True{}, ""}
1308	
1309	# a decimal digit joined to the numeral
1310	def num.digit.go(st: Num, +cc: Char, nk: NK) -> Num:
1311	  Num{_nk, sign, +base, ds, _us, _saw, _why} = st
1312	  num.digit.ok(dig.ok(dig.val(cc), base), cc, nk, sign, base, ds)
1313	
1314	# a decimal digit joined to the numeral
1315	def num.digit(st: Num, +cc: Char, nk: NK) -> Num:
1316	  num.digit.go(st, cc, nk)
1317	
1318	# an underscore between digits
1319	def num.us.go(ok: Bool, nk: NK, sign: Sign, base: U32, ds: List<&2, U32>, why: String) -> Num:
1320	  match ok:
1321	    case False{}:
1322	      num.bad(Num{NLead{}, Plus{}, 10, [], False{}, False{}, ""}, "invalid underscore")
1323	    case True{}:
1324	      Num{nk, sign, base, ds, True{}, True{}, why}
1325	
1326	# an underscore between digits
1327	def num.us(st: Num) -> Num:
1328	  Num{nk, sign, base, ds, us, saw, why} = st
1329	  num.us.go(Bool.and(saw, Bool.not(us)), nk, sign, base, ds, why)
1330	
1331	# the base prefix after a leading zero
1332	def num.base(st: Num, base: U32) -> Num:
1333	  Num{_nk, sign, _b, _ds, _us, _saw, _why} = st
1334	  Num{NBase{}, sign, base, [], False{}, False{}, ""}
1335	
1336	# a dot begins the fraction
1337	def num.dot.go(ok: Bool, sign: Sign) -> Num:
1338	  match ok:
1339	    case False{}:
1340	      num.bad(Num{NLead{}, Plus{}, 10, [], False{}, False{}, ""}, "invalid fraction")
1341	    case True{}:
1342	      Num{NFrac{}, sign, 10, [], False{}, False{}, ""}
1343	
1344	# a dot begins the fraction
1345	def num.dot(st: Num) -> Num:
1346	  Num{_nk, sign, _b, _ds, us, saw, _why} = st
1347	  num.dot.go(Bool.and(saw, Bool.not(us)), sign)
1348	
1349	# an exponent marker
1350	def num.exp.go(ok: Bool, sign: Sign) -> Num:
1351	  match ok:
1352	    case False{}:
1353	      num.bad(Num{NLead{}, Plus{}, 10, [], False{}, False{}, ""}, "invalid exponent")
1354	    case True{}:
1355	      Num{NExp{}, sign, 10, [], False{}, False{}, ""}
1356	
1357	# an exponent marker
1358	def num.exp(st: Num) -> Num:
1359	  Num{_nk, sign, _b, _ds, us, saw, _why} = st
1360	  num.exp.go(Bool.and(saw, Bool.not(us)), sign)
1361	
1362	# the sign already chosen
1363	def num.sign.of(st: Num) -> Sign:
1364	  Num{_nk, sign, _b, _ds, _us, _saw, _why} = st
1365	  sign
1366	
1367	# a first digit
1368	def num.lead.digit(digit: Bool, st: Num, +cc: Char) -> Num:
1369	  match digit:
1370	    case True{}:
1371	      num.digit(st, cc, NDig{})
1372	    case False{}:
1373	      num.bad(st, "invalid number")
1374	
1375	# a leading zero, or another digit
1376	def num.lead.zero(zero: Bool, digit: Bool, st: Num, +cc: Char) -> Num:
1377	  match zero:
1378	    case True{}:
1379	      Num{NZero{}, num.sign.of(st), 10, [], False{}, True{}, ""}
1380	    case False{}:
1381	      num.lead.digit(digit, st, cc)
1382	
1383	# a minus, a zero, or a digit
1384	def num.lead.minus(minus: Bool, zero: Bool, digit: Bool, st: Num, +cc: Char) -> Num:
1385	  match minus:
1386	    case True{}:
1387	      num.sign(st, Minus{})
1388	    case False{}:
1389	      num.lead.zero(zero, digit, st, cc)
1390	
1391	# a sign, a zero, or a digit
1392	def num.lead.go(plus: Bool, minus: Bool, zero: Bool, digit: Bool, st: Num, +cc: Char) -> Num:
1393	  match plus:
1394	    case True{}:
1395	      num.sign(st, Plus{})
1396	    case False{}:
1397	      num.lead.minus(minus, zero, digit, st, cc)
1398	
1399	# the first character after an optional sign
1400	def num.lead(st: Num, +cc: Char) -> Num:
1401	  num.lead.go(Char.is_eq(cc, '+'), Char.is_eq(cc, '-'), Char.is_eq(cc, '0'),
1402	    Char.is_digit(cc), st, cc)
1403	
1404	# a second sign is refused; any other character is read as the first one of
1405	# an unsigned numeral, with the sign kept
1406	def num.after.sign.go(twice: Bool, sign: Sign, +cc: Char) -> Num:
1407	  match twice:
1408	    case True{}:
1409	      num.bad(num.start(), "invalid number")
1410	    case False{}:
1411	      num.lead(Num{NLead{}, sign, 10, [], False{}, False{}, ""}, cc)
1412	
1413	# the character after a sign
1414	def num.after.sign(st: Num, +cc: Char) -> Num:
1415	  num.after.sign.go(Bool.or(Char.is_eq(cc, '+'), Char.is_eq(cc, '-')), num.sign.of(st), cc)
1416	
1417	# a capital exponent; any other character is refused, since a digit or an
1418	# underscore after a leading zero (`01`, `0_1`) would hide it
1419	def num.zero.exp2(ee: Bool, st: Num, _c: Char) -> Num:
1420	  match ee:
1421	    case True{}:
1422	      num.exp(st)
1423	    case False{}:
1424	      num.bad(st, "invalid number")
1425	
1426	# an exponent after zero, or a rejected extra digit
1427	def num.zero.exp(eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1428	  match eee:
1429	    case True{}:
1430	      num.exp(st)
1431	    case False{}:
1432	      num.zero.exp2(ee, st, cc)
1433	
1434	# a fraction or an exponent after zero
1435	def num.zero.dot(dot: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1436	  match dot:
1437	    case True{}:
1438	      num.dot(st)
1439	    case False{}:
1440	      num.zero.exp(eee, ee, st, cc)
1441	
1442	# a binary prefix, or a float
1443	def num.zero.b(bb: Bool, dot: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1444	  match bb:
1445	    case True{}:
1446	      num.base(st, 2)
1447	    case False{}:
1448	      num.zero.dot(dot, eee, ee, st, cc)
1449	
1450	# an octal prefix, or the rest
1451	def num.zero.o(oo: Bool, bb: Bool, dot: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1452	  match oo:
1453	    case True{}:
1454	      num.base(st, 8)
1455	    case False{}:
1456	      num.zero.b(bb, dot, eee, ee, st, cc)
1457	
1458	# a base prefix, a fraction, or an exponent
1459	def num.zero.go(xx: Bool, oo: Bool, bb: Bool, dot: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1460	  match xx:
1461	    case True{}:
1462	      num.base(st, 16)
1463	    case False{}:
1464	      num.zero.o(oo, bb, dot, eee, ee, st, cc)
1465	
1466	# the character after a lone zero
1467	def num.zero(st: Num, +cc: Char) -> Num:
1468	  num.zero.go(Char.is_eq(cc, 'x'), Char.is_eq(cc, 'o'), Char.is_eq(cc, 'b'),
1469	    Char.is_eq(cc, '.'), Char.is_eq(cc, 'e'), Char.is_eq(cc, 'E'), st, cc)
1470	
1471	# a capital exponent, or a rejected character
1472	def num.digs.exp2(ee: Bool, st: Num, _c: Char) -> Num:
1473	  match ee:
1474	    case True{}:
1475	      num.exp(st)
1476	    case False{}:
1477	      num.bad(st, "invalid number")
1478	
1479	# an exponent
1480	def num.digs.exp(eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1481	  match eee:
1482	    case True{}:
1483	      num.exp(st)
1484	    case False{}:
1485	      num.digs.exp2(ee, st, cc)
1486	
1487	# a dot or an exponent
1488	def num.digs.dot(dot: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1489	  match dot:
1490	    case True{}:
1491	      num.dot(st)
1492	    case False{}:
1493	      num.digs.exp(eee, ee, st, cc)
1494	
1495	# an underscore, a dot, or an exponent
1496	def num.digs.us(us: Bool, dot: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1497	  match us:
1498	    case True{}:
1499	      num.us(st)
1500	    case False{}:
1501	      num.digs.dot(dot, eee, ee, st, cc)
1502	
1503	# a decimal digit, an underscore, a dot, or an exponent
1504	def num.digs.go(digit: Bool, us: Bool, dot: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1505	  match digit:
1506	    case True{}:
1507	      num.digit(st, cc, NDig{})
1508	    case False{}:
1509	      num.digs.us(us, dot, eee, ee, st, cc)
1510	
1511	# a decimal digit, an underscore, a dot, or an exponent
1512	def num.digs(st: Num, +cc: Char) -> Num:
1513	  num.digs.go(Char.is_digit(cc), Char.is_eq(cc, '_'), Char.is_eq(cc, '.'),
1514	    Char.is_eq(cc, 'e'), Char.is_eq(cc, 'E'), st, cc)
1515	
1516	# an underscore, or a digit of the base
1517	def num.based.go(us: Bool, st: Num, +cc: Char) -> Num:
1518	  match us:
1519	    case True{}:
1520	      num.us(st)
1521	    case False{}:
1522	      num.digit(st, cc, NBase{})
1523	
1524	# a digit of a prefixed integer, or an underscore
1525	def num.based(st: Num, +cc: Char) -> Num:
1526	  num.based.go(Char.is_eq(cc, '_'), st, cc)
1527	
1528	# a capital exponent, or a rejected character
1529	def num.frac.exp2(ee: Bool, st: Num, _c: Char) -> Num:
1530	  match ee:
1531	    case True{}:
1532	      num.exp(st)
1533	    case False{}:
1534	      num.bad(st, "invalid fraction")
1535	
1536	# an exponent in a fraction
1537	def num.frac.exp(eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1538	  match eee:
1539	    case True{}:
1540	      num.exp(st)
1541	    case False{}:
1542	      num.frac.exp2(ee, st, cc)
1543	
1544	# an underscore or an exponent in a fraction
1545	def num.frac.us(us: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1546	  match us:
1547	    case True{}:
1548	      num.us(st)
1549	    case False{}:
1550	      num.frac.exp(eee, ee, st, cc)
1551	
1552	# a fraction digit, an underscore, or an exponent
1553	def num.frac.go(digit: Bool, us: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1554	  match digit:
1555	    case True{}:
1556	      num.digit(st, cc, NFrac{})
1557	    case False{}:
1558	      num.frac.us(us, eee, ee, st, cc)
1559	
1560	# a fraction digit, an underscore, or an exponent
1561	def num.frac(st: Num, +cc: Char) -> Num:
1562	  num.frac.go(Char.is_digit(cc), Char.is_eq(cc, '_'), Char.is_eq(cc, 'e'),
1563	    Char.is_eq(cc, 'E'), st, cc)
1564	
1565	# the exponent sign is part of the spelling; digits follow
1566	def num.exp.sign(st: Num) -> Num:
1567	  Num{_nk, sign, _b, _ds, _us, _saw, _why} = st
1568	  Num{NEDig{}, sign, 10, [], False{}, False{}, ""}
1569	
1570	# a digit of the exponent
1571	def num.expon.digit(digit: Bool, st: Num, +cc: Char) -> Num:
1572	  match digit:
1573	    case True{}:
1574	      num.digit(st, cc, NEDig{})
1575	    case False{}:
1576	      num.bad(st, "invalid exponent")
1577	
1578	# a minus or a digit in an exponent
1579	def num.expon.minus(minus: Bool, digit: Bool, st: Num, +cc: Char) -> Num:
1580	  match minus:
1581	    case True{}:
1582	      num.exp.sign(st)
1583	    case False{}:
1584	      num.expon.digit(digit, st, cc)
1585	
1586	# the sign or the first digit of an exponent
1587	def num.expon.go(plus: Bool, minus: Bool, digit: Bool, st: Num, +cc: Char) -> Num:
1588	  match plus:
1589	    case True{}:
1590	      num.exp.sign(st)
1591	    case False{}:
1592	      num.expon.minus(minus, digit, st, cc)
1593	
1594	# the sign or the first digit of an exponent
1595	def num.expon(st: Num, +cc: Char) -> Num:
1596	  num.expon.go(Char.is_eq(cc, '+'), Char.is_eq(cc, '-'), Char.is_digit(cc), st, cc)
1597	
1598	# an underscore in an exponent
1599	def num.edig.us(us: Bool, st: Num, _c: Char) -> Num:
1600	  match us:
1601	    case True{}:
1602	      num.us(st)
1603	    case False{}:
1604	      num.bad(st, "invalid exponent")
1605	
1606	# an exponent digit or an underscore
1607	def num.edig.go(digit: Bool, us: Bool, st: Num, +cc: Char) -> Num:
1608	  match digit:
1609	    case True{}:
1610	      num.digit(st, cc, NEDig{})
1611	    case False{}:
1612	      num.edig.us(us, st, cc)
1613	
1614	# an exponent digit or an underscore
1615	def num.edig(st: Num, +cc: Char) -> Num:
1616	  num.edig.go(Char.is_digit(cc), Char.is_eq(cc, '_'), st, cc)
1617	
1618	# one character of a numeral
1619	def num.on(nk: NK, st: Num, +cc: Char) -> Num:
1620	  match nk:
1621	    case NLead{}:
1622	      num.lead(st, cc)
1623	    case NSign{}:
1624	      num.after.sign(st, cc)
1625	    case NZero{}:
1626	      num.zero(st, cc)
1627	    case NDig{}:
1628	      num.digs(st, cc)
1629	    case NBase{}:
1630	      num.based(st, cc)
1631	    case NFrac{}:
1632	      num.frac(st, cc)
1633	    case NExp{}:
1634	      num.expon(st, cc)
1635	    case NEDig{}:
1636	      num.edig(st, cc)
1637	    case NBad{}:
1638	      st
1639	
1640	# one character of a numeral
1641	def num.step.go(st: Num, +cc: Char) -> Num:
1642	  Num{+nk, sign, base, ds, us, saw, why} = st
1643	  num.on(nk, Num{nk, sign, base, ds, us, saw, why}, cc)
1644	
1645	# one character of a numeral
1646	def num.step(st: Num, +cc: Char) -> Num:
1647	  num.step.go(st, cc)
1648	
1649	# the walk over a numeral
1650	def num.go(cs: List<&2, Char>, st: Num) -> Num:
1651	  match cs:
1652	    case []:
1653	      st
1654	    case +h <> t:
1655	      num.go(t, num.step(st, h))
1656	
1657	# the positive limit is 2^63-1; the negative limit is 2^63
1658	def i64.limit(sign: Sign) -> String:
1659	  match sign:
1660	    case Plus{}:
1661	      "9223372036854775807"
1662	    case Minus{}:
1663	      "9223372036854775808"
1664	
1665	# the first differing digit stands; a tie takes the new order
1666	def i64.ord(seen: Cmp, now: Cmp) -> Cmp:
1667	  match seen now:
1668	    case EQ{} n:
1669	      n
1670	    case LT{} _n:
1671	      LT{}
1672	    case GT{} _n:
1673	      GT{}
1674	
1675	# a shorter digit string fits and a longer one does not. equal length uses
1676	# digit order. the walk does not rebuild either string
1677	def i64.step(+digits: String, +limit: String, ord: Cmp) -> Bool:
1678	  match digits limit:
1679	    case SNil{} SNil{}:
1680	      Cmp.is_le(ord)
1681	    case SNil{} SCon{_h, _t}:
1682	      True{}
1683	    case SCon{_h, _t} SNil{}:
1684	      False{}
1685	    case SCon{x, xt} SCon{y, yt}:
1686	      i64.step(xt, yt, i64.ord(ord, U32.cmp(Char.to_u32(x), Char.to_u32(y))))
1687	
1688	# whether the integer fits in a signed 64-bit integer
1689	def i64.fits(+sign: Sign, +digits: String) -> Bool:
1690	  i64.step(digits, i64.limit(sign), EQ{})
1691	
1692	# an integer inside the signed 64-bit range
1693	def num.fin.range(ok: Bool, sign: Sign, digits: String) -> Got:
1694	  match ok:
1695	    case True{}:
1696	      GotVal{VInt{sign, digits}}
1697	    case False{}:
1698	      GotBad{"out of range"}
1699	
1700	# a finished integer, rejected when it falls outside signed 64-bit
1701	def num.fin.int(saw: Bool, +sign: Sign, +digits: String) -> Got:
1702	  match saw:
1703	    case False{}:
1704	      GotBad{"invalid number"}
1705	    case True{}:
1706	      num.fin.range(i64.fits(sign, digits), sign, digits)
1707	
1708	# a numeral needs a digit in its last run
1709	def num.fin.saw(saw: Bool, val: Val) -> Got:
1710	  match saw:
1711	    case False{}:
1712	      GotBad{"invalid number"}
1713	    case True{}:
1714	      GotVal{val}
1715	
1716	# a prefixed integer may not carry a sign
1717	def num.signed(cs: List<&2, Char>) -> Bool:
1718	  match cs:
1719	    case []:
1720	      False{}
1721	    case +c <> _:
1722	      Bool.or(Char.is_eq(c, '+'), Char.is_eq(c, '-'))
1723	
1724	# a prefixed integer, rejected when a sign was written
1725	def num.fin.base(signed: Bool, saw: Bool, sign: Sign, ds: List<&2, U32>) -> Got:
1726	  match signed:
1727	    case True{}:
1728	      GotBad{"invalid number"}
1729	    case False{}:
1730	      num.fin.int(saw, sign, dec.text(ds))
1731	
1732	# the kind of numeral the scan finished in
1733	def num.fin.nk(nk: NK, sign: Sign, ds: List<&2, U32>, saw: Bool, why: String, cs: List<&2, Char>) -> Got:
1734	  match nk:
1735	    case NBad{}:
1736	      GotBad{why}
1737	    case NLead{}:
1738	      GotBad{"invalid number"}
1739	    case NSign{}:
1740	      GotBad{"invalid number"}
1741	    case NZero{}:
1742	      GotVal{VInt{sign, "0"}}
1743	    case NDig{}:
1744	      num.fin.int(saw, sign, dec.text(ds))
1745	    case NBase{}:
1746	      num.fin.base(num.signed(cs), saw, sign, ds)
1747	    case NFrac{}:
1748	      num.fin.saw(saw, VFlo{sign, word.body(cs)})
1749	    case NExp{}:
1750	      GotBad{"invalid exponent"}
1751	    case NEDig{}:
1752	      num.fin.saw(saw, VFlo{sign, word.body(cs)})
1753	
1754	# a trailing underscore is rejected
1755	def num.fin.us(us: Bool, nk: NK, sign: Sign, ds: List<&2, U32>, saw: Bool, why: String, cs: List<&2, Char>) -> Got:
1756	  match us:
1757	    case True{}:
1758	      GotBad{"invalid underscore"}
1759	    case False{}:
1760	      num.fin.nk(nk, sign, ds, saw, why, cs)
1761	
1762	# the value of a finished numeral
1763	def num.fin(st: Num, cs: List<&2, Char>) -> Got:
1764	  Num{nk, sign, _base, ds, us, saw, why} = st
1765	  num.fin.us(us, nk, sign, ds, saw, why, cs)
1766	
1767	# a numeral token
1768	def word.num(+cs: List<&2, Char>) -> Got:
1769	  num.fin(num.go(cs, num.start()), cs)
1770	
1771	# a datetime when the token has a colon or a dash, otherwise a numeral
1772	def word.route.date(date: Bool, cs: List<&2, Char>) -> Got:
1773	  match date:
1774	    case True{}:
1775	      word.from.when(when.read(cs))
1776	    case False{}:
1777	      word.num(cs)
1778	
1779	# a special word, or a numeral
1780	def word.route(gg: Got, date: Bool, +cs: List<&2, Char>) -> Got:
1781	  match gg:
1782	    case GotVal{val}:
1783	      GotVal{val}
1784	    case GotBad{_}:
1785	      word.route.date(word.as_date(date, word.ee(cs)), cs)
1786	
1787	# '-' can start a signed inf or nan
1788	def word.special.minus(+cc: Char) -> Bool:
1789	  Char.is_eq(cc, '-')
1790	
1791	# '+' or '-'
1792	def word.special.plus(hit: Bool, +cc: Char) -> Bool:
1793	  match hit:
1794	    case True{}:
1795	      True{}
1796	    case False{}:
1797	      word.special.minus(cc)
1798	
1799	# 'n', or a sign
1800	def word.special.n(hit: Bool, +cc: Char) -> Bool:
1801	  match hit:
1802	    case True{}:
1803	      True{}
1804	    case False{}:
1805	      word.special.plus(Char.is_eq(cc, '+'), cc)
1806	
1807	# 'i', or nan, or a sign
1808	def word.special.i(hit: Bool, +cc: Char) -> Bool:
1809	  match hit:
1810	    case True{}:
1811	      True{}
1812	    case False{}:
1813	      word.special.n(Char.is_eq(cc, 'n'), cc)
1814	
1815	# 'f', or inf, or nan, or a sign
1816	def word.special.f(hit: Bool, +cc: Char) -> Bool:
1817	  match hit:
1818	    case True{}:
1819	      True{}
1820	    case False{}:
1821	      word.special.i(Char.is_eq(cc, 'i'), cc)
1822	
1823	# 't', or false, or inf, or nan, or a sign
1824	def word.special.t(hit: Bool, +cc: Char) -> Bool:
1825	  match hit:
1826	    case True{}:
1827	      True{}
1828	    case False{}:
1829	      word.special.f(Char.is_eq(cc, 'f'), cc)
1830	
1831	# whether this character can start a special bare word
1832	def word.special(+cc: Char) -> Bool:
1833	  word.special.t(Char.is_eq(cc, 't'), cc)
1834	
1835	# the first character, when the word has one
1836	def word.lead(cs: List<&2, Char>) -> Bool:
1837	  match cs:
1838	    case []:
1839	      False{}
1840	    case +h <> _t:
1841	      word.special(h)
1842	
1843	# a numeral or a datetime. the token cannot be a keyword
1844	def word.val.num(+cs: List<&2, Char>) -> Got:
1845	  word.route(GotBad{""}, word.or(word.colon(cs), word.dash(cs, True{})), cs)
1846	
1847	# a special word, or a numeral. a digit does not build a string to compare
1848	def word.val.pick(special: Bool, +cs: List<&2, Char>) -> Got:
1849	  match special:
1850	    case True{}:
1851	      word.route(word.spec(String.from_list(cs)),
1852	        word.or(word.colon(cs), word.dash(cs, True{})), cs)
1853	    case False{}:
1854	      word.val.num(cs)
1855	
1856	# a bare word: a special, a datetime, or a numeral
1857	def word.val(+cs: List<&2, Char>) -> Got:
1858	  word.val.pick(word.lead(cs), cs)
1859	
1860	# a change applied at the end of a key path
1861	type Job is Data:
1862	  JPut{val: Val}
1863	  JDef{}
1864	  JAot{}
1865	
1866	# one table the walk has entered
1867	type Fr is Data:
1868	  FrNew{name: String, parent: List<&2, Val>, path: String}
1869	  FrRep{name: String, parent: List<&2, Val>, path: String}
1870	  FrAot{name: String, parent: List<&2, Val>, pre: List<&2, Val>, path: String}
1871	
1872	# the walk: the table being edited, and the frames above it
1873	type Tw is Data:
1874	  Tw{vs: List<&2, Val>, job: Job, stack: List<&2, Fr>, bad: String, pre: String,
1875	    heads: List<&2, String>, inl: Bool}
1876	
1877	# the root table after a walk
1878	type End is Data:
1879	  End{vs: List<&2, Val>, bad: String, heads: List<&2, String>}
1880	
1881	# what a key in a table refers to
1882	type Look is Data:
1883	  KMiss{}
1884	  KHead{path: String, rows: List<&2, Val>}
1885	  KInl{}
1886	  KAots{path: String, elems: List<&2, Val>}
1887	  KNo{why: String}
1888	
1889	# the last element of an array of tables
1890	type Last is Data:
1891	  LastSome{path: String, pre: List<&2, Val>, rows: List<&2, Val>}
1892	  LastNo{why: String}
1893	
1894	# the first error is kept
1895	def err.first.go(empty: Bool, bad: String, why: String) -> String:
1896	  match empty:
1897	    case True{}:
1898	      why
1899	    case False{}:
1900	      bad
1901	
1902	# the first error is kept
1903	def err.first(+bad: String, why: String) -> String:
1904	  err.first.go(String.is_empty(bad), bad, why)
1905	
1906	# a key found earlier wins
1907	def find.step(eq: Bool, vv: Val, more: Unit -> Hit) -> Hit:
1908	  match eq:
1909	    case True{}:
1910	      Found{vv}
1911	    case False{}:
1912	      more(Unit{})
1913	
1914	# the first pair of this name
1915	def rows.find(rows: List<&2, Val>, +name: String) -> Hit:
1916	  match rows:
1917	    case []:
1918	      Miss{}
1919	    case VPair{n, v} <> t:
1920	      find.step(str.eq(n, name), v, _u => rows.find(t, name))
1921	    case _ <> t:
1922	      rows.find(t, name)
1923	
1924	# the value written for a key, or Miss
1925	def get(rows: List<&2, Val>, +name: String) -> Hit:
1926	  rows.find(rows, name)
1927	
1928	# replace the value of one pair
1929	def rows.repl.step(eq: Bool, nn: String, old: Val, val: Val, more: Unit -> List<&2, Val>) -> List<&2, Val>:
1930	  match eq:
1931	    case True{}:
1932	      VPair{nn, val} <> more(Unit{})
1933	    case False{}:
1934	      VPair{nn, old} <> more(Unit{})
1935	
1936	# replace every pair of this name
1937	def rows.repl(rows: List<&2, Val>, +name: String, +val: Val) -> List<&2, Val>:
1938	  match rows:
1939	    case []:
1940	      []
1941	    case VPair{+n, old} <> t:
1942	      rows.repl.step(str.eq(n, name), n, old, val, _u => rows.repl(t, name, val))
1943	    case h <> t:
1944	      h <> rows.repl(t, name, val)
1945	
1946	# either flag
1947	def heads.or(aa: Bool, bb: Bool) -> Bool:
1948	  match aa:
1949	    case True{}:
1950	      True{}
1951	    case False{}:
1952	      bb
1953	
1954	# heads records each table the document has defined as its path behind one
1955	# mark: `[` when a header defined it, `.` when dotted keys did
1956	def heads.by.head(path: String) -> String:
1957	  SCon{'[', path}
1958	
1959	# a table dotted keys defined, as heads records it
1960	def heads.by.dot(path: String) -> String:
1961	  SCon{'.', path}
1962	
1963	# whether a table path was defined, by a header or by dotted keys
1964	def heads.has(hs: List<&2, String>, +pp: String) -> Bool:
1965	  match hs:
1966	    case []:
1967	      False{}
1968	    case SCon{_mark, h} <> t:
1969	      heads.or(str.eq(h, pp), heads.has(t, pp))
1970	    case SNil{} <> t:
1971	      heads.has(t, pp)
1972	
1973	# whether a table path was defined by a header
1974	def heads.head(hs: List<&2, String>, +pp: String) -> Bool:
1975	  match hs:
1976	    case []:
1977	      False{}
1978	    case SCon{mark, h} <> t:
1979	      heads.or(Bool.and(Char.is_eq(mark, '['), str.eq(h, pp)), heads.head(t, pp))
1980	    case SNil{} <> t:
1981	      heads.head(t, pp)
1982	
1983	# a recorded table under the prefix is dropped
1984	def heads.drop.step(
1985	  under: Bool,
1986	  mark: Char,
1987	  path: String,
1988	  rest: List<&2, String>
1989	) -> List<&2, String>:
1990	  match under:
1991	    case True{}:
1992	      rest
1993	    case False{}:
1994	      SCon{mark, path} <> rest
1995	
1996	# forget every table whose path starts with the prefix. A new element of an
1997	# array of tables starts with none of the tables the element before defined
1998	def heads.drop(hs: List<&2, String>, +pre: String) -> List<&2, String>:
1999	  match hs:
2000	    case []:
Lines 1-2000 of 6370. More: https://jend.leeeet.dev/read.txt?path=emerging-eztoml@0.8.0.0/main.bend&start_line=2001