main.bend

emerging-eztoml@0.9.0.0 · 6,369 lines · 704 definitions

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
10import Base
11
12# the sign of an integer, a float, or a zone offset
13type Sign is Data:
14  Plus{}
15  Minus{}
16
17# a calendar date: year, month, day
18type 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
22type Clock is Data:
23  Clock{h: U32, mi: U32, s: U32, frac: String}
24
25# a zone offset: Z, or a numeric offset
26type Zone is Data:
27  Zulu{}
28  Shift{sign: Sign, h: U32, mi: U32}
29
30# the four TOML datetime forms
31type 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.
41type 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
56type Hit is Data:
57  Found{val: Val}
58  Miss{}
59
60# a parsed document: the first error, and the root table in order
61type 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
65type Got is Data:
66  GotVal{val: Val}
67  GotBad{why: String}
68
69# digits taken from the front of a character list
70type Dig is Data:
71  DigOk{n: U32, cs: List<&2, Char>}
72  DigBad{}
73
74# what a datetime scan produced
75type WhenOut is Data:
76  WSome{when: When}
77  WFail{why: String}
78  WSkip{}
79
80# a decimal numeral being built, least-significant digit first
81type 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
93type 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
98type BK is Data:
99  BKCh{}
100  BKHex{}
101  BKEsc{mark: Char}
102
103# where the scanner is in a document
104type 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
142type QKind is Data:
143  QBasic{}
144  QLit{}
145  QMulti{}
146  QMultiLit{}
147
148# one character to read again
149type Hold is Data:
150  HNone{}
151  HChar{c: Char}
152
153# an open array or inline table
154type 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
159type 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
166type 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
173def 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
178def 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
186def 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
194def 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
198def 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
206def 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
210def 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
216def 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
220def basic.cls.hex(hit: Bool) -> BK:
221  match hit:
222    case True{}:
223      BKHex{}
224    case False{}:
225      BKCh{}
226
227# backslash
228def 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
236def 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
244def 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
252def 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
260def 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
268def 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
276def 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
284def 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
288def 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
298def 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
303def 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# the buffer is reversed, so each head goes on the front of the text
311def buf.str.go(buf: List<&2, Char>, acc: String) -> String:
312  match buf:
313    case []:
314      acc
315    case +h <> t:
316      buf.str.go(t, SCon{h, acc})
317
318# the buffer, in order
319def buf.str(buf: List<&2, Char>) -> String:
320  buf.str.go(buf, "")
321
322# a basic string: quotes, with controls and quotes escaped
323def key.basic(+ss: String) -> String:
324  "\"" ++ buf.str(basic.go(String.to_list(ss), [])) ++ "\""
325
326# bare when the name allows it, otherwise a basic string
327def key.go(ok: Bool, +ss: String) -> String:
328  match ok:
329    case True{}:
330      ss
331    case False{}:
332      key.basic(ss)
333
334# a key as TOML writes it
335def key(+ss: String) -> String:
336  key.go(bare(ss), ss)
337
338# the overflow of a decimal step, least-significant digit first
339def dec.carry.c0(zz: Bool, cc: U32) -> List<&2, U32>:
340  match zz:
341    case True{}:
342      []
343    case False{}:
344      [U32.mod(cc, 10)]
345
346# the overflow of a decimal step
347def dec.carry.c(+cc: U32) -> List<&2, U32>:
348  dec.carry.c0(U32.is_zero(cc), cc)
349
350# the next digit of an overflow
351def dec.carry.b0(zz: Bool, +cc: U32) -> List<&2, U32>:
352  match zz:
353    case True{}:
354      []
355    case False{}:
356      U32.mod(cc, 10) <> dec.carry.c(U32.div(cc, 10))
357
358# the next digit of an overflow
359def dec.carry.b(+cc: U32) -> List<&2, U32>:
360  dec.carry.b0(U32.is_zero(cc), cc)
361
362# the first digit of an overflow
363def dec.carry.a(zz: Bool, +cc: U32) -> List<&2, U32>:
364  match zz:
365    case True{}:
366      []
367    case False{}:
368      U32.mod(cc, 10) <> dec.carry.b(U32.div(cc, 10))
369
370# the digits of a leftover carry
371def dec.carry(+cc: U32) -> List<&2, U32>:
372  dec.carry.a(U32.is_zero(cc), cc)
373
374# multiply a decimal numeral by a radix and add a digit
375def dec.go(ds: List<&2, U32>, +radix: U32, +carry: U32) -> List<&2, U32>:
376  match ds:
377    case []:
378      dec.carry(carry)
379    case +d <> t:
380      U32.mod(U32.add(U32.mul(d, radix), carry), 10) <> dec.go(t, radix,
381        U32.div(U32.add(U32.mul(d, radix), carry), 10))
382
383# a digit character
384def dec.ch(dd: U32) -> Char:
385  Chr{U32.add(48, dd)}
386
387# digits as characters, in the order given
388def dec.chars(ds: List<&2, U32>) -> List<&2, Char>:
389  match ds:
390    case []:
391      []
392    case d <> t:
393      dec.ch(d) <> dec.chars(t)
394
395# whether a leading zero is still being skipped
396def dec.drop.lead(lead: Bool, +hh: Char) -> Bool:
397  match lead:
398    case False{}:
399      False{}
400    case True{}:
401      Char.is_eq(hh, '0')
402
403# a leading zero is skipped; any other character is kept
404def dec.drop.outz(zz: Bool, hh: Char, out: List<&2, Char>) -> List<&2, Char>:
405  match zz:
406    case True{}:
407      out
408    case False{}:
409      hh <> out
410
411# the output after one character, reversed
412def dec.drop.out(lead: Bool, +hh: Char, out: List<&2, Char>) -> List<&2, Char>:
413  match lead:
414    case False{}:
415      hh <> out
416    case True{}:
417      dec.drop.outz(Char.is_eq(hh, '0'), hh, out)
418
419# the numeral, or 0 when every digit was zero
420def dec.drop.end(lead: Bool, out: List<&2, Char>) -> String:
421  match lead:
422    case True{}:
423      "0"
424    case False{}:
425      buf.str(out)
426
427# drop leading zeros from a most-significant-first digit list
428def dec.drop(cs: List<&2, Char>, +lead: Bool, out: List<&2, Char>) -> String:
429  match cs:
430    case []:
431      dec.drop.end(lead, out)
432    case +h <> t:
433      dec.drop(t, dec.drop.lead(lead, h), dec.drop.out(lead, h, out))
434
435# a decimal numeral. The digit list is least-significant first
436def dec.text(ds: List<&2, U32>) -> String:
437  dec.drop(dec.chars(List.reverse(&2, U32, ds)), True{}, [])
438
439# a code point's digit value, or 99 when the character is not a digit
440def dig.up(ok: Bool, uu: U32) -> U32:
441  match ok:
442    case True{}:
443      U32.sub(uu, 55)
444    case False{}:
445      99
446
447# a lowercase hex digit, otherwise an uppercase one
448def dig.low(ok: Bool, +uu: U32) -> U32:
449  match ok:
450    case True{}:
451      U32.sub(uu, 87)
452    case False{}:
453      dig.up(Bool.and(U32.is_ge(uu, 65), U32.is_le(uu, 70)), uu)
454
455# a decimal digit, otherwise a hex letter
456def dig.dec(ok: Bool, +uu: U32) -> U32:
457  match ok:
458    case True{}:
459      U32.sub(uu, 48)
460    case False{}:
461      dig.low(Bool.and(U32.is_ge(uu, 97), U32.is_le(uu, 102)), uu)
462
463# the value of a digit character, or 99
464def dig.val(+cc: Char) -> U32:
465  +u = Char.to_u32(cc)
466  dig.dec(Bool.and(U32.is_ge(u, 48), U32.is_le(u, 57)), u)
467
468# whether a digit value fits a base
469def dig.ok(dd: U32, base: U32) -> Bool:
470  U32.is_lt(dd, base)
471
472# exactly k digits, or DigBad
473def take.acc.d(digit: Bool, nn: U32, +cc: Char) -> U32:
474  match digit:
475    case False{}:
476      nn
477    case True{}:
478      U32.add(U32.mul(nn, 10), U32.sub(Char.to_u32(cc), 48))
479
480# the accumulator after one character
481def take.acc(ok: Bool, nn: U32, +cc: Char) -> U32:
482  match ok:
483    case False{}:
484      nn
485    case True{}:
486      take.acc.d(Char.is_digit(cc), nn, cc)
487
488# the scan stays well only while every character is a digit
489def take.ok(ok: Bool, +cc: Char) -> Bool:
490  match ok:
491    case False{}:
492      False{}
493    case True{}:
494      Char.is_digit(cc)
495
496# the finished take
497def take.fin(ok: Bool, nn: U32, cs: List<&2, Char>) -> Dig:
498  match ok:
499    case True{}:
500      DigOk{nn, cs}
501    case False{}:
502      DigBad{}
503
504# exactly k digits from the front of a list
505def take.n(kk: Nat, cs: List<&2, Char>, nn: U32, +ok: Bool) -> Dig:
506  match kk:
507    case 0n:
508      take.fin(ok, nn, cs)
509    case 1n+p:
510      match cs:
511        case []:
512          DigBad{}
513        case +h <> t:
514          take.n(p, t, take.acc(ok, nn, h), take.ok(ok, h))
515
516# a number is inside the inclusive bounds
517def bound.rng(+nn: U32, lo: U32, hi: U32) -> Bool:
518  Bool.and(U32.is_ge(nn, lo), U32.is_le(nn, hi))
519
520# two digits, zero padded
521def pad2.go(small: Bool, nn: U32) -> String:
522  match small:
523    case True{}:
524      "0" ++ U32.show(nn)
525    case False{}:
526      U32.show(nn)
527
528# two digits, zero padded
529def text.pad2(+nn: U32) -> String:
530  pad2.go(U32.is_lt(nn, 10), nn)
531
532# the one-zero pad, or the digits themselves
533def pad4.big(nn: U32, big: Bool) -> String:
534  match big:
535    case True{}:
536      "0" ++ U32.show(nn)
537    case False{}:
538      U32.show(nn)
539
540# the three-digit and two-digit pads
541def pad4.mid(nn: U32, mid: Bool, big: Bool) -> String:
542  match mid:
543    case True{}:
544      "00" ++ U32.show(nn)
545    case False{}:
546      pad4.big(nn, big)
547
548# four digits, zero padded
549def pad4.go(nn: U32, small: Bool, mid: Bool, big: Bool) -> String:
550  match small:
551    case True{}:
552      "000" ++ U32.show(nn)
553    case False{}:
554      pad4.mid(nn, mid, big)
555
556# four digits, zero padded
557def text.pad4(+nn: U32) -> String:
558  pad4.go(nn, U32.is_lt(nn, 10), U32.is_lt(nn, 100), U32.is_lt(nn, 1000))
559
560# the sign of a zone offset
561def zone.mark(sign: Sign) -> String:
562  match sign:
563    case Plus{}:
564      "+"
565    case Minus{}:
566      "-"
567
568# a numeric zone offset
569def zone.shift(sign: Sign, hh: U32, mi: U32) -> String:
570  zone.mark(sign) ++ text.pad2(hh) ++ ":" ++ text.pad2(mi)
571
572# a zone suffix
573def zone.text(zz: Zone) -> String:
574  match zz:
575    case Zulu{}:
576      "Z"
577    case Shift{sign, h, mi}:
578      zone.shift(sign, h, mi)
579
580# the fractional second, or nothing
581def clock.frac.go(empty: Bool, frac: String) -> String:
582  match empty:
583    case True{}:
584      ""
585    case False{}:
586      "." ++ frac
587
588# the fractional second, or nothing
589def clock.frac(+frac: String) -> String:
590  clock.frac.go(String.is_empty(frac), frac)
591
592# a clock, with a fractional second when it has one
593def clock.text(cc: Clock) -> String:
594  Clock{h, mi, s, frac} = cc
595  text.pad2(h) ++ ":" ++ text.pad2(mi) ++ ":" ++ text.pad2(s) ++ clock.frac(frac)
596
597# a date
598def date.text(dd: Date) -> String:
599  Date{y, mo, day} = dd
600  text.pad4(y) ++ "-" ++ text.pad2(mo) ++ "-" ++ text.pad2(day)
601
602# a datetime in TOML spelling
603def when.text(ww: When) -> String:
604  match ww:
605    case WOff{date, clock, zone}:
606      date.text(date) ++ "T" ++ clock.text(clock) ++ zone.text(zone)
607    case WLocal{date, clock}:
608      date.text(date) ++ "T" ++ clock.text(clock)
609    case WDate{date}:
610      date.text(date)
611    case WTime{clock}:
612      clock.text(clock)
613
614# the sign of an integer or a float, empty when it is positive
615def sign.text(sign: Sign) -> String:
616  match sign:
617    case Plus{}:
618      ""
619    case Minus{}:
620      "-"
621
622# whether the list still has a character
623def cs.some(cs: List<&2, Char>) -> Bool:
624  match cs:
625    case []:
626      False{}
627    case _ <> _:
628      True{}
629
630# one character, when the list has one
631def cs.head(cs: List<&2, Char>) -> Char:
632  match cs:
633    case []:
634      ' '
635    case h <> _:
636      h
637
638# the tail of a list
639def cs.tail(cs: List<&2, Char>) -> List<&2, Char>:
640  match cs:
641    case []:
642      []
643    case _ <> t:
644      t
645
646# a clock with its fraction filled in
647def clock.with(cc: Clock, frac: String) -> Clock:
648  Clock{h, mi, s, _f} = cc
649  Clock{h, mi, s, frac}
650
651# a finished local datetime, or one with a zone still to read
652def when.done(_date: Date, _clock: Clock, ww: When) -> WhenOut:
653  WSome{ww}
654
655# Z ends the token
656def when.zone.z(tt: List<&2, Char>, clock: Clock, date: Date) -> WhenOut:
657  match tt:
658    case []:
659      WSome{WOff{date, clock, Zulu{}}}
660    case _ <> _:
661      WFail{"invalid zone"}
662
663# the offset minute is in range
664def when.zone.mm.ok2(mi_ok: Bool, sign: Sign, hh: U32, mi: U32, clock: Clock, date: Date) -> WhenOut:
665  match mi_ok:
666    case False{}:
667      WFail{"zone minute is out of range"}
668    case True{}:
669      WSome{WOff{date, clock, Shift{sign, hh, mi}}}
670
671# the offset fields are in range
672def when.zone.mm.ok(h_ok: Bool, mi_ok: Bool, sign: Sign, hh: U32, mi: U32, clock: Clock, date: Date) -> WhenOut:
673  match h_ok:
674    case False{}:
675      WFail{"zone hour is out of range"}
676    case True{}:
677      when.zone.mm.ok2(mi_ok, sign, hh, mi, clock, date)
678
679# nothing follows an offset, and its fields are in range
680def when.zone.mm.end(
681  cs: List<&2, Char>,
682  h_ok: Bool,
683  mi_ok: Bool,
684  sign: Sign,
685  hh: U32,
686  mi: U32,
687  clock: Clock,
688  date: Date
689) -> WhenOut:
690  match cs:
691    case []:
692      when.zone.mm.ok(h_ok, mi_ok, sign, hh, mi, clock, date)
693    case _ <> _:
694      WFail{"invalid zone"}
695
696# the offset minute is in range
697def when.zone.mm.go(dd: Dig, sign: Sign, +hh: U32, clock: Clock, date: Date) -> WhenOut:
698  match dd:
699    case DigBad{}:
700      WFail{"invalid zone"}
701    case DigOk{+n, cs}:
702      when.zone.mm.end(cs, bound.rng(hh, 0, 23), bound.rng(n, 0, 59), sign, hh, n, clock, date)
703
704# the offset minute
705def when.zone.mm(hit: Bool, dd: Dig, sign: Sign, hh: U32, clock: Clock, date: Date) -> WhenOut:
706  match hit:
707    case False{}:
708      WFail{"invalid zone"}
709    case True{}:
710      when.zone.mm.go(dd, sign, hh, clock, date)
711
712# the colon in an offset
713def when.zone.hh.colon(cs: List<&2, Char>, sign: Sign, hh: U32, clock: Clock, date: Date) -> WhenOut:
714  match cs:
715    case []:
716      WFail{"invalid zone"}
717    case +c <> t:
718      when.zone.mm(Char.is_eq(c, ':'), take.n(2n, t, 0, True{}), sign, hh, clock, date)
719
720# the offset hour
721def when.zone.hh(dd: Dig, sign: Sign, clock: Clock, date: Date) -> WhenOut:
722  match dd:
723    case DigBad{}:
724      WFail{"invalid zone"}
725    case DigOk{n, cs}:
726      when.zone.hh.colon(cs, sign, n, clock, date)
727
728# HH:MM of a numeric offset
729def when.zone.off(sign: Sign, tt: List<&2, Char>, clock: Clock, date: Date) -> WhenOut:
730  when.zone.hh(take.n(2n, tt, 0, True{}), sign, clock, date)
731
732# a minus starts a numeric offset
733def when.zone.minus(minus: Bool, tt: List<&2, Char>, clock: Clock, date: Date) -> WhenOut:
734  match minus:
735    case True{}:
736      when.zone.off(Minus{}, tt, clock, date)
737    case False{}:
738      WFail{"invalid zone"}
739
740# a plus or a minus starts a numeric offset
741def when.zone.sign(plus: Bool, minus: Bool, tt: List<&2, Char>, clock: Clock, date: Date) -> WhenOut:
742  match plus:
743    case True{}:
744      when.zone.off(Plus{}, tt, clock, date)
745    case False{}:
746      when.zone.minus(minus, tt, clock, date)
747
748# Z, or a signed numeric offset
749def when.zone.go(zee: Bool, plus: Bool, minus: Bool, tt: List<&2, Char>, clock: Clock, date: Date) -> WhenOut:
750  match zee:
751    case True{}:
752      when.zone.z(tt, clock, date)
753    case False{}:
754      when.zone.sign(plus, minus, tt, clock, date)
755
756# a zone, or the end of a local datetime
757def when.zone(cs: List<&2, Char>, clock: Clock, date: Date) -> WhenOut:
758  match cs:
759    case []:
760      WSome{WLocal{date, clock}}
761    case +c <> t:
762      when.zone.go(Bool.or(Char.is_eq(c, 'Z'), Char.is_eq(c, 'z')),
763        Char.is_eq(c, '+'), Char.is_eq(c, '-'), t, clock, date)
764
765# the fraction must hold a digit
766def when.frac.end.go(some: Bool, rev: List<&2, Char>, clock: Clock, date: Date, rest: List<&2, Char>) -> WhenOut:
767  match some:
768    case False{}:
769      WFail{"invalid fraction"}
770    case True{}:
771      when.zone(rest, clock.with(clock, buf.str(rev)),
772        date)
773
774# the fraction must hold a digit
775def when.frac.end(+rev: List<&2, Char>, clock: Clock, date: Date, rest: List<&2, Char>) -> WhenOut:
776  when.frac.end.go(cs.some(rev), rev, clock, date, rest)
777
778# one fractional digit, or the end of the fraction
779def when.frac.digit(
780  digit: Bool,
781  +cc: Char,
782  tt: List<&2, Char>,
783  rev: List<&2, Char>,
784  clock: Clock,
785  date: Date,
786  more: Unit -> WhenOut
787) -> WhenOut:
788  match digit:
789    case True{}:
790      more(Unit{})
791    case False{}:
792      when.frac.end(rev, clock, date, cc <> tt)
793
794# fractional digits
795def when.frac.digits(cs: List<&2, Char>, +rev: List<&2, Char>, +clock: Clock, +date: Date) -> WhenOut:
796  match cs:
797    case []:
798      when.frac.end(rev, clock, date, [])
799    case +c <> +t:
800      when.frac.digit(Char.is_digit(c), c, t, rev, clock, date,
801        _u => when.frac.digits(t, c <> rev, clock, date))
802
803# a dot starts a fraction; anything else is a zone
804def when.frac.go(dot: Bool, tt: List<&2, Char>, clock: Clock, date: Date, +cc: Char) -> WhenOut:
805  match dot:
806    case True{}:
807      when.frac.digits(tt, [], clock, date)
808    case False{}:
809      when.zone(cc <> tt, clock, date)
810
811# an optional fractional second
812def when.frac(cs: List<&2, Char>, +clock: Clock, +date: Date) -> WhenOut:
813  match cs:
814    case []:
815      when.done(date, clock, WLocal{date, clock})
816    case +c <> t:
817      when.frac.go(Char.is_eq(c, '.'), t, clock, date, c)
818
819# the second is in range, then the fraction and the zone
820def when.clock.range.s(s_ok: Bool, hh: U32, mi: U32, ss: U32, cs: List<&2, Char>, date: Date) -> WhenOut:
821  match s_ok:
822    case False{}:
823      WFail{"second is out of range"}
824    case True{}:
825      when.frac(cs, Clock{hh, mi, ss, ""}, date)
826
827# minute and second are in range
828def when.clock.range.m(mi_ok: Bool, s_ok: Bool, hh: U32, mi: U32, ss: U32, cs: List<&2, Char>, date: Date) -> WhenOut:
829  match mi_ok:
830    case False{}:
831      WFail{"minute is out of range"}
832    case True{}:
833      when.clock.range.s(s_ok, hh, mi, ss, cs, date)
834
835# hour, minute, and second are in range
836def when.clock.range(
837  h_ok: Bool,
838  mi_ok: Bool,
839  s_ok: Bool,
840  hh: U32,
841  mi: U32,
842  ss: U32,
843  cs: List<&2, Char>,
844  date: Date
845) -> WhenOut:
846  match h_ok:
847    case False{}:
848      WFail{"hour is out of range"}
849    case True{}:
850      when.clock.range.m(mi_ok, s_ok, hh, mi, ss, cs, date)
851
852# seconds, then an optional fraction and zone
853def when.clock.ss.go(dd: Dig, +hh: U32, +mi: U32, date: Date) -> WhenOut:
854  match dd:
855    case DigBad{}:
856      WFail{"invalid time"}
857    case DigOk{+n, cs}:
858      when.clock.range(bound.rng(hh, 0, 23), bound.rng(mi, 0, 59), bound.rng(n, 0, 60), hh, mi, n,
859        cs, date)
860
861# seconds after the colon
862def when.clock.ss(hit: Bool, dd: Dig, hh: U32, mi: U32, date: Date) -> WhenOut:
863  match hit:
864    case False{}:
865      WFail{"invalid time"}
866    case True{}:
867      when.clock.ss.go(dd, hh, mi, date)
868
869# the colon after the minutes
870def when.clock.mm.colon(cs: List<&2, Char>, hh: U32, mi: U32, date: Date) -> WhenOut:
871  match cs:
872    case []:
873      WFail{"invalid time"}
874    case +c <> t:
875      when.clock.ss(Char.is_eq(c, ':'), take.n(2n, t, 0, True{}), hh, mi, date)
876
877# minutes, then seconds
878def when.clock.mm(dd: Dig, hh: U32, date: Date) -> WhenOut:
879  match dd:
880    case DigBad{}:
881      WFail{"invalid time"}
882    case DigOk{n, cs}:
883      when.clock.mm.colon(cs, hh, n, date)
884
885# the colon after the hour
886def when.clock.colon.go(hit: Bool, hh: U32, tt: List<&2, Char>, date: Date) -> WhenOut:
887  match hit:
888    case False{}:
889      WFail{"invalid time"}
890    case True{}:
891      when.clock.mm(take.n(2n, tt, 0, True{}), hh, date)
892
893# the colon after the hour
894def when.clock.colon(cs: List<&2, Char>, hh: U32, date: Date) -> WhenOut:
895  match cs:
896    case []:
897      WFail{"invalid time"}
898    case +c <> t:
899      when.clock.colon.go(Char.is_eq(c, ':'), hh, t, date)
900
901# a clock following a date
902def when.clock.of(dd: Dig, date: Date) -> WhenOut:
903  match dd:
904    case DigBad{}:
905      WFail{"invalid time"}
906    case DigOk{n, cs}:
907      when.clock.colon(cs, n, date)
908
909# a space separates a date from a time
910def when.after.sp(sp: Bool, date: Date, tt: List<&2, Char>) -> WhenOut:
911  match sp:
912    case True{}:
913      when.clock.of(take.n(2n, tt, 0, True{}), date)
914    case False{}:
915      WFail{"invalid datetime"}
916
917# T or a space separates a date from a time
918def when.after.sep(tee: Bool, sp: Bool, date: Date, tt: List<&2, Char>) -> WhenOut:
919  match tee:
920    case True{}:
921      when.clock.of(take.n(2n, tt, 0, True{}), date)
922    case False{}:
923      when.after.sp(sp, date, tt)
924
925# the character after a date: nothing, T, or a space, and then a time
926def when.after.date(date: Date, cs: List<&2, Char>) -> WhenOut:
927  match cs:
928    case []:
929      WSome{WDate{date}}
930    case +c <> t:
931      when.after.sep(Bool.or(Char.is_eq(c, 'T'), Char.is_eq(c, 't')),
932        Char.is_eq(c, ' '), date, t)
933
934# the day is in range, then the rest of the token is a time or nothing
935def when.date.ok.d(d_ok: Bool, yy: U32, mo: U32, dd: U32, cs: List<&2, Char>) -> WhenOut:
936  match d_ok:
937    case False{}:
938      WFail{"day is out of range"}
939    case True{}:
940      when.after.date(Date{yy, mo, dd}, cs)
941
942# a date whose fields are in range
943def when.date.ok.go(mo_ok: Bool, d_ok: Bool, yy: U32, mo: U32, dd: U32, cs: List<&2, Char>) -> WhenOut:
944  match mo_ok:
945    case False{}:
946      WFail{"month is out of range"}
947    case True{}:
948      when.date.ok.d(d_ok, yy, mo, dd, cs)
949
950# February in a year divisible by 4 and by 100: 29 days only when the year
951# is also divisible by 400
952def when.feb.quad(four_hundred: Bool) -> U32:
953  match four_hundred:
954    case True{}:
955      29
956    case False{}:
957      28
958
959# February in a year divisible by 4: 29 days unless the year is a century
960def when.feb.cent(hundred: Bool, four_hundred: Bool) -> U32:
961  match hundred:
962    case False{}:
963      29
964    case True{}:
965      when.feb.quad(four_hundred)
966
967# February: 29 days in a leap year and 28 otherwise. A leap year is divisible
968# by 4, except by 100 unless also by 400 (RFC 3339, Appendix C)
969def when.feb.go(four: Bool, hundred: Bool, four_hundred: Bool) -> U32:
970  match four:
971    case False{}:
972      28
973    case True{}:
974      when.feb.cent(hundred, four_hundred)
975
976# the days of February in a year
977def when.feb(+yy: U32) -> U32:
978  when.feb.go(U32.is_eq(U32.mod(yy, 4), 0), U32.is_eq(U32.mod(yy, 100), 0),
979    U32.is_eq(U32.mod(yy, 400), 0))
980
981# April, June, September and November have 30 days
982def when.short(+mo: U32) -> Bool:
983  Bool.or(Bool.or(U32.is_eq(mo, 4), U32.is_eq(mo, 6)),
984    Bool.or(U32.is_eq(mo, 9), U32.is_eq(mo, 11)))
985
986# 30 days in a short month and 31 in the others
987def when.days.short(short: Bool) -> U32:
988  match short:
989    case True{}:
990      30
991    case False{}:
992      31
993
994# the days of a month, by whether it is February or a short month
995def when.days.go(feb: Bool, short: Bool, +yy: U32) -> U32:
996  match feb:
997    case True{}:
998      when.feb(yy)
999    case False{}:
1000      when.days.short(short)
1001
1002# the days of month mo in year yy
1003def when.days(+yy: U32, +mo: U32) -> U32:
1004  when.days.go(U32.is_eq(mo, 2), when.short(mo), yy)
1005
1006# a date whose fields are in range: the day within its month in that year
1007def when.date.ok(+yy: U32, +mo: U32, +dd: U32, cs: List<&2, Char>) -> WhenOut:
1008  when.date.ok.go(bound.rng(mo, 1, 12), bound.rng(dd, 1, when.days(yy, mo)), yy, mo, dd, cs)
1009
1010# a local time: HH:MM:SS, with the hour already taken
1011def when.time.rest(tt: List<&2, Char>, hh: U32) -> WhenOut:
1012  when.clock.mm(take.n(2n, tt, 0, True{}), hh, Date{0, 1, 1})
1013
1014# a local time uses a dummy date and then keeps only the clock
1015def when.time.only(ww: WhenOut) -> WhenOut:
1016  match ww:
1017    case WSome{WLocal{_date, clock}}:
1018      WSome{WTime{clock}}
1019    case WSome{WOff{_date, clock, zone}}:
1020      WFail{"invalid time"}
1021    case WSome{other}:
1022      WFail{"invalid time"}
1023    case WFail{why}:
1024      WFail{why}
1025    case WSkip{}:
1026      WFail{"invalid time"}
1027
1028# a complete date, then whatever follows it
1029def when.day.end(dd: Dig, yy: U32, mo: U32) -> WhenOut:
1030  match dd:
1031    case DigBad{}:
1032      WFail{"invalid date"}
1033    case DigOk{n, cs}:
1034      when.date.ok(yy, mo, n, cs)
1035
1036# the day is two digits
1037def when.day.go(hit: Bool, dd: Dig, yy: U32, mo: U32) -> WhenOut:
1038  match hit:
1039    case False{}:
1040      WFail{"invalid date"}
1041    case True{}:
1042      when.day.end(dd, yy, mo)
1043
1044# the day
1045def when.day(cs: List<&2, Char>, yy: U32, mo: U32) -> WhenOut:
1046  match cs:
1047    case []:
1048      WFail{"invalid date"}
1049    case +c <> t:
1050      when.day.go(Char.is_eq(c, '-'), take.n(2n, t, 0, True{}), yy, mo)
1051
1052# the dash after the month
1053def when.month.go(dd: Dig, yy: U32) -> WhenOut:
1054  match dd:
1055    case DigBad{}:
1056      WFail{"invalid date"}
1057    case DigOk{n, cs}:
1058      when.day(cs, yy, n)
1059
1060# the month
1061def when.month(hit: Bool, dd: Dig, yy: U32) -> WhenOut:
1062  match hit:
1063    case False{}:
1064      WFail{"invalid date"}
1065    case True{}:
1066      when.month.go(dd, yy)
1067
1068# the dash after the year
1069def when.year.dash(cs: List<&2, Char>, yy: U32) -> WhenOut:
1070  match cs:
1071    case []:
1072      WFail{"invalid date"}
1073    case +c <> t:
1074      when.month(Char.is_eq(c, '-'), take.n(2n, t, 0, True{}), yy)
1075
1076# the fourth year digit, then the month
1077def when.year4(dd: Dig) -> WhenOut:
1078  match dd:
1079    case DigBad{}:
1080      WFail{"invalid date"}
1081    case DigOk{n, cs}:
1082      when.year.dash(cs, n)
1083
1084# two more year digits, then a dash
1085def when.year.more(digit: Bool, nn: U32, +cc: Char, tt: List<&2, Char>) -> WhenOut:
1086  match digit:
1087    case False{}:
1088      WFail{"invalid datetime"}
1089    case True{}:
1090      when.year4(take.n(1n, tt, U32.add(U32.mul(nn, 10), dig.val(cc)), True{}))
1091
1092# a colon means a local time; another digit continues a year
1093def when.branch(colon: Bool, digit: Bool, nn: U32, +cc: Char, tt: List<&2, Char>) -> WhenOut:
1094  match colon:
1095    case True{}:
1096      when.time.only(when.time.rest(tt, nn))
1097    case False{}:
1098      when.year.more(digit, nn, cc, tt)
1099
1100# two digits decide a time or a date
1101def when.after2.go(cs: List<&2, Char>, nn: U32) -> WhenOut:
1102  match cs:
1103    case []:
1104      WFail{"invalid datetime"}
1105    case +c <> t:
1106      when.branch(Char.is_eq(c, ':'), Char.is_digit(c), nn, c, t)
1107
1108# two digits decide a time (HH:) or a date (YYYY-)
1109def when.after2(dd: Dig) -> WhenOut:
1110  match dd:
1111    case DigBad{}:
1112      WFail{"invalid datetime"}
1113    case DigOk{n, cs}:
1114      when.after2.go(cs, n)
1115
1116# a datetime token
1117def when.read(cs: List<&2, Char>) -> WhenOut:
1118  when.after2(take.n(2n, cs, 0, True{}))
1119
1120# a dash after the first character
1121def word.dash.hit(first: Bool, +cc: Char) -> Bool:
1122  match first:
1123    case True{}:
1124      False{}
1125    case False{}:
1126      Char.is_eq(cc, '-')
1127
1128# either flag
1129def word.or(aa: Bool, bb: Bool) -> Bool:
1130  match aa:
1131    case True{}:
1132      True{}
1133    case False{}:
1134      bb
1135
1136# a colon anywhere in the token
1137def word.colon(cs: List<&2, Char>) -> Bool:
1138  match cs:
1139    case []:
1140      False{}
1141    case +c <> t:
1142      word.or(Char.is_eq(c, ':'), word.colon(t))
1143
1144# e or E: an exponent, so the token is a numeral rather than a datetime
1145def word.ee.hit(+cc: Char) -> Bool:
1146  Bool.or(Char.is_eq(cc, 'e'), Char.is_eq(cc, 'E'))
1147
1148# whether the token holds an exponent marker
1149def word.ee(cs: List<&2, Char>) -> Bool:
1150  match cs:
1151    case []:
1152      False{}
1153    case +c <> t:
1154      word.or(word.ee.hit(c), word.ee(t))
1155
1156# a datetime scan only when the token is not an exponent numeral
1157def word.as_date(date: Bool, exp: Bool) -> Bool:
1158  match exp:
1159    case True{}:
1160      False{}
1161    case False{}:
1162      date
1163
1164# a dash after the first character
1165def word.dash(cs: List<&2, Char>, first: Bool) -> Bool:
1166  match cs:
1167    case []:
1168      False{}
1169    case +c <> t:
1170      word.or(word.dash.hit(first, c), word.dash(t, False{}))
1171
1172# a negative nan, or not a special
1173def word.spec.nan3(cc: Bool) -> Got:
1174  match cc:
1175    case True{}:
1176      GotVal{VFlo{Minus{}, "nan"}}
1177    case False{}:
1178      GotBad{""}
1179
1180# a signed nan
1181def word.spec.nan2(bb: Bool, cc: Bool) -> Got:
1182  match bb:
1183    case True{}:
1184      GotVal{VFlo{Plus{}, "nan"}}
1185    case False{}:
1186      word.spec.nan3(cc)
1187
1188# nan
1189def word.spec.nan(aa: Bool, bb: Bool, cc: Bool) -> Got:
1190  match aa:
1191    case True{}:
1192      GotVal{VFlo{Plus{}, "nan"}}
1193    case False{}:
1194      word.spec.nan2(bb, cc)
1195
1196# character-for-character equality. a mismatch drops the rest and stops
1197def str.eq.step(aa: String, bb: String, same: Bool) -> Bool:
1198  match aa bb same:
1199    case SNil{} SNil{} True{}:
1200      True{}
1201    case SCon{x, xt} SCon{y, yt} True{}:
1202      str.eq.step(xt, yt, Char.is_eq(x, y))
1203    case _a _b _s:
1204      False{}
1205
1206# the search only needs the bool, not a rebuilt copy of either string
1207def str.eq(aa: String, bb: String) -> Bool:
1208  str.eq.step(aa, bb, True{})
1209
1210# a negative inf, or nan
1211def word.spec.inf3(cc: Bool, +ss: String) -> Got:
1212  match cc:
1213    case True{}:
1214      GotVal{VFlo{Minus{}, "inf"}}
1215    case False{}:
1216      word.spec.nan(str.eq(ss, "nan"), str.eq(ss, "+nan"), str.eq(ss, "-nan"))
1217
1218# a signed inf, or nan
1219def word.spec.inf2(bb: Bool, cc: Bool, +ss: String) -> Got:
1220  match bb:
1221    case True{}:
1222      GotVal{VFlo{Plus{}, "inf"}}
1223    case False{}:
1224      word.spec.inf3(cc, ss)
1225
1226# inf, or nan
1227def word.spec.inf(aa: Bool, bb: Bool, cc: Bool, +ss: String) -> Got:
1228  match aa:
1229    case True{}:
1230      GotVal{VFlo{Plus{}, "inf"}}
1231    case False{}:
1232      word.spec.inf2(bb, cc, ss)
1233
1234# false, or the rest of the specials
1235def word.spec.f(hit: Bool, +ss: String) -> Got:
1236  match hit:
1237    case True{}:
1238      GotVal{VBool{False{}}}
1239    case False{}:
1240      word.spec.inf(str.eq(ss, "inf"), str.eq(ss, "+inf"), str.eq(ss, "-inf"), ss)
1241
1242# true, or the rest of the specials
1243def word.spec.t(hit: Bool, other: Bool, +ss: String) -> Got:
1244  match hit:
1245    case True{}:
1246      GotVal{VBool{True{}}}
1247    case False{}:
1248      word.spec.f(other, ss)
1249
1250# true, false, inf, and nan, including a sign on inf and nan
1251def word.spec(+ss: String) -> Got:
1252  word.spec.t(str.eq(ss, "true"), str.eq(ss, "false"), ss)
1253
1254# a datetime result as a value
1255def word.from.when(ww: WhenOut) -> Got:
1256  match ww:
1257    case WSome{when}:
1258      GotVal{VWhen{when}}
1259    case WFail{why}:
1260      GotBad{why}
1261    case WSkip{}:
1262      GotBad{"invalid datetime"}
1263
1264# the spelling of a numeral with the leading sign and underscores removed
1265def word.body.put.sign(is_sign: Bool, cc: Char, out: List<&2, Char>) -> List<&2, Char>:
1266  match is_sign:
1267    case True{}:
1268      out
1269    case False{}:
1270      cc <> out
1271
1272# an underscore is dropped; every other character is kept
1273def word.body.put.us(is_us: Bool, cc: Char, out: List<&2, Char>) -> List<&2, Char>:
1274  match is_us:
1275    case True{}:
1276      out
1277    case False{}:
1278      cc <> out
1279
1280# one character of a numeral spelling
1281def word.body.put(lead: Bool, +cc: Char, out: List<&2, Char>) -> List<&2, Char>:
1282  match lead:
1283    case True{}:
1284      word.body.put.sign(Bool.or(Char.is_eq(cc, '+'), Char.is_eq(cc, '-')), cc, out)
1285    case False{}:
1286      word.body.put.us(Char.is_eq(cc, '_'), cc, out)
1287
1288# the spelling, reversed, then put back in order at the end
1289def word.body.go(cs: List<&2, Char>, lead: Bool, out: List<&2, Char>) -> List<&2, Char>:
1290  match cs:
1291    case []:
1292      List.reverse(&2, Char, out)
1293    case +c <> t:
1294      word.body.go(t, False{}, word.body.put(lead, c, out))
1295
1296# the spelling of a numeral with the leading sign and underscores removed
1297def word.body(cs: List<&2, Char>) -> String:
1298  String.from_list(word.body.go(cs, True{}, []))
1299
1300# a fresh numeral scan
1301def num.start() -> Num:
1302  Num{NLead{}, Plus{}, 10, [], False{}, False{}, ""}
1303
1304# a scan that has failed
1305def num.bad(_st: Num, why: String) -> Num:
1306  Num{NBad{}, Plus{}, 10, [], False{}, False{}, why}
1307
1308# set the sign and wait for a digit
1309def num.sign(_st: Num, sign: Sign) -> Num:
1310  Num{NSign{}, sign, 10, [], False{}, False{}, ""}
1311
1312# a digit that fits the base
1313def num.digit.ok(ok: Bool, +cc: Char, nk: NK, sign: Sign, +base: U32, ds: List<&2, U32>) -> Num:
1314  match ok:
1315    case False{}:
1316      num.bad(Num{NLead{}, Plus{}, 10, [], False{}, False{}, ""}, "invalid digit")
1317    case True{}:
1318      Num{nk, sign, base, dec.go(ds, base, dig.val(cc)), False{}, True{}, ""}
1319
1320# a decimal digit joined to the numeral
1321def num.digit.go(st: Num, +cc: Char, nk: NK) -> Num:
1322  Num{_nk, sign, +base, ds, _us, _saw, _why} = st
1323  num.digit.ok(dig.ok(dig.val(cc), base), cc, nk, sign, base, ds)
1324
1325# a decimal digit joined to the numeral
1326def num.digit(st: Num, +cc: Char, nk: NK) -> Num:
1327  num.digit.go(st, cc, nk)
1328
1329# an underscore between digits
1330def num.us.go(ok: Bool, nk: NK, sign: Sign, base: U32, ds: List<&2, U32>, why: String) -> Num:
1331  match ok:
1332    case False{}:
1333      num.bad(Num{NLead{}, Plus{}, 10, [], False{}, False{}, ""}, "invalid underscore")
1334    case True{}:
1335      Num{nk, sign, base, ds, True{}, True{}, why}
1336
1337# an underscore between digits
1338def num.us(st: Num) -> Num:
1339  Num{nk, sign, base, ds, us, saw, why} = st
1340  num.us.go(Bool.and(saw, Bool.not(us)), nk, sign, base, ds, why)
1341
1342# the base prefix after a leading zero
1343def num.base(st: Num, base: U32) -> Num:
1344  Num{_nk, sign, _b, _ds, _us, _saw, _why} = st
1345  Num{NBase{}, sign, base, [], False{}, False{}, ""}
1346
1347# a dot begins the fraction
1348def num.dot.go(ok: Bool, sign: Sign) -> Num:
1349  match ok:
1350    case False{}:
1351      num.bad(Num{NLead{}, Plus{}, 10, [], False{}, False{}, ""}, "invalid fraction")
1352    case True{}:
1353      Num{NFrac{}, sign, 10, [], False{}, False{}, ""}
1354
1355# a dot begins the fraction
1356def num.dot(st: Num) -> Num:
1357  Num{_nk, sign, _b, _ds, us, saw, _why} = st
1358  num.dot.go(Bool.and(saw, Bool.not(us)), sign)
1359
1360# an exponent marker
1361def num.exp.go(ok: Bool, sign: Sign) -> Num:
1362  match ok:
1363    case False{}:
1364      num.bad(Num{NLead{}, Plus{}, 10, [], False{}, False{}, ""}, "invalid exponent")
1365    case True{}:
1366      Num{NExp{}, sign, 10, [], False{}, False{}, ""}
1367
1368# an exponent marker
1369def num.exp(st: Num) -> Num:
1370  Num{_nk, sign, _b, _ds, us, saw, _why} = st
1371  num.exp.go(Bool.and(saw, Bool.not(us)), sign)
1372
1373# the sign already chosen
1374def num.sign.of(st: Num) -> Sign:
1375  Num{_nk, sign, _b, _ds, _us, _saw, _why} = st
1376  sign
1377
1378# a first digit
1379def num.lead.digit(digit: Bool, st: Num, +cc: Char) -> Num:
1380  match digit:
1381    case True{}:
1382      num.digit(st, cc, NDig{})
1383    case False{}:
1384      num.bad(st, "invalid number")
1385
1386# a leading zero, or another digit
1387def num.lead.zero(zero: Bool, digit: Bool, st: Num, +cc: Char) -> Num:
1388  match zero:
1389    case True{}:
1390      Num{NZero{}, num.sign.of(st), 10, [], False{}, True{}, ""}
1391    case False{}:
1392      num.lead.digit(digit, st, cc)
1393
1394# a minus, a zero, or a digit
1395def num.lead.minus(minus: Bool, zero: Bool, digit: Bool, st: Num, +cc: Char) -> Num:
1396  match minus:
1397    case True{}:
1398      num.sign(st, Minus{})
1399    case False{}:
1400      num.lead.zero(zero, digit, st, cc)
1401
1402# a sign, a zero, or a digit
1403def num.lead.go(plus: Bool, minus: Bool, zero: Bool, digit: Bool, st: Num, +cc: Char) -> Num:
1404  match plus:
1405    case True{}:
1406      num.sign(st, Plus{})
1407    case False{}:
1408      num.lead.minus(minus, zero, digit, st, cc)
1409
1410# the first character after an optional sign
1411def num.lead(st: Num, +cc: Char) -> Num:
1412  num.lead.go(Char.is_eq(cc, '+'), Char.is_eq(cc, '-'), Char.is_eq(cc, '0'),
1413    Char.is_digit(cc), st, cc)
1414
1415# a second sign is refused; any other character is read as the first one of
1416# an unsigned numeral, with the sign kept
1417def num.after.sign.go(twice: Bool, sign: Sign, +cc: Char) -> Num:
1418  match twice:
1419    case True{}:
1420      num.bad(num.start(), "invalid number")
1421    case False{}:
1422      num.lead(Num{NLead{}, sign, 10, [], False{}, False{}, ""}, cc)
1423
1424# the character after a sign
1425def num.after.sign(st: Num, +cc: Char) -> Num:
1426  num.after.sign.go(Bool.or(Char.is_eq(cc, '+'), Char.is_eq(cc, '-')), num.sign.of(st), cc)
1427
1428# a capital exponent; any other character is refused, since a digit or an
1429# underscore after a leading zero (`01`, `0_1`) would hide it
1430def num.zero.exp2(ee: Bool, st: Num, _c: Char) -> Num:
1431  match ee:
1432    case True{}:
1433      num.exp(st)
1434    case False{}:
1435      num.bad(st, "invalid number")
1436
1437# an exponent after zero, or a rejected extra digit
1438def num.zero.exp(eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1439  match eee:
1440    case True{}:
1441      num.exp(st)
1442    case False{}:
1443      num.zero.exp2(ee, st, cc)
1444
1445# a fraction or an exponent after zero
1446def num.zero.dot(dot: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1447  match dot:
1448    case True{}:
1449      num.dot(st)
1450    case False{}:
1451      num.zero.exp(eee, ee, st, cc)
1452
1453# a binary prefix, or a float
1454def num.zero.b(bb: Bool, dot: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1455  match bb:
1456    case True{}:
1457      num.base(st, 2)
1458    case False{}:
1459      num.zero.dot(dot, eee, ee, st, cc)
1460
1461# an octal prefix, or the rest
1462def num.zero.o(oo: Bool, bb: Bool, dot: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1463  match oo:
1464    case True{}:
1465      num.base(st, 8)
1466    case False{}:
1467      num.zero.b(bb, dot, eee, ee, st, cc)
1468
1469# a base prefix, a fraction, or an exponent
1470def num.zero.go(xx: Bool, oo: Bool, bb: Bool, dot: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1471  match xx:
1472    case True{}:
1473      num.base(st, 16)
1474    case False{}:
1475      num.zero.o(oo, bb, dot, eee, ee, st, cc)
1476
1477# the character after a lone zero
1478def num.zero(st: Num, +cc: Char) -> Num:
1479  num.zero.go(Char.is_eq(cc, 'x'), Char.is_eq(cc, 'o'), Char.is_eq(cc, 'b'),
1480    Char.is_eq(cc, '.'), Char.is_eq(cc, 'e'), Char.is_eq(cc, 'E'), st, cc)
1481
1482# a capital exponent, or a rejected character
1483def num.digs.exp2(ee: Bool, st: Num, _c: Char) -> Num:
1484  match ee:
1485    case True{}:
1486      num.exp(st)
1487    case False{}:
1488      num.bad(st, "invalid number")
1489
1490# an exponent
1491def num.digs.exp(eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1492  match eee:
1493    case True{}:
1494      num.exp(st)
1495    case False{}:
1496      num.digs.exp2(ee, st, cc)
1497
1498# a dot or an exponent
1499def num.digs.dot(dot: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1500  match dot:
1501    case True{}:
1502      num.dot(st)
1503    case False{}:
1504      num.digs.exp(eee, ee, st, cc)
1505
1506# an underscore, a dot, or an exponent
1507def num.digs.us(us: Bool, dot: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1508  match us:
1509    case True{}:
1510      num.us(st)
1511    case False{}:
1512      num.digs.dot(dot, eee, ee, st, cc)
1513
1514# a decimal digit, an underscore, a dot, or an exponent
1515def num.digs.go(digit: Bool, us: Bool, dot: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1516  match digit:
1517    case True{}:
1518      num.digit(st, cc, NDig{})
1519    case False{}:
1520      num.digs.us(us, dot, eee, ee, st, cc)
1521
1522# a decimal digit, an underscore, a dot, or an exponent
1523def num.digs(st: Num, +cc: Char) -> Num:
1524  num.digs.go(Char.is_digit(cc), Char.is_eq(cc, '_'), Char.is_eq(cc, '.'),
1525    Char.is_eq(cc, 'e'), Char.is_eq(cc, 'E'), st, cc)
1526
1527# an underscore, or a digit of the base
1528def num.based.go(us: Bool, st: Num, +cc: Char) -> Num:
1529  match us:
1530    case True{}:
1531      num.us(st)
1532    case False{}:
1533      num.digit(st, cc, NBase{})
1534
1535# a digit of a prefixed integer, or an underscore
1536def num.based(st: Num, +cc: Char) -> Num:
1537  num.based.go(Char.is_eq(cc, '_'), st, cc)
1538
1539# a capital exponent, or a rejected character
1540def num.frac.exp2(ee: Bool, st: Num, _c: Char) -> Num:
1541  match ee:
1542    case True{}:
1543      num.exp(st)
1544    case False{}:
1545      num.bad(st, "invalid fraction")
1546
1547# an exponent in a fraction
1548def num.frac.exp(eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1549  match eee:
1550    case True{}:
1551      num.exp(st)
1552    case False{}:
1553      num.frac.exp2(ee, st, cc)
1554
1555# an underscore or an exponent in a fraction
1556def num.frac.us(us: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1557  match us:
1558    case True{}:
1559      num.us(st)
1560    case False{}:
1561      num.frac.exp(eee, ee, st, cc)
1562
1563# a fraction digit, an underscore, or an exponent
1564def num.frac.go(digit: Bool, us: Bool, eee: Bool, ee: Bool, st: Num, +cc: Char) -> Num:
1565  match digit:
1566    case True{}:
1567      num.digit(st, cc, NFrac{})
1568    case False{}:
1569      num.frac.us(us, eee, ee, st, cc)
1570
1571# a fraction digit, an underscore, or an exponent
1572def num.frac(st: Num, +cc: Char) -> Num:
1573  num.frac.go(Char.is_digit(cc), Char.is_eq(cc, '_'), Char.is_eq(cc, 'e'),
1574    Char.is_eq(cc, 'E'), st, cc)
1575
1576# the exponent sign is part of the spelling; digits follow
1577def num.exp.sign(st: Num) -> Num:
1578  Num{_nk, sign, _b, _ds, _us, _saw, _why} = st
1579  Num{NEDig{}, sign, 10, [], False{}, False{}, ""}
1580
1581# a digit of the exponent
1582def num.expon.digit(digit: Bool, st: Num, +cc: Char) -> Num:
1583  match digit:
1584    case True{}:
1585      num.digit(st, cc, NEDig{})
1586    case False{}:
1587      num.bad(st, "invalid exponent")
1588
1589# a minus or a digit in an exponent
1590def num.expon.minus(minus: Bool, digit: Bool, st: Num, +cc: Char) -> Num:
1591  match minus:
1592    case True{}:
1593      num.exp.sign(st)
1594    case False{}:
1595      num.expon.digit(digit, st, cc)
1596
1597# the sign or the first digit of an exponent
1598def num.expon.go(plus: Bool, minus: Bool, digit: Bool, st: Num, +cc: Char) -> Num:
1599  match plus:
1600    case True{}:
1601      num.exp.sign(st)
1602    case False{}:
1603      num.expon.minus(minus, digit, st, cc)
1604
1605# the sign or the first digit of an exponent
1606def num.expon(st: Num, +cc: Char) -> Num:
1607  num.expon.go(Char.is_eq(cc, '+'), Char.is_eq(cc, '-'), Char.is_digit(cc), st, cc)
1608
1609# an underscore in an exponent
1610def num.edig.us(us: Bool, st: Num, _c: Char) -> Num:
1611  match us:
1612    case True{}:
1613      num.us(st)
1614    case False{}:
1615      num.bad(st, "invalid exponent")
1616
1617# an exponent digit or an underscore
1618def num.edig.go(digit: Bool, us: Bool, st: Num, +cc: Char) -> Num:
1619  match digit:
1620    case True{}:
1621      num.digit(st, cc, NEDig{})
1622    case False{}:
1623      num.edig.us(us, st, cc)
1624
1625# an exponent digit or an underscore
1626def num.edig(st: Num, +cc: Char) -> Num:
1627  num.edig.go(Char.is_digit(cc), Char.is_eq(cc, '_'), st, cc)
1628
1629# one character of a numeral
1630def num.on(nk: NK, st: Num, +cc: Char) -> Num:
1631  match nk:
1632    case NLead{}:
1633      num.lead(st, cc)
1634    case NSign{}:
1635      num.after.sign(st, cc)
1636    case NZero{}:
1637      num.zero(st, cc)
1638    case NDig{}:
1639      num.digs(st, cc)
1640    case NBase{}:
1641      num.based(st, cc)
1642    case NFrac{}:
1643      num.frac(st, cc)
1644    case NExp{}:
1645      num.expon(st, cc)
1646    case NEDig{}:
1647      num.edig(st, cc)
1648    case NBad{}:
1649      st
1650
1651# one character of a numeral
1652def num.step.go(st: Num, +cc: Char) -> Num:
1653  Num{+nk, sign, base, ds, us, saw, why} = st
1654  num.on(nk, Num{nk, sign, base, ds, us, saw, why}, cc)
1655
1656# one character of a numeral
1657def num.step(st: Num, +cc: Char) -> Num:
1658  num.step.go(st, cc)
1659
1660# the walk over a numeral
1661def num.go(cs: List<&2, Char>, st: Num) -> Num:
1662  match cs:
1663    case []:
1664      st
1665    case +h <> t:
1666      num.go(t, num.step(st, h))
1667
1668# the positive limit is 2^63-1; the negative limit is 2^63
1669def i64.limit(sign: Sign) -> String:
1670  match sign:
1671    case Plus{}:
1672      "9223372036854775807"
1673    case Minus{}:
1674      "9223372036854775808"
1675
1676# the first differing digit stands; a tie takes the new order
1677def i64.ord(seen: Cmp, now: Cmp) -> Cmp:
1678  match seen now:
1679    case EQ{} n:
1680      n
1681    case LT{} _n:
1682      LT{}
1683    case GT{} _n:
1684      GT{}
1685
1686# a shorter digit string fits and a longer one does not. equal length uses
1687# digit order. the walk does not rebuild either string
1688def i64.step(+digits: String, +limit: String, ord: Cmp) -> Bool:
1689  match digits limit:
1690    case SNil{} SNil{}:
1691      Cmp.is_le(ord)
1692    case SNil{} SCon{_h, _t}:
1693      True{}
1694    case SCon{_h, _t} SNil{}:
1695      False{}
1696    case SCon{x, xt} SCon{y, yt}:
1697      i64.step(xt, yt, i64.ord(ord, U32.cmp(Char.to_u32(x), Char.to_u32(y))))
1698
1699# whether the integer fits in a signed 64-bit integer
1700def i64.fits(+sign: Sign, +digits: String) -> Bool:
1701  i64.step(digits, i64.limit(sign), EQ{})
1702
1703# an integer inside the signed 64-bit range
1704def num.fin.range(ok: Bool, sign: Sign, digits: String) -> Got:
1705  match ok:
1706    case True{}:
1707      GotVal{VInt{sign, digits}}
1708    case False{}:
1709      GotBad{"out of range"}
1710
1711# a finished integer, rejected when it falls outside signed 64-bit
1712def num.fin.int(saw: Bool, +sign: Sign, +digits: String) -> Got:
1713  match saw:
1714    case False{}:
1715      GotBad{"invalid number"}
1716    case True{}:
1717      num.fin.range(i64.fits(sign, digits), sign, digits)
1718
1719# a numeral needs a digit in its last run
1720def num.fin.saw(saw: Bool, val: Val) -> Got:
1721  match saw:
1722    case False{}:
1723      GotBad{"invalid number"}
1724    case True{}:
1725      GotVal{val}
1726
1727# a prefixed integer may not carry a sign
1728def num.signed(cs: List<&2, Char>) -> Bool:
1729  match cs:
1730    case []:
1731      False{}
1732    case +c <> _:
1733      Bool.or(Char.is_eq(c, '+'), Char.is_eq(c, '-'))
1734
1735# a prefixed integer, rejected when a sign was written
1736def num.fin.base(signed: Bool, saw: Bool, sign: Sign, ds: List<&2, U32>) -> Got:
1737  match signed:
1738    case True{}:
1739      GotBad{"invalid number"}
1740    case False{}:
1741      num.fin.int(saw, sign, dec.text(ds))
1742
1743# the kind of numeral the scan finished in
1744def num.fin.nk(nk: NK, sign: Sign, ds: List<&2, U32>, saw: Bool, why: String, cs: List<&2, Char>) -> Got:
1745  match nk:
1746    case NBad{}:
1747      GotBad{why}
1748    case NLead{}:
1749      GotBad{"invalid number"}
1750    case NSign{}:
1751      GotBad{"invalid number"}
1752    case NZero{}:
1753      GotVal{VInt{sign, "0"}}
1754    case NDig{}:
1755      num.fin.int(saw, sign, dec.text(ds))
1756    case NBase{}:
1757      num.fin.base(num.signed(cs), saw, sign, ds)
1758    case NFrac{}:
1759      num.fin.saw(saw, VFlo{sign, word.body(cs)})
1760    case NExp{}:
1761      GotBad{"invalid exponent"}
1762    case NEDig{}:
1763      num.fin.saw(saw, VFlo{sign, word.body(cs)})
1764
1765# a trailing underscore is rejected
1766def num.fin.us(us: Bool, nk: NK, sign: Sign, ds: List<&2, U32>, saw: Bool, why: String, cs: List<&2, Char>) -> Got:
1767  match us:
1768    case True{}:
1769      GotBad{"invalid underscore"}
1770    case False{}:
1771      num.fin.nk(nk, sign, ds, saw, why, cs)
1772
1773# the value of a finished numeral
1774def num.fin(st: Num, cs: List<&2, Char>) -> Got:
1775  Num{nk, sign, _base, ds, us, saw, why} = st
1776  num.fin.us(us, nk, sign, ds, saw, why, cs)
1777
1778# a numeral token
1779def word.num(+cs: List<&2, Char>) -> Got:
1780  num.fin(num.go(cs, num.start()), cs)
1781
1782# a datetime when the token has a colon or a dash, otherwise a numeral
1783def word.route.date(date: Bool, cs: List<&2, Char>) -> Got:
1784  match date:
1785    case True{}:
1786      word.from.when(when.read(cs))
1787    case False{}:
1788      word.num(cs)
1789
1790# a special word, or a numeral
1791def word.route(gg: Got, date: Bool, +cs: List<&2, Char>) -> Got:
1792  match gg:
1793    case GotVal{val}:
1794      GotVal{val}
1795    case GotBad{_}:
1796      word.route.date(word.as_date(date, word.ee(cs)), cs)
1797
1798# '-' can start a signed inf or nan
1799def word.special.minus(+cc: Char) -> Bool:
1800  Char.is_eq(cc, '-')
1801
1802# '+' or '-'
1803def word.special.plus(hit: Bool, +cc: Char) -> Bool:
1804  match hit:
1805    case True{}:
1806      True{}
1807    case False{}:
1808      word.special.minus(cc)
1809
1810# 'n', or a sign
1811def word.special.n(hit: Bool, +cc: Char) -> Bool:
1812  match hit:
1813    case True{}:
1814      True{}
1815    case False{}:
1816      word.special.plus(Char.is_eq(cc, '+'), cc)
1817
1818# 'i', or nan, or a sign
1819def word.special.i(hit: Bool, +cc: Char) -> Bool:
1820  match hit:
1821    case True{}:
1822      True{}
1823    case False{}:
1824      word.special.n(Char.is_eq(cc, 'n'), cc)
1825
1826# 'f', or inf, or nan, or a sign
1827def word.special.f(hit: Bool, +cc: Char) -> Bool:
1828  match hit:
1829    case True{}:
1830      True{}
1831    case False{}:
1832      word.special.i(Char.is_eq(cc, 'i'), cc)
1833
1834# 't', or false, or inf, or nan, or a sign
1835def word.special.t(hit: Bool, +cc: Char) -> Bool:
1836  match hit:
1837    case True{}:
1838      True{}
1839    case False{}:
1840      word.special.f(Char.is_eq(cc, 'f'), cc)
1841
1842# whether this character can start a special bare word
1843def word.special(+cc: Char) -> Bool:
1844  word.special.t(Char.is_eq(cc, 't'), cc)
1845
1846# the first character, when the word has one
1847def word.lead(cs: List<&2, Char>) -> Bool:
1848  match cs:
1849    case []:
1850      False{}
1851    case +h <> _t:
1852      word.special(h)
1853
1854# a numeral or a datetime. the token cannot be a keyword
1855def word.val.num(+cs: List<&2, Char>) -> Got:
1856  word.route(GotBad{""}, word.or(word.colon(cs), word.dash(cs, True{})), cs)
1857
1858# a special word, or a numeral. a digit does not build a string to compare
1859def word.val.pick(special: Bool, +cs: List<&2, Char>) -> Got:
1860  match special:
1861    case True{}:
1862      word.route(word.spec(String.from_list(cs)),
1863        word.or(word.colon(cs), word.dash(cs, True{})), cs)
1864    case False{}:
1865      word.val.num(cs)
1866
1867# a bare word: a special, a datetime, or a numeral
1868def word.val(+cs: List<&2, Char>) -> Got:
1869  word.val.pick(word.lead(cs), cs)
1870
1871# a change applied at the end of a key path
1872type Job is Data:
1873  JPut{val: Val}
1874  JDef{}
1875  JAot{}
1876
1877# one table the walk has entered
1878type Fr is Data:
1879  FrNew{name: String, parent: List<&2, Val>, path: String}
1880  FrRep{name: String, parent: List<&2, Val>, path: String}
1881  FrAot{name: String, parent: List<&2, Val>, pre: List<&2, Val>, path: String}
1882
1883# the walk: the table being edited, and the frames above it
1884type Tw is Data:
1885  Tw{vs: List<&2, Val>, job: Job, stack: List<&2, Fr>, bad: String, pre: String,
1886    heads: List<&2, String>, inl: Bool}
1887
1888# the root table after a walk
1889type End is Data:
1890  End{vs: List<&2, Val>, bad: String, heads: List<&2, String>}
1891
1892# what a key in a table refers to
1893type Look is Data:
1894  KMiss{}
1895  KHead{path: String, rows: List<&2, Val>}
1896  KInl{}
1897  KAots{path: String, elems: List<&2, Val>}
1898  KNo{why: String}
1899
1900# the last element of an array of tables
1901type Last is Data:
1902  LastSome{path: String, pre: List<&2, Val>, rows: List<&2, Val>}
1903  LastNo{why: String}
1904
1905# the first error is kept
1906def err.first.go(empty: Bool, bad: String, why: String) -> String:
1907  match empty:
1908    case True{}:
1909      why
1910    case False{}:
1911      bad
1912
1913# the first error is kept
1914def err.first(+bad: String, why: String) -> String:
1915  err.first.go(String.is_empty(bad), bad, why)
1916
1917# a key found earlier wins
1918def find.step(eq: Bool, vv: Val, more: Unit -> Hit) -> Hit:
1919  match eq:
1920    case True{}:
1921      Found{vv}
1922    case False{}:
1923      more(Unit{})
1924
1925# the first pair of this name
1926def rows.find(rows: List<&2, Val>, +name: String) -> Hit:
1927  match rows:
1928    case []:
1929      Miss{}
1930    case VPair{n, v} <> t:
1931      find.step(str.eq(n, name), v, _u => rows.find(t, name))
1932    case _ <> t:
1933      rows.find(t, name)
1934
1935# the value written for a key, or Miss
1936def get(rows: List<&2, Val>, +name: String) -> Hit:
1937  rows.find(rows, name)
1938
1939# replace the value of one pair
1940def rows.repl.step(eq: Bool, nn: String, old: Val, val: Val, more: Unit -> List<&2, Val>) -> List<&2, Val>:
1941  match eq:
1942    case True{}:
1943      VPair{nn, val} <> more(Unit{})
1944    case False{}:
1945      VPair{nn, old} <> more(Unit{})
1946
1947# replace every pair of this name
1948def rows.repl(rows: List<&2, Val>, +name: String, +val: Val) -> List<&2, Val>:
1949  match rows:
1950    case []:
1951      []
1952    case VPair{+n, old} <> t:
1953      rows.repl.step(str.eq(n, name), n, old, val, _u => rows.repl(t, name, val))
1954    case h <> t:
1955      h <> rows.repl(t, name, val)
1956
1957# either flag
1958def heads.or(aa: Bool, bb: Bool) -> Bool:
1959  match aa:
1960    case True{}:
1961      True{}
1962    case False{}:
1963      bb
1964
1965# heads records each table the document has defined as its path behind one
1966# mark: `[` when a header defined it, `.` when dotted keys did
1967def heads.by.head(path: String) -> String:
1968  SCon{'[', path}
1969
1970# a table dotted keys defined, as heads records it
1971def heads.by.dot(path: String) -> String:
1972  SCon{'.', path}
1973
1974# whether a table path was defined, by a header or by dotted keys
1975def heads.has(hs: List<&2, String>, +pp: String) -> Bool:
1976  match hs:
1977    case []:
1978      False{}
1979    case SCon{_mark, h} <> t:
1980      heads.or(str.eq(h, pp), heads.has(t, pp))
1981    case SNil{} <> t:
1982      heads.has(t, pp)
1983
1984# whether a table path was defined by a header
1985def heads.head(hs: List<&2, String>, +pp: String) -> Bool:
1986  match hs:
1987    case []:
1988      False{}
1989    case SCon{mark, h} <> t:
1990      heads.or(Bool.and(Char.is_eq(mark, '['), str.eq(h, pp)), heads.head(t, pp))
1991    case SNil{} <> t:
1992      heads.head(t, pp)
1993
1994# a recorded table under the prefix is dropped
1995def heads.drop.step(
1996  under: Bool,
1997  mark: Char,
1998  path: String,
1999  rest: List<&2, String>
2000) -> List<&2, String>:
2001  match under:
2002    case True{}:
2003      rest
2004    case False{}:
2005      SCon{mark, path} <> rest
2006
2007# forget every table whose path starts with the prefix. A new element of an
2008# array of tables starts with none of the tables the element before defined
2009def heads.drop(hs: List<&2, String>, +pre: String) -> List<&2, String>:
2010  match hs:
2011    case []:
2012      []
2013    case SCon{mark, +path} <> t:
2014      heads.drop.step(String.starts_with(path, pre), mark, path, heads.drop(t, pre))
2015    case SNil{} <> t:
2016      heads.drop(t, pre)
2017
2018# a table defined by a dotted key is recorded once
2019def heads.define.new(seen: Bool, path: String, heads: List<&2, String>) -> List<&2, String>:
2020  match seen:
2021    case True{}:
2022      heads
2023    case False{}:
2024      heads.by.dot(path) <> heads
2025
2026# a dotted key defines each table before its last segment
2027def heads.define(job: Job, +path: String, +heads: List<&2, String>) -> List<&2, String>:
2028  match job:
2029    case JPut{_val}:
2030      heads.define.new(heads.has(heads, path), path, heads)
2031    case _:
2032      heads
2033
2034# a dotted path from a prefix and one segment
2035def tree.pre.go(empty: Bool, pre: String, name: String) -> String:
2036  match empty:
2037    case True{}:
2038      key(name)
2039    case False{}:
2040      pre ++ "." ++ key(name)
2041
2042# a dotted path from a prefix and one segment
2043def tree.pre(+pre: String, name: String) -> String:
2044  tree.pre.go(String.is_empty(pre), pre, name)
2045
2046# the value a key already holds
2047def look.of(vv: Val) -> Look:
2048  match vv:
2049    case VHead{path, rows}:
2050      KHead{path, rows}
2051    case VInl{_rows}:
2052      KInl{}
2053    case VAots{path, elems}:
2054      KAots{path, elems}
2055    case _:
2056      KNo{"not a table"}
2057
2058# the matching pair, or the rest of the table
2059def look.step(eq: Bool, vv: Val, more: Unit -> Look) -> Look:
2060  match eq:
2061    case True{}:
2062      look.of(vv)
2063    case False{}:
2064      more(Unit{})
2065
2066# what a key in this table refers to
2067def rows.look(rows: List<&2, Val>, +name: String) -> Look:
2068  match rows:
2069    case []:
2070      KMiss{}
2071    case VPair{n, v} <> t:
2072      look.step(str.eq(n, name), v, _u => rows.look(t, name))
2073    case _ <> t:
2074      rows.look(t, name)
2075
2076# the newest element. rows stay newest-first until the document is sealed
2077def look.last.one(vv: Val, path: String, older: List<&2, Val>) -> Last:
2078  match vv:
2079    case VAot{_p, rows}:
2080      LastSome{path, older, rows}
2081    case _:
2082      LastNo{"not a table"}
2083
2084# the newest element of an array of tables, and the older elements behind it
2085def look.last(elems: List<&2, Val>, path: String) -> Last:
2086  match elems:
2087    case []:
2088      LastNo{"empty array of tables"}
2089    case h <> t:
2090      look.last.one(h, path, t)
2091
2092# put the child rows back into the parent table. A new implicit table is
2093# consed, not copied on. Inside an inline table it is a table too until the
2094# inline table closes, so the next dotted key can go on in it (inl.seal)
2095def tree.wrap(fr: Fr, child: List<&2, Val>) -> List<&2, Val>:
2096  match fr:
2097    case FrNew{name, parent, path}:
2098      VPair{name, VHead{path, child}} <> parent
2099    case FrRep{name, parent, path}:
2100      rows.repl(parent, name, VHead{path, child})
2101    case FrAot{name, parent, pre, +path}:
2102      rows.repl(parent, name, VAots{path, VAot{path, child} <> pre})
2103
2104# walk the frames back to the root
2105def tree.rebuild(stack: List<&2, Fr>, vs: List<&2, Val>, bad: String, heads: List<&2, String>) -> End:
2106  match stack:
2107    case []:
2108      End{vs, bad, heads}
2109    case fr <> t:
2110      tree.rebuild(t, tree.wrap(fr, vs), bad, heads)
2111
2112# a key that is already present is a duplicate
2113def tree.leaf.put(
2114  hit: Hit,
2115  name: String,
2116  vs: List<&2, Val>,
2117  val: Val,
2118  stack: List<&2, Fr>,
2119  bad: String,
2120  heads: List<&2, String>
2121) -> End:
2122  match hit:
2123    case Found{_v}:
2124      tree.rebuild(stack, vs, err.first(bad, "duplicate key"), heads)
2125    case Miss{}:
2126      tree.rebuild(stack, VPair{name, val} <> vs, bad, heads)
2127
2128# an explicit header for a table that already exists
2129def tree.leaf.def.head(
2130  seen: Bool,
2131  name: String,
2132  vs: List<&2, Val>,
2133  rows: List<&2, Val>,
2134  stack: List<&2, Fr>,
2135  bad: String,
2136  +path: String,
2137  heads: List<&2, String>
2138) -> End:
2139  match seen:
2140    case True{}:
2141      tree.rebuild(stack, vs, err.first(bad, "duplicate table"), heads)
2142    case False{}:
2143      tree.rebuild(stack, rows.repl(vs, name, VHead{path, rows}), bad,
2144        heads.by.head(path) <> heads)
2145
2146# open a standard table
2147def tree.leaf.def.hit(
2148  hit: Look,
2149  name: String,
2150  vs: List<&2, Val>,
2151  stack: List<&2, Fr>,
2152  bad: String,
2153  +path: String,
2154  +heads: List<&2, String>
2155) -> End:
2156  match hit:
2157    case KMiss{}:
2158      tree.rebuild(stack, VPair{name, VHead{path, []}} <> vs, bad,
2159        heads.by.head(path) <> heads)
2160    case KHead{_p, rows}:
2161      tree.leaf.def.head(heads.has(heads, path), name, vs, rows, stack, bad, path,
2162        heads)
2163    case KInl{}:
2164      tree.rebuild(stack, vs, err.first(bad, "inline table is closed"), heads)
2165    case KAots{_p, _elems}:
2166      tree.rebuild(stack, vs, err.first(bad, "not a table"), heads)
2167    case KNo{why}:
2168      tree.rebuild(stack, vs, err.first(bad, why), heads)
2169
2170# open a standard table
2171def tree.leaf.def(
2172  hit: Look,
2173  +name: String,
2174  vs: List<&2, Val>,
2175  stack: List<&2, Fr>,
2176  bad: String,
2177  pre: String,
2178  heads: List<&2, String>
2179) -> End:
2180  tree.leaf.def.hit(hit, name, vs, stack, bad, tree.pre(pre, name), heads)
2181
2182# append one element of an array of tables
2183def tree.leaf.aot.hit(
2184  hit: Look,
2185  name: String,
2186  vs: List<&2, Val>,
2187  stack: List<&2, Fr>,
2188  bad: String,
2189  +path: String,
2190  heads: List<&2, String>
2191) -> End:
2192  match hit:
2193    case KMiss{}:
2194      tree.rebuild(stack, VPair{name, VAots{path, [VAot{path, []}]}} <> vs, bad, heads)
2195    case KAots{_p, elems}:
2196      tree.rebuild(stack, rows.repl(vs, name, VAots{path, VAot{path, []} <> elems}),
2197        bad, heads.drop(heads, path ++ "."))
2198    case KHead{_p, _rows}:
2199      tree.rebuild(stack, vs, err.first(bad, "not a table"), heads)
2200    case KInl{}:
2201      tree.rebuild(stack, vs, err.first(bad, "inline table is closed"), heads)
2202    case KNo{why}:
2203      tree.rebuild(stack, vs, err.first(bad, why), heads)
2204
2205# append one element of an array of tables
2206def tree.leaf.aot(
2207  hit: Look,
2208  +name: String,
2209  vs: List<&2, Val>,
2210  stack: List<&2, Fr>,
2211  bad: String,
2212  pre: String,
2213  heads: List<&2, String>
2214) -> End:
2215  tree.leaf.aot.hit(hit, name, vs, stack, bad, tree.pre(pre, name), heads)
2216
2217# the key at the end of the path
2218def tree.leaf.job(
2219  job: Job,
2220  +name: String,
2221  +vs: List<&2, Val>,
2222  stack: List<&2, Fr>,
2223  bad: String,
2224  pre: String,
2225  heads: List<&2, String>
2226) -> End:
2227  match job:
2228    case JPut{val}:
2229      tree.leaf.put(get(vs, name), name, vs, val, stack, bad, heads)
2230    case JDef{}:
2231      tree.leaf.def(rows.look(vs, name), name, vs, stack, bad, pre, heads)
2232    case JAot{}:
2233      tree.leaf.aot(rows.look(vs, name), name, vs, stack, bad, pre, heads)
2234
2235# a failed walk rebuilds what it has
2236def tree.leaf.bad(
2237  ok: Bool,
2238  name: String,
2239  vs: List<&2, Val>,
2240  job: Job,
2241  stack: List<&2, Fr>,
2242  bad: String,
2243  pre: String,
2244  heads: List<&2, String>
2245) -> End:
2246  match ok:
2247    case False{}:
2248      tree.rebuild(stack, vs, bad, heads)
2249    case True{}:
2250      tree.leaf.job(job, name, vs, stack, bad, pre, heads)
2251
2252# the key at the end of the path
2253def tree.leaf(name: String, tw: Tw) -> End:
2254  Tw{vs, job, stack, +bad, pre, heads, _inl} = tw
2255  tree.leaf.bad(String.is_empty(bad), name, vs, job, stack, bad, pre, heads)
2256
2257# enter the last element of an array of tables
2258def tree.sub.aots(
2259  last: Last,
2260  +name: String,
2261  +vs: List<&2, Val>,
2262  job: Job,
2263  stack: List<&2, Fr>,
2264  +pre: String,
2265  heads: List<&2, String>,
2266  inl: Bool,
2267  path: String
2268) -> Tw:
2269  match last:
2270    case LastSome{_p, prefix, rows}:
2271      Tw{rows, job, FrAot{name, vs, prefix, path} <> stack, "", tree.pre(pre, name),
2272        heads, inl}
2273    case LastNo{why}:
2274      Tw{vs, job, stack, why, pre, heads, inl}
2275
2276# a prefix of the current table is navigation; a dotted segment defines a table
2277def tree.sub.job(mark: Bool, job: Job) -> Job:
2278  match mark:
2279    case True{}:
2280      job
2281    case False{}:
2282      JDef{}
2283
2284# a segment of a dotted key, which defines tables as it goes
2285def tree.sub.dot(job: Job) -> Bool:
2286  match job:
2287    case JPut{_val}:
2288      True{}
2289    case _:
2290      False{}
2291
2292# enter a table, unless a dotted key would add to a table a header defined
2293def tree.sub.head.go(
2294  shut: Bool,
2295  path: String,
2296  rows: List<&2, Val>,
2297  +name: String,
2298  vs: List<&2, Val>,
2299  +job: Job,
2300  stack: List<&2, Fr>,
2301  +pre: String,
2302  heads: List<&2, String>,
2303  inl: Bool,
2304  mark: Bool
2305) -> Tw:
2306  match shut:
2307    case True{}:
2308      Tw{vs, job, stack, "duplicate table", pre, heads, inl}
2309    case False{}:
2310      Tw{rows, job, FrRep{name, vs, path} <> stack, "", tree.pre(pre, name),
2311        heads.define(tree.sub.job(mark, job), tree.pre(pre, name), heads), inl}
2312
2313# a dotted key asks whether a header defined the table; a header walk does not
2314def tree.sub.head(
2315  dot: Bool,
2316  path: String,
2317  rows: List<&2, Val>,
2318  +name: String,
2319  vs: List<&2, Val>,
2320  job: Job,
2321  stack: List<&2, Fr>,
2322  +pre: String,
2323  +heads: List<&2, String>,
2324  inl: Bool,
2325  mark: Bool
2326) -> Tw:
2327  match dot:
2328    case True{}:
2329      tree.sub.head.go(heads.head(heads, tree.pre(pre, name)), path, rows, name, vs, job,
2330        stack, pre, heads, inl, mark)
2331    case False{}:
2332      tree.sub.head.go(False{}, path, rows, name, vs, job, stack, pre, heads, inl, mark)
2333
2334# a header enters the last element of an array of tables; a dotted key cannot
2335# add to an array of tables
2336def tree.sub.arr(
2337  dot: Bool,
2338  +path: String,
2339  elems: List<&2, Val>,
2340  +name: String,
2341  +vs: List<&2, Val>,
2342  job: Job,
2343  stack: List<&2, Fr>,
2344  +pre: String,
2345  heads: List<&2, String>,
2346  inl: Bool
2347) -> Tw:
2348  match dot:
2349    case True{}:
2350      Tw{vs, job, stack, "duplicate table", pre, heads, inl}
2351    case False{}:
2352      tree.sub.aots(look.last(elems, path), name, vs, job, stack, pre, heads, inl, path)
2353
2354# descend into one key, or record why it cannot be entered
2355def tree.sub.look(
2356  hit: Look,
2357  +name: String,
2358  +vs: List<&2, Val>,
2359  +job: Job,
2360  stack: List<&2, Fr>,
2361  +pre: String,
2362  heads: List<&2, String>,
2363  +inl: Bool,
2364  +mark: Bool
2365) -> Tw:
2366  match hit:
2367    case KMiss{}:
2368      Tw{[], job, FrNew{name, vs, tree.pre(pre, name)} <> stack, "",
2369        tree.pre(pre, name), heads.define(tree.sub.job(mark, job), tree.pre(pre, name),
2370          heads), inl}
2371    case KHead{path, rows}:
2372      tree.sub.head(tree.sub.dot(tree.sub.job(mark, job)), path, rows, name, vs, job,
2373        stack, pre, heads, inl, mark)
2374    case KInl{}:
2375      Tw{vs, job, stack, "inline table is closed", pre, heads, inl}
2376    case KAots{path, elems}:
2377      tree.sub.arr(tree.sub.dot(tree.sub.job(mark, job)), path, elems, name, vs, job,
2378        stack, pre, heads, inl)
2379    case KNo{why}:
2380      Tw{vs, job, stack, why, pre, heads, inl}
2381
2382# descend into one key when the walk is still well
2383def tree.sub.bad(
2384  ok: Bool,
2385  +name: String,
2386  +vs: List<&2, Val>,
2387  job: Job,
2388  stack: List<&2, Fr>,
2389  bad: String,
2390  pre: String,
2391  heads: List<&2, String>,
2392  inl: Bool,
2393  mark: Bool
2394) -> Tw:
2395  match ok:
2396    case False{}:
2397      Tw{vs, job, stack, bad, pre, heads, inl}
2398    case True{}:
2399      tree.sub.look(rows.look(vs, name), name, vs, job, stack, pre, heads, inl, mark)
2400
2401# descend into one key
2402def tree.sub(name: String, tw: Tw, mark: Bool) -> Tw:
2403  Tw{+vs, job, stack, +bad, pre, heads, inl} = tw
2404  tree.sub.bad(String.is_empty(bad), name, vs, job, stack, bad, pre, heads, inl, mark)
2405
2406# how many segments are already the current table
2407def path.len(xs: List<&2, String>, nn: U32) -> U32:
2408  match xs:
2409    case []:
2410      nn
2411    case _ <> t:
2412      path.len(t, U32.add(nn, 1))
2413
2414# one fewer prefix segment, staying at zero
2415def path.dec.z(zz: Bool, skip: U32) -> U32:
2416  match zz:
2417    case True{}:
2418      0
2419    case False{}:
2420      U32.sub(skip, 1)
2421
2422# one fewer prefix segment, staying at zero
2423def path.dec(+skip: U32) -> U32:
2424  path.dec.z(U32.is_zero(skip), skip)
2425
2426# an empty path records an error
2427def tree.walk.none(tw: Tw) -> End:
2428  Tw{vs, _job, stack, bad, _pre, heads, _inl} = tw
2429  tree.rebuild(stack, vs, err.first(bad, "empty key"), heads)
2430
2431# follow a key path and apply the job at its end. skip is the current table
2432def tree.walk(path: List<&2, String>, tw: Tw, +skip: U32) -> End:
2433  match path:
2434    case []:
2435      tree.walk.none(tw)
2436    case name <> rest:
2437      match rest:
2438        case []:
2439          tree.leaf(name, tw)
2440        case _ <> _:
2441          tree.walk(rest, tree.sub(name, tw, U32.is_zero(skip)), path.dec(skip))
2442
2443# space or tab
2444def ch.sp(+cc: Char) -> Bool:
2445  Bool.or(U32.is_eq(Char.to_u32(cc), 32), U32.is_eq(Char.to_u32(cc), 9))
2446
2447# the space character itself, U+0020, the only one a datetime may hold
2448def ch.space(+cc: Char) -> Bool:
2449  U32.is_eq(Char.to_u32(cc), 32)
2450
2451# line feed or carriage return
2452def ch.nl(+cc: Char) -> Bool:
2453  Bool.or(U32.is_eq(Char.to_u32(cc), 10), U32.is_eq(Char.to_u32(cc), 13))
2454
2455# a control: U+0000 to U+001F, or U+007F
2456def ch.ctl(+cc: Char) -> Bool:
2457  Bool.or(U32.is_lt(Char.to_u32(cc), 32), U32.is_eq(Char.to_u32(cc), 127))
2458
2459# a character that ends a bare value
2460def ch.delim(+cc: Char) -> Bool:
2461  Bool.or(ch.sp(cc), Bool.or(ch.nl(cc), Bool.or(Char.is_eq(cc, '#'),
2462    Bool.or(Char.is_eq(cc, ','), Bool.or(Char.is_eq(cc, ']'), Char.is_eq(cc, '}'))))))
2463
2464# whitespace that a bare value swallows
2465def ch.skip(+cc: Char) -> Bool:
2466  Bool.or(ch.sp(cc), ch.nl(cc))
2467
2468# the quote character of a string kind
2469def q.char(kk: QKind) -> Char:
2470  match kk:
2471    case QLit{}:
2472      '\''
2473    case QMultiLit{}:
2474      '\''
2475    case _:
2476      '"'
2477
2478# a multiline string
2479def q.multi(kk: QKind) -> Bool:
2480  match kk:
2481    case QMulti{}:
2482      True{}
2483    case QMultiLit{}:
2484      True{}
2485    case _:
2486      False{}
2487
2488# a basic string, which has escapes
2489def q.basic(kk: QKind) -> Bool:
2490  match kk:
2491    case QBasic{}:
2492      True{}
2493    case QMulti{}:
2494      True{}
2495    case _:
2496      False{}
2497
2498# the multiline kind of a one-line kind
2499def q.as.multi(kk: QKind) -> QKind:
2500  match kk:
2501    case QLit{}:
2502      QMultiLit{}
2503    case _:
2504      QMulti{}
2505
2506# a pattern character that stands for a digit
2507def date.mode(pp: Char) -> Bool:
2508  U32.is_eq(Char.to_u32(pp), 68)
2509
2510# whether the rest of the shape matches
2511def date.eq.go(ok: Bool, more: Unit -> Bool) -> Bool:
2512  match ok:
2513    case False{}:
2514      False{}
2515    case True{}:
2516      more(Unit{})
2517
2518# one character of a date shape
2519def date.step(mode: Bool, digit: Bool, same: Bool, more: Unit -> Bool) -> Bool:
2520  match mode:
2521    case True{}:
2522      date.eq.go(digit, more)
2523    case False{}:
2524      date.eq.go(same, more)
2525
2526# both lists ended together
2527def date.eq.nil(pat: List<&2, Char>) -> Bool:
2528  match pat:
2529    case []:
2530      True{}
2531    case _ <> _:
2532      False{}
2533
2534# YYYY-MM-DD, with D standing for a digit
2535def date.eq(cs: List<&2, Char>, pat: List<&2, Char>) -> Bool:
2536  match cs:
2537    case []:
2538      date.eq.nil(pat)
2539    case +h <> t:
2540      match pat:
2541        case []:
2542          False{}
2543        case +p <> r:
2544          date.step(date.mode(p), Char.is_digit(h), Char.is_eq(h, p),
2545            _u => date.eq(t, r))
2546
2547# the buffer is a calendar date
2548def date.shaped(buf: List<&2, Char>) -> Bool:
2549  date.eq(List.reverse(&2, Char, buf), String.to_list("DDDD-DD-DD"))
2550
2551# the first n characters of a source span
2552def span.str(src: String, +nn: U32, zz: Bool) -> String:
2553  match src zz:
2554    case _s True{}:
2555      ""
2556    case SNil{} False{}:
2557      ""
2558    case SCon{+h, t} False{}:
2559      SCon{h, span.str(t, U32.sub(nn, 1), U32.is_zero(U32.sub(nn, 1)))}
2560
2561# the first n characters, reversed, so an escape can keep copying
2562def span.rev(src: String, +nn: U32, zz: Bool, acc: List<&2, Char>) -> List<&2, Char>:
2563  match src zz:
2564    case _s True{}:
2565      acc
2566    case SNil{} False{}:
2567      acc
2568    case SCon{h, t} False{}:
2569      span.rev(t, U32.sub(nn, 1), U32.is_zero(U32.sub(nn, 1)), h <> acc)
2570
2571# the unread suffix of a span that will not be stored
2572def span.drop(src: String) -> Unit:
2573  match src:
2574    case SNil{}:
2575      Unit{}
2576    case SCon{_h, t}:
2577      span.drop(t)
2578
2579# the key path, document table then this key
2580def path.cat(here: List<&2, String>, parts: List<&2, String>) -> List<&2, String>:
2581  List.append(&2, String, here, List.reverse(&2, String, parts))
2582
2583# a multiline string keeps a newline
2584def str.bad.nl(nl: Bool, multi: Bool) -> Bool:
2585  match nl:
2586    case False{}:
2587      True{}
2588    case True{}:
2589      Bool.not(multi)
2590
2591# tab is kept
2592def str.bad.tab(tab: Bool, nl: Bool, multi: Bool) -> Bool:
2593  match tab:
2594    case True{}:
2595      False{}
2596    case False{}:
2597      str.bad.nl(nl, multi)
2598
2599# a raw control is rejected
2600def str.bad.go(ctrl: Bool, tab: Bool, nl: Bool, multi: Bool) -> Bool:
2601  match ctrl:
2602    case False{}:
2603      False{}
2604    case True{}:
2605      str.bad.tab(tab, nl, multi)
2606
2607# a raw control is rejected. Tab is kept. A multiline string also keeps newlines
2608def str.bad(+uu: U32, multi: Bool) -> Bool:
2609  str.bad.go(Bool.or(U32.is_lt(uu, 32), U32.is_eq(uu, 127)), U32.is_eq(uu, 9),
2610    Bool.or(U32.is_eq(uu, 10), U32.is_eq(uu, 13)), multi)
2611
2612# the scanner has failed
2613def st.err(st: St, why: String) -> St:
2614  St{+bad, rows, heads, here, parts, buf, _lex, back, qkind, stack, _hold, uni, left,
2615    arrtab, lead} = st
2616  St{err.first(bad, why), rows, heads, here, parts, buf, LSink{}, back, qkind, stack,
2617    HNone{}, uni, left, arrtab, lead}
2618
2619# replace the lex state
2620def st.lex(st: St, lex: Lex) -> St:
2621  St{bad, rows, heads, here, parts, buf, _lex, back, qkind, stack, hold, uni, left,
2622    arrtab, lead} = st
2623  St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, hold, uni, left,
2624    arrtab, lead}
2625
2626# hold one character and set the lex state
2627def st.hold(st: St, +lex: Lex, cc: Char) -> St:
2628  St{bad, rows, heads, here, parts, buf, _lex, _back, qkind, stack, _hold, uni, left,
2629    arrtab, lead} = st
2630  St{bad, rows, heads, here, parts, buf, lex, lex, qkind, stack, HChar{cc}, uni, left,
2631    arrtab, lead}
2632
2633# append one character
2634def st.push(st: St, cc: Char, lex: Lex) -> St:
2635  St{bad, rows, heads, here, parts, buf, _lex, back, qkind, stack, hold, uni, left,
2636    arrtab, lead} = st
2637  St{bad, rows, heads, here, parts, cc <> buf, lex, back, qkind, stack, hold, uni, left,
2638    arrtab, lead}
2639
2640# the segment in the buffer joins the key, and the buffer is cleared
2641def seg.push(st: St, lex: Lex) -> St:
2642  St{bad, rows, heads, here, parts, buf, _lex, back, qkind, stack, hold, uni, left,
2643    arrtab, lead} = st
2644  St{bad, rows, heads, here, buf.str(buf) <> parts, [], lex, back, qkind, stack, hold,
2645    uni, left, arrtab, lead}
2646
2647# a finished value at the document root
2648def take.root(
2649  end: End,
2650  here: List<&2, String>,
2651  back: Lex,
2652  qkind: QKind,
2653  uni: U32,
2654  left: U32,
2655  arrtab: Bool,
2656  lead: Bool
2657) -> St:
2658  End{rows, bad, heads} = end
2659  St{bad, rows, heads, here, [], [], LLine{}, back, qkind, [], HNone{}, uni, left, arrtab,
2660    lead}
2661
2662# a finished value inside an inline table
2663def take.inl(
2664  end: End,
2665  rows: List<&2, Val>,
2666  heads: List<&2, String>,
2667  +here: List<&2, String>,
2668  +parts: List<&2, String>,
2669  rest: List<&2, Ctx>,
2670  back: Lex,
2671  qkind: QKind,
2672  uni: U32,
2673  left: U32,
2674  arrtab: Bool,
2675  lead: Bool
2676) -> St:
2677  End{inl, bad, _h} = end
2678  St{bad, rows, heads, here, [], [], LInlC{}, back, qkind,
2679    CInl{inl, parts, here} <> rest, HNone{}, uni, left, arrtab, lead}
2680
2681# place a finished value into the current table, array, or inline table
2682def take.top(
2683  stack: List<&2, Ctx>,
2684  val: Val,
2685  bad: String,
2686  rows: List<&2, Val>,
2687  heads: List<&2, String>,
2688  +here: List<&2, String>,
2689  parts: List<&2, String>,
2690  back: Lex,
2691  qkind: QKind,
2692  uni: U32,
2693  left: U32,
2694  arrtab: Bool,
2695  lead: Bool
2696) -> St:
2697  match stack:
2698    case []:
2699      take.root(tree.walk(path.cat(here, parts),
2700        Tw{rows, JPut{val}, [], bad, "", heads, False{}}, path.len(here, 0)), here,
2701        back, qkind, uni, left, arrtab, lead)
2702    case CArr{items, +saved, +at} <> rest:
2703      St{bad, rows, heads, at, saved, [], LArrC{}, back, qkind,
2704        CArr{val <> items, saved, at} <> rest, HNone{}, uni, left, arrtab, lead}
2705    case CInl{inl, +saved, +at} <> rest:
2706      take.inl(tree.walk(List.reverse(&2, String, parts),
2707        Tw{inl, JPut{val}, [], bad, "", [], True{}}, 0), rows, heads, at, saved, rest,
2708        back,
2709        qkind, uni, left, arrtab, lead)
2710
2711# place a finished value
2712def val.take(st: St, val: Val) -> St:
2713  St{bad, rows, heads, here, parts, _buf, _lex, back, qkind, stack, _hold, uni, left,
2714    arrtab, lead} = st
2715  take.top(stack, val, bad, rows, heads, here, parts, back, qkind, uni, left, arrtab,
2716    lead)
2717
2718# hold the delimiter when the following state must see it
2719def bare.hold.on(st: St, cc: Char) -> St:
2720  St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, _h, uni, left,
2721    arrtab, lead} = st
2722  St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, HChar{cc}, uni, left,
2723    arrtab, lead}
2724
2725# hold the delimiter when the following state must see it
2726# a newline that ended a root value already separates the next expression
2727def bare.line.lex(lex: Lex, st: St) -> St:
2728  match lex:
2729    case LLine{}:
2730      st.lex(st, LTop{})
2731    case _:
2732      st
2733
2734# a consumed newline returns to the top level after a root value
2735def bare.line.go(st: St) -> St:
2736  St{bad, rows, heads, here, parts, buf, +lex, back, qkind, stack, hold, uni, left,
2737    arrtab, lead} = st
2738  bare.line.lex(lex, St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack,
2739    hold, uni, left, arrtab, lead})
2740
2741# a consumed newline returns to the top level after a root value
2742def bare.line(st: St, nl: Bool) -> St:
2743  match nl:
2744    case True{}:
2745      bare.line.go(st)
2746    case False{}:
2747      st
2748
2749# hold the delimiter when the following state must see it
2750def bare.hold(st: St, cc: Char, hold: Bool) -> St:
2751  match hold:
2752    case False{}:
2753      bare.line(st, ch.nl(cc))
2754    case True{}:
2755      bare.hold.on(st, cc)
2756
2757# a bare word has been classified
2758def bare.got(gg: Got, st: St, cc: Char, hold: Bool) -> St:
2759  match gg:
2760    case GotBad{why}:
2761      st.err(st, why)
2762    case GotVal{val}:
2763      bare.hold(val.take(st, val), cc, hold)
2764
2765# finish a bare word. hold is true when the delimiter is not whitespace
2766def bare.finish(st: St, cc: Char, hold: Bool) -> St:
2767  St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, h, uni, left, arrtab,
2768    lead} = st
2769  bare.got(word.val(List.reverse(&2, Char, buf)),
2770    St{bad, rows, heads, here, parts, [], lex, back, qkind, stack, h, uni, left, arrtab,
2771      lead}, cc, hold)
2772
2773# close the header that was just read
2774def head.apply(end: End, segs: List<&2, String>, back: Lex, qkind: QKind, uni: U32, left: U32, lead: Bool) -> St:
2775  End{rows, bad, heads} = end
2776  St{bad, rows, heads, segs, [], [], LLine{}, back, qkind, [], HNone{}, uni, left,
2777    False{}, lead}
2778
2779# an array-of-tables header, or a table header
2780def head.job(
2781  arr: Bool,
2782  bad: String,
2783  rows: List<&2, Val>,
2784  heads: List<&2, String>,
2785  +segs: List<&2, String>,
2786  back: Lex,
2787  qkind: QKind,
2788  uni: U32,
2789  left: U32,
2790  lead: Bool
2791) -> St:
2792  match arr:
2793    case True{}:
2794      head.apply(tree.walk(segs, Tw{rows, JAot{}, [], bad, "", heads, False{}}, 0),
2795        segs,
2796        back, qkind, uni, left, lead)
2797    case False{}:
2798      head.apply(tree.walk(segs, Tw{rows, JDef{}, [], bad, "", heads, False{}}, 0),
2799        segs,
2800        back, qkind, uni, left, lead)
2801
2802# open the table or the array of tables named by the header
2803def head.on(st: St, segs: List<&2, String>) -> St:
2804  St{bad, rows, heads, _here, _parts, _buf, _lex, back, qkind, _stack, _hold, uni, left,
2805    arrtab, lead} = st
2806  head.job(arrtab, bad, rows, heads, segs, back, qkind, uni, left, lead)
2807
2808# the header key is ready
2809def head.go(empty: Bool, st: St, segs: List<&2, String>) -> St:
2810  match empty:
2811    case True{}:
2812      st.err(st, "empty key")
2813    case False{}:
2814      head.on(st, segs)
2815
2816# the segment was pushed
2817def head.use(st: St) -> St:
2818  St{bad, rows, heads, here, +parts, buf, lex, back, qkind, stack, hold, uni, left,
2819    arrtab, lead} = st
2820  head.go(List.is_empty(&2, String, parts),
2821    St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, hold, uni, left,
2822      arrtab, lead}, List.reverse(&2, String, parts))
2823
2824# the buffer is the last segment when it holds one
2825def head.fin.buf(empty: Bool, st: St) -> St:
2826  match empty:
2827    case True{}:
2828      head.use(st)
2829    case False{}:
2830      head.use(seg.push(st, LTop{}))
2831
2832# push a trailing segment, then open the header
2833def head.fin(st: St) -> St:
2834  St{bad, rows, heads, here, parts, +buf, lex, back, qkind, stack, hold, uni, left,
2835    arrtab, lead} = st
2836  head.fin.buf(List.is_empty(&2, Char, buf),
2837    St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, hold, uni, left,
2838      arrtab, lead})
2839
2840# close an array and place it
2841def arr.top(
2842  stack: List<&2, Ctx>,
2843  bad: String,
2844  rows: List<&2, Val>,
2845  heads: List<&2, String>,
2846  back: Lex,
2847  qkind: QKind,
2848  uni: U32,
2849  left: U32,
2850  arrtab: Bool,
2851  lead: Bool
2852) -> St:
2853  match stack:
2854    case CArr{items, parts, here} <> rest:
2855      val.take(St{bad, rows, heads, here, parts, [], LTop{}, back, qkind, rest, HNone{},
2856        uni, left, arrtab, lead}, VArr{List.reverse(&2, Val, items)})
2857    case _:
2858      St{err.first(bad, "unclosed"), rows, heads, [], [], [], LSink{}, back, qkind, [],
2859        HNone{}, uni, left, arrtab, lead}
2860
2861# close an array and place it
2862def arr.close(st: St) -> St:
2863  St{bad, rows, heads, _here, _parts, _buf, _lex, back, qkind, stack, _hold, uni, left,
2864    arrtab, lead} = st
2865  arr.top(stack, bad, rows, heads, back, qkind, uni, left, arrtab, lead)
2866
2867# an inline table is closed once written: the tables its dotted keys made,
2868# open while it was read, close with it
2869def inl.seal(rows: List<&2, Val>) -> List<&2, Val>:
2870  match rows:
2871    case []:
2872      []
2873    case VPair{name, VHead{_path, sub}} <> t:
2874      VPair{name, VInl{inl.seal(sub)}} <> inl.seal(t)
2875    case h <> t:
2876      h <> inl.seal(t)
2877
2878# close an inline table and place it
2879def inl.top(
2880  stack: List<&2, Ctx>,
2881  bad: String,
2882  rows: List<&2, Val>,
2883  heads: List<&2, String>,
2884  back: Lex,
2885  qkind: QKind,
2886  uni: U32,
2887  left: U32,
2888  arrtab: Bool,
2889  lead: Bool
2890) -> St:
2891  match stack:
2892    case CInl{inl, parts, here} <> rest:
2893      val.take(St{bad, rows, heads, here, parts, [], LTop{}, back, qkind, rest, HNone{},
2894        uni, left, arrtab, lead}, VInl{inl.seal(inl)})
2895    case _:
2896      St{err.first(bad, "unclosed"), rows, heads, [], [], [], LSink{}, back, qkind, [],
2897        HNone{}, uni, left, arrtab, lead}
2898
2899# close an inline table and place it
2900def inl.close(st: St) -> St:
2901  St{bad, rows, heads, _here, _parts, _buf, _lex, back, qkind, stack, _hold, uni, left,
2902    arrtab, lead} = st
2903  inl.top(stack, bad, rows, heads, back, qkind, uni, left, arrtab, lead)
2904
2905# the innermost frame is an inline table
2906def inl.open(stack: List<&2, Ctx>) -> Bool:
2907  match stack:
2908    case CInl{_rows, _parts, _here} <> _rest:
2909      True{}
2910    case _:
2911      False{}
2912
2913# a string is finished
2914def str.fin(st: St) -> St:
2915  St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, hold, uni, left, arrtab,
2916    lead} = st
2917  val.take(St{bad, rows, heads, here, parts, [], lex, back, qkind, stack, hold, uni, left,
2918    arrtab, lead}, VStr{buf.str(buf)})
2919
2920# one or two quotes that did not close a multiline string
2921def mq.put(one: Bool, +qq: Char, buf: List<&2, Char>) -> List<&2, Char>:
2922  match one:
2923    case True{}:
2924      qq <> buf
2925    case False{}:
2926      qq <> (qq <> buf)
2927
2928# a code point may be written as a character
2929def uni.ok(+uu: U32) -> Bool:
2930  Bool.and(U32.is_le(uu, 1114111),
2931    Bool.not(Bool.and(U32.is_ge(uu, 55296), U32.is_le(uu, 57343))))
2932
2933# a finished unicode escape written into the buffer
2934def uni.finish.on(st: St, uu: U32, back: Lex) -> St:
2935  St{bad, rows, heads, here, parts, buf, _lex, b, qkind, stack, _hold, _uni, _left,
2936    arrtab, lead} = st
2937  St{bad, rows, heads, here, parts, Char.from_u32(uu) <> buf, back, b, qkind, stack,
2938    HNone{}, 0, 0, arrtab, lead}
2939
2940# a finished unicode escape
2941def uni.finish(ok: Bool, st: St, uu: U32, back: Lex) -> St:
2942  match ok:
2943    case False{}:
2944      st.err(st, "invalid escape")
2945    case True{}:
2946      uni.finish.on(st, uu, back)
2947
2948# another hex digit is still required
2949def uni.next.more(st: St, uu: U32, left: U32) -> St:
2950  St{bad, rows, heads, here, parts, buf, lex, b, qkind, stack, hold, _uni, _left,
2951    arrtab, lead} = st
2952  St{bad, rows, heads, here, parts, buf, lex, b, qkind, stack, hold, uu,
2953    U32.sub(left, 1), arrtab, lead}
2954
2955# the escape is finished, or another hex digit is required
2956def uni.next(last: Bool, st: St, +uu: U32, back: Lex, left: U32) -> St:
2957  match last:
2958    case True{}:
2959      uni.finish(uni.ok(uu), st, uu, back)
2960    case False{}:
2961      uni.next.more(st, uu, left)
2962
2963# one hex digit of a unicode escape
2964def uni.go(ok: Bool, st: St, +cc: Char, back: Lex, uni: U32, +left: U32) -> St:
2965  match ok:
2966    case False{}:
2967      st.err(st, "invalid escape")
2968    case True{}:
2969      uni.next(U32.is_eq(left, 1), st, U32.add(U32.mul(uni, 16), dig.val(cc)), back, left)
2970
2971# one hex digit of a unicode escape
2972def uni.step(st: St, +cc: Char, back: Lex) -> St:
2973  St{bad, rows, heads, here, parts, buf, lex, b, qkind, stack, hold, +uni, +left, arrtab,
2974    lead} = st
2975  uni.go(dig.ok(dig.val(cc), 16),
2976    St{bad, rows, heads, here, parts, buf, lex, b, qkind, stack, hold, uni, left, arrtab,
2977      lead}, cc, back, uni, left)
2978
2979# a long unicode escape, or an unknown escape
2980def esc.uu(uu: Bool) -> Esc:
2981  match uu:
2982    case True{}:
2983      EUni{8}
2984    case False{}:
2985      EBad{}
2986
2987# a unicode escape
2988def esc.u(uuu: Bool, uu: Bool) -> Esc:
2989  match uuu:
2990    case True{}:
2991      EUni{4}
2992    case False{}:
2993      esc.uu(uu)
2994
2995# carriage return or a unicode escape
2996def esc.r(rr: Bool, uuu: Bool, uu: Bool) -> Esc:
2997  match rr:
2998    case True{}:
2999      EChar{'\r'}
3000    case False{}:
3001      esc.u(uuu, uu)
3002
3003# form feed or the rest
3004def esc.f(ff: Bool, rr: Bool, uuu: Bool, uu: Bool) -> Esc:
3005  match ff:
3006    case True{}:
3007      EChar{Chr{12}}
3008    case False{}:
3009      esc.r(rr, uuu, uu)
3010
3011# newline or the rest
3012def esc.n(nn: Bool, ff: Bool, rr: Bool, uuu: Bool, uu: Bool) -> Esc:
3013  match nn:
3014    case True{}:
3015      EChar{'\n'}
3016    case False{}:
3017      esc.f(ff, rr, uuu, uu)
3018
3019# tab, newline, form feed, carriage return, or a unicode escape
3020def esc.t(tt: Bool, nn: Bool, ff: Bool, rr: Bool, uuu: Bool, uu: Bool) -> Esc:
3021  match tt:
3022    case True{}:
3023      EChar{'\t'}
3024    case False{}:
3025      esc.n(nn, ff, rr, uuu, uu)
3026
3027# backslash, quotation mark, or a letter escape
3028def esc.letter(bb: Bool, tt: Bool, nn: Bool, ff: Bool, rr: Bool, uuu: Bool, uu: Bool) -> Esc:
3029  match bb:
3030    case True{}:
3031      EChar{Chr{8}}
3032    case False{}:
3033      esc.t(tt, nn, ff, rr, uuu, uu)
3034
3035# spaces before the newline of a line-ending backslash
3036def esc.sp(sp: Bool, bb: Bool, tt: Bool, nn: Bool, ff: Bool, rr: Bool, uuu: Bool, uu: Bool) -> Esc:
3037  match sp:
3038    case True{}:
3039      EFold{False{}}
3040    case False{}:
3041      esc.letter(bb, tt, nn, ff, rr, uuu, uu)
3042
3043# a line-ending backslash, or a letter
3044def esc.fold(nl: Bool, sp: Bool, bb: Bool, tt: Bool, nn: Bool, ff: Bool, rr: Bool, uuu: Bool, uu: Bool) -> Esc:
3045  match nl:
3046    case True{}:
3047      EFold{True{}}
3048    case False{}:
3049      esc.sp(sp, bb, tt, nn, ff, rr, uuu, uu)
3050
3051# a backslash or a letter
3052def esc.bs(bs: Bool, bb: Bool, tt: Bool, nn: Bool, ff: Bool, rr: Bool, uuu: Bool, uu: Bool, nl: Bool, sp: Bool) -> Esc:
3053  match bs:
3054    case True{}:
3055      EChar{'\\'}
3056    case False{}:
3057      esc.fold(nl, sp, bb, tt, nn, ff, rr, uuu, uu)
3058
3059# a quote, a backslash, or a letter
3060def esc.of.go(
3061  qq: Bool,
3062  bs: Bool,
3063  bb: Bool,
3064  tt: Bool,
3065  nn: Bool,
3066  ff: Bool,
3067  rr: Bool,
3068  uuu: Bool,
3069  uu: Bool,
3070  nl: Bool,
3071  sp: Bool
3072) -> Esc:
3073  match qq:
3074    case True{}:
3075      EChar{'"'}
3076    case False{}:
3077      esc.bs(bs, bb, tt, nn, ff, rr, uuu, uu, nl, sp)
3078
3079# classify one escaped character
3080def esc.of(+cc: Char) -> Esc:
3081  esc.of.go(Char.is_eq(cc, '"'), Char.is_eq(cc, '\\'), Char.is_eq(cc, 'b'),
3082    Char.is_eq(cc, 't'), Char.is_eq(cc, 'n'), Char.is_eq(cc, 'f'), Char.is_eq(cc, 'r'),
3083    Char.is_eq(cc, 'u'), Char.is_eq(cc, 'U'), ch.nl(cc), ch.sp(cc))
3084
3085# the lex state that reads the hex digits of an escape
3086def esc.uni.lex(back: Lex) -> Lex:
3087  match back:
3088    case LKeyQ{}:
3089      LKeyU{}
3090    case LHeadQ{}:
3091      LHeadU{}
3092    case _:
3093      LUni{}
3094
3095# a unicode escape starts with no digits seen
3096def esc.uni(st: St, back: Lex, nn: U32) -> St:
3097  St{bad, rows, heads, here, parts, buf, _lex, b, qkind, stack, hold, _uni, _left,
3098    arrtab, lead} = st
3099  St{bad, rows, heads, here, parts, buf, esc.uni.lex(back), b, qkind, stack, hold, 0, nn,
3100    arrtab, lead}
3101
3102# 1 once a newline has been seen
3103def esc.fold.bit(saw: Bool) -> U32:
3104  match saw:
3105    case True{}:
3106      1
3107    case False{}:
3108      0
3109
3110# a line-ending backslash skips following whitespace
3111def esc.fold.on(st: St, saw: Bool) -> St:
3112  St{bad, rows, heads, here, parts, buf, _lex, b, qkind, stack, hold, _uni, _left,
3113    arrtab, lead} = st
3114  St{bad, rows, heads, here, parts, buf, LFold{}, b, qkind, stack, hold, 0,
3115    esc.fold.bit(saw), arrtab, lead}
3116
3117# a line-ending backslash is only part of a multiline string
3118def esc.fold.kind(multi: Bool, st: St, saw: Bool) -> St:
3119  match multi:
3120    case True{}:
3121      esc.fold.on(st, saw)
3122    case False{}:
3123      st.err(st, "invalid escape")
3124
3125# a line-ending backslash is only part of a multiline string
3126def esc.fold.str(st: St, saw: Bool) -> St:
3127  St{bad, rows, heads, here, parts, buf, lex, b, +qkind, stack, hold, uni, left,
3128    arrtab, lead} = st
3129  esc.fold.kind(q.multi(qkind), St{bad, rows, heads, here, parts, buf, lex, b, qkind,
3130    stack, hold, uni, left, arrtab, lead}, saw)
3131
3132# a line-ending backslash is only part of a string
3133def esc.fold.use(back: Lex, st: St, saw: Bool) -> St:
3134  match back:
3135    case LStr{}:
3136      esc.fold.str(st, saw)
3137    case _:
3138      st.err(st, "invalid escape")
3139
3140# apply one escape and return to the string
3141def esc.use(ee: Esc, st: St, back: Lex) -> St:
3142  match ee:
3143    case EChar{c}:
3144      st.push(st, c, back)
3145    case EUni{n}:
3146      esc.uni(st, back, n)
3147    case EFold{saw}:
3148      esc.fold.use(back, st, saw)
3149    case EBad{}:
3150      st.err(st, "invalid escape")
3151
3152# the lex state a comment returns to
3153def com.enter(st: St, back: Lex) -> St:
3154  St{bad, rows, heads, here, parts, buf, _lex, _back, qkind, stack, hold, uni, left,
3155    arrtab, lead} = st
3156  St{bad, rows, heads, here, parts, buf, LCom{}, back, qkind, stack, hold, uni, left,
3157    arrtab, lead}
3158
3159# a bare key, or a rejected character
3160def lex.top.bare(bare: Bool, st: St, cc: Char) -> St:
3161  match bare:
3162    case True{}:
3163      st.push(st, cc, LKey{})
3164    case False{}:
3165      st.err(st, "invalid key")
3166
3167# a header starts with a clear key
3168def lex.bracket(st: St) -> St:
3169  St{bad, rows, heads, here, _parts, _buf, _lex, back, qkind, stack, hold, uni, left,
3170    _arr, lead} = st
3171  St{bad, rows, heads, here, [], [], LHead{}, back, qkind, stack, hold, uni, left,
3172    False{}, lead}
3173
3174# a quoted key starts with an empty buffer
3175def lex.qkey(st: St, kind: QKind, lex: Lex) -> St:
3176  St{bad, rows, heads, here, parts, _buf, _lex, back, _q, stack, hold, uni, left, arrtab,
3177    lead} = st
3178  St{bad, rows, heads, here, parts, [], lex, back, kind, stack, hold, uni, left, arrtab,
3179    lead}
3180
3181# a literal key or a bare key
3182def lex.top.lit(lit: Bool, bare: Bool, st: St, cc: Char) -> St:
3183  match lit:
3184    case True{}:
3185      lex.qkey(st, QLit{}, LKeyQ{})
3186    case False{}:
3187      lex.top.bare(bare, st, cc)
3188
3189# a quoted key or a bare key
3190def lex.top.q(qq: Bool, lit: Bool, bare: Bool, st: St, cc: Char) -> St:
3191  match qq:
3192    case True{}:
3193      lex.qkey(st, QBasic{}, LKeyQ{})
3194    case False{}:
3195      lex.top.lit(lit, bare, st, cc)
3196
3197# a header or a key
3198def lex.top.br(br: Bool, qq: Bool, lit: Bool, bare: Bool, st: St, cc: Char) -> St:
3199  match br:
3200    case True{}:
3201      lex.bracket(st)
3202    case False{}:
3203      lex.top.q(qq, lit, bare, st, cc)
3204
3205# a comment, a header, or a key
3206def lex.top.hash(hash: Bool, br: Bool, qq: Bool, lit: Bool, bare: Bool, st: St, cc: Char) -> St:
3207  match hash:
3208    case True{}:
3209      com.enter(st, LTop{})
3210    case False{}:
3211      lex.top.br(br, qq, lit, bare, st, cc)
3212
3213# a newline, a comment, a header, or a key
3214def lex.top.nl(nl: Bool, hash: Bool, br: Bool, qq: Bool, lit: Bool, bare: Bool, st: St, cc: Char) -> St:
3215  match nl:
3216    case True{}:
3217      st
3218    case False{}:
3219      lex.top.hash(hash, br, qq, lit, bare, st, cc)
3220
3221# whitespace, a comment, a header, or a key
3222def lex.top.go(sp: Bool, nl: Bool, hash: Bool, br: Bool, qq: Bool, lit: Bool, bare: Bool, st: St, cc: Char) -> St:
3223  match sp:
3224    case True{}:
3225      st
3226    case False{}:
3227      lex.top.nl(nl, hash, br, qq, lit, bare, st, cc)
3228
3229# top level: a key, a header, a comment, or whitespace
3230def lex.top(st: St, +cc: Char) -> St:
3231  lex.top.go(ch.sp(cc), ch.nl(cc), Char.is_eq(cc, '#'), Char.is_eq(cc, '['),
3232    Char.is_eq(cc, '"'), Char.is_eq(cc, '\''), bare.at(cc), st, cc)
3233
3234# a newline before equals is rejected
3235def lex.key.nl(nl: Bool, st: St, _c: Char) -> St:
3236  match nl:
3237    case True{}:
3238      st.err(st, "newline in key")
3239    case False{}:
3240      st.err(st, "invalid key")
3241
3242# an empty segment is rejected
3243def lex.key.end.go(empty: Bool, st: St, lex: Lex) -> St:
3244  match empty:
3245    case True{}:
3246      st.err(st, "empty key")
3247    case False{}:
3248      seg.push(st, lex)
3249
3250# end a nonempty segment
3251def lex.key.end(st: St, next: Lex) -> St:
3252  St{bad, rows, heads, here, parts, +buf, lx, back, qkind, stack, hold, uni, left,
3253    arrtab, lead} = st
3254  lex.key.end.go(List.is_empty(&2, Char, buf),
3255    St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left,
3256      arrtab, lead}, next)
3257
3258# a comment ends the segment and waits for equals
3259def lex.key.hash(hash: Bool, nl: Bool, st: St, cc: Char) -> St:
3260  match hash:
3261    case True{}:
3262      com.enter(lex.key.end(st, LAfter{}), LAfter{})
3263    case False{}:
3264      lex.key.nl(nl, st, cc)
3265
3266# an equals ends the key
3267def lex.key.eq(eq: Bool, hash: Bool, nl: Bool, st: St, +cc: Char) -> St:
3268  match eq:
3269    case True{}:
3270      lex.key.end(st, LVal{})
3271    case False{}:
3272      lex.key.hash(hash, nl, st, cc)
3273
3274# a dot ends the segment and skips whitespace before the next one
3275def lex.key.dot(dot: Bool, eq: Bool, hash: Bool, nl: Bool, st: St, cc: Char) -> St:
3276  match dot:
3277    case True{}:
3278      lex.key.end(st, LKeyDot{})
3279    case False{}:
3280      lex.key.eq(eq, hash, nl, st, cc)
3281
3282# whitespace ends the segment
3283def lex.key.sp(sp: Bool, dot: Bool, eq: Bool, hash: Bool, nl: Bool, st: St, cc: Char) -> St:
3284  match sp:
3285    case True{}:
3286      lex.key.end(st, LAfter{})
3287    case False{}:
3288      lex.key.dot(dot, eq, hash, nl, st, cc)
3289
3290# a bare character, whitespace, a dot, or an equals
3291def lex.key.go(bare: Bool, sp: Bool, dot: Bool, eq: Bool, hash: Bool, nl: Bool, st: St, cc: Char) -> St:
3292  match bare:
3293    case True{}:
3294      st.push(st, cc, LKey{})
3295    case False{}:
3296      lex.key.sp(sp, dot, eq, hash, nl, st, cc)
3297
3298# inside a bare key segment
3299def lex.key(st: St, +cc: Char) -> St:
3300  lex.key.go(bare.at(cc), ch.sp(cc), Char.is_eq(cc, '.'), Char.is_eq(cc, '='),
3301    Char.is_eq(cc, '#'), ch.nl(cc), st, cc)
3302
3303# a newline before equals is rejected
3304def lex.after.nl(nl: Bool, st: St, _c: Char) -> St:
3305  match nl:
3306    case True{}:
3307      st.err(st, "newline in key")
3308    case False{}:
3309      st.err(st, "invalid key")
3310
3311# a comment waits for equals
3312def lex.after.hash(hash: Bool, nl: Bool, st: St, cc: Char) -> St:
3313  match hash:
3314    case True{}:
3315      com.enter(st, LAfter{})
3316    case False{}:
3317      lex.after.nl(nl, st, cc)
3318
3319# equals starts the value
3320def lex.after.eq(eq: Bool, hash: Bool, nl: Bool, st: St, cc: Char) -> St:
3321  match eq:
3322    case True{}:
3323      st.lex(st, LVal{})
3324    case False{}:
3325      lex.after.hash(hash, nl, st, cc)
3326
3327# a dot starts the next segment, after any whitespace
3328def lex.after.dot(dot: Bool, eq: Bool, hash: Bool, nl: Bool, st: St, cc: Char) -> St:
3329  match dot:
3330    case True{}:
3331      st.lex(st, LKeyDot{})
3332    case False{}:
3333      lex.after.eq(eq, hash, nl, st, cc)
3334
3335# whitespace, a dot, or an equals
3336def lex.after.go(sp: Bool, dot: Bool, eq: Bool, hash: Bool, nl: Bool, st: St, cc: Char) -> St:
3337  match sp:
3338    case True{}:
3339      st
3340    case False{}:
3341      lex.after.dot(dot, eq, hash, nl, st, cc)
3342
3343# after a key segment, before equals or a dot
3344def lex.after(st: St, +cc: Char) -> St:
3345  lex.after.go(ch.sp(cc), Char.is_eq(cc, '.'), Char.is_eq(cc, '='), Char.is_eq(cc, '#'),
3346    ch.nl(cc), st, cc)
3347
3348# a value starts on the line of its key
3349def lex.val.nl3(inside: Bool, st: St) -> St:
3350  match inside:
3351    case True{}:
3352      st.err(st, "newline in inline table")
3353    case False{}:
3354      st.err(st, "newline before value")
3355
3356# a newline before a value is rejected
3357def lex.val.nl2(st: St, _c: Char) -> St:
3358  St{bad, rows, heads, here, parts, buf, lx, back, qkind, +stack, hold, uni, left,
3359    arrtab, lead} = st
3360  lex.val.nl3(inl.open(stack),
3361    St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left,
3362      arrtab, lead})
3363
3364# an array starts a frame and waits for a value
3365def lex.array(st: St) -> St:
3366  St{bad, rows, heads, +here, +parts, _buf, _lex, back, qkind, stack, hold, uni, left,
3367    arrtab, lead} = st
3368  St{bad, rows, heads, here, [], [], LArr{}, back, qkind,
3369    CArr{[], parts, here} <> stack, hold, uni, left, arrtab, lead}
3370
3371# an inline table starts a frame and waits for a key
3372def lex.inline(st: St) -> St:
3373  St{bad, rows, heads, +here, +parts, _buf, _lex, back, qkind, stack, hold, uni, left,
3374    arrtab, lead} = st
3375  St{bad, rows, heads, here, [], [], LInl{}, back, qkind,
3376    CInl{[], parts, here} <> stack, hold, uni, left, arrtab, lead}
3377
3378# an inline table, or a bare value
3379def lex.val.inl(inl: Bool, st: St, cc: Char) -> St:
3380  match inl:
3381    case True{}:
3382      lex.inline(st)
3383    case False{}:
3384      st.push(st, cc, LBare{})
3385
3386# an array, or another value
3387def lex.val.br(br: Bool, inl: Bool, st: St, cc: Char) -> St:
3388  match br:
3389    case True{}:
3390      lex.array(st)
3391    case False{}:
3392      lex.val.inl(inl, st, cc)
3393
3394# a literal string, or another value
3395def lex.val.lit(lit: Bool, br: Bool, inl: Bool, st: St, cc: Char) -> St:
3396  match lit:
3397    case True{}:
3398      lex.qkey(st, QLit{}, LQ{})
3399    case False{}:
3400      lex.val.br(br, inl, st, cc)
3401
3402# a basic string, or another value
3403def lex.val.q(qq: Bool, lit: Bool, br: Bool, inl: Bool, st: St, cc: Char) -> St:
3404  match qq:
3405    case True{}:
3406      lex.qkey(st, QBasic{}, LQ{})
3407    case False{}:
3408      lex.val.lit(lit, br, inl, st, cc)
3409
3410# a comment, a string, an array, an inline table, or a bare value
3411def lex.val.hash(hash: Bool, qq: Bool, lit: Bool, br: Bool, inl: Bool, st: St, cc: Char) -> St:
3412  match hash:
3413    case True{}:
3414      com.enter(st, LVal{})
3415    case False{}:
3416      lex.val.q(qq, lit, br, inl, st, cc)
3417
3418# a newline before a value is rejected
3419def lex.val.nl(nl: Bool, hash: Bool, qq: Bool, lit: Bool, br: Bool, inl: Bool, st: St, cc: Char) -> St:
3420  match nl:
3421    case True{}:
3422      lex.val.nl2(st, cc)
3423    case False{}:
3424      lex.val.hash(hash, qq, lit, br, inl, st, cc)
3425
3426# whitespace or the value itself
3427def lex.val.go(sp: Bool, nl: Bool, hash: Bool, qq: Bool, lit: Bool, br: Bool, inl: Bool, st: St, cc: Char) -> St:
3428  match sp:
3429    case True{}:
3430      st
3431    case False{}:
3432      lex.val.nl(nl, hash, qq, lit, br, inl, st, cc)
3433
3434# the start of a value
3435def lex.val(st: St, +cc: Char) -> St:
3436  lex.val.go(ch.sp(cc), ch.nl(cc), Char.is_eq(cc, '#'), Char.is_eq(cc, '"'),
3437    Char.is_eq(cc, '\''), Char.is_eq(cc, '['), Char.is_eq(cc, '{'), st, cc)
3438
3439# a second quote may start a multiline string; otherwise the first character is held
3440def lex.q.go(same: Bool, st: St, cc: Char) -> St:
3441  match same:
3442    case True{}:
3443      st.lex(st, LQ2{})
3444    case False{}:
3445      st.hold(st.lex(st, LStr{}), LStr{}, cc)
3446
3447# the first quote has been seen
3448def lex.q(st: St, +cc: Char) -> St:
3449  St{bad, rows, heads, here, parts, buf, lx, back, +qkind, stack, hold, uni, left,
3450    arrtab, lead} = st
3451  lex.q.go(Char.is_eq(cc, q.char(qkind)),
3452    St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left,
3453      arrtab, lead}, cc)
3454
3455# a multiline string, about to trim one opening newline
3456def lex.multi(st: St, kind: QKind) -> St:
3457  St{bad, rows, heads, here, parts, buf, _lex, back, _q, stack, hold, uni, left, arrtab,
3458    lead} = st
3459  St{bad, rows, heads, here, parts, buf, LTrim{}, back, q.as.multi(kind), stack, hold,
3460    uni, left, arrtab, lead}
3461
3462# a third quote starts a multiline string; two quotes are an empty string
3463def lex.q2.go(same: Bool, st: St, cc: Char, kind: QKind) -> St:
3464  match same:
3465    case True{}:
3466      lex.multi(st, kind)
3467    case False{}:
3468      bare.hold(val.take(st, VStr{""}), cc, True{})
3469
3470# two quotes have been seen
3471def lex.q2(st: St, +cc: Char) -> St:
3472  St{bad, rows, heads, here, parts, buf, lx, back, +qkind, stack, hold, uni, left,
3473    arrtab, lead} = st
3474  lex.q2.go(Char.is_eq(cc, q.char(qkind)),
3475    St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left,
3476      arrtab, lead}, cc, qkind)
3477
3478# a line feed is trimmed; any other character is the first of the string
3479def lex.trim.nl(nl: Bool, st: St, cc: Char) -> St:
3480  match nl:
3481    case True{}:
3482      st.lex(st, LStr{})
3483    case False{}:
3484      st.hold(st.lex(st, LStr{}), LStr{}, cc)
3485
3486# a carriage return may still have a line feed after it
3487def lex.trim.go(cr: Bool, nl: Bool, st: St, cc: Char) -> St:
3488  match cr:
3489    case True{}:
3490      st.lex(st, LTrim2{})
3491    case False{}:
3492      lex.trim.nl(nl, st, cc)
3493
3494# trim one opening newline of a multiline string
3495def lex.trim(st: St, +cc: Char) -> St:
3496  lex.trim.go(U32.is_eq(Char.to_u32(cc), 13), ch.nl(cc), st, cc)
3497
3498# the line feed of a CRLF opening newline
3499def lex.trim2.go(lf: Bool, st: St, cc: Char) -> St:
3500  match lf:
3501    case True{}:
3502      st.lex(st, LStr{})
3503    case False{}:
3504      st.hold(st.lex(st, LStr{}), LStr{}, cc)
3505
3506# the line feed of a CRLF opening newline
3507def lex.trim2(st: St, +cc: Char) -> St:
3508  lex.trim2.go(U32.is_eq(Char.to_u32(cc), 10), st, cc)
3509
3510# a forbidden control, or one character of the string
3511def lex.str.char.go(bad: Bool, st: St, cc: Char) -> St:
3512  match bad:
3513    case True{}:
3514      st.err(st, "invalid control")
3515    case False{}:
3516      st.push(st, cc, LStr{})
3517
3518# a raw character, rejected when it is a forbidden control
3519def lex.str.char(multi: Bool, st: St, +cc: Char) -> St:
3520  lex.str.char.go(str.bad(Char.to_u32(cc), multi), st, cc)
3521
3522# an escape, or a plain character
3523def lex.str.bs(bs: Bool, multi: Bool, st: St, cc: Char, _kind: QKind) -> St:
3524  match bs:
3525    case True{}:
3526      st.lex(st, LEsc{})
3527    case False{}:
3528      lex.str.char(multi, st, cc)
3529
3530# a backslash starts an escape in a basic string
3531def lex.str.esc(basic: Bool, multi: Bool, st: St, +cc: Char, kind: QKind) -> St:
3532  match basic:
3533    case True{}:
3534      lex.str.bs(Char.is_eq(cc, '\\'), multi, st, cc, kind)
3535    case False{}:
3536      lex.str.char(multi, st, cc)
3537
3538# count closing quotes of a multiline string
3539def lex.mq(st: St, nn: U32) -> St:
3540  St{bad, rows, heads, here, parts, buf, _lex, back, qkind, stack, hold, _uni, _left,
3541    arrtab, lead} = st
3542  St{bad, rows, heads, here, parts, buf, LMq{}, back, qkind, stack, hold, 0, nn, arrtab,
3543    lead}
3544
3545# one quote closes a one-line string and may close a multiline string
3546def lex.str.quote(multi: Bool, st: St) -> St:
3547  match multi:
3548    case False{}:
3549      str.fin(st)
3550    case True{}:
3551      lex.mq(st, 1)
3552
3553# a quote, an escape, or a character
3554def lex.str.go(quote: Bool, multi: Bool, basic: Bool, st: St, +cc: Char, kind: QKind) -> St:
3555  match quote:
3556    case True{}:
3557      lex.str.quote(multi, st)
3558    case False{}:
3559      lex.str.esc(basic, multi, st, cc, kind)
3560
3561# inside a string
3562def lex.str(st: St, +cc: Char) -> St:
3563  St{bad, rows, heads, here, parts, buf, lx, back, +qkind, stack, hold, uni, left,
3564    arrtab, lead} = st
3565  lex.str.go(Char.is_eq(cc, q.char(qkind)), q.multi(qkind), q.basic(qkind),
3566    St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left,
3567      arrtab, lead}, cc, qkind)
3568
3569# a closing delimiter has been read. up to two more quotes are still the string's
3570def lex.mq.shut(st: St) -> St:
3571  St{bad, rows, heads, here, parts, buf, _lex, back, qkind, stack, hold, uni, _left,
3572    arrtab, lead} = st
3573  St{bad, rows, heads, here, parts, buf, LMqEnd{}, back, qkind, stack, hold, uni, 0,
3574    arrtab, lead}
3575
3576# the second quote waits; the third is a closing delimiter
3577def lex.mq.one(one: Bool, st: St) -> St:
3578  match one:
3579    case True{}:
3580      lex.mq(st, 2)
3581    case False{}:
3582      lex.mq.shut(st)
3583
3584# quotes that were not a closer return to the string, and the character is held
3585def lex.mq.back(st: St, cc: Char, buf: List<&2, Char>) -> St:
3586  St{bad, rows, heads, here, parts, _buf, _lex, back, qkind, stack, _hold, uni, _left,
3587    arrtab, lead} = st
3588  St{bad, rows, heads, here, parts, buf, LStr{}, back, qkind, stack, HChar{cc}, uni, 0,
3589    arrtab, lead}
3590
3591# a quote continues the closer; anything else is content
3592def lex.mq.go(quote: Bool, one: Bool, st: St, cc: Char, buf: List<&2, Char>, kind: QKind, _left: U32) -> St:
3593  match quote:
3594    case True{}:
3595      lex.mq.one(one, st)
3596    case False{}:
3597      lex.mq.back(st, cc, mq.put(one, q.char(kind), buf))
3598
3599# one character while closing a multiline string
3600def lex.mq.step(st: St, +cc: Char) -> St:
3601  St{bad, rows, heads, here, parts, +buf, lx, back, +qkind, stack, hold, uni, +left,
3602    arrtab, lead} = st
3603  lex.mq.go(Char.is_eq(cc, q.char(qkind)), U32.is_eq(left, 1),
3604    St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left,
3605      arrtab, lead}, cc, buf, qkind, left)
3606
3607# a quote after the closing delimiter: the delimiter moves one quote on
3608def lex.mq.more(st: St, cc: Char) -> St:
3609  St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left, arrtab,
3610    lead} = st
3611  St{bad, rows, heads, here, parts, cc <> buf, lx, back, qkind, stack, hold, uni,
3612    U32.add(left, 1), arrtab, lead}
3613
3614# the string ends before this character, which the next state reads
3615def lex.mq.fin(st: St, cc: Char) -> St:
3616  bare.hold(str.fin(st), cc, True{})
3617
3618# a third quote after the delimiter would make three in the string
3619def lex.mq.room(room: Bool, st: St, cc: Char) -> St:
3620  match room:
3621    case True{}:
3622      lex.mq.more(st, cc)
3623    case False{}:
3624      lex.mq.fin(st, cc)
3625
3626# a quote may still belong to the string; anything else follows it
3627def lex.mq.end.go(quote: Bool, room: Bool, st: St, cc: Char) -> St:
3628  match quote:
3629    case True{}:
3630      lex.mq.room(room, st, cc)
3631    case False{}:
3632      lex.mq.fin(st, cc)
3633
3634# one character after a multiline string's closing delimiter
3635def lex.mq.end(st: St, +cc: Char) -> St:
3636  St{bad, rows, heads, here, parts, buf, lx, back, +qkind, stack, hold, uni, +left,
3637    arrtab, lead} = st
3638  lex.mq.end.go(Char.is_eq(cc, q.char(qkind)), U32.is_lt(left, 2),
3639    St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left,
3640      arrtab, lead}, cc)
3641
3642# one escaped character
3643def lex.esc(st: St, +cc: Char) -> St:
3644  esc.use(esc.of(cc), st, LStr{})
3645
3646# remember that a newline was seen
3647def lex.fold.saw(st: St) -> St:
3648  St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, hold, uni, _left,
3649    arrtab, lead} = st
3650  St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, hold, uni, 1, arrtab,
3651    lead}
3652
3653# a character before the newline is rejected
3654def lex.fold.end.go(saw: Bool, st: St, cc: Char) -> St:
3655  match saw:
3656    case True{}:
3657      st.hold(st.lex(st, LStr{}), LStr{}, cc)
3658    case False{}:
3659      st.err(st, "invalid escape")
3660
3661# the next character ends the fold only after a newline
3662def lex.fold.end(st: St, cc: Char) -> St:
3663  St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, +left,
3664    arrtab, lead} = st
3665  lex.fold.end.go(U32.is_eq(left, 1),
3666    St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left,
3667      arrtab, lead}, cc)
3668
3669# a newline has been seen, so later whitespace may still be skipped
3670def lex.fold.nl(nl: Bool, st: St, cc: Char) -> St:
3671  match nl:
3672    case True{}:
3673      lex.fold.saw(st)
3674    case False{}:
3675      lex.fold.end(st, cc)
3676
3677# more whitespace, or the next character of the string
3678def lex.fold.go(sp: Bool, nl: Bool, st: St, cc: Char) -> St:
3679  match sp:
3680    case True{}:
3681      st
3682    case False{}:
3683      lex.fold.nl(nl, st, cc)
3684
3685# whitespace after a line-ending backslash
3686def lex.fold(st: St, +cc: Char) -> St:
3687  lex.fold.go(ch.sp(cc), ch.nl(cc), st, cc)
3688
3689# keep the space only when the buffer is a date; otherwise it ends the token
3690def lex.bare.date.go(date: Bool, st: St, cc: Char) -> St:
3691  match date:
3692    case True{}:
3693      st.lex(st, LDate{})
3694    case False{}:
3695      bare.finish(st, cc, False{})
3696
3697# a date may continue after one space
3698def lex.bare.date(st: St, cc: Char) -> St:
3699  St{bad, rows, heads, here, parts, +buf, lx, back, qkind, stack, hold, uni, left,
3700    arrtab, lead} = st
3701  lex.bare.date.go(date.shaped(buf),
3702    St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left,
3703      arrtab, lead}, cc)
3704
3705# a newline inside an inline table is held, and so is any other delimiter
3706def lex.bare.hold(skip: Bool, nl: Bool, inside: Bool) -> Bool:
3707  Bool.or(Bool.not(skip), Bool.and(nl, inside))
3708
3709# a delimiter other than a date-space is held unless it is whitespace
3710def lex.bare.end(st: St, +cc: Char) -> St:
3711  St{bad, rows, heads, here, parts, buf, lx, back, qkind, +stack, hold, uni, left,
3712    arrtab, lead} = st
3713  bare.finish(St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold,
3714    uni, left, arrtab, lead}, cc, lex.bare.hold(ch.skip(cc), ch.nl(cc), inl.open(stack)))
3715
3716# a space may be the space inside a datetime
3717def lex.bare.sp(sp: Bool, st: St, cc: Char) -> St:
3718  match sp:
3719    case True{}:
3720      lex.bare.date(st, cc)
3721    case False{}:
3722      lex.bare.end(st, cc)
3723
3724# a delimiter ends the token
3725def lex.bare.go(delim: Bool, sp: Bool, st: St, cc: Char) -> St:
3726  match delim:
3727    case False{}:
3728      st.push(st, cc, LBare{})
3729    case True{}:
3730      lex.bare.sp(sp, st, cc)
3731
3732# a bare value
3733def lex.bare(st: St, +cc: Char) -> St:
3734  lex.bare.go(ch.delim(cc), ch.space(cc), st, cc)
3735
3736# the space and the digit belong to the datetime
3737def lex.date.digit(st: St, cc: Char) -> St:
3738  St{bad, rows, heads, here, parts, buf, _lex, back, qkind, stack, hold, uni, left,
3739    arrtab, lead} = st
3740  St{bad, rows, heads, here, parts, cc <> (' ' <> buf), LBare{}, back, qkind, stack, hold,
3741    uni, left, arrtab, lead}
3742
3743# the character after the space of a possible datetime
3744def lex.date.go(digit: Bool, st: St, cc: Char) -> St:
3745  match digit:
3746    case True{}:
3747      lex.date.digit(st, cc)
3748    case False{}:
3749      bare.finish(st, cc, True{})
3750
3751# the character after the space of a possible datetime
3752def lex.date(st: St, +cc: Char) -> St:
3753  lex.date.go(Char.is_digit(cc), st, cc)
3754
3755# the newline is read again in the state that was waiting
3756def lex.com.nl(st: St, cc: Char) -> St:
3757  St{bad, rows, heads, here, parts, buf, _lex, +back, qkind, stack, _hold, uni, left,
3758    arrtab, lead} = st
3759  St{bad, rows, heads, here, parts, buf, back, back, qkind, stack, HChar{cc}, uni, left,
3760    arrtab, lead}
3761
3762# tab is the one control a comment may hold
3763def lex.com.tab(tab: Bool, st: St) -> St:
3764  match tab:
3765    case True{}:
3766      st
3767    case False{}:
3768      st.err(st, "invalid control in comment")
3769
3770# any other character is part of the comment
3771def lex.com.ctl(ctl: Bool, tab: Bool, st: St) -> St:
3772  match ctl:
3773    case False{}:
3774      st
3775    case True{}:
3776      lex.com.tab(tab, st)
3777
3778# a comment runs to the end of the line and holds no control but tab
3779def lex.com.go(nl: Bool, ctl: Bool, tab: Bool, st: St, cc: Char) -> St:
3780  match nl:
3781    case False{}:
3782      lex.com.ctl(ctl, tab, st)
3783    case True{}:
3784      lex.com.nl(st, cc)
3785
3786# a comment runs to the end of the line
3787def lex.com(st: St, +cc: Char) -> St:
3788  lex.com.go(ch.nl(cc), ch.ctl(cc), U32.is_eq(Char.to_u32(cc), 9), st, cc)
3789
3790# the header is an array of tables
3791def lex.head.arr(st: St) -> St:
3792  St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, hold, uni, left, _arr,
3793    lead} = st
3794  St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, hold, uni, left,
3795    True{}, lead}
3796
3797# one extra bracket
3798def lex.head.br2(once: Bool, st: St) -> St:
3799  match once:
3800    case False{}:
3801      st.err(st, "invalid header")
3802    case True{}:
3803      lex.head.arr(st)
3804
3805# the second bracket is only legal at the start
3806def lex.head.br.go(fresh: Bool, once: Bool, st: St) -> St:
3807  match fresh:
3808    case False{}:
3809      st.err(st, "invalid header")
3810    case True{}:
3811      lex.head.br2(once, st)
3812
3813# [[ opens an array of tables when the key has not started
3814def lex.head.br(st: St) -> St:
3815  St{bad, rows, heads, here, +parts, +buf, lx, back, qkind, stack, hold, uni, left,
3816    +arrtab, lead} = st
3817  lex.head.br.go(Bool.and(List.is_empty(&2, String, parts),
3818    List.is_empty(&2, Char, buf)), Bool.not(arrtab),
3819    St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left,
3820      arrtab, lead})
3821
3822# between segments a dot is required
3823def lex.head.ch.go(gap: Bool, st: St, cc: Char) -> St:
3824  match gap:
3825    case True{}:
3826      st.err(st, "invalid header")
3827    case False{}:
3828      st.push(st, cc, LHead{})
3829
3830# a bare character continues the segment, or starts one at the beginning
3831def lex.head.ch(st: St, cc: Char) -> St:
3832  St{bad, rows, heads, here, +parts, +buf, lx, back, qkind, stack, hold, uni, left,
3833    arrtab, lead} = st
3834  lex.head.ch.go(Bool.and(Bool.not(List.is_empty(&2, String, parts)),
3835    List.is_empty(&2, Char, buf)),
3836    St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left,
3837      arrtab, lead}, cc)
3838
3839# whitespace with no segment open still needs a segment after it, so a second
3840# bracket there is refused: `[[` is two brackets with nothing between
3841def lex.head.gap.go(empty: Bool, st: St) -> St:
3842  match empty:
3843    case True{}:
3844      st.lex(st, LHeadDot{})
3845    case False{}:
3846      seg.push(st, LHeadGap{})
3847
3848# whitespace ends a segment when one is open
3849def lex.head.gap(st: St) -> St:
3850  St{bad, rows, heads, here, parts, +buf, lx, back, qkind, stack, hold, uni, left,
3851    arrtab, lead} = st
3852  lex.head.gap.go(List.is_empty(&2, Char, buf),
3853    St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left,
3854      arrtab, lead})
3855
3856# a dot with no segment is rejected
3857def lex.head.dot3(empty: Bool, st: St) -> St:
3858  match empty:
3859    case True{}:
3860      st.err(st, "empty key")
3861    case False{}:
3862      seg.push(st, LHeadDot{})
3863
3864# a dot ends the open segment
3865def lex.head.dot2(st: St) -> St:
3866  St{bad, rows, heads, here, parts, +buf, lx, back, qkind, stack, hold, uni, left,
3867    arrtab, lead} = st
3868  lex.head.dot3(List.is_empty(&2, Char, buf),
3869    St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left,
3870      arrtab, lead})
3871
3872# an array of tables still needs one ]
3873def lex.head.close2(arr: Bool, st: St) -> St:
3874  match arr:
3875    case True{}:
3876      st.lex(st, LHeadR{})
3877    case False{}:
3878      head.fin(st)
3879
3880# push the last segment when the buffer holds one
3881def lex.head.close.go(empty: Bool, arr: Bool, st: St) -> St:
3882  match empty:
3883    case True{}:
3884      lex.head.close2(arr, st)
3885    case False{}:
3886      lex.head.close2(arr, seg.push(st, LHead{}))
3887
3888# ] closes, or waits for the second ] of an array of tables
3889def lex.head.close(st: St) -> St:
3890  St{bad, rows, heads, here, parts, +buf, lx, back, qkind, stack, hold, uni, left,
3891    +arrtab, lead} = st
3892  lex.head.close.go(List.is_empty(&2, Char, buf), arrtab,
3893    St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left,
3894      arrtab, lead})
3895
3896# a comment in a header
3897def lex.head.hash(hash: Bool, st: St) -> St:
3898  match hash:
3899    case True{}:
3900      com.enter(st, LHead{})
3901    case False{}:
3902      st.err(st, "invalid header")
3903
3904# a quote opens a segment only where none has started. After a bare character
3905# it would glue two keys into one segment, which toml.abnf does not allow
3906def lex.head.quote.go(fresh: Bool, st: St, kind: QKind) -> St:
3907  match fresh:
3908    case True{}:
3909      lex.qkey(st, kind, LHeadQ{})
3910    case False{}:
3911      st.err(st, "invalid header")
3912
3913# a quoted header segment, right after the bracket
3914def lex.head.quote(st: St, kind: QKind) -> St:
3915  St{bad, rows, heads, here, +parts, +buf, lx, back, qkind, stack, hold, uni, left,
3916    arrtab, lead} = st
3917  lex.head.quote.go(Bool.and(List.is_empty(&2, Char, buf),
3918    List.is_empty(&2, String, parts)),
3919    St{bad, rows, heads, here, parts, buf, lx, back, qkind, stack, hold, uni, left,
3920      arrtab, lead}, kind)
3921
3922# a literal header segment or a comment
3923def lex.head.lit(lit: Bool, hash: Bool, st: St) -> St:
3924  match lit:
3925    case True{}:
3926      lex.head.quote(st, QLit{})
3927    case False{}:
3928      lex.head.hash(hash, st)
3929
3930# a quoted header segment or a comment
3931def lex.head.q(qq: Bool, lit: Bool, hash: Bool, st: St, _c: Char) -> St:
3932  match qq:
3933    case True{}:
3934      lex.head.quote(st, QBasic{})
3935    case False{}:
3936      lex.head.lit(lit, hash, st)
3937
3938# the closing bracket, a quoted key, or a comment
3939def lex.head.end(end: Bool, qq: Bool, lit: Bool, hash: Bool, st: St, cc: Char) -> St:
3940  match end:
3941    case True{}:
3942      lex.head.close(st)
3943    case False{}:
3944      lex.head.q(qq, lit, hash, st, cc)
3945
3946# a dot, the end, or a quoted segment
3947def lex.head.dot(dot: Bool, end: Bool, qq: Bool, lit: Bool, hash: Bool, st: St, cc: Char) -> St:
3948  match dot:
3949    case True{}:
3950      lex.head.dot2(st)
3951    case False{}:
3952      lex.head.end(end, qq, lit, hash, st, cc)
3953
3954# whitespace, a dot, or the closing bracket
3955def lex.head.sp(sp: Bool, dot: Bool, end: Bool, qq: Bool, lit: Bool, hash: Bool, st: St, cc: Char) -> St:
3956  match sp:
3957    case True{}:
3958      lex.head.gap(st)
3959    case False{}:
3960      lex.head.dot(dot, end, qq, lit, hash, st, cc)
3961
3962# a bare character, whitespace, a dot, or the end
3963def lex.head.bare(bare: Bool, sp: Bool, dot: Bool, end: Bool, qq: Bool, lit: Bool, hash: Bool, st: St, cc: Char) -> St:
3964  match bare:
3965    case True{}:
3966      lex.head.ch(st, cc)
3967    case False{}:
3968      lex.head.sp(sp, dot, end, qq, lit, hash, st, cc)
3969
3970# a second bracket, a key character, or whitespace
3971def lex.head.go(
3972  br: Bool,
3973  bare: Bool,
3974  sp: Bool,
3975  dot: Bool,
3976  end: Bool,
3977  qq: Bool,
3978  lit: Bool,
3979  hash: Bool,
3980  st: St,
3981  cc: Char
3982) -> St:
3983  match br:
3984    case True{}:
3985      lex.head.br(st)
3986    case False{}:
3987      lex.head.bare(bare, sp, dot, end, qq, lit, hash, st, cc)
3988
3989# inside a header
3990def lex.head(st: St, +cc: Char) -> St:
3991  lex.head.go(Char.is_eq(cc, '['), bare.at(cc), ch.sp(cc), Char.is_eq(cc, '.'),
3992    Char.is_eq(cc, ']'), Char.is_eq(cc, '"'), Char.is_eq(cc, '\''), Char.is_eq(cc, '#'),
3993    st, cc)
3994
3995# the end, or a comment
3996def lex.hgap.end(end: Bool, hash: Bool, st: St) -> St:
3997  match end:
3998    case True{}:
3999      lex.head.close(st)
4000    case False{}:
4001      lex.head.hash(hash, st)
4002
4003# a dot starts the next segment
4004def lex.hgap.dot(dot: Bool, end: Bool, hash: Bool, st: St) -> St:
4005  match dot:
4006    case True{}:
4007      st.lex(st, LHeadDot{})
4008    case False{}:
4009      lex.hgap.end(end, hash, st)
4010
4011# whitespace, a dot, or the end
4012def lex.hgap(sp: Bool, dot: Bool, end: Bool, hash: Bool, st: St, _c: Char) -> St:
4013  match sp:
4014    case True{}:
4015      st
4016    case False{}:
4017      lex.hgap.dot(dot, end, hash, st)
4018
4019# between header segments
4020def lex.head.gap.step(st: St, +cc: Char) -> St:
4021  lex.hgap(ch.sp(cc), Char.is_eq(cc, '.'), Char.is_eq(cc, ']'), Char.is_eq(cc, '#'), st, cc)
4022
4023# a literal segment, or a rejected character
4024def lex.hdot.lit(lit: Bool, st: St, _c: Char) -> St:
4025  match lit:
4026    case True{}:
4027      lex.qkey(st, QLit{}, LHeadQ{})
4028    case False{}:
4029      st.err(st, "invalid header")
4030
4031# a quoted segment
4032def lex.hdot.q(qq: Bool, lit: Bool, st: St, cc: Char) -> St:
4033  match qq:
4034    case True{}:
4035      lex.qkey(st, QBasic{}, LHeadQ{})
4036    case False{}:
4037      lex.hdot.lit(lit, st, cc)
4038
4039# a bare segment or a quoted one
4040def lex.hdot.bare(bare: Bool, qq: Bool, lit: Bool, st: St, cc: Char) -> St:
4041  match bare:
4042    case True{}:
4043      st.push(st, cc, LHead{})
4044    case False{}:
4045      lex.hdot.q(qq, lit, st, cc)
4046
4047# whitespace or the next segment
4048def lex.hdot(sp: Bool, bare: Bool, qq: Bool, lit: Bool, st: St, cc: Char) -> St:
4049  match sp:
4050    case True{}:
4051      st
4052    case False{}:
4053      lex.hdot.bare(bare, qq, lit, st, cc)
4054
4055# after a dot, a segment must start
4056def lex.head.dot.step(st: St, +cc: Char) -> St:
4057  lex.hdot(ch.sp(cc), bare.at(cc), Char.is_eq(cc, '"'), Char.is_eq(cc, '\''), st, cc)
4058
4059# a forbidden control, or one character of the key
4060def lex.kq.char.go(bad: Bool, st: St, cc: Char, stay: Lex) -> St:
4061  match bad:
4062    case True{}:
4063      st.err(st, "invalid control")
4064    case False{}:
4065      st.push(st, cc, stay)
4066
4067# one character of a quoted key
4068def lex.kq.char(st: St, +cc: Char, stay: Lex) -> St:
4069  lex.kq.char.go(str.bad(Char.to_u32(cc), False{}), st, cc, stay)
4070
4071# a newline in a key is rejected
4072def lex.kq.nl(nl: Bool, st: St, +cc: Char, stay: Lex) -> St:
4073  match nl:
4074    case True{}:
4075      st.err(st, "newline in key")
4076    case False{}:
4077      lex.kq.char(st, cc, stay)
4078
4079# the escape state for a quoted key
4080def lex.esc.lex(stay: Lex) -> Lex:
4081  match stay:
4082    case LHeadQ{}:
4083      LHeadE{}
4084    case _:
4085      LKeyE{}
4086
4087# the escape returns to the quoted key
4088def lex.kesc(st: St, +stay: Lex) -> St:
4089  St{bad, rows, heads, here, parts, buf, _lex, _b, qkind, stack, hold, uni, left, arrtab,
4090    lead} = st
4091  St{bad, rows, heads, here, parts, buf, lex.esc.lex(stay), stay, qkind, stack, hold,
4092    uni, left, arrtab, lead}
4093
4094# only a basic key treats the backslash as an escape
4095def lex.kq.esc(basic: Bool, st: St, stay: Lex) -> St:
4096  match basic:
4097    case True{}:
4098      lex.kesc(st, stay)
4099    case False{}:
4100      st.push(st, '\\', stay)
4101
4102# an escape in a basic key
4103def lex.kq.bs(bs: Bool, basic: Bool, nl: Bool, st: St, cc: Char, stay: Lex) -> St:
4104  match bs:
4105    case True{}:
4106      lex.kq.esc(basic, st, stay)
4107    case False{}:
4108      lex.kq.nl(nl, st, cc, stay)
4109
4110# a quoted segment may be empty
4111def lex.qkey.end(st: St, next: Lex) -> St:
4112  seg.push(st, next)
4113
4114# the closer, an escape, or a character
4115def lex.kq.go(quote: Bool, bs: Bool, basic: Bool, nl: Bool, st: St, cc: Char, back: Lex, stay: Lex) -> St:
4116  match quote:
4117    case True{}:
4118      lex.qkey.end(st, back)
4119    case False{}:
4120      lex.kq.bs(bs, basic, nl, st, cc, stay)
4121
4122# a quoted key segment. back is the state after the closer; stay is this quote
4123def lex.kq(st: St, +cc: Char, back: Lex, stay: Lex) -> St:
4124  St{bad, rows, heads, here, parts, buf, lex, b, +qkind, stack, hold, uni, left, arrtab,
4125    lead} = st
4126  lex.kq.go(Char.is_eq(cc, q.char(qkind)), Char.is_eq(cc, '\\'), q.basic(qkind), ch.nl(cc),
4127    St{bad, rows, heads, here, parts, buf, lex, b, qkind, stack, hold, uni, left, arrtab,
4128      lead}, cc, back, stay)
4129
4130# the second ] of an array of tables
4131def lex.head.r.go(end: Bool, st: St) -> St:
4132  match end:
4133    case True{}:
4134      head.fin(st)
4135    case False{}:
4136      st.err(st, "invalid header")
4137
4138# the second ] of an array of tables
4139def lex.head.r(st: St, +cc: Char) -> St:
4140  lex.head.r.go(Char.is_eq(cc, ']'), st)
4141
4142# ] closes; anything else is a value
4143def lex.arr.end(end: Bool, st: St, cc: Char) -> St:
4144  match end:
4145    case True{}:
4146      arr.close(st)
4147    case False{}:
4148      st.hold(st.lex(st, LVal{}), LVal{}, cc)
4149
4150# a comment, the end, or a value
4151def lex.arr.hash(hash: Bool, end: Bool, st: St, cc: Char) -> St:
4152  match hash:
4153    case True{}:
4154      com.enter(st, LArr{})
4155    case False{}:
4156      lex.arr.end(end, st, cc)
4157
4158# a newline is whitespace in an array
4159def lex.arr.nl(nl: Bool, hash: Bool, end: Bool, st: St, cc: Char) -> St:
4160  match nl:
4161    case True{}:
4162      st
4163    case False{}:
4164      lex.arr.hash(hash, end, st, cc)
4165
4166# whitespace, a comment, the end, or a value
4167def lex.arr.go(sp: Bool, nl: Bool, hash: Bool, end: Bool, st: St, cc: Char) -> St:
4168  match sp:
4169    case True{}:
4170      st
4171    case False{}:
4172      lex.arr.nl(nl, hash, end, st, cc)
4173
4174# an array waits for a value or ]
4175def lex.arr(st: St, +cc: Char) -> St:
4176  lex.arr.go(ch.sp(cc), ch.nl(cc), Char.is_eq(cc, '#'), Char.is_eq(cc, ']'), st, cc)
4177
4178# ] closes the array
4179def lex.arrc.end(end: Bool, st: St) -> St:
4180  match end:
4181    case True{}:
4182      arr.close(st)
4183    case False{}:
4184      st.err(st, "invalid array")
4185
4186# a comma waits for another value
4187def lex.arrc.comma(comma: Bool, end: Bool, st: St) -> St:
4188  match comma:
4189    case True{}:
4190      st.lex(st, LArr{})
4191    case False{}:
4192      lex.arrc.end(end, st)
4193
4194# a comment, a comma, or the end
4195def lex.arrc.hash(hash: Bool, comma: Bool, end: Bool, st: St, _c: Char) -> St:
4196  match hash:
4197    case True{}:
4198      com.enter(st, LArrC{})
4199    case False{}:
4200      lex.arrc.comma(comma, end, st)
4201
4202# a newline is whitespace
4203def lex.arrc.nl(nl: Bool, hash: Bool, comma: Bool, end: Bool, st: St, cc: Char) -> St:
4204  match nl:
4205    case True{}:
4206      st
4207    case False{}:
4208      lex.arrc.hash(hash, comma, end, st, cc)
4209
4210# whitespace, a comment, a comma, or the end
4211def lex.arrc.go(sp: Bool, nl: Bool, hash: Bool, comma: Bool, end: Bool, st: St, cc: Char) -> St:
4212  match sp:
4213    case True{}:
4214      st
4215    case False{}:
4216      lex.arrc.nl(nl, hash, comma, end, st, cc)
4217
4218# after an array value: a comma, ], or whitespace
4219def lex.arrc(st: St, +cc: Char) -> St:
4220  lex.arrc.go(ch.sp(cc), ch.nl(cc), Char.is_eq(cc, '#'), Char.is_eq(cc, ','),
4221    Char.is_eq(cc, ']'), st, cc)
4222
4223# a new key starts with an empty segment list
4224def lex.key.clear(st: St) -> St:
4225  St{bad, rows, heads, here, _parts, _buf, _lex, back, qkind, stack, hold, uni, left,
4226    arrtab, lead} = st
4227  St{bad, rows, heads, here, [], [], LKey{}, back, qkind, stack, hold, uni, left,
4228    arrtab, lead}
4229
4230# a bare character opens the key
4231def lex.key.bare(ok: Bool, st: St, cc: Char) -> St:
4232  match ok:
4233    case True{}:
4234      st.push(st, cc, LKey{})
4235    case False{}:
4236      st.err(st, "invalid key")
4237
4238# a literal quote or a bare character opens the key
4239def lex.key.lit(lit: Bool, st: St, +cc: Char) -> St:
4240  match lit:
4241    case True{}:
4242      lex.qkey(st, QLit{}, LKeyQ{})
4243    case False{}:
4244      lex.key.bare(bare.at(cc), st, cc)
4245
4246# a quote or a bare character opens the key
4247def lex.key.q(qq: Bool, st: St, +cc: Char) -> St:
4248  match qq:
4249    case True{}:
4250      lex.qkey(st, QBasic{}, LKeyQ{})
4251    case False{}:
4252      lex.key.lit(Char.is_eq(cc, '\''), st, cc)
4253
4254# the first character of a key inside an inline table
4255def lex.key.start(st: St, +cc: Char) -> St:
4256  lex.key.q(Char.is_eq(cc, '"'), lex.key.clear(st), cc)
4257
4258# a newline is rejected; anything else is a key
4259def lex.inl.nl(nl: Bool, st: St, cc: Char) -> St:
4260  match nl:
4261    case True{}:
4262      st.err(st, "newline in inline table")
4263    case False{}:
4264      lex.key.start(st, cc)
4265
4266# } closes an empty inline table
4267def lex.inl.end(end: Bool, nl: Bool, st: St, cc: Char) -> St:
4268  match end:
4269    case True{}:
4270      inl.close(st)
4271    case False{}:
4272      lex.inl.nl(nl, st, cc)
4273
4274# a comment, the end, or a key
4275def lex.inl.hash(hash: Bool, end: Bool, nl: Bool, st: St, cc: Char) -> St:
4276  match hash:
4277    case True{}:
4278      com.enter(st, LInl{})
4279    case False{}:
4280      lex.inl.end(end, nl, st, cc)
4281
4282# whitespace, a comment, the end, or a key
4283def lex.inl.go(sp: Bool, hash: Bool, end: Bool, nl: Bool, st: St, cc: Char) -> St:
4284  match sp:
4285    case True{}:
4286      st
4287    case False{}:
4288      lex.inl.hash(hash, end, nl, st, cc)
4289
4290# an inline table waits for a key or }
4291def lex.inl(st: St, +cc: Char) -> St:
4292  lex.inl.go(ch.sp(cc), Char.is_eq(cc, '#'), Char.is_eq(cc, '}'), ch.nl(cc), st, cc)
4293
4294# a comment or a key
4295def lex.inlk.hash(hash: Bool, nl: Bool, st: St, cc: Char) -> St:
4296  match hash:
4297    case True{}:
4298      com.enter(st, LInlK{})
4299    case False{}:
4300      lex.inl.nl(nl, st, cc)
4301
4302# whitespace or a key
4303def lex.inlk.go(sp: Bool, hash: Bool, nl: Bool, st: St, cc: Char) -> St:
4304  match sp:
4305    case True{}:
4306      st
4307    case False{}:
4308      lex.inlk.hash(hash, nl, st, cc)
4309
4310# after a comma, a key is required
4311def lex.inlk(st: St, +cc: Char) -> St:
4312  lex.inlk.go(ch.sp(cc), Char.is_eq(cc, '#'), ch.nl(cc), st, cc)
4313
4314# a newline is rejected
4315def lex.inlc.nl(nl: Bool, st: St) -> St:
4316  match nl:
4317    case True{}:
4318      st.err(st, "newline in inline table")
4319    case False{}:
4320      st.err(st, "invalid inline table")
4321
4322# } closes the inline table
4323def lex.inlc.end(end: Bool, nl: Bool, st: St, _c: Char) -> St:
4324  match end:
4325    case True{}:
4326      inl.close(st)
4327    case False{}:
4328      lex.inlc.nl(nl, st)
4329
4330# a comma requires another key
4331def lex.inlc.comma(comma: Bool, end: Bool, nl: Bool, st: St, cc: Char) -> St:
4332  match comma:
4333    case True{}:
4334      st.lex(st, LInlK{})
4335    case False{}:
4336      lex.inlc.end(end, nl, st, cc)
4337
4338# a comment, a comma, or the end
4339def lex.inlc.hash(hash: Bool, comma: Bool, end: Bool, nl: Bool, st: St, cc: Char) -> St:
4340  match hash:
4341    case True{}:
4342      com.enter(st, LInlC{})
4343    case False{}:
4344      lex.inlc.comma(comma, end, nl, st, cc)
4345
4346# whitespace, a comment, a comma, or the end
4347def lex.inlc.go(sp: Bool, hash: Bool, comma: Bool, end: Bool, nl: Bool, st: St, cc: Char) -> St:
4348  match sp:
4349    case True{}:
4350      st
4351    case False{}:
4352      lex.inlc.hash(hash, comma, end, nl, st, cc)
4353
4354# after an inline value: a comma or }
4355def lex.inlc(st: St, +cc: Char) -> St:
4356  lex.inlc.go(ch.sp(cc), Char.is_eq(cc, '#'), Char.is_eq(cc, ','), Char.is_eq(cc, '}'),
4357    ch.nl(cc), st, cc)
4358
4359# the rest of a failed document is ignored
4360def lex.sink(st: St, _c: Char) -> St:
4361  st
4362
4363# anything else on the same line is another expression
4364def lex.line.nl(nl: Bool, st: St) -> St:
4365  match nl:
4366    case True{}:
4367      st.lex(st, LTop{})
4368    case False{}:
4369      st.err(st, "newline required")
4370
4371# a comment may follow an expression
4372def lex.line.hash(hash: Bool, nl: Bool, st: St, _c: Char) -> St:
4373  match hash:
4374    case True{}:
4375      com.enter(st, LLine{})
4376    case False{}:
4377      lex.line.nl(nl, st)
4378
4379# whitespace, a comment, or a newline after an expression
4380def lex.line.go(sp: Bool, hash: Bool, nl: Bool, st: St, cc: Char) -> St:
4381  match sp:
4382    case True{}:
4383      st
4384    case False{}:
4385      lex.line.hash(hash, nl, st, cc)
4386
4387# after an expression, the rest of the line is whitespace or a comment
4388def lex.line(st: St, +cc: Char) -> St:
4389  lex.line.go(ch.sp(cc), Char.is_eq(cc, '#'), ch.nl(cc), st, cc)
4390
4391# a newline in a dotted key is rejected
4392def lex.kdot.nl(nl: Bool, st: St) -> St:
4393  match nl:
4394    case True{}:
4395      st.err(st, "newline in key")
4396    case False{}:
4397      st.err(st, "invalid key")
4398
4399# a second dot is an empty segment
4400def lex.kdot.dot(dot: Bool, nl: Bool, st: St) -> St:
4401  match dot:
4402    case True{}:
4403      st.err(st, "empty key")
4404    case False{}:
4405      lex.kdot.nl(nl, st)
4406
4407# a bare character starts the segment
4408def lex.kdot.bare(bare: Bool, dot: Bool, nl: Bool, st: St, cc: Char) -> St:
4409  match bare:
4410    case True{}:
4411      st.push(st, cc, LKey{})
4412    case False{}:
4413      lex.kdot.dot(dot, nl, st)
4414
4415# a literal quote starts the segment
4416def lex.kdot.lit(lit: Bool, dot: Bool, nl: Bool, st: St, +cc: Char) -> St:
4417  match lit:
4418    case True{}:
4419      lex.qkey(st, QLit{}, LKeyQ{})
4420    case False{}:
4421      lex.kdot.bare(bare.at(cc), dot, nl, st, cc)
4422
4423# a quote starts the segment
4424def lex.kdot.q(qq: Bool, lit: Bool, dot: Bool, nl: Bool, st: St, cc: Char) -> St:
4425  match qq:
4426    case True{}:
4427      lex.qkey(st, QBasic{}, LKeyQ{})
4428    case False{}:
4429      lex.kdot.lit(lit, dot, nl, st, cc)
4430
4431# whitespace or the next segment
4432def lex.kdot.go(sp: Bool, qq: Bool, lit: Bool, dot: Bool, nl: Bool, st: St, cc: Char) -> St:
4433  match sp:
4434    case True{}:
4435      st
4436    case False{}:
4437      lex.kdot.q(qq, lit, dot, nl, st, cc)
4438
4439# after a dot, whitespace and then a segment
4440def lex.kdot(st: St, +cc: Char) -> St:
4441  lex.kdot.go(ch.sp(cc), Char.is_eq(cc, '"'), Char.is_eq(cc, '\''), Char.is_eq(cc, '.'),
4442    ch.nl(cc), st, cc)
4443
4444# a quoted header segment
4445def lex.hq(st: St, +cc: Char) -> St:
4446  lex.kq(st, cc, LHeadGap{}, LHeadQ{})
4447
4448# one character, dispatched on the lex state
4449def read.on(lex: Lex, st: St, cc: Char) -> St:
4450  match lex:
4451    case LTop{}:
4452      lex.top(st, cc)
4453    case LLine{}:
4454      lex.line(st, cc)
4455    case LKey{}:
4456      lex.key(st, cc)
4457    case LKeyDot{}:
4458      lex.kdot(st, cc)
4459    case LAfter{}:
4460      lex.after(st, cc)
4461    case LKeyQ{}:
4462      lex.kq(st, cc, LAfter{}, LKeyQ{})
4463    case LKeyE{}:
4464      esc.use(esc.of(cc), st, LKeyQ{})
4465    case LKeyU{}:
4466      uni.step(st, cc, LKeyQ{})
4467    case LVal{}:
4468      lex.val(st, cc)
4469    case LQ{}:
4470      lex.q(st, cc)
4471    case LQ2{}:
4472      lex.q2(st, cc)
4473    case LStr{}:
4474      lex.str(st, cc)
4475    case LEsc{}:
4476      lex.esc(st, cc)
4477    case LUni{}:
4478      uni.step(st, cc, LStr{})
4479    case LFold{}:
4480      lex.fold(st, cc)
4481    case LMq{}:
4482      lex.mq.step(st, cc)
4483    case LMqEnd{}:
4484      lex.mq.end(st, cc)
4485    case LTrim{}:
4486      lex.trim(st, cc)
4487    case LTrim2{}:
4488      lex.trim2(st, cc)
4489    case LBare{}:
4490      lex.bare(st, cc)
4491    case LDate{}:
4492      lex.date(st, cc)
4493    case LCom{}:
4494      lex.com(st, cc)
4495    case LHead{}:
4496      lex.head(st, cc)
4497    case LHeadGap{}:
4498      lex.head.gap.step(st, cc)
4499    case LHeadDot{}:
4500      lex.head.dot.step(st, cc)
4501    case LHeadQ{}:
4502      lex.hq(st, cc)
4503    case LHeadE{}:
4504      esc.use(esc.of(cc), st, LHeadQ{})
4505    case LHeadU{}:
4506      uni.step(st, cc, LHeadQ{})
4507    case LHeadR{}:
4508      lex.head.r(st, cc)
4509    case LArr{}:
4510      lex.arr(st, cc)
4511    case LArrC{}:
4512      lex.arrc(st, cc)
4513    case LInl{}:
4514      lex.inl(st, cc)
4515    case LInlK{}:
4516      lex.inlk(st, cc)
4517    case LInlC{}:
4518      lex.inlc(st, cc)
4519    case LSink{}:
4520      lex.sink(st, cc)
4521
4522# read the lex state and step
4523def read.on.st(st: St, cc: Char) -> St:
4524  St{bad, rows, heads, here, parts, buf, +lex, back, qkind, stack, hold, uni, left,
4525    arrtab, lead} = st
4526  read.on(lex, St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, hold, uni,
4527    left, arrtab, lead}, cc)
4528
4529# one character, after a leading mark has been decided
4530def read.step.bom(bom: Bool, st: St, cc: Char) -> St:
4531  match bom:
4532    case True{}:
4533      st
4534    case False{}:
4535      read.on.st(st, cc)
4536
4537# the first character may be a byte-order mark
4538def read.step.lead(lead: Bool, st: St, +cc: Char) -> St:
4539  match lead:
4540    case False{}:
4541      read.on.st(st, cc)
4542    case True{}:
4543      read.step.bom(U32.is_eq(Char.to_u32(cc), 65279), st, cc)
4544
4545# one character of the document
4546def read.step(st: St, +cc: Char) -> St:
4547  St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, hold, uni, left,
4548    arrtab, +lead} = st
4549  read.step.lead(lead, St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack,
4550    hold, uni, left, arrtab, False{}}, cc)
4551
4552# a held character is read once
4553def read.once.hold(hold: Hold, st: St) -> St:
4554  match hold:
4555    case HNone{}:
4556      st
4557    case HChar{c}:
4558      read.step(st, c)
4559
4560# a held character is read once
4561def read.once2(st: St) -> St:
4562  St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, hold, uni, left,
4563    arrtab, lead} = st
4564  read.once.hold(hold, St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack,
4565    HNone{}, uni, left, arrtab, lead})
4566
4567# one new character, then a held character if the step asked for one
4568def read.once(st: St, cc: Char) -> St:
4569  read.once2(read.step(st, cc))
4570
4571# a bare token, an empty string or a closed multiline string still open at the end
4572def read.fin.lex(lex: Lex, st: St) -> St:
4573  match lex:
4574    case LBare{}:
4575      bare.finish(st, ' ', False{})
4576    case LDate{}:
4577      bare.finish(st, ' ', False{})
4578    case LQ2{}:
4579      val.take(st, VStr{""})
4580    case LMqEnd{}:
4581      str.fin(st)
4582    case _:
4583      st
4584
4585# a bare token still open at the end is closed
4586def read.fin.close(st: St) -> St:
4587  St{bad, rows, heads, here, parts, buf, +lex, back, qkind, stack, hold, uni, left,
4588    arrtab, lead} = st
4589  read.fin.lex(lex, St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, hold,
4590    uni, left, arrtab, lead})
4591
4592# builder order is newest-first. a kept list is reversed back; a builder list is not
4593def rows.seal.fin(rev: Bool, acc: List<&2, Val>) -> List<&2, Val>:
4594  match rev:
4595    case True{}:
4596      acc
4597    case False{}:
4598      List.reverse(&2, Val, acc)
4599
4600# put every table back in insertion order. one pass, no append along the way
4601def rows.seal.go(vs: List<&2, Val>, rev: Bool, acc: List<&2, Val>) -> List<&2, Val>:
4602  match vs:
4603    case []:
4604      rows.seal.fin(rev, acc)
4605    case VPair{name, VHead{path, rows}} <> t:
4606      rows.seal.go(t, rev, VPair{name, VHead{path, rows.seal.go(rows, True{}, [])}} <> acc)
4607    case VPair{name, VAots{path, elems}} <> t:
4608      rows.seal.go(t, rev,
4609        VPair{name, VAots{path, rows.seal.go(elems, True{}, [])}} <> acc)
4610    case VPair{name, VInl{rows}} <> t:
4611      rows.seal.go(t, rev, VPair{name, VInl{rows.seal.go(rows, True{}, [])}} <> acc)
4612    case VPair{name, VArr{items}} <> t:
4613      rows.seal.go(t, rev, VPair{name, VArr{rows.seal.go(items, False{}, [])}} <> acc)
4614    case VAot{path, rows} <> t:
4615      rows.seal.go(t, rev, VAot{path, rows.seal.go(rows, True{}, [])} <> acc)
4616    case VAots{path, elems} <> t:
4617      rows.seal.go(t, rev, VAots{path, rows.seal.go(elems, True{}, [])} <> acc)
4618    case VInl{rows} <> t:
4619      rows.seal.go(t, rev, VInl{rows.seal.go(rows, True{}, [])} <> acc)
4620    case VArr{items} <> t:
4621      rows.seal.go(t, rev, VArr{rows.seal.go(items, False{}, [])} <> acc)
4622    case h <> t:
4623      rows.seal.go(t, rev, h <> acc)
4624
4625# insertion order of a table built newest-first
4626def rows.seal(rows: List<&2, Val>) -> List<&2, Val>:
4627  rows.seal.go(rows, True{}, [])
4628
4629# an open frame at the end is an error
4630def read.fin.stack(stack: List<&2, Ctx>, bad: String, rows: List<&2, Val>) -> Doc:
4631  match stack:
4632    case []:
4633      Doc{bad, rows.seal(rows)}
4634    case _ <> _:
4635      Doc{err.first(bad, "unclosed"), rows.seal(rows)}
4636
4637# the document from a finished state
4638def read.fin.doc(st: St) -> Doc:
4639  St{bad, rows, _heads, _here, _parts, _buf, _lex, _back, _q, stack, _hold, _uni, _left,
4640    _arr, _lead} = st
4641  read.fin.stack(stack, bad, rows)
4642
4643# an unfinished document keeps the first error
4644def read.fin.unclosed(st: St) -> Doc:
4645  St{bad, rows, _heads, _here, _parts, _buf, _lex, _back, _q, _stack, _hold, _uni,
4646    _left, _arr, _lead} = st
4647  Doc{err.first(bad, "unclosed"), rows.seal(rows)}
4648
4649# a comment may end a document only where the line already could
4650def read.fin.end(lex: Lex) -> Bool:
4651  match lex:
4652    case LTop{}:
4653      True{}
4654    case LLine{}:
4655      True{}
4656    case LSink{}:
4657      True{}
4658    case _:
4659      False{}
4660
4661# a comment at the end is unfinished when it interrupted a key or a value
4662def read.fin.com(ok: Bool, st: St) -> Doc:
4663  match ok:
4664    case True{}:
4665      read.fin.doc(st)
4666    case False{}:
4667      read.fin.unclosed(st)
4668
4669# a comment at the end is unfinished when it interrupted a key or a value
4670def read.fin.com.st(st: St) -> Doc:
4671  St{bad, rows, heads, here, parts, buf, lex, +back, qkind, stack, hold, uni, left,
4672    arrtab, lead} = st
4673  read.fin.com(read.fin.end(back), St{bad, rows, heads, here, parts, buf, lex, back,
4674    qkind, stack, hold, uni, left, arrtab, lead})
4675
4676# any other state is unfinished
4677def read.fin.bad(st: St) -> Doc:
4678  read.fin.unclosed(st)
4679
4680# the states that may end a document
4681def read.fin.ok(lex: Lex, st: St) -> Doc:
4682  match lex:
4683    case LTop{}:
4684      read.fin.doc(st)
4685    case LLine{}:
4686      read.fin.doc(st)
4687    case LCom{}:
4688      read.fin.com.st(st)
4689    case LSink{}:
4690      read.fin.doc(st)
4691    case _:
4692      read.fin.bad(st)
4693
4694# the document once the last token has been closed
4695def read.fin2(st: St) -> Doc:
4696  St{bad, rows, heads, here, parts, buf, +lex, back, qkind, stack, hold, uni, left,
4697    arrtab, lead} = st
4698  read.fin.ok(lex, St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, hold,
4699    uni, left, arrtab, lead})
4700
4701# the document at the end of the text
4702def read.fin(st: St) -> Doc:
4703  read.fin2(read.fin.close(st))
4704
4705# one scanner state, with the hold cleared and the first character already taken
4706def read.fast.st(
4707  bad: String,
4708  rows: List<&2, Val>,
4709  heads: List<&2, String>,
4710  here: List<&2, String>,
4711  parts: List<&2, String>,
4712  buf: List<&2, Char>,
4713  lex: Lex,
4714  back: Lex,
4715  qkind: QKind,
4716  stack: List<&2, Ctx>,
4717  uni: U32,
4718  left: U32,
4719  arrtab: Bool
4720) -> St:
4721  St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, HNone{}, uni, left,
4722    arrtab, False{}}
4723
4724# the character joins the buffer and the state stays
4725def read.fast.cons(
4726  bad: String,
4727  rows: List<&2, Val>,
4728  heads: List<&2, String>,
4729  here: List<&2, String>,
4730  parts: List<&2, String>,
4731  buf: List<&2, Char>,
4732  lex: Lex,
4733  back: Lex,
4734  qkind: QKind,
4735  stack: List<&2, Ctx>,
4736  uni: U32,
4737  left: U32,
4738  arrtab: Bool,
4739  +cc: Char
4740) -> St:
4741  read.fast.st(bad, rows, heads, here, parts, cc <> buf, lex, back, qkind, stack, uni,
4742    left, arrtab)
4743
4744# a quote, an escape, or a state this step does not special-case
4745def read.fast.old(
4746  bad: String,
4747  rows: List<&2, Val>,
4748  heads: List<&2, String>,
4749  here: List<&2, String>,
4750  parts: List<&2, String>,
4751  buf: List<&2, Char>,
4752  lex: Lex,
4753  back: Lex,
4754  qkind: QKind,
4755  stack: List<&2, Ctx>,
4756  uni: U32,
4757  left: U32,
4758  arrtab: Bool,
4759  +cc: Char
4760) -> St:
4761  read.once2(read.on.st(read.fast.st(bad, rows, heads, here, parts, buf, lex, back,
4762    qkind, stack, uni, left, arrtab), cc))
4763
4764# a forbidden control takes the full step; a plain character is stored
4765def read.fast.push(
4766  ctrl: Bool,
4767  bad: String,
4768  rows: List<&2, Val>,
4769  heads: List<&2, String>,
4770  here: List<&2, String>,
4771  parts: List<&2, String>,
4772  buf: List<&2, Char>,
4773  lex: Lex,
4774  back: Lex,
4775  qkind: QKind,
4776  stack: List<&2, Ctx>,
4777  uni: U32,
4778  left: U32,
4779  arrtab: Bool,
4780  +cc: Char
4781) -> St:
4782  match ctrl:
4783    case False{}:
4784      read.fast.cons(bad, rows, heads, here, parts, buf, lex, back, qkind, stack, uni,
4785        left, arrtab, cc)
4786    case True{}:
4787      read.fast.old(bad, rows, heads, here, parts, buf, lex, back, qkind, stack, uni,
4788        left, arrtab, cc)
4789
4790# a basic-string character that is not a quote
4791def read.fast.basic.bs(
4792  bs: Bool,
4793  bad: String,
4794  rows: List<&2, Val>,
4795  heads: List<&2, String>,
4796  here: List<&2, String>,
4797  parts: List<&2, String>,
4798  buf: List<&2, Char>,
4799  back: Lex,
4800  stack: List<&2, Ctx>,
4801  uni: U32,
4802  left: U32,
4803  arrtab: Bool,
4804  +cc: Char
4805) -> St:
4806  match bs:
4807    case True{}:
4808      read.fast.old(bad, rows, heads, here, parts, buf, LStr{}, back, QBasic{}, stack,
4809        uni, left, arrtab, cc)
4810    case False{}:
4811      read.fast.push(str.bad(Char.to_u32(cc), False{}), bad, rows, heads, here, parts,
4812        buf, LStr{}, back, QBasic{}, stack, uni, left, arrtab, cc)
4813
4814# a basic-string character: a quote or a backslash still takes the full step
4815def read.fast.basic(
4816  quote: Bool,
4817  bs: Bool,
4818  bad: String,
4819  rows: List<&2, Val>,
4820  heads: List<&2, String>,
4821  here: List<&2, String>,
4822  parts: List<&2, String>,
4823  buf: List<&2, Char>,
4824  back: Lex,
4825  stack: List<&2, Ctx>,
4826  uni: U32,
4827  left: U32,
4828  arrtab: Bool,
4829  +cc: Char
4830) -> St:
4831  match quote:
4832    case True{}:
4833      read.fast.old(bad, rows, heads, here, parts, buf, LStr{}, back, QBasic{}, stack,
4834        uni, left, arrtab, cc)
4835    case False{}:
4836      read.fast.basic.bs(bs, bad, rows, heads, here, parts, buf, back, stack, uni, left,
4837        arrtab, cc)
4838
4839# a literal-string character: a quote still takes the full step
4840def read.fast.lit(
4841  quote: Bool,
4842  bad: String,
4843  rows: List<&2, Val>,
4844  heads: List<&2, String>,
4845  here: List<&2, String>,
4846  parts: List<&2, String>,
4847  buf: List<&2, Char>,
4848  back: Lex,
4849  stack: List<&2, Ctx>,
4850  uni: U32,
4851  left: U32,
4852  arrtab: Bool,
4853  +cc: Char
4854) -> St:
4855  match quote:
4856    case True{}:
4857      read.fast.old(bad, rows, heads, here, parts, buf, LStr{}, back, QLit{}, stack,
4858        uni, left, arrtab, cc)
4859    case False{}:
4860      read.fast.push(str.bad(Char.to_u32(cc), False{}), bad, rows, heads, here, parts,
4861        buf, LStr{}, back, QLit{}, stack, uni, left, arrtab, cc)
4862
4863# one character of a string
4864def read.fast.str(
4865  qkind: QKind,
4866  bad: String,
4867  rows: List<&2, Val>,
4868  heads: List<&2, String>,
4869  here: List<&2, String>,
4870  parts: List<&2, String>,
4871  buf: List<&2, Char>,
4872  back: Lex,
4873  stack: List<&2, Ctx>,
4874  uni: U32,
4875  left: U32,
4876  arrtab: Bool,
4877  +cc: Char
4878) -> St:
4879  match qkind:
4880    case QBasic{}:
4881      read.fast.basic(Char.is_eq(cc, '"'), Char.is_eq(cc, '\\'), bad, rows, heads, here,
4882        parts, buf, back, stack, uni, left, arrtab, cc)
4883    case QLit{}:
4884      read.fast.lit(Char.is_eq(cc, '\''), bad, rows, heads, here, parts, buf, back,
4885        stack, uni, left, arrtab, cc)
4886    case other:
4887      read.fast.old(bad, rows, heads, here, parts, buf, LStr{}, back, other, stack,
4888        uni, left, arrtab, cc)
4889
4890# one character of a bare key
4891def read.fast.key(
4892  ok: Bool,
4893  bad: String,
4894  rows: List<&2, Val>,
4895  heads: List<&2, String>,
4896  here: List<&2, String>,
4897  parts: List<&2, String>,
4898  buf: List<&2, Char>,
4899  back: Lex,
4900  qkind: QKind,
4901  stack: List<&2, Ctx>,
4902  uni: U32,
4903  left: U32,
4904  arrtab: Bool,
4905  +cc: Char
4906) -> St:
4907  match ok:
4908    case True{}:
4909      read.fast.cons(bad, rows, heads, here, parts, buf, LKey{}, back, qkind, stack,
4910        uni, left, arrtab, cc)
4911    case False{}:
4912      read.fast.old(bad, rows, heads, here, parts, buf, LKey{}, back, qkind, stack,
4913        uni, left, arrtab, cc)
4914
4915# one character of a bare value
4916def read.fast.bare(
4917  delim: Bool,
4918  bad: String,
4919  rows: List<&2, Val>,
4920  heads: List<&2, String>,
4921  here: List<&2, String>,
4922  parts: List<&2, String>,
4923  buf: List<&2, Char>,
4924  back: Lex,
4925  qkind: QKind,
4926  stack: List<&2, Ctx>,
4927  uni: U32,
4928  left: U32,
4929  arrtab: Bool,
4930  +cc: Char
4931) -> St:
4932  match delim:
4933    case False{}:
4934      read.fast.cons(bad, rows, heads, here, parts, buf, LBare{}, back, qkind, stack,
4935        uni, left, arrtab, cc)
4936    case True{}:
4937      read.fast.old(bad, rows, heads, here, parts, buf, LBare{}, back, qkind, stack,
4938        uni, left, arrtab, cc)
4939
4940# one character of a comment. a control, a newline among them, takes the full step
4941def read.fast.com(
4942  ctl: Bool,
4943  bad: String,
4944  rows: List<&2, Val>,
4945  heads: List<&2, String>,
4946  here: List<&2, String>,
4947  parts: List<&2, String>,
4948  buf: List<&2, Char>,
4949  back: Lex,
4950  qkind: QKind,
4951  stack: List<&2, Ctx>,
4952  uni: U32,
4953  left: U32,
4954  arrtab: Bool,
4955  +cc: Char
4956) -> St:
4957  match ctl:
4958    case False{}:
4959      read.fast.st(bad, rows, heads, here, parts, buf, LCom{}, back, qkind, stack,
4960        uni, left, arrtab)
4961    case True{}:
4962      read.fast.old(bad, rows, heads, here, parts, buf, LCom{}, back, qkind, stack,
4963        uni, left, arrtab, cc)
4964
4965# whitespace that this state ignores. keep is true when a newline is also ignored
4966def read.fast.ws.keep(
4967  keep: Bool,
4968  bad: String,
4969  rows: List<&2, Val>,
4970  heads: List<&2, String>,
4971  here: List<&2, String>,
4972  parts: List<&2, String>,
4973  buf: List<&2, Char>,
4974  lex: Lex,
4975  back: Lex,
4976  qkind: QKind,
4977  stack: List<&2, Ctx>,
4978  uni: U32,
4979  left: U32,
4980  arrtab: Bool,
4981  +cc: Char
4982) -> St:
4983  match keep:
4984    case True{}:
4985      read.fast.st(bad, rows, heads, here, parts, buf, lex, back, qkind, stack, uni,
4986        left, arrtab)
4987    case False{}:
4988      read.fast.old(bad, rows, heads, here, parts, buf, lex, back, qkind, stack, uni,
4989        left, arrtab, cc)
4990
4991# a newline this state ignores, or the full step
4992def read.fast.ws.nl(
4993  nl: Bool,
4994  keep: Bool,
4995  bad: String,
4996  rows: List<&2, Val>,
4997  heads: List<&2, String>,
4998  here: List<&2, String>,
4999  parts: List<&2, String>,
5000  buf: List<&2, Char>,
5001  lex: Lex,
5002  back: Lex,
5003  qkind: QKind,
5004  stack: List<&2, Ctx>,
5005  uni: U32,
5006  left: U32,
5007  arrtab: Bool,
5008  +cc: Char
5009) -> St:
5010  match nl:
5011    case True{}:
5012      read.fast.ws.keep(keep, bad, rows, heads, here, parts, buf, lex, back, qkind,
5013        stack, uni, left, arrtab, cc)
5014    case False{}:
5015      read.fast.old(bad, rows, heads, here, parts, buf, lex, back, qkind, stack, uni,
5016        left, arrtab, cc)
5017
5018# space stays in this state; a newline stays only when keep is set
5019def read.fast.ws(
5020  sp: Bool,
5021  nl: Bool,
5022  keep: Bool,
5023  bad: String,
5024  rows: List<&2, Val>,
5025  heads: List<&2, String>,
5026  here: List<&2, String>,
5027  parts: List<&2, String>,
5028  buf: List<&2, Char>,
5029  lex: Lex,
5030  back: Lex,
5031  qkind: QKind,
5032  stack: List<&2, Ctx>,
5033  uni: U32,
5034  left: U32,
5035  arrtab: Bool,
5036  +cc: Char
5037) -> St:
5038  match sp:
5039    case True{}:
5040      read.fast.st(bad, rows, heads, here, parts, buf, lex, back, qkind, stack, uni,
5041        left, arrtab)
5042    case False{}:
5043      read.fast.ws.nl(nl, keep, bad, rows, heads, here, parts, buf, lex, back, qkind,
5044        stack, uni, left, arrtab, cc)
5045
5046# the states whose plain characters do not change the scanner
5047def read.fast.lex(
5048  lex: Lex,
5049  qkind: QKind,
5050  bad: String,
5051  rows: List<&2, Val>,
5052  heads: List<&2, String>,
5053  here: List<&2, String>,
5054  parts: List<&2, String>,
5055  buf: List<&2, Char>,
5056  back: Lex,
5057  stack: List<&2, Ctx>,
5058  uni: U32,
5059  left: U32,
5060  arrtab: Bool,
5061  +cc: Char
5062) -> St:
5063  match lex:
5064    case LStr{}:
5065      read.fast.str(qkind, bad, rows, heads, here, parts, buf, back, stack, uni, left,
5066        arrtab, cc)
5067    case LKey{}:
5068      read.fast.key(bare.at(cc), bad, rows, heads, here, parts, buf, back, qkind,
5069        stack, uni, left, arrtab, cc)
5070    case LBare{}:
5071      read.fast.bare(ch.delim(cc), bad, rows, heads, here, parts, buf, back, qkind,
5072        stack, uni, left, arrtab, cc)
5073    case LCom{}:
5074      read.fast.com(ch.ctl(cc), bad, rows, heads, here, parts, buf, back, qkind, stack,
5075        uni, left, arrtab, cc)
5076    case LTop{}:
5077      read.fast.ws(ch.sp(cc), ch.nl(cc), True{}, bad, rows, heads, here, parts, buf,
5078        LTop{}, back, qkind, stack, uni, left, arrtab, cc)
5079    case LArr{}:
5080      read.fast.ws(ch.sp(cc), ch.nl(cc), True{}, bad, rows, heads, here, parts, buf,
5081        LArr{}, back, qkind, stack, uni, left, arrtab, cc)
5082    case LArrC{}:
5083      read.fast.ws(ch.sp(cc), ch.nl(cc), True{}, bad, rows, heads, here, parts, buf,
5084        LArrC{}, back, qkind, stack, uni, left, arrtab, cc)
5085    case LLine{}:
5086      read.fast.ws(ch.sp(cc), ch.nl(cc), False{}, bad, rows, heads, here, parts, buf,
5087        LLine{}, back, qkind, stack, uni, left, arrtab, cc)
5088    case LVal{}:
5089      read.fast.ws(ch.sp(cc), ch.nl(cc), False{}, bad, rows, heads, here, parts, buf,
5090        LVal{}, back, qkind, stack, uni, left, arrtab, cc)
5091    case LAfter{}:
5092      read.fast.ws(ch.sp(cc), ch.nl(cc), False{}, bad, rows, heads, here, parts, buf,
5093        LAfter{}, back, qkind, stack, uni, left, arrtab, cc)
5094    case LInl{}:
5095      read.fast.ws(ch.sp(cc), ch.nl(cc), False{}, bad, rows, heads, here, parts, buf,
5096        LInl{}, back, qkind, stack, uni, left, arrtab, cc)
5097    case LInlK{}:
5098      read.fast.ws(ch.sp(cc), ch.nl(cc), False{}, bad, rows, heads, here, parts, buf,
5099        LInlK{}, back, qkind, stack, uni, left, arrtab, cc)
5100    case LInlC{}:
5101      read.fast.ws(ch.sp(cc), ch.nl(cc), False{}, bad, rows, heads, here, parts, buf,
5102        LInlC{}, back, qkind, stack, uni, left, arrtab, cc)
5103    case other:
5104      read.fast.old(bad, rows, heads, here, parts, buf, other, back, qkind, stack,
5105        uni, left, arrtab, cc)
5106
5107# the first character may be a byte-order mark; later characters take the fast step
5108def read.fast.lead(
5109  lead: Bool,
5110  lex: Lex,
5111  qkind: QKind,
5112  bad: String,
5113  rows: List<&2, Val>,
5114  heads: List<&2, String>,
5115  here: List<&2, String>,
5116  parts: List<&2, String>,
5117  buf: List<&2, Char>,
5118  back: Lex,
5119  stack: List<&2, Ctx>,
5120  uni: U32,
5121  left: U32,
5122  arrtab: Bool,
5123  +cc: Char
5124) -> St:
5125  match lead:
5126    case True{}:
5127      read.once(St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack,
5128        HNone{}, uni, left, arrtab, True{}}, cc)
5129    case False{}:
5130      read.fast.lex(lex, qkind, bad, rows, heads, here, parts, buf, back, stack, uni,
5131        left, arrtab, cc)
5132
5133# a held character is still read by the full step, then this character
5134def read.fast.hold(
5135  hold: Hold,
5136  lead: Bool,
5137  lex: Lex,
5138  qkind: QKind,
5139  bad: String,
5140  rows: List<&2, Val>,
5141  heads: List<&2, String>,
5142  here: List<&2, String>,
5143  parts: List<&2, String>,
5144  buf: List<&2, Char>,
5145  back: Lex,
5146  stack: List<&2, Ctx>,
5147  uni: U32,
5148  left: U32,
5149  arrtab: Bool,
5150  +cc: Char
5151) -> St:
5152  match hold:
5153    case HChar{held}:
5154      read.once(read.once2(St{bad, rows, heads, here, parts, buf, lex, back, qkind,
5155        stack, HChar{held}, uni, left, arrtab, lead}), cc)
5156    case HNone{}:
5157      read.fast.lead(lead, lex, qkind, bad, rows, heads, here, parts, buf, back,
5158        stack, uni, left, arrtab, cc)
5159
5160# one source character
5161def read.fast(st: St, +cc: Char) -> St:
5162  St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, hold, uni, left,
5163    arrtab, lead} = st
5164  read.fast.hold(hold, lead, lex, qkind, bad, rows, heads, here, parts, buf, back,
5165    stack, uni, left, arrtab, cc)
5166
5167# where the next source character is read. MEat is the body of a plain string, and
5168# MCr follows a carriage return, which only a line feed may follow
5169type Mode is Data:
5170  MScan{st: St}
5171  MCr{st: St}
5172  MOpen{basic: Bool, q: Char, qkind: QKind, bad: String, rows: List<&2, Val>,
5173    heads: List<&2, String>, here: List<&2, String>, parts: List<&2, String>,
5174    buf: List<&2, Char>, back: Lex, stack: List<&2, Ctx>, uni: U32, left: U32,
5175    arrtab: Bool}
5176  MEat{basic: Bool, q: Char, cut: String, n: U32, bad: String, rows: List<&2, Val>,
5177    heads: List<&2, String>, here: List<&2, String>, parts: List<&2, String>,
5178    qkind: QKind, stack: List<&2, Ctx>, uni: U32, left: U32, arrtab: Bool}
5179
5180# an unclosed string
5181def eat.fin(
5182  _n: U32,
5183  _u: Unit,
5184  bad: String,
5185  rows: List<&2, Val>,
5186  heads: List<&2, String>,
5187  here: List<&2, String>,
5188  parts: List<&2, String>,
5189  qkind: QKind,
5190  stack: List<&2, Ctx>,
5191  uni: U32,
5192  left: U32,
5193  arrtab: Bool
5194) -> Doc:
5195  read.fin.unclosed(St{bad, rows, heads, here, parts, [], LStr{}, LStr{}, qkind, stack,
5196    HNone{}, uni, left, arrtab, False{}})
5197
5198# a plain string is the first n characters of the source suffix
5199def eat.close(
5200  cut: String,
5201  nn: U32,
5202  bad: String,
5203  rows: List<&2, Val>,
5204  heads: List<&2, String>,
5205  here: List<&2, String>,
5206  parts: List<&2, String>,
5207  qkind: QKind,
5208  stack: List<&2, Ctx>,
5209  uni: U32,
5210  left: U32,
5211  arrtab: Bool
5212) -> St:
5213  val.take(St{bad, rows, heads, here, parts, [], LStr{}, LStr{}, qkind, stack, HNone{},
5214    uni, left, arrtab, False{}}, VSpan{cut, nn})
5215
5216# an escape or a forbidden control copies the span so far and continues
5217def eat.copy(
5218  +cc: Char,
5219  cut: String,
5220  +nn: U32,
5221  bad: String,
5222  rows: List<&2, Val>,
5223  heads: List<&2, String>,
5224  here: List<&2, String>,
5225  parts: List<&2, String>,
5226  qkind: QKind,
5227  stack: List<&2, Ctx>,
5228  uni: U32,
5229  left: U32,
5230  arrtab: Bool
5231) -> Mode:
5232  MScan{lex.str(St{bad, rows, heads, here, parts, span.rev(cut, nn, U32.is_zero(nn), []),
5233    LStr{}, LStr{}, qkind, stack, HNone{}, uni, left, arrtab, False{}}, cc)}
5234
5235# a forbidden control leaves the span; a plain character extends it
5236def eat.ctrl(
5237  badc: Bool,
5238  basic: Bool,
5239  qq: Char,
5240  cc: Char,
5241  cut: String,
5242  nn: U32,
5243  bad: String,
5244  rows: List<&2, Val>,
5245  heads: List<&2, String>,
5246  here: List<&2, String>,
5247  parts: List<&2, String>,
5248  qkind: QKind,
5249  stack: List<&2, Ctx>,
5250  uni: U32,
5251  left: U32,
5252  arrtab: Bool
5253) -> Mode:
5254  match badc:
5255    case True{}:
5256      eat.copy(cc, cut, nn, bad, rows, heads, here, parts, qkind, stack, uni, left,
5257        arrtab)
5258    case False{}:
5259      MEat{basic, qq, cut, U32.add(nn, 1), bad, rows, heads, here, parts, qkind, stack,
5260        uni, left, arrtab}
5261
5262# a backslash in a basic string leaves the span
5263def eat.bs(
5264  bs: Bool,
5265  basic: Bool,
5266  qq: Char,
5267  +cc: Char,
5268  cut: String,
5269  nn: U32,
5270  bad: String,
5271  rows: List<&2, Val>,
5272  heads: List<&2, String>,
5273  here: List<&2, String>,
5274  parts: List<&2, String>,
5275  qkind: QKind,
5276  stack: List<&2, Ctx>,
5277  uni: U32,
5278  left: U32,
5279  arrtab: Bool
5280) -> Mode:
5281  match bs:
5282    case True{}:
5283      eat.copy(cc, cut, nn, bad, rows, heads, here, parts, qkind, stack, uni, left,
5284        arrtab)
5285    case False{}:
5286      eat.ctrl(str.bad(Char.to_u32(cc), False{}), basic, qq, cc, cut, nn, bad, rows, heads,
5287        here, parts, qkind, stack, uni, left, arrtab)
5288
5289# a literal string keeps a backslash; a basic string does not
5290def eat.basic(
5291  basic: Bool,
5292  qq: Char,
5293  +cc: Char,
5294  cut: String,
5295  nn: U32,
5296  bad: String,
5297  rows: List<&2, Val>,
5298  heads: List<&2, String>,
5299  here: List<&2, String>,
5300  parts: List<&2, String>,
5301  qkind: QKind,
5302  stack: List<&2, Ctx>,
5303  uni: U32,
5304  left: U32,
5305  arrtab: Bool
5306) -> Mode:
5307  match basic:
5308    case False{}:
5309      eat.ctrl(str.bad(Char.to_u32(cc), False{}), False{}, qq, cc, cut, nn, bad, rows, heads,
5310        here, parts, qkind, stack, uni, left, arrtab)
5311    case True{}:
5312      eat.bs(Char.is_eq(cc, '\\'), True{}, qq, cc, cut, nn, bad, rows, heads, here, parts,
5313        qkind, stack, uni, left, arrtab)
5314
5315# a quote closes the span
5316def eat.feed.q(
5317  quote: Bool,
5318  basic: Bool,
5319  qq: Char,
5320  cc: Char,
5321  cut: String,
5322  nn: U32,
5323  bad: String,
5324  rows: List<&2, Val>,
5325  heads: List<&2, String>,
5326  here: List<&2, String>,
5327  parts: List<&2, String>,
5328  qkind: QKind,
5329  stack: List<&2, Ctx>,
5330  uni: U32,
5331  left: U32,
5332  arrtab: Bool
5333) -> Mode:
5334  match quote:
5335    case True{}:
5336      MScan{eat.close(cut, nn, bad, rows, heads, here, parts, qkind, stack, uni, left,
5337        arrtab)}
5338    case False{}:
5339      eat.basic(basic, qq, cc, cut, nn, bad, rows, heads, here, parts, qkind, stack, uni,
5340        left, arrtab)
5341
5342# one character of a plain string. cut is the suffix where the text began
5343def eat.feed(
5344  basic: Bool,
5345  +qq: Char,
5346  cut: String,
5347  nn: U32,
5348  bad: String,
5349  rows: List<&2, Val>,
5350  heads: List<&2, String>,
5351  here: List<&2, String>,
5352  parts: List<&2, String>,
5353  qkind: QKind,
5354  stack: List<&2, Ctx>,
5355  uni: U32,
5356  left: U32,
5357  arrtab: Bool,
5358  +cc: Char
5359) -> Mode:
5360  eat.feed.q(Char.is_eq(cc, qq), basic, qq, cc, cut, nn, bad, rows, heads, here, parts,
5361    qkind, stack, uni, left, arrtab)
5362
5363# the opening quote's back state is not kept on the span
5364def doc.open.eat(_back: Lex, mode: Mode) -> Mode:
5365  mode
5366
5367# a suffix the span does not keep
5368def doc.drop(_tail: String, mode: Mode) -> Mode:
5369  mode
5370
5371# an empty buffer starts a span; a buffer already in use stays on the old path
5372def doc.open.buf(
5373  basic: Bool,
5374  qq: Char,
5375  qkind: QKind,
5376  bad: String,
5377  rows: List<&2, Val>,
5378  heads: List<&2, String>,
5379  here: List<&2, String>,
5380  parts: List<&2, String>,
5381  buf: List<&2, Char>,
5382  back: Lex,
5383  stack: List<&2, Ctx>,
5384  uni: U32,
5385  left: U32,
5386  arrtab: Bool,
5387  cc: Char,
5388  tail: String
5389) -> Mode:
5390  match buf:
5391    case []:
5392      doc.open.eat(back, MEat{basic, qq, SCon{cc, tail}, 1, bad, rows, heads, here, parts,
5393        qkind, stack, uni, left, arrtab})
5394    case h <> t:
5395      doc.drop(tail, MScan{read.fast.lex(LQ{}, qkind, bad, rows, heads, here, parts,
5396        h <> t, back, stack, uni, left, arrtab, cc)})
5397
5398# a forbidden control leaves the span
5399def doc.open.ok(
5400  badc: Bool,
5401  basic: Bool,
5402  qq: Char,
5403  qkind: QKind,
5404  bad: String,
5405  rows: List<&2, Val>,
5406  heads: List<&2, String>,
5407  here: List<&2, String>,
5408  parts: List<&2, String>,
5409  buf: List<&2, Char>,
5410  back: Lex,
5411  stack: List<&2, Ctx>,
5412  uni: U32,
5413  left: U32,
5414  arrtab: Bool,
5415  cc: Char,
5416  tail: String
5417) -> Mode:
5418  match badc:
5419    case True{}:
5420      doc.drop(tail, MScan{read.fast.lex(LQ{}, qkind, bad, rows, heads, here, parts,
5421        buf, back, stack, uni, left, arrtab, cc)})
5422    case False{}:
5423      doc.open.buf(basic, qq, qkind, bad, rows, heads, here, parts, buf, back, stack,
5424        uni, left, arrtab, cc, tail)
5425
5426# a backslash in a basic string leaves the span
5427def doc.open.bs(
5428  bs: Bool,
5429  qq: Char,
5430  qkind: QKind,
5431  bad: String,
5432  rows: List<&2, Val>,
5433  heads: List<&2, String>,
5434  here: List<&2, String>,
5435  parts: List<&2, String>,
5436  buf: List<&2, Char>,
5437  back: Lex,
5438  stack: List<&2, Ctx>,
5439  uni: U32,
5440  left: U32,
5441  arrtab: Bool,
5442  +cc: Char,
5443  tail: String
5444) -> Mode:
5445  match bs:
5446    case True{}:
5447      doc.drop(tail, MScan{read.fast.lex(LQ{}, qkind, bad, rows, heads, here, parts,
5448        buf, back, stack, uni, left, arrtab, cc)})
5449    case False{}:
5450      doc.open.ok(str.bad(Char.to_u32(cc), False{}), True{}, qq, qkind, bad, rows, heads,
5451        here, parts, buf, back, stack, uni, left, arrtab, cc, tail)
5452
5453# a literal string keeps a backslash; a basic string does not
5454def doc.open.b(
5455  basic: Bool,
5456  qq: Char,
5457  qkind: QKind,
5458  bad: String,
5459  rows: List<&2, Val>,
5460  heads: List<&2, String>,
5461  here: List<&2, String>,
5462  parts: List<&2, String>,
5463  buf: List<&2, Char>,
5464  back: Lex,
5465  stack: List<&2, Ctx>,
5466  uni: U32,
5467  left: U32,
5468  arrtab: Bool,
5469  +cc: Char,
5470  tail: String
5471) -> Mode:
5472  match basic:
5473    case False{}:
5474      doc.open.ok(str.bad(Char.to_u32(cc), False{}), False{}, qq, qkind, bad, rows, heads,
5475        here, parts, buf, back, stack, uni, left, arrtab, cc, tail)
5476    case True{}:
5477      doc.open.bs(Char.is_eq(cc, '\\'), qq, qkind, bad, rows, heads, here, parts, buf,
5478        back, stack, uni, left, arrtab, cc, tail)
5479
5480# a second quote is an empty string or the start of a multiline string
5481def doc.open.q(
5482  same: Bool,
5483  basic: Bool,
5484  qq: Char,
5485  qkind: QKind,
5486  bad: String,
5487  rows: List<&2, Val>,
5488  heads: List<&2, String>,
5489  here: List<&2, String>,
5490  parts: List<&2, String>,
5491  buf: List<&2, Char>,
5492  back: Lex,
5493  stack: List<&2, Ctx>,
5494  uni: U32,
5495  left: U32,
5496  arrtab: Bool,
5497  cc: Char,
5498  tail: String
5499) -> Mode:
5500  match same:
5501    case True{}:
5502      doc.drop(tail, MScan{read.fast.lex(LQ{}, qkind, bad, rows, heads, here, parts,
5503        buf, back, stack, uni, left, arrtab, cc)})
5504    case False{}:
5505      doc.open.b(basic, qq, qkind, bad, rows, heads, here, parts, buf, back, stack, uni,
5506        left, arrtab, cc, tail)
5507
5508# the character after an opening quote
5509def doc.open(
5510  basic: Bool,
5511  +qq: Char,
5512  qkind: QKind,
5513  bad: String,
5514  rows: List<&2, Val>,
5515  heads: List<&2, String>,
5516  here: List<&2, String>,
5517  parts: List<&2, String>,
5518  buf: List<&2, Char>,
5519  back: Lex,
5520  stack: List<&2, Ctx>,
5521  uni: U32,
5522  left: U32,
5523  arrtab: Bool,
5524  +cc: Char,
5525  tail: String
5526) -> Mode:
5527  doc.open.q(Char.is_eq(cc, qq), basic, qq, qkind, bad, rows, heads, here, parts, buf,
5528    back, stack, uni, left, arrtab, cc, tail)
5529
5530# a one-line string may be a span; a multiline string stays on the old path
5531def doc.scan.kind(
5532  qkind: QKind,
5533  bad: String,
5534  rows: List<&2, Val>,
5535  heads: List<&2, String>,
5536  here: List<&2, String>,
5537  parts: List<&2, String>,
5538  buf: List<&2, Char>,
5539  back: Lex,
5540  stack: List<&2, Ctx>,
5541  uni: U32,
5542  left: U32,
5543  arrtab: Bool
5544) -> Mode:
5545  match qkind:
5546    case QBasic{}:
5547      MOpen{True{}, '"', QBasic{}, bad, rows, heads, here, parts, buf, back, stack,
5548        uni, left, arrtab}
5549    case QLit{}:
5550      MOpen{False{}, '\'', QLit{}, bad, rows, heads, here, parts, buf, back, stack,
5551        uni, left, arrtab}
5552    case other:
5553      MScan{St{bad, rows, heads, here, parts, buf, LQ{}, back, other, stack, HNone{},
5554        uni, left, arrtab, False{}}}
5555
5556# the first character of the file is still the old step
5557def doc.scan.lead(
5558  lead: Bool,
5559  qkind: QKind,
5560  bad: String,
5561  rows: List<&2, Val>,
5562  heads: List<&2, String>,
5563  here: List<&2, String>,
5564  parts: List<&2, String>,
5565  buf: List<&2, Char>,
5566  back: Lex,
5567  stack: List<&2, Ctx>,
5568  uni: U32,
5569  left: U32,
5570  arrtab: Bool
5571) -> Mode:
5572  match lead:
5573    case True{}:
5574      MScan{St{bad, rows, heads, here, parts, buf, LQ{}, back, qkind, stack, HNone{},
5575        uni, left, arrtab, True{}}}
5576    case False{}:
5577      doc.scan.kind(qkind, bad, rows, heads, here, parts, buf, back, stack, uni, left,
5578        arrtab)
5579
5580# a held character is not the start of a span
5581def doc.scan.hold(
5582  hold: Hold,
5583  lead: Bool,
5584  qkind: QKind,
5585  bad: String,
5586  rows: List<&2, Val>,
5587  heads: List<&2, String>,
5588  here: List<&2, String>,
5589  parts: List<&2, String>,
5590  buf: List<&2, Char>,
5591  back: Lex,
5592  stack: List<&2, Ctx>,
5593  uni: U32,
5594  left: U32,
5595  arrtab: Bool
5596) -> Mode:
5597  match hold:
5598    case HChar{held}:
5599      MScan{St{bad, rows, heads, here, parts, buf, LQ{}, back, qkind, stack,
5600        HChar{held}, uni, left, arrtab, lead}}
5601    case HNone{}:
5602      doc.scan.lead(lead, qkind, bad, rows, heads, here, parts, buf, back, stack, uni,
5603        left, arrtab)
5604
5605# a quote opened a one-line string, or the state is rebuilt around that quote
5606def doc.wrap.lex(
5607  lex: Lex,
5608  bad: String,
5609  rows: List<&2, Val>,
5610  heads: List<&2, String>,
5611  here: List<&2, String>,
5612  parts: List<&2, String>,
5613  buf: List<&2, Char>,
5614  back: Lex,
5615  qkind: QKind,
5616  stack: List<&2, Ctx>,
5617  hold: Hold,
5618  uni: U32,
5619  left: U32,
5620  arrtab: Bool,
5621  lead: Bool
5622) -> Mode:
5623  match lex:
5624    case LQ{}:
5625      doc.scan.hold(hold, lead, qkind, bad, rows, heads, here, parts, buf, back, stack,
5626        uni, left, arrtab)
5627    case other:
5628      MScan{St{bad, rows, heads, here, parts, buf, other, back, qkind, stack, hold,
5629        uni, left, arrtab, lead}}
5630
5631# a quote may have opened a string
5632def doc.wrap(st: St) -> Mode:
5633  St{bad, rows, heads, here, parts, buf, lex, back, qkind, stack, hold, uni, left,
5634    arrtab, lead} = st
5635  doc.wrap.lex(lex, bad, rows, heads, here, parts, buf, back, qkind, stack, hold,
5636    uni, left, arrtab, lead)
5637
5638# a carriage return must be followed by a line feed
5639def doc.scan.cr(cr: Bool, st: St, cc: Char) -> Mode:
5640  match cr:
5641    case True{}:
5642      MCr{read.fast(st, cc)}
5643    case False{}:
5644      MScan{read.fast(st, cc)}
5645
5646# an apostrophe may open a literal string
5647def doc.scan.sq(sq: Bool, cr: Bool, st: St, cc: Char) -> Mode:
5648  match sq:
5649    case True{}:
5650      doc.wrap(read.fast(st, cc))
5651    case False{}:
5652      doc.scan.cr(cr, st, cc)
5653
5654# a quote may open a basic string. any other character is the old step
5655def doc.scan.q(dq: Bool, sq: Bool, cr: Bool, st: St, cc: Char) -> Mode:
5656  match dq:
5657    case True{}:
5658      doc.wrap(read.fast(st, cc))
5659    case False{}:
5660      doc.scan.sq(sq, cr, st, cc)
5661
5662# one source character outside a plain string
5663def doc.scan(st: St, +cc: Char) -> Mode:
5664  doc.scan.q(Char.is_eq(cc, '"'), Char.is_eq(cc, '\''), U32.is_eq(Char.to_u32(cc), 13),
5665    st, cc)
5666
5667# the character after a carriage return: a line feed ends the line, anything else fails
5668def doc.cr(lf: Bool, st: St, cc: Char) -> Mode:
5669  match lf:
5670    case True{}:
5671      MScan{read.fast(st, cc)}
5672    case False{}:
5673      MScan{st.err(st, "carriage return without line feed")}
5674
5675# one character at a time. a plain string keeps a span of this suffix
5676def doc.read(text: String, mode: Mode) -> Doc:
5677  match text mode:
5678    case SNil{} MScan{st}:
5679      read.fin(read.once2(st))
5680    case SNil{} MCr{st}:
5681      read.fin(read.once2(st.err(st, "carriage return without line feed")))
5682    case SNil{} MOpen{_basic, _q, qkind, bad, rows, heads, here, parts, buf, back,
5683      stack, uni, left, arrtab}:
5684      read.fin(read.once2(St{bad, rows, heads, here, parts, buf, LQ{}, back, qkind,
5685        stack, HNone{}, uni, left, arrtab, False{}}))
5686    case SNil{} MEat{_basic, _q, cut, n, bad, rows, heads, here, parts, qkind, stack,
5687      uni, left, arrtab}:
5688      eat.fin(n, span.drop(cut), bad, rows, heads, here, parts, qkind, stack, uni,
5689        left, arrtab)
5690    case SCon{+h, +t} MOpen{basic, q, qkind, bad, rows, heads, here, parts, buf, back,
5691      stack, uni, left, arrtab}:
5692      doc.read(t, doc.open(basic, q, qkind, bad, rows, heads, here, parts, buf, back,
5693        stack, uni, left, arrtab, h, t))
5694    case SCon{+h, t} MEat{basic, q, cut, n, bad, rows, heads, here, parts, qkind,
5695      stack, uni, left, arrtab}:
5696      doc.read(t, eat.feed(basic, q, cut, n, bad, rows, heads, here, parts, qkind,
5697        stack, uni, left, arrtab, h))
5698    case SCon{+h, t} MScan{st}:
5699      doc.read(t, doc.scan(st, h))
5700    case SCon{+h, t} MCr{st}:
5701      doc.read(t, doc.cr(Char.is_eq(h, '\n'), st, h))
5702
5703# a scanner at the start of a document
5704def st.start() -> St:
5705  St{"", [], [], [], [], [], LTop{}, LTop{}, QBasic{}, [], HNone{}, 0, 0, False{},
5706    True{}}
5707
5708# a span walked for quoting. SqOk is the body reversed, with the closing quote already on
5709type Sq is Data:
5710  SqOk{rev: List<&2, Char>}
5711  SqNo{}
5712
5713# the reversed body while a span is still plain. SqStop means an escape was seen
5714type SqAcc is Data:
5715  SqRun{rev: List<&2, Char>}
5716  SqStop{}
5717
5718# quote, backslash, or a control. those still take the escaping writer
5719def span.esc(+uu: U32) -> Bool:
5720  Bool.or(U32.is_lt(uu, 32), Bool.or(U32.is_eq(uu, 34), Bool.or(U32.is_eq(uu, 92),
5721    U32.is_eq(uu, 127))))
5722
5723# cons one plain character. an escape, or a stop already seen, stays stopped
5724def span.quote.push(esc: Bool, acc: SqAcc, +hh: Char) -> SqAcc:
5725  match esc acc:
5726    case True{} _a:
5727      SqStop{}
5728    case False{} SqStop{}:
5729      SqStop{}
5730    case False{} SqRun{rev}:
5731      SqRun{hh <> rev}
5732
5733# the reversed body, or a stop, as the quoting result
5734def span.quote.end(acc: SqAcc) -> Sq:
5735  match acc:
5736    case SqStop{}:
5737      SqNo{}
5738    case SqRun{rev}:
5739      SqOk{rev}
5740
5741# the first n characters, reversed onto acc. a character that needs an escape stops
5742def span.quote.go(src: String, +nn: U32, zz: Bool, acc: SqAcc) -> Sq:
5743  match src zz:
5744    case _s True{}:
5745      span.quote.end(acc)
5746    case SNil{} False{}:
5747      span.quote.end(acc)
5748    case SCon{+h, t} False{}:
5749      span.quote.go(t, U32.sub(nn, 1), U32.is_zero(U32.sub(nn, 1)),
5750        span.quote.push(span.esc(Char.to_u32(h)), acc, h))
5751
5752# quotes around a plain span, or the escaping writer when a character needs it
5753def span.quote.fin(hit: Sq, src: String, +nn: U32) -> String:
5754  match hit:
5755    case SqNo{}:
5756      key.basic(span.str(src, nn, U32.is_zero(nn)))
5757    case SqOk{rev}:
5758      buf.str('"' <> rev)
5759
5760# a plain string span, quoted without rebuilding an escaped copy
5761def span.quote(+src: String, +nn: U32) -> String:
5762  span.quote.fin(span.quote.go(src, nn, U32.is_zero(nn), SqRun{'"' <> []}), src, nn)
5763
5764# true or false
5765def render.bool(bit: Bool) -> String:
5766  match bit:
5767    case True{}:
5768      "true"
5769    case False{}:
5770      "false"
5771
5772# a scalar value
5773def render.atom(vv: Val) -> String:
5774  match vv:
5775    case VStr{text}:
5776      key.basic(text)
5777    case VSpan{src, +n}:
5778      span.quote(src, n)
5779    case VInt{sign, digits}:
5780      sign.text(sign) ++ digits
5781    case VFlo{sign, text}:
5782      sign.text(sign) ++ text
5783    case VBool{bit}:
5784      render.bool(bit)
5785    case VWhen{w}:
5786      when.text(w)
5787    case _:
5788      ""
5789
5790# a separator that is omitted after the last item
5791def render.suf.last(last: Bool, gap: String) -> String:
5792  match last:
5793    case True{}:
5794      ""
5795    case False{}:
5796      gap
5797
5798# a separator. trail keeps the separator after the last item
5799def render.suf(+gap: String, trail: Bool, last: Bool) -> String:
5800  match trail:
5801    case True{}:
5802      gap
5803    case False{}:
5804      render.suf.last(last, gap)
5805
5806# the values of a table, an array, or an inline table
5807def render.go(vs: List<&2, Val>, +gap: String, +trail: Bool) -> String:
5808  match vs:
5809    case []:
5810      ""
5811    case VPair{_name, VHead{path, rows}} <> +t:
5812      "[" ++ path ++ "]\n" ++ render.go(rows, "\n", True{}) ++
5813        render.suf(gap, trail, List.is_empty(&2, Val, t)) ++ render.go(t, gap, trail)
5814    case VPair{_name, VAots{_path, elems}} <> +t:
5815      render.go(elems, "\n", True{}) ++
5816        render.suf(gap, trail, List.is_empty(&2, Val, t)) ++ render.go(t, gap, trail)
5817    case VAot{path, rows} <> +t:
5818      "[[" ++ path ++ "]]\n" ++ render.go(rows, "\n", True{}) ++
5819        render.suf(gap, trail, List.is_empty(&2, Val, t)) ++ render.go(t, gap, trail)
5820    case VPair{name, VArr{items}} <> +t:
5821      key(name) ++ " = [" ++ render.go(items, ", ", False{}) ++ "]" ++
5822        render.suf(gap, trail, List.is_empty(&2, Val, t)) ++ render.go(t, gap, trail)
5823    case VPair{name, VInl{rows}} <> +t:
5824      key(name) ++ " = {" ++ render.go(rows, ", ", False{}) ++ "}" ++
5825        render.suf(gap, trail, List.is_empty(&2, Val, t)) ++ render.go(t, gap, trail)
5826    case VPair{name, val} <> +t:
5827      key(name) ++ " = " ++ render.atom(val) ++
5828        render.suf(gap, trail, List.is_empty(&2, Val, t)) ++ render.go(t, gap, trail)
5829    case VArr{items} <> +t:
5830      "[" ++ render.go(items, ", ", False{}) ++ "]" ++
5831        render.suf(gap, trail, List.is_empty(&2, Val, t)) ++ render.go(t, gap, trail)
5832    case VInl{rows} <> +t:
5833      "{" ++ render.go(rows, ", ", False{}) ++ "}" ++
5834        render.suf(gap, trail, List.is_empty(&2, Val, t)) ++ render.go(t, gap, trail)
5835    case v <> +t:
5836      render.atom(v) ++ render.suf(gap, trail, List.is_empty(&2, Val, t)) ++
5837        render.go(t, gap, trail)
5838
5839# a nested table rendering that this pass does not print
5840def render.skip(
5841  _path: String,
5842  _rows: List<&2, Val>,
5843  _tail: List<&2, Val>,
5844  _gap: String,
5845  _trail: Bool,
5846  nest: Unit -> String,
5847  rest: Unit -> String
5848) -> String:
5849  _n = nest
5850  rest(Unit{})
5851
5852# the rows are already closed over by the nested rendering
5853def render.use(_rows: List<&2, Val>, text: String) -> String:
5854  text
5855
5856# a header already ends in a newline
5857def render.rest(_tail: List<&2, Val>, _gap: String, _trail: Bool, rest: Unit -> String) -> String:
5858  rest(Unit{})
5859
5860# a table header. Direct keys are printed by the other pass
5861def render.head(
5862  tabs: Bool,
5863  path: String,
5864  rows: List<&2, Val>,
5865  tail: List<&2, Val>,
5866  gap: String,
5867  trail: Bool,
5868  nest: Unit -> String,
5869  rest: Unit -> String
5870) -> String:
5871  match tabs:
5872    case False{}:
5873      render.skip(path, rows, tail, gap, trail, nest, rest)
5874    case True{}:
5875      "[" ++ path ++ "]\n" ++ render.use(rows, nest(Unit{})) ++
5876        render.rest(tail, gap, trail, rest)
5877
5878# an array of tables. Its elements are headers
5879def render.aots(
5880  tabs: Bool,
5881  elems: List<&2, Val>,
5882  tail: List<&2, Val>,
5883  gap: String,
5884  trail: Bool,
5885  nest: Unit -> String,
5886  rest: Unit -> String
5887) -> String:
5888  match tabs:
5889    case False{}:
5890      render.skip("", elems, tail, gap, trail, nest, rest)
5891    case True{}:
5892      render.use(elems, nest(Unit{})) ++ render.rest(tail, gap, trail, rest)
5893
5894# one element of an array of tables
5895def render.aot(
5896  tabs: Bool,
5897  path: String,
5898  rows: List<&2, Val>,
5899  tail: List<&2, Val>,
5900  gap: String,
5901  trail: Bool,
5902  nest: Unit -> String,
5903  rest: Unit -> String
5904) -> String:
5905  match tabs:
5906    case False{}:
5907      render.skip(path, rows, tail, gap, trail, nest, rest)
5908    case True{}:
5909      "[[" ++ path ++ "]]\n" ++ render.use(rows, nest(Unit{})) ++
5910        render.rest(tail, gap, trail, rest)
5911
5912# a key, an array, or an inline table. The text is built only by the pass that writes keys
5913def render.late(
5914  tabs: Bool,
5915  text: Unit -> String,
5916  tail: List<&2, Val>,
5917  gap: String,
5918  trail: Bool,
5919  rest: Unit -> String
5920) -> String:
5921  match tabs:
5922    case True{}:
5923      rest(Unit{})
5924    case False{}:
5925      text(Unit{}) ++ render.suf(gap, trail, List.is_empty(&2, Val, tail)) ++ rest(Unit{})
5926
5927# one pass: keys, or the tables that follow them
5928def render.pass(vs: List<&2, Val>, +gap: String, +trail: Bool, +tabs: Bool) -> String:
5929  match vs:
5930    case []:
5931      ""
5932    case VPair{_name, VHead{path, +rows}} <> +t:
5933      render.head(tabs, path, rows, t, gap, trail,
5934        _u => render.pass(rows, "\n", True{}, False{}) ++
5935          render.pass(rows, "\n", True{}, True{}),
5936        _u => render.pass(t, gap, trail, tabs))
5937    case VPair{_name, VAots{_path, +elems}} <> +t:
5938      render.aots(tabs, elems, t, gap, trail,
5939        _u => render.pass(elems, "\n", True{}, False{}) ++
5940          render.pass(elems, "\n", True{}, True{}),
5941        _u => render.pass(t, gap, trail, tabs))
5942    case VAot{path, +rows} <> +t:
5943      render.aot(tabs, path, rows, t, gap, trail,
5944        _u => render.pass(rows, "\n", True{}, False{}) ++
5945          render.pass(rows, "\n", True{}, True{}),
5946        _u => render.pass(t, gap, trail, tabs))
5947    case VPair{name, VArr{items}} <> +t:
5948      render.late(tabs, _u => key(name) ++ " = [" ++ render.go(items, ", ", False{}) ++ "]",
5949        t, gap, trail, _v => render.pass(t, gap, trail, tabs))
5950    case VPair{name, VInl{rows}} <> +t:
5951      render.late(tabs, _u => key(name) ++ " = {" ++ render.go(rows, ", ", False{}) ++ "}",
5952        t, gap, trail, _v => render.pass(t, gap, trail, tabs))
5953    case VPair{name, val} <> +t:
5954      render.late(tabs, _u => key(name) ++ " = " ++ render.atom(val), t, gap, trail,
5955        _v => render.pass(t, gap, trail, tabs))
5956    case VArr{items} <> +t:
5957      render.late(tabs, _u => "[" ++ render.go(items, ", ", False{}) ++ "]",
5958        t, gap, trail, _v => render.pass(t, gap, trail, tabs))
5959    case VInl{rows} <> +t:
5960      render.late(tabs, _u => "{" ++ render.go(rows, ", ", False{}) ++ "}",
5961        t, gap, trail, _v => render.pass(t, gap, trail, tabs))
5962    case v <> +t:
5963      render.late(tabs, _u => render.atom(v), t, gap, trail,
5964        _v => render.pass(t, gap, trail, tabs))
5965
5966# keys first, then tables and arrays of tables
5967def render.both(+vs: List<&2, Val>, +gap: String, +trail: Bool) -> String:
5968  render.pass(vs, gap, trail, False{}) ++ render.pass(vs, gap, trail, True{})
5969
5970# the text of a string value
5971def string(vv: Val) -> String:
5972  match vv:
5973    case VStr{text}:
5974      text
5975    case VSpan{src, +n}:
5976      span.str(src, n, U32.is_zero(n))
5977    case _:
5978      ""
5979
5980# the digits of an integer value
5981def digits(vv: Val) -> String:
5982  match vv:
5983    case VInt{_sign, text}:
5984      text
5985    case _:
5986      ""
5987
5988# the bit of a boolean value
5989def flag(vv: Val) -> Bool:
5990  match vv:
5991    case VBool{bit}:
5992      bit
5993    case _:
5994      False{}
5995
5996# the rows of a table value
5997def at.rows(vv: Val) -> List<&2, Val>:
5998  match vv:
5999    case VHead{_path, rows}:
6000      rows
6001    case VInl{rows}:
6002      rows
6003    case VAot{_path, rows}:
6004      rows
6005    case _:
6006      []
6007
6008# the rows of a hit, when it is a table
6009def at.rows_of(hh: Hit) -> List<&2, Val>:
6010  match hh:
6011    case Found{val}:
6012      at.rows(val)
6013    case Miss{}:
6014      []
6015
6016# the rest of a path after the first key
6017def at.step(rest: List<&2, String>, hit: Hit) -> Hit:
6018  match rest:
6019    case []:
6020      hit
6021    case name <> t:
6022      at.step(t, get(at.rows_of(hit), name))
6023
6024# the value at a dotted path
6025def at(rows: List<&2, Val>, path: List<&2, String>) -> Hit:
6026  match path:
6027    case []:
6028      Miss{}
6029    case name <> rest:
6030      at.step(rest, get(rows, name))
6031
6032# the root table
6033def root(doc: Doc) -> List<&2, Val>:
6034  Doc{_bad, rows} = doc
6035  rows
6036
6037# the first error, or "" when the document is well formed
6038def bad(doc: Doc) -> String:
6039  Doc{text, _rows} = doc
6040  text
6041
6042# a string value
6043def str(text: String) -> Val:
6044  VStr{text}
6045
6046# an integer value
6047def integer(sign: Sign, text: String) -> Val:
6048  VInt{sign, text}
6049
6050# a float value
6051def float(sign: Sign, text: String) -> Val:
6052  VFlo{sign, text}
6053
6054# a boolean value
6055def boolean(bit: Bool) -> Val:
6056  VBool{bit}
6057
6058# an array value
6059def array(items: List<&2, Val>) -> Val:
6060  VArr{items}
6061
6062# an inline table
6063def inline(rows: List<&2, Val>) -> Val:
6064  VInl{rows}
6065
6066# a table
6067def table(path: String, rows: List<&2, Val>) -> Val:
6068  VHead{path, rows}
6069
6070# a key and a value
6071def pair(name: String, val: Val) -> Val:
6072  VPair{name, val}
6073
6074# a document written back as TOML
6075def render(doc: Doc) -> String:
6076  Doc{_bad, rows} = doc
6077  render.both(rows, "\n", True{})
6078
6079# a document read from TOML text
6080def parse(text: String) -> Doc:
6081  doc.read(text, MScan{st.start()})
6082
6083# Well-formed documents: the shapes parse returns. The builders make any shape,
6084# and render writes TOML only for these.
6085
6086# where a list of values sits: a table's rows under its path (the root's is
6087# ""), an inline table's rows, an array's items, or the elements of an array of
6088# tables under its path
6089type WfAt is Data:
6090  WfRows{path: String}
6091  WfInl{}
6092  WfItems{}
6093  WfElems{path: String}
6094
6095# how far a float's spelling has been read: toml.abnf's float with no sign
6096# and no underscore, `dec-int ( exp / frac [ exp ] )`
6097type Fl is Data:
6098  FlStart{}
6099  FlZero{}
6100  FlInt{}
6101  FlDot{}
6102  FlFrac{}
6103  FlE{}
6104  FlESign{}
6105  FlExp{}
6106  FlNo{}
6107
6108# the rest when this part holds, and False otherwise
6109def wf.then(ok: Bool, more: Unit -> Bool) -> Bool:
6110  match ok:
6111    case True{}:
6112      more(Unit{})
6113    case False{}:
6114      False{}
6115
6116# a Unicode scalar value: no surrogate, and nothing past U+10FFFF
6117def wf.char(+cc: Char) -> Bool:
6118  uni.ok(Char.to_u32(cc))
6119
6120# every character of a string or a key is a Unicode scalar value
6121def wf.text(ss: String) -> Bool:
6122  match ss:
6123    case SNil{}:
6124      True{}
6125    case SCon{+h, t}:
6126      wf.then(wf.char(h), _u => wf.text(t))
6127
6128# a span's source holds its n characters, each a Unicode scalar value
6129def wf.span(src: String, +nn: U32, zz: Bool) -> Bool:
6130  match src zz:
6131    case _s True{}:
6132      True{}
6133    case SNil{} False{}:
6134      False{}
6135    case SCon{+h, t} False{}:
6136      wf.then(wf.char(h), _u => wf.span(t, U32.sub(nn, 1), U32.is_zero(U32.sub(nn, 1))))
6137
6138# every character is an ASCII digit
6139def wf.digits(ss: String) -> Bool:
6140  match ss:
6141    case SNil{}:
6142      True{}
6143    case SCon{+h, t}:
6144      wf.then(Char.is_digit(h), _u => wf.digits(t))
6145
6146# a lone 0, or a first digit that is not 0 and more digits
6147def wf.dec.lead(zero: Bool, +cc: Char, rest: String) -> Bool:
6148  match zero:
6149    case True{}:
6150      String.is_empty(rest)
6151    case False{}:
6152      Bool.and(Char.is_digit(cc), wf.digits(rest))
6153
6154# decimal digits with no leading zero, except 0 itself
6155def wf.dec(ss: String) -> Bool:
6156  match ss:
6157    case SNil{}:
6158      False{}
6159    case SCon{+h, t}:
6160      wf.dec.lead(Char.is_eq(h, '0'), h, t)
6161
6162# an integer: decimal digits within signed 64 bits
6163def wf.int(+sign: Sign, +digits: String) -> Bool:
6164  Bool.and(wf.dec(digits), i64.fits(sign, digits))
6165
6166# e or E
6167def wf.flo.is_e(+cc: Char) -> Bool:
6168  Bool.or(Char.is_eq(cc, 'e'), Char.is_eq(cc, 'E'))
6169
6170# after the integer part: a fraction or an exponent
6171def wf.flo.tail(+cc: Char) -> Fl:
6172  Bool.pick(Fl, Char.is_eq(cc, '.'), FlDot{}, Bool.pick(Fl, wf.flo.is_e(cc), FlE{}, FlNo{}))
6173
6174# one character of a float's spelling
6175def wf.flo.step(st: Fl, +cc: Char) -> Fl:
6176  match st:
6177    case FlStart{}:
6178      Bool.pick(Fl, Char.is_eq(cc, '0'), FlZero{}, Bool.pick(Fl, Char.is_digit(cc), FlInt{}, FlNo{}))
6179    case FlZero{}:
6180      wf.flo.tail(cc)
6181    case FlInt{}:
6182      Bool.pick(Fl, Char.is_digit(cc), FlInt{}, wf.flo.tail(cc))
6183    case FlDot{}:
6184      Bool.pick(Fl, Char.is_digit(cc), FlFrac{}, FlNo{})
6185    case FlFrac{}:
6186      Bool.pick(Fl, Char.is_digit(cc), FlFrac{}, Bool.pick(Fl, wf.flo.is_e(cc), FlE{}, FlNo{}))
6187    case FlE{}:
6188      Bool.pick(Fl, Bool.or(Char.is_eq(cc, '+'), Char.is_eq(cc, '-')), FlESign{},
6189        Bool.pick(Fl, Char.is_digit(cc), FlExp{}, FlNo{}))
6190    case FlESign{}:
6191      Bool.pick(Fl, Char.is_digit(cc), FlExp{}, FlNo{})
6192    case FlExp{}:
6193      Bool.pick(Fl, Char.is_digit(cc), FlExp{}, FlNo{})
6194    case FlNo{}:
6195      FlNo{}
6196
6197# a float's spelling read from the given state
6198def wf.flo.go(cs: List<&2, Char>, st: Fl) -> Fl:
6199  match cs:
6200    case []:
6201      st
6202    case +h <> t:
6203      wf.flo.go(t, wf.flo.step(st, h))
6204
6205# a spelling ends after a fraction's digit or an exponent's digit
6206def wf.flo.end(st: Fl) -> Bool:
6207  match st:
6208    case FlFrac{}:
6209      True{}
6210    case FlExp{}:
6211      True{}
6212    case _:
6213      False{}
6214
6215# a float's spelling: inf, nan, or toml.abnf's float with no sign and no `_`
6216def wf.flo(+text: String) -> Bool:
6217  Bool.or(str.eq(text, "inf"), Bool.or(str.eq(text, "nan"),
6218    wf.flo.end(wf.flo.go(String.to_list(text), FlStart{}))))
6219
6220# a date: a four-digit year, a month, and a day within that month in that year
6221def wf.date(dd: Date) -> Bool:
6222  Date{+y, +mo, +day} = dd
6223  Bool.and(U32.is_le(y, 9999), Bool.and(bound.rng(mo, 1, 12), bound.rng(day, 1, when.days(y, mo))))
6224
6225# a time of day: hour, minute and second in range, and a fraction of digits
6226def wf.clock(cc: Clock) -> Bool:
6227  Clock{+h, +mi, +s, frac} = cc
6228  Bool.and(U32.is_le(h, 23), Bool.and(U32.is_le(mi, 59), Bool.and(U32.is_le(s, 60), wf.digits(frac))))
6229
6230# a zone offset in range
6231def wf.zone(zz: Zone) -> Bool:
6232  match zz:
6233    case Zulu{}:
6234      True{}
6235    case Shift{_sign, +h, +mi}:
6236      Bool.and(U32.is_le(h, 23), U32.is_le(mi, 59))
6237
6238# a datetime whose fields are in range
6239def wf.when(ww: When) -> Bool:
6240  match ww:
6241    case WOff{date, clock, zone}:
6242      Bool.and(wf.date(date), Bool.and(wf.clock(clock), wf.zone(zone)))
6243    case WLocal{date, clock}:
6244      Bool.and(wf.date(date), wf.clock(clock))
6245    case WDate{date}:
6246      wf.date(date)
6247    case WTime{clock}:
6248      wf.clock(clock)
6249
6250# a string, a number, a boolean or a datetime, well-formed. Nothing else is a
6251# scalar
6252def wf.atom(vv: Val) -> Bool:
6253  match vv:
6254    case VStr{text}:
6255      wf.text(text)
6256    case VSpan{src, +n}:
6257      wf.span(src, n, U32.is_zero(n))
6258    case VInt{+sign, +digits}:
6259      wf.int(sign, digits)
6260    case VFlo{_sign, +text}:
6261      wf.flo(text)
6262    case VBool{_bit}:
6263      True{}
6264    case VWhen{w}:
6265      wf.when(w)
6266    case _:
6267      False{}
6268
6269# a name no later pair of the table has
6270def wf.fresh(hit: Hit) -> Bool:
6271  match hit:
6272    case Found{_v}:
6273      False{}
6274    case Miss{}:
6275      True{}
6276
6277# a pair's key: Unicode scalar values, and no later pair of the same name
6278def wf.key(+name: String, +rest: List<&2, Val>) -> Bool:
6279  Bool.and(wf.text(name), wf.fresh(get(rest, name)))
6280
6281# a table as a pair's value, in a table's rows, at the path its name gives
6282def wf.head(at: WfAt, +name: String, +path: String, +rest: List<&2, Val>, more: Unit -> Bool) -> Bool:
6283  match at:
6284    case WfRows{+here}:
6285      wf.then(Bool.and(wf.key(name, rest), str.eq(path, tree.pre(here, name))), more)
6286    case _:
6287      False{}
6288
6289# an array of tables as a pair's value, in a table's rows, at the path its
6290# name gives, with at least one element
6291def wf.aots(
6292  at: WfAt,
6293  +name: String,
6294  +path: String,
6295  some: Bool,
6296  +rest: List<&2, Val>,
6297  more: Unit -> Bool
6298) -> Bool:
6299  match at:
6300    case WfRows{+here}:
6301      wf.then(Bool.and(some, Bool.and(wf.key(name, rest), str.eq(path, tree.pre(here, name)))), more)
6302    case _:
6303      False{}
6304
6305# an element of an array of tables, at the array's path
6306def wf.aot(at: WfAt, +path: String, more: Unit -> Bool) -> Bool:
6307  match at:
6308    case WfElems{here}:
6309      wf.then(str.eq(path, here), more)
6310    case _:
6311      False{}
6312
6313# a pair of any other value, in a table's or an inline table's rows
6314def wf.pair(at: WfAt, +name: String, +rest: List<&2, Val>, ok: Bool, more: Unit -> Bool) -> Bool:
6315  match at:
6316    case WfRows{_here}:
6317      wf.then(Bool.and(ok, wf.key(name, rest)), more)
6318    case WfInl{}:
6319      wf.then(Bool.and(ok, wf.key(name, rest)), more)
6320    case _:
6321      False{}
6322
6323# a value that is not a pair, as an array's item
6324def wf.item(at: WfAt, ok: Bool, more: Unit -> Bool) -> Bool:
6325  match at:
6326    case WfItems{}:
6327      wf.then(ok, more)
6328    case _:
6329      False{}
6330
6331# a list of values, well-formed where it sits
6332def wf.go(vs: List<&2, Val>, +at: WfAt) -> Bool:
6333  match vs:
6334    case []:
6335      True{}
6336    case VPair{+name, VHead{+path, rows}} <> +t:
6337      wf.head(at, name, path, t,
6338        _u => wf.then(wf.go(rows, WfRows{path}), _v => wf.go(t, at)))
6339    case VPair{+name, VAots{+path, +elems}} <> +t:
6340      wf.aots(at, name, path, Bool.not(List.is_empty(&2, Val, elems)), t,
6341        _u => wf.then(wf.go(elems, WfElems{path}), _v => wf.go(t, at)))
6342    case VPair{+name, VArr{items}} <> +t:
6343      wf.pair(at, name, t, True{},
6344        _u => wf.then(wf.go(items, WfItems{}), _v => wf.go(t, at)))
6345    case VPair{+name, VInl{rows}} <> +t:
6346      wf.pair(at, name, t, True{},
6347        _u => wf.then(wf.go(rows, WfInl{}), _v => wf.go(t, at)))
6348    case VPair{+name, val} <> +t:
6349      wf.pair(at, name, t, wf.atom(val), _u => wf.go(t, at))
6350    case VAot{+path, rows} <> t:
6351      wf.aot(at, path,
6352        _u => wf.then(wf.go(rows, WfRows{path}), _v => wf.go(t, at)))
6353    case VArr{items} <> t:
6354      wf.item(at, True{},
6355        _u => wf.then(wf.go(items, WfItems{}), _v => wf.go(t, at)))
6356    case VInl{rows} <> t:
6357      wf.item(at, True{},
6358        _u => wf.then(wf.go(rows, WfInl{}), _v => wf.go(t, at)))
6359    case val <> t:
6360      wf.item(at, wf.atom(val), _u => wf.go(t, at))
6361
6362# whether a document is well-formed: the shapes parse returns. Tables and
6363# arrays of tables sit only as a pair's value in a table's rows, each at the
6364# path its parent's path and its name give; a table's keys are distinct;
6365# numbers, datetimes and strings are as parse reads them. The error is not
6366# looked at
6367def wf(doc: Doc) -> Bool:
6368  Doc{_bad, rows} = doc
6369  wf.go(rows, WfRows{""})