libs/JSON.bend

qasim-bend-kit@0.1.0.2 · 1,289 lines · 111 definitions

1import Base
2
3# JSON values preserve number lexemes as strings. This keeps integers and

4# fractional/exponent forms lossless without imposing a fixed numeric width.

5# Number carries grammar evidence so every constructible number is valid JSON.

6# Use number(text) or parse(text) to create numbers from runtime strings.

7def BoolType() -> Data:
8    Bool
9
10type NumberCert<-s: String> is Data:
11    Certified{witness: NumberProof(s)}
12
13type Value is Data:
14    Null{}
15    Bool{value: BoolType()}
16    Number{lexeme: String, certificate: NumberCert<lexeme>}
17    Str{value: String}
18    Arr{values: List<&2, Value>}
19    Obj{fields: List<&2, Sigma<&2, &2, String, key => Value>>}
20
21type Error is Data:
22    Error{}
23
24type Parsed is Type:
25    Parsed{value: Value, rest: String}
26
27type StringScan is Data:
28    StringScan{value: String, rest: String}
29
30type StringScanState is Type:
31    ScanText{input: String, reversed: String}
32    ScanControl{character: Char, rest: String, reversed: String, control: BoolType()}
33    ScanUnicode{parsed: Result<&1, &1, Error, HexScan>, reversed: String}
34    ScanUnicodeHigh{code: U32, rest: String, reversed: String, is_high: BoolType()}
35    ScanUnicodeLow{high: U32, original: String, parsed: Result<&1, &1, Error, HexScan>, reversed: String}
36    ScanUnicodeLowClass{high: U32, low: U32, rest: String, original: String, reversed: String, valid: BoolType()}
37
38type NumberState is Data:
39    NumberStart{}
40    NumberMinus{}
41    NumberZero{}
42    NumberInteger{}
43    NumberDot{}
44    NumberFraction{}
45    NumberExponent{}
46    NumberExponentSign{}
47    NumberExponentDigits{}
48    NumberInvalid{}
49
50def whitespace(s: String) -> String:
51    match s:
52        case SNil{}:
53            SNil{}
54        case SCon{+h, t}:
55            match h:
56                case ' ':
57                    whitespace(t)
58                case '\t':
59                    whitespace(t)
60                case '\r':
61                    whitespace(t)
62                case '\n':
63                    whitespace(t)
64                case _:
65                    SCon{h, t}
66
67def is_control(c: Char) -> BoolType():
68    match c:
69        case '\u{0}': True{}
70        case '\u{1}': True{}
71        case '\u{2}': True{}
72        case '\u{3}': True{}
73        case '\u{4}': True{}
74        case '\u{5}': True{}
75        case '\u{6}': True{}
76        case '\u{7}': True{}
77        case '\u{8}': True{}
78        case '\u{9}': True{}
79        case '\u{a}': True{}
80        case '\u{b}': True{}
81        case '\u{c}': True{}
82        case '\u{d}': True{}
83        case '\u{e}': True{}
84        case '\u{f}': True{}
85        case '\u{10}': True{}
86        case '\u{11}': True{}
87        case '\u{12}': True{}
88        case '\u{13}': True{}
89        case '\u{14}': True{}
90        case '\u{15}': True{}
91        case '\u{16}': True{}
92        case '\u{17}': True{}
93        case '\u{18}': True{}
94        case '\u{19}': True{}
95        case '\u{1a}': True{}
96        case '\u{1b}': True{}
97        case '\u{1c}': True{}
98        case '\u{1d}': True{}
99        case '\u{1e}': True{}
100        case '\u{1f}': True{}
101        case _: False{}
102
103def escape_char_special(c: Char) -> String:
104    match c:
105        case '\u{0}': "\\u0000"
106        case '\u{1}': "\\u0001"
107        case '\u{2}': "\\u0002"
108        case '\u{3}': "\\u0003"
109        case '\u{4}': "\\u0004"
110        case '\u{5}': "\\u0005"
111        case '\u{6}': "\\u0006"
112        case '\u{7}': "\\u0007"
113        case '\u{8}': "\\b"
114        case '\u{9}': "\\t"
115        case '\u{a}': "\\n"
116        case '\u{b}': "\\u000b"
117        case '\u{c}': "\\f"
118        case '\u{d}': "\\r"
119        case '\u{e}': "\\u000e"
120        case '\u{f}': "\\u000f"
121        case '\u{10}': "\\u0010"
122        case '\u{11}': "\\u0011"
123        case '\u{12}': "\\u0012"
124        case '\u{13}': "\\u0013"
125        case '\u{14}': "\\u0014"
126        case '\u{15}': "\\u0015"
127        case '\u{16}': "\\u0016"
128        case '\u{17}': "\\u0017"
129        case '\u{18}': "\\u0018"
130        case '\u{19}': "\\u0019"
131        case '\u{1a}': "\\u001a"
132        case '\u{1b}': "\\u001b"
133        case '\u{1c}': "\\u001c"
134        case '\u{1d}': "\\u001d"
135        case '\u{1e}': "\\u001e"
136        case '\u{1f}': "\\u001f"
137        case '\u{22}': "\\\""
138        case '\u{5c}': "\\\\"
139        case _: SCon{c, SNil{}}
140
141type EscapeClass is Data:
142    Raw{}
143    Backslash{}
144    Quote{}
145    Control0{}
146    Control1{}
147    Control2{}
148    Control3{}
149    Control4{}
150    Control5{}
151    Control6{}
152    Control7{}
153    Control8{}
154    Control9{}
155    Control10{}
156    Control11{}
157    Control12{}
158    Control13{}
159    Control14{}
160    Control15{}
161    Control16{}
162    Control17{}
163    Control18{}
164    Control19{}
165    Control20{}
166    Control21{}
167    Control22{}
168    Control23{}
169    Control24{}
170    Control25{}
171    Control26{}
172    Control27{}
173    Control28{}
174    Control29{}
175    Control30{}
176    Control31{}
177
178def escape_class(character: Char) -> EscapeClass:
179    match character:
180        case '\u{0}': Control0{}
181        case '\u{1}': Control1{}
182        case '\u{2}': Control2{}
183        case '\u{3}': Control3{}
184        case '\u{4}': Control4{}
185        case '\u{5}': Control5{}
186        case '\u{6}': Control6{}
187        case '\u{7}': Control7{}
188        case '\u{8}': Control8{}
189        case '\u{9}': Control9{}
190        case '\u{a}': Control10{}
191        case '\u{b}': Control11{}
192        case '\u{c}': Control12{}
193        case '\u{d}': Control13{}
194        case '\u{e}': Control14{}
195        case '\u{f}': Control15{}
196        case '\u{10}': Control16{}
197        case '\u{11}': Control17{}
198        case '\u{12}': Control18{}
199        case '\u{13}': Control19{}
200        case '\u{14}': Control20{}
201        case '\u{15}': Control21{}
202        case '\u{16}': Control22{}
203        case '\u{17}': Control23{}
204        case '\u{18}': Control24{}
205        case '\u{19}': Control25{}
206        case '\u{1a}': Control26{}
207        case '\u{1b}': Control27{}
208        case '\u{1c}': Control28{}
209        case '\u{1d}': Control29{}
210        case '\u{1e}': Control30{}
211        case '\u{1f}': Control31{}
212        case '"': Quote{}
213        case '\\': Backslash{}
214        case _: Raw{}
215
216type QuoteAction is Data:
217    QuoteBackslash{}
218    QuoteEnd{}
219    QuotePlain{}
220
221def quote_action_from_class(class: EscapeClass) -> QuoteAction:
222    match class:
223        case Backslash{}: QuoteBackslash{}
224        case Quote{}: QuoteEnd{}
225        case _: QuotePlain{}
226
227def quote_action(character: Char) -> QuoteAction:
228    quote_action_from_class(escape_class(character))
229
230def quote_lex_action(action: QuoteAction) -> LexAction:
231    match action:
232        case QuoteBackslash{}: LexBackslash{}
233        case QuoteEnd{}: LexStringEnd{}
234        case QuotePlain{}: LexStringChar{}
235
236def escape_char_from_class(character: Char, class: EscapeClass) -> String:
237    match class:
238        case Raw{}: SCon{character, SNil{}}
239        case Backslash{}: "\\\\"
240        case Quote{}: "\\\""
241        case Control0{}: "\\u0000"
242        case Control1{}: "\\u0001"
243        case Control2{}: "\\u0002"
244        case Control3{}: "\\u0003"
245        case Control4{}: "\\u0004"
246        case Control5{}: "\\u0005"
247        case Control6{}: "\\u0006"
248        case Control7{}: "\\u0007"
249        case Control8{}: "\\b"
250        case Control9{}: "\\t"
251        case Control10{}: "\\n"
252        case Control11{}: "\\u000b"
253        case Control12{}: "\\f"
254        case Control13{}: "\\r"
255        case Control14{}: "\\u000e"
256        case Control15{}: "\\u000f"
257        case Control16{}: "\\u0010"
258        case Control17{}: "\\u0011"
259        case Control18{}: "\\u0012"
260        case Control19{}: "\\u0013"
261        case Control20{}: "\\u0014"
262        case Control21{}: "\\u0015"
263        case Control22{}: "\\u0016"
264        case Control23{}: "\\u0017"
265        case Control24{}: "\\u0018"
266        case Control25{}: "\\u0019"
267        case Control26{}: "\\u001a"
268        case Control27{}: "\\u001b"
269        case Control28{}: "\\u001c"
270        case Control29{}: "\\u001d"
271        case Control30{}: "\\u001e"
272        case Control31{}: "\\u001f"
273
274def escape_char(+character: Char) -> String:
275    escape_char_from_class(character, escape_class(character))
276
277def escape_string(s: String) -> String:
278    match s:
279        case SNil{}:
280            ""
281        case SCon{h, t}:
282            escape_char(h) ++ escape_string(t)
283
284# Structural rendering has no fuel limit. Tail mode emits the comma before

285# each subsequent member and the closing delimiter at the empty tail.

286def render_object_field(prefix: String, key: String, value_text: String) -> String:
287    (prefix ++ ("\"" ++ escape_string(key) ++ "\":")) ++ value_text
288
289def render(value: Value, members: BoolType(), suffix: String) -> String:
290    match value:
291        case Null{}: "null" ++ suffix
292        case Bool{truth}:
293            match truth:
294                case True{}: "true" ++ suffix
295                case False{}: "false" ++ suffix
296        case Number{lexeme, certificate}: lexeme ++ suffix
297        case Str{text}: "\"" ++ escape_string(text) ++ "\"" ++ suffix
298        case Arr{Nil{}}:
299            match members:
300                case False{}: "[]" ++ suffix
301                case True{}: "]" ++ suffix
302        case Arr{head <> tail}:
303            match members:
304                case False{}: "[" ++ render(head, False{}, render(Arr{tail}, True{}, suffix))
305                case True{}: "," ++ render(head, False{}, render(Arr{tail}, True{}, suffix))
306        case Obj{Nil{}}:
307            match members:
308                case False{}: "{}" ++ suffix
309                case True{}: "}" ++ suffix
310        case Obj{(key, value) <> tail}:
311            match members:
312                case False{}: render_object_field("{", key, render(value, False{}, render(Obj{tail}, True{}, suffix)))
313                case True{}: render_object_field(",", key, render(value, False{}, render(Obj{tail}, True{}, suffix)))
314
315def stringify(value: Value) -> String:
316    render(value, False{}, SNil{})
317
318# A hexadecimal escape is exactly four digits. The code preserves standalone

319# UTF-16 surrogate escapes and combines adjacent high/low pairs into a scalar.

320# This accepts the JSON string grammar without silently replacing code units.

321type HexScan is Data:
322    HexScan{code: U32, rest: String}
323
324def hex_digit(c: Char) -> Maybe<&2, U32>:
325    match c:
326        case '0': Some{0}
327        case '1': Some{1}
328        case '2': Some{2}
329        case '3': Some{3}
330        case '4': Some{4}
331        case '5': Some{5}
332        case '6': Some{6}
333        case '7': Some{7}
334        case '8': Some{8}
335        case '9': Some{9}
336        case 'a': Some{10}
337        case 'b': Some{11}
338        case 'c': Some{12}
339        case 'd': Some{13}
340        case 'e': Some{14}
341        case 'f': Some{15}
342        case 'A': Some{10}
343        case 'B': Some{11}
344        case 'C': Some{12}
345        case 'D': Some{13}
346        case 'E': Some{14}
347        case 'F': Some{15}
348        case _: None{}
349
350def scan_hex(n: Nat, s: String, acc: U32) -> Result<&1, &1, Error, HexScan>:
351    match n:
352        case 0n:
353            Done{HexScan{acc, s}}
354        case 1n+p:
355            match s:
356                case SNil{}:
357                    Fail{Error{}}
358                case SCon{'0', t}:
359                    scan_hex(p, t, (acc * 16 + 0 : U32))
360                case SCon{'1', t}:
361                    scan_hex(p, t, (acc * 16 + 1 : U32))
362                case SCon{'2', t}:
363                    scan_hex(p, t, (acc * 16 + 2 : U32))
364                case SCon{'3', t}:
365                    scan_hex(p, t, (acc * 16 + 3 : U32))
366                case SCon{'4', t}:
367                    scan_hex(p, t, (acc * 16 + 4 : U32))
368                case SCon{'5', t}:
369                    scan_hex(p, t, (acc * 16 + 5 : U32))
370                case SCon{'6', t}:
371                    scan_hex(p, t, (acc * 16 + 6 : U32))
372                case SCon{'7', t}:
373                    scan_hex(p, t, (acc * 16 + 7 : U32))
374                case SCon{'8', t}:
375                    scan_hex(p, t, (acc * 16 + 8 : U32))
376                case SCon{'9', t}:
377                    scan_hex(p, t, (acc * 16 + 9 : U32))
378                case SCon{'a', t}:
379                    scan_hex(p, t, (acc * 16 + 10 : U32))
380                case SCon{'b', t}:
381                    scan_hex(p, t, (acc * 16 + 11 : U32))
382                case SCon{'c', t}:
383                    scan_hex(p, t, (acc * 16 + 12 : U32))
384                case SCon{'d', t}:
385                    scan_hex(p, t, (acc * 16 + 13 : U32))
386                case SCon{'e', t}:
387                    scan_hex(p, t, (acc * 16 + 14 : U32))
388                case SCon{'f', t}:
389                    scan_hex(p, t, (acc * 16 + 15 : U32))
390                case SCon{'A', t}:
391                    scan_hex(p, t, (acc * 16 + 10 : U32))
392                case SCon{'B', t}:
393                    scan_hex(p, t, (acc * 16 + 11 : U32))
394                case SCon{'C', t}:
395                    scan_hex(p, t, (acc * 16 + 12 : U32))
396                case SCon{'D', t}:
397                    scan_hex(p, t, (acc * 16 + 13 : U32))
398                case SCon{'E', t}:
399                    scan_hex(p, t, (acc * 16 + 14 : U32))
400                case SCon{'F', t}:
401                    scan_hex(p, t, (acc * 16 + 15 : U32))
402                case _:
403                    Fail{Error{}}
404
405def string_push(c: Char,
406                result: Result<&1, &1, Error, StringScan>) -> Result<&1, &1, Error, StringScan>:
407    match result:
408        case Fail{e}:
409            Fail{e}
410        case Done{scan}:
411            match scan:
412                case StringScan{s, rest}:
413                    Done{StringScan{SCon{c, s}, rest}}
414
415def scan_string_machine(fuel: Nat, state: StringScanState) -> Result<&1, &1, Error, StringScan>:
416    match fuel:
417        case 0n:
418            Fail{Error{}}
419        case 1n+p:
420            match state:
421                case ScanText{input, reversed}:
422                    match input:
423                        case SNil{}:
424                            Fail{Error{}}
425                        case SCon{+h, +t}:
426                            match h:
427                                case '"':
428                                    Done{StringScan{String.reverse(reversed), t}}
429                                case '\\':
430                                    match t:
431                                        case SNil{}:
432                                            Fail{Error{}}
433                                        case SCon{e, et}:
434                                            match e:
435                                                case '"': scan_string_machine(p, ScanText{et, SCon{'"', reversed}})
436                                                case '\\': scan_string_machine(p, ScanText{et, SCon{'\\', reversed}})
437                                                case '/': scan_string_machine(p, ScanText{et, SCon{'/', reversed}})
438                                                case 'b': scan_string_machine(p, ScanText{et, SCon{'\u{8}', reversed}})
439                                                case 'f': scan_string_machine(p, ScanText{et, SCon{'\u{c}', reversed}})
440                                                case 'n': scan_string_machine(p, ScanText{et, SCon{'\n', reversed}})
441                                                case 'r': scan_string_machine(p, ScanText{et, SCon{'\r', reversed}})
442                                                case 't': scan_string_machine(p, ScanText{et, SCon{'\t', reversed}})
443                                                case 'u': scan_string_machine(p, ScanUnicode{scan_hex(4n, et, 0), reversed})
444                                                case _: Fail{Error{}}
445                                case _:
446                                    scan_string_machine(p, ScanControl{h, t, reversed, is_control(h)})
447                case ScanControl{character, rest, reversed, control}:
448                    match control:
449                        case True{}:
450                            Fail{Error{}}
451                        case False{}:
452                            scan_string_machine(p, ScanText{rest, SCon{character, reversed}})
453                case ScanUnicode{parsed, reversed}:
454                    match parsed:
455                        case Fail{e}:
456                            Fail{e}
457                        case Done{scan}:
458                            match scan:
459                                case HexScan{+code, +rest}:
460                                    scan_string_machine(p, ScanUnicodeHigh{code, rest, reversed, U32.is_ge(code, 55296) && U32.is_le(code, 56319)})
461                case ScanUnicodeHigh{code, +rest, +reversed, is_high}:
462                    match rest:
463                        case SCon{'\\', SCon{'u', t}}:
464                            match is_high:
465                                case True{}:
466                                    scan_string_machine(p, ScanUnicodeLow{code, rest, scan_hex(4n, t, 0), reversed})
467                                case False{}:
468                                    scan_string_machine(p, ScanText{rest, SCon{Char.from_u32(code), reversed}})
469                        case _:
470                            scan_string_machine(p, ScanText{rest, SCon{Char.from_u32(code), reversed}})
471                case ScanUnicodeLow{high, original, parsed, reversed}:
472                    match parsed:
473                        case Fail{e}:
474                            scan_string_machine(p, ScanText{original, SCon{Char.from_u32(high), reversed}})
475                        case Done{scan}:
476                            match scan:
477                                case HexScan{+low, +rest}:
478                                    scan_string_machine(p, ScanUnicodeLowClass{high, low, rest, original, reversed, U32.is_ge(low, 56320) && U32.is_le(low, 57343)})
479                case ScanUnicodeLowClass{high, low, rest, original, reversed, valid}:
480                    match valid:
481                        case True{}:
482                            scan_string_machine(p, ScanText{rest, SCon{Char.from_u32((65536 + (high - 55296) * 1024 + (low - 56320) : U32)), reversed}})
483                        case False{}:
484                            scan_string_machine(p, ScanText{original, SCon{Char.from_u32(high), reversed}})
485
486def scan_string(+s: String) -> Result<&1, &1, Error, StringScan>:
487    scan_string_machine((String.length(s) * 2n + 16n : Nat), ScanText{s, SNil{}})
488
489def scan_number(s: String, acc: String) -> StringScan:
490    match s:
491        case SNil{}:
492            StringScan{String.reverse(acc), SNil{}}
493        case SCon{h, t}:
494            match h:
495                case '-': scan_number(t, SCon{h, acc})
496                case '+': scan_number(t, SCon{h, acc})
497                case '.': scan_number(t, SCon{h, acc})
498                case 'e': scan_number(t, SCon{h, acc})
499                case 'E': scan_number(t, SCon{h, acc})
500                case '0': scan_number(t, SCon{h, acc})
501                case '1': scan_number(t, SCon{h, acc})
502                case '2': scan_number(t, SCon{h, acc})
503                case '3': scan_number(t, SCon{h, acc})
504                case '4': scan_number(t, SCon{h, acc})
505                case '5': scan_number(t, SCon{h, acc})
506                case '6': scan_number(t, SCon{h, acc})
507                case '7': scan_number(t, SCon{h, acc})
508                case '8': scan_number(t, SCon{h, acc})
509                case '9': scan_number(t, SCon{h, acc})
510                case _: StringScan{String.reverse(acc), SCon{h, t}}
511
512type NumberChar is Data:
513    NMinus{}
514    NPlus{}
515    NDot{}
516    NExp{}
517    NZero{}
518    NDigit{}
519    NOther{}
520
521def number_char(c: Char) -> NumberChar:
522    match c:
523        case '-': NMinus{}
524        case '+': NPlus{}
525        case '.': NDot{}
526        case 'e': NExp{}
527        case 'E': NExp{}
528        case '0': NZero{}
529        case '1': NDigit{}
530        case '2': NDigit{}
531        case '3': NDigit{}
532        case '4': NDigit{}
533        case '5': NDigit{}
534        case '6': NDigit{}
535        case '7': NDigit{}
536        case '8': NDigit{}
537        case '9': NDigit{}
538        case _: NOther{}
539
540def number_step(character: NumberChar, state: NumberState) -> NumberState:
541    match character state:
542        case NOther{} _: NumberInvalid{}
543        case NMinus{} NumberStart{}: NumberMinus{}
544        case NMinus{} NumberExponent{}: NumberExponentSign{}
545        case NPlus{} NumberExponent{}: NumberExponentSign{}
546        case NDot{} NumberZero{}: NumberDot{}
547        case NDot{} NumberInteger{}: NumberDot{}
548        case NExp{} NumberZero{}: NumberExponent{}
549        case NExp{} NumberInteger{}: NumberExponent{}
550        case NExp{} NumberFraction{}: NumberExponent{}
551        case NZero{} NumberStart{}: NumberZero{}
552        case NZero{} NumberMinus{}: NumberZero{}
553        case NZero{} NumberInteger{}: NumberInteger{}
554        case NZero{} NumberDot{}: NumberFraction{}
555        case NZero{} NumberFraction{}: NumberFraction{}
556        case NZero{} NumberExponent{}: NumberExponentDigits{}
557        case NZero{} NumberExponentSign{}: NumberExponentDigits{}
558        case NZero{} NumberExponentDigits{}: NumberExponentDigits{}
559        case NDigit{} NumberStart{}: NumberInteger{}
560        case NDigit{} NumberMinus{}: NumberInteger{}
561        case NDigit{} NumberInteger{}: NumberInteger{}
562        case NDigit{} NumberDot{}: NumberFraction{}
563        case NDigit{} NumberFraction{}: NumberFraction{}
564        case NDigit{} NumberExponent{}: NumberExponentDigits{}
565        case NDigit{} NumberExponentSign{}: NumberExponentDigits{}
566        case NDigit{} NumberExponentDigits{}: NumberExponentDigits{}
567        case _ _: NumberInvalid{}
568
569def number_next(state: NumberState, c: Char) -> NumberState:
570    match state:
571        case NumberInvalid{}: NumberInvalid{}
572        case _: number_step(number_char(c), state)
573
574def number_valid_end(state: NumberState) -> BoolType():
575    match state:
576        case NumberZero{}:
577            True{}
578        case NumberInteger{}:
579            True{}
580        case NumberFraction{}:
581            True{}
582        case NumberExponentDigits{}:
583            True{}
584        case _:
585            False{}
586
587def number_valid_step(s: String, state: NumberState) -> NumberState:
588    match s state:
589        case _ NumberInvalid{}:
590            NumberInvalid{}
591        case SNil{} _:
592            state
593        case SCon{h, t} _:
594            number_valid_step(t, number_next(state, h))
595
596def number_valid(+s: String) -> BoolType():
597    number_valid_end(number_valid_step(s, NumberStart{}))
598
599def NumberProofFrom(valid: BoolType()) -> Data:
600    match valid:
601        case True{}:
602            Unit
603        case False{}:
604            Empty
605
606def NumberProof(s: String) -> Data:
607    NumberProofFrom(number_valid(s))
608
609def null_token(s: String, matches: BoolType()) -> Result<&1, &1, Error, Parsed>:
610    match matches:
611        case True{}:
612            Done{Parsed{Null{}, String.drop(s, 4n)}}
613        case False{}:
614            Fail{Error{}}
615
616def true_token(s: String, matches: BoolType()) -> Result<&1, &1, Error, Parsed>:
617    match matches:
618        case True{}:
619            Done{Parsed{Bool{True{}}, String.drop(s, 4n)}}
620        case False{}:
621            Fail{Error{}}
622
623def false_token(s: String, matches: BoolType()) -> Result<&1, &1, Error, Parsed>:
624    match matches:
625        case True{}:
626            Done{Parsed{Bool{False{}}, String.drop(s, 5n)}}
627        case False{}:
628            Fail{Error{}}
629
630def from_string_scan(scanned: Result<&1, &1, Error, StringScan>) -> Result<&1, &1, Error, Parsed>:
631    match scanned:
632        case Fail{e}:
633            Fail{e}
634        case Done{scan}:
635            match scan:
636                case StringScan{value, rest}:
637                    Done{Parsed{Str{value}, rest}}
638
639def number_proof(+lexeme: String,
640                 evidence: {number_valid(lexeme) == True{} : BoolType()}) -> NumberProof(lexeme):
641    %Equal.sym(BoolType(), number_valid(lexeme), True{}, evidence) : NumberProofFrom(_)
642    Unit{}
643
644def number_lexeme(+lexeme: String,
645                  rest: String,
646                  valid: BoolType(),
647                  evidence: {number_valid(lexeme) == valid : BoolType()}) -> Result<&1, &1, Error, Parsed>:
648    match valid:
649        case True{}:
650            Done{Parsed{Number{lexeme, Certified{number_proof(lexeme, evidence)}}, rest}}
651        case False{}:
652            Fail{Error{}}
653
654def from_number_scan(scan: StringScan) -> Result<&1, &1, Error, Parsed>:
655    match scan:
656        case StringScan{+lexeme, rest}:
657            number_lexeme(lexeme, rest, number_valid(lexeme), {==})
658
659def parse_number(s: String) -> Result<&1, &1, Error, Parsed>:
660    from_number_scan(scan_number(s, SNil{}))
661
662def number_from_digit(s: String, digit: BoolType()) -> Result<&1, &1, Error, Parsed>:
663    match digit:
664        case True{}:
665            parse_number(s)
666        case False{}:
667            Fail{Error{}}
668
669# The parser is an explicit machine. Its fuel decreases on every state

670# transition, including transitions between container contexts.

671type ParserKont is Data:
672    Top{}
673    InArray{acc: List<&2, Value>, parent: ParserKont}
674    InObject{key: String, acc: List<&2, Sigma<&2, &2, String, key => Value>>, parent: ParserKont}
675
676type ParserState is Type:
677    ParseValue{clean: String, kont: ParserKont}
678    ParsedResult{result: Result<&1, &1, Error, Parsed>, kont: ParserKont}
679    StringResult{result: Result<&1, &1, Error, StringScan>, kont: ParserKont}
680    ArrayStart{clean: String, acc: List<&2, Value>, empty_allowed: BoolType(), kont: ParserKont}
681    ArrayAfter{value: Value, clean: String, acc: List<&2, Value>, kont: ParserKont}
682    ObjectStart{clean: String, acc: List<&2, Sigma<&2, &2, String, key => Value>>, empty_allowed: BoolType(), kont: ParserKont}
683    ObjectKey{result: Result<&1, &1, Error, StringScan>, acc: List<&2, Sigma<&2, &2, String, key => Value>>, kont: ParserKont}
684    ObjectColon{key: String, clean: String, acc: List<&2, Sigma<&2, &2, String, key => Value>>, kont: ParserKont}
685    ObjectAfter{key: String, value: Value, clean: String, acc: List<&2, Sigma<&2, &2, String, key => Value>>, kont: ParserKont}
686    Complete{parsed: Parsed}
687
688def resume_value(value: Value, rest: String, kont: ParserKont) -> ParserState:
689    match kont:
690        case Top{}:
691            Complete{Parsed{value, rest}}
692        case InArray{acc, parent}:
693            ArrayAfter{value, whitespace(rest), acc, parent}
694        case InObject{key, acc, parent}:
695            ObjectAfter{key, value, whitespace(rest), acc, parent}
696
697def parse_machine(fuel: Nat, state: ParserState) -> Result<&1, &1, Error, Parsed>:
698    match fuel:
699        case 0n:
700            Fail{Error{}}
701        case 1n+p:
702            match state:
703                case Complete{parsed}:
704                    Done{parsed}
705                case ParseValue{+clean, +kont}:
706                    match clean:
707                        case SNil{}:
708                            Fail{Error{}}
709                        case SCon{+h, +t}:
710                            match h:
711                                case 'n':
712                                    parse_machine(p, ParsedResult{null_token(clean, String.starts_with(clean, "null")), kont})
713                                case 't':
714                                    parse_machine(p, ParsedResult{true_token(clean, String.starts_with(clean, "true")), kont})
715                                case 'f':
716                                    parse_machine(p, ParsedResult{false_token(clean, String.starts_with(clean, "false")), kont})
717                                case '"':
718                                    +budget = p
719                                    parse_machine(budget, StringResult{scan_string_machine(budget, ScanText{t, SNil{}}), kont})
720                                case '[':
721                                    parse_machine(p, ArrayStart{whitespace(t), Nil{}, True{}, kont})
722                                case '{':
723                                    parse_machine(p, ObjectStart{whitespace(t), Nil{}, True{}, kont})
724                                case '-':
725                                    parse_machine(p, ParsedResult{parse_number(clean), kont})
726                                case _:
727                                    parse_machine(p, ParsedResult{number_from_digit(clean, Char.is_digit(h)), kont})
728                case ParsedResult{result, kont}:
729                    match result:
730                        case Fail{e}:
731                            Fail{e}
732                        case Done{parsed}:
733                            match parsed:
734                                case Parsed{value, rest}:
735                                    parse_machine(p, resume_value(value, rest, kont))
736                case StringResult{result, kont}:
737                    match result:
738                        case Fail{e}:
739                            Fail{e}
740                        case Done{scan}:
741                            match scan:
742                                case StringScan{value, rest}:
743                                    parse_machine(p, resume_value(Str{value}, rest, kont))
744                case ArrayStart{clean, acc, empty_allowed, kont}:
745                    match clean:
746                        case SNil{}:
747                            Fail{Error{}}
748                        case SCon{h, t}:
749                            match h:
750                                case ']':
751                                    match empty_allowed:
752                                        case True{}:
753                                            parse_machine(p, resume_value(Arr{List.reverse(&2, Value, acc)}, t, kont))
754                                        case False{}:
755                                            Fail{Error{}}
756                                case _:
757                                    parse_machine(p, ParseValue{clean, InArray{acc, kont}})
758                case ArrayAfter{value, clean, acc, kont}:
759                    match clean:
760                        case SNil{}:
761                            Fail{Error{}}
762                        case SCon{h, t}:
763                            match h:
764                                case ']':
765                                    parse_machine(p, resume_value(Arr{List.reverse(&2, Value, value <> acc)}, t, kont))
766                                case ',':
767                                    parse_machine(p, ArrayStart{whitespace(t), value <> acc, False{}, kont})
768                                case _:
769                                    Fail{Error{}}
770                case ObjectStart{clean, acc, empty_allowed, kont}:
771                    match clean:
772                        case SNil{}:
773                            Fail{Error{}}
774                        case SCon{h, t}:
775                            match h:
776                                case '}':
777                                    match empty_allowed:
778                                        case True{}:
779                                            parse_machine(p, resume_value(Obj{List.reverse(&2, Sigma<&2, &2, String, key => Value>, acc)}, t, kont))
780                                        case False{}:
781                                            Fail{Error{}}
782                                case '"':
783                                    +budget = p
784                                    parse_machine(budget, ObjectKey{scan_string_machine(budget, ScanText{t, SNil{}}), acc, kont})
785                                case _:
786                                    Fail{Error{}}
787                case ObjectKey{result, acc, kont}:
788                    match result:
789                        case Fail{e}:
790                            Fail{e}
791                        case Done{scan}:
792                            match scan:
793                                case StringScan{key, rest}:
794                                    parse_machine(p, ObjectColon{key, whitespace(rest), acc, kont})
795                case ObjectColon{key, clean, acc, kont}:
796                    match clean:
797                        case SNil{}:
798                            Fail{Error{}}
799                        case SCon{h, t}:
800                            match h:
801                                case ':':
802                                    parse_machine(p, ParseValue{whitespace(t), InObject{key, acc, kont}})
803                                case _:
804                                    Fail{Error{}}
805                case ObjectAfter{key, value, clean, acc, kont}:
806                    match clean:
807                        case SNil{}:
808                            Fail{Error{}}
809                        case SCon{h, t}:
810                            match h:
811                                case '}':
812                                    parse_machine(p, resume_value(Obj{List.reverse(&2, Sigma<&2, &2, String, key => Value>, (key, value) <> acc)}, t, kont))
813                                case ',':
814                                    parse_machine(p, ObjectStart{whitespace(t), (key, value) <> acc, False{}, kont})
815                                case _:
816                                    Fail{Error{}}
817
818def parse_value(+s: String) -> Result<&1, &1, Error, Parsed>:
819    parse_machine((String.length(s) * 8n + 16n : Nat), ParseValue{whitespace(s), Top{}})
820
821def finish_rest_clean(value: Value, clean: String) -> Result<&1, &1, Error, Value>:
822    match clean:
823        case SNil{}:
824            Done{value}
825        case _:
826            Fail{Error{}}
827
828def finish_rest(value: Value, rest: String) -> Result<&1, &1, Error, Value>:
829    finish_rest_clean(value, whitespace(rest))
830
831def finish(r: Result<&1, &1, Error, Parsed>) -> Result<&1, &1, Error, Value>:
832    match r:
833        case Fail{e}:
834            Fail{e}
835        case Done{parsed}:
836            match parsed:
837                case Parsed{value, rest}:
838                    finish_rest(value, rest)
839
840# Common JSON escapes have a structural decoder. Less common Unicode

841# escape spellings use the complete UTF-16 decoder below through the fallback.

842type FastString is Data:
843    Decoded{text: String}
844    InvalidString{}
845    UnicodeFallback{}
846
847def fast_push(result: FastString, character: Char) -> FastString:
848    match result:
849        case Decoded{text}: Decoded{SCon{character, text}}
850        case InvalidString{}: InvalidString{}
851        case UnicodeFallback{}: UnicodeFallback{}
852
853def fast_raw(control: BoolType(), result: FastString, character: Char) -> FastString:
854    match control:
855        case True{}: InvalidString{}
856        case False{}: fast_push(result, character)
857
858def fast_string(text: String) -> FastString:
859    match text:
860        case SCon{'"', SNil{}}: Decoded{SNil{}}
861        case SCon{'\\', SCon{'"', tail}}: fast_push(fast_string(tail), '\u{22}')
862        case SCon{'\\', SCon{'\\', tail}}: fast_push(fast_string(tail), '\u{5c}')
863        case SCon{'\\', SCon{'/', tail}}: fast_push(fast_string(tail), '/')
864        case SCon{'\\', SCon{'b', tail}}: fast_push(fast_string(tail), '\u{8}')
865        case SCon{'\\', SCon{'f', tail}}: fast_push(fast_string(tail), '\u{c}')
866        case SCon{'\\', SCon{'n', tail}}: fast_push(fast_string(tail), '\n')
867        case SCon{'\\', SCon{'r', tail}}: fast_push(fast_string(tail), '\r')
868        case SCon{'\\', SCon{'t', tail}}: fast_push(fast_string(tail), '\t')
869        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'0', tail}}}}}}: fast_push(fast_string(tail), '\u{0}')
870        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'1', tail}}}}}}: fast_push(fast_string(tail), '\u{1}')
871        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'2', tail}}}}}}: fast_push(fast_string(tail), '\u{2}')
872        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'3', tail}}}}}}: fast_push(fast_string(tail), '\u{3}')
873        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'4', tail}}}}}}: fast_push(fast_string(tail), '\u{4}')
874        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'5', tail}}}}}}: fast_push(fast_string(tail), '\u{5}')
875        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'6', tail}}}}}}: fast_push(fast_string(tail), '\u{6}')
876        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'7', tail}}}}}}: fast_push(fast_string(tail), '\u{7}')
877        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'8', tail}}}}}}: fast_push(fast_string(tail), '\u{8}')
878        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'9', tail}}}}}}: fast_push(fast_string(tail), '\u{9}')
879        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'a', tail}}}}}}: fast_push(fast_string(tail), '\u{a}')
880        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'b', tail}}}}}}: fast_push(fast_string(tail), '\u{b}')
881        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'c', tail}}}}}}: fast_push(fast_string(tail), '\u{c}')
882        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'d', tail}}}}}}: fast_push(fast_string(tail), '\u{d}')
883        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'e', tail}}}}}}: fast_push(fast_string(tail), '\u{e}')
884        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'0', SCon{'f', tail}}}}}}: fast_push(fast_string(tail), '\u{f}')
885        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'0', tail}}}}}}: fast_push(fast_string(tail), '\u{10}')
886        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'1', tail}}}}}}: fast_push(fast_string(tail), '\u{11}')
887        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'2', tail}}}}}}: fast_push(fast_string(tail), '\u{12}')
888        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'3', tail}}}}}}: fast_push(fast_string(tail), '\u{13}')
889        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'4', tail}}}}}}: fast_push(fast_string(tail), '\u{14}')
890        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'5', tail}}}}}}: fast_push(fast_string(tail), '\u{15}')
891        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'6', tail}}}}}}: fast_push(fast_string(tail), '\u{16}')
892        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'7', tail}}}}}}: fast_push(fast_string(tail), '\u{17}')
893        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'8', tail}}}}}}: fast_push(fast_string(tail), '\u{18}')
894        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'9', tail}}}}}}: fast_push(fast_string(tail), '\u{19}')
895        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'a', tail}}}}}}: fast_push(fast_string(tail), '\u{1a}')
896        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'b', tail}}}}}}: fast_push(fast_string(tail), '\u{1b}')
897        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'c', tail}}}}}}: fast_push(fast_string(tail), '\u{1c}')
898        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'d', tail}}}}}}: fast_push(fast_string(tail), '\u{1d}')
899        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'e', tail}}}}}}: fast_push(fast_string(tail), '\u{1e}')
900        case SCon{'\\', SCon{'u', SCon{'0', SCon{'0', SCon{'1', SCon{'f', tail}}}}}}: fast_push(fast_string(tail), '\u{1f}')
901        case SCon{'\\', SCon{'u', _}}: UnicodeFallback{}
902        case SCon{'\\', _}: InvalidString{}
903        case SCon{'"', _}: InvalidString{}
904        case SNil{}: InvalidString{}
905        case SCon{+c, tail}: fast_raw(is_control(c), fast_string(tail), c)
906
907def fast_result(result: FastString, original: String) -> Result<&1, &1, Error, Value>:
908    match result:
909        case Decoded{text}: Done{Str{text}}
910        case InvalidString{}: Fail{Error{}}
911        case UnicodeFallback{}: finish(parse_value(original))
912
913def payload_other(text: String) -> Result<&1, &1, Error, Value>:
914    match text:
915        case "null": Done{Null{}}
916        case "true": Done{Bool{True{}}}
917        case "false": Done{Bool{False{}}}
918        case SCon{'"', +tail}: fast_result(fast_string(tail), SCon{'"', tail})
919        case _: Fail{Error{}}
920
921def payload_number(+text: String,
922                   valid: BoolType(),
923                   evidence: {number_valid(text) == valid : BoolType()}) -> Result<&1, &1, Error, Value>:
924    match valid:
925        case True{}: Done{Number{text, Certified{number_proof(text, evidence)}}}
926        case False{}: payload_other(text)
927
928def decode_payload(+text: String) -> Result<&1, &1, Error, Value>:
929    payload_number(text, number_valid(text), {==})
930
931# Lexical boundaries are found once. Token payloads are then parsed on a

932# balanced fork tree, so strings and numbers in one document can use different

933# GPU lanes. Delimiter assembly follows token order.

934type Lexeme is Data:
935    Punctuation{character: Char}
936    Payload{text: String}
937
938def flush_lexeme(reversed: String, acc: List<&2, Lexeme>) -> List<&2, Lexeme>:
939    match reversed:
940        case SNil{}: acc
941        case SCon{h, t}: Payload{String.reverse(SCon{h, t})} <> acc
942
943type LexMode is Data:
944    Outside{}
945    Quoted{}
946    Escaped{}
947
948type LexAction is Data:
949    LexStop{}
950    LexEscapedChar{}
951    LexBackslash{}
952    LexStringEnd{}
953    LexStringChar{}
954    LexQuote{}
955    LexWhitespace{}
956    LexPunctuation{character: Char}
957    LexRaw{}
958
959def lex_outside_other(character: Char) -> LexAction:
960    match character:
961        case '"': LexQuote{}
962        case ' ': LexWhitespace{}
963        case '\t': LexWhitespace{}
964        case '\r': LexWhitespace{}
965        case '\n': LexWhitespace{}
966        case '[': LexPunctuation{'['}
967        case ']': LexPunctuation{']'}
968        case '{': LexPunctuation{'{'}
969        case '}': LexPunctuation{'}'}
970        case ':': LexPunctuation{':' }
971        case ',': LexPunctuation{','}
972        case _: LexRaw{}
973
974def lex_outside_action(character: Char, number_kind: NumberChar) -> LexAction:
975    match number_kind:
976        case NOther{}: lex_outside_other(character)
977        case _: LexRaw{}
978
979def lex_action(mode: LexMode, character: Char, number_kind: NumberChar) -> LexAction:
980    match mode:
981        case Escaped{}: LexEscapedChar{}
982        case Quoted{}: quote_lex_action(quote_action(character))
983        case Outside{}: lex_outside_action(character, number_kind)
984
985def lex_seed_action(text: String, mode: LexMode) -> LexAction:
986    match text:
987        case SNil{}: LexStop{}
988        case SCon{+character, _}: lex_action(mode, character, number_char(character))
989
990def lex_end(+mode: LexMode, reversed: String, acc: List<&2, Lexeme>) -> List<&2, Lexeme>:
991    match mode:
992        case Outside{}: List.reverse(&2, Lexeme, flush_lexeme(reversed, acc))
993        case Quoted{}: List.reverse(&2, Lexeme, Payload{"\""} <> acc)
994        case Escaped{}: List.reverse(&2, Lexeme, Payload{"\""} <> acc)
995
996def lexemes(text: String,
997            +mode: LexMode,
998            reversed: String,
999            acc: List<&2, Lexeme>,
1000            action: LexAction) -> List<&2, Lexeme>:
1001    match text action:
1002        case SNil{} LexStop{}:
1003            lex_end(mode, reversed, acc)
1004        case SNil{} _:
1005            List.reverse(&2, Lexeme, flush_lexeme(reversed, acc))
1006        case SCon{h, +t} LexStop{}:
1007            lexemes(t, mode, SCon{h, reversed}, acc, lex_seed_action(t, mode))
1008        case SCon{h, +t} LexEscapedChar{}:
1009            lexemes(t, Quoted{}, SCon{h, reversed}, acc, lex_seed_action(t, Quoted{}))
1010        case SCon{_, +t} LexBackslash{}:
1011            lexemes(t, Escaped{}, SCon{'\\', reversed}, acc, lex_seed_action(t, Escaped{}))
1012        case SCon{_, +t} LexStringEnd{}:
1013            lexemes(t, Outside{}, SNil{}, Payload{String.reverse(SCon{'"', reversed})} <> acc, lex_seed_action(t, Outside{}))
1014        case SCon{h, +t} LexStringChar{}:
1015            lexemes(t, Quoted{}, SCon{h, reversed}, acc, lex_seed_action(t, Quoted{}))
1016        case SCon{_, +t} LexQuote{}:
1017            lexemes(t, Quoted{}, SCon{'"', SNil{}}, flush_lexeme(reversed, acc), lex_seed_action(t, Quoted{}))
1018        case SCon{_, +t} LexWhitespace{}:
1019            lexemes(t, Outside{}, SNil{}, flush_lexeme(reversed, acc), lex_seed_action(t, Outside{}))
1020        case SCon{_, +t} LexPunctuation{character}:
1021            lexemes(t, Outside{}, SNil{}, Punctuation{character} <> flush_lexeme(reversed, acc), lex_seed_action(t, Outside{}))
1022        case SCon{h, +t} LexRaw{}:
1023            lexemes(t, Outside{}, SCon{h, reversed}, acc, lex_seed_action(t, Outside{}))
1024
1025def lex_scan(+text: String,
1026             +mode: LexMode,
1027             reversed: String,
1028             acc: List<&2, Lexeme>) -> List<&2, Lexeme>:
1029    lexemes(text, mode, reversed, acc, lex_seed_action(text, mode))
1030
1031# The reverse token stream that corresponds to render(value, mode, suffix).

1032# It is used for the structural parser/renderer proof.

1033def source_text(text: String, acc: List<&2, Lexeme>) -> List<&2, Lexeme>:
1034    Payload{text} <> acc
1035
1036def source(value: Value, members: BoolType(), acc: List<&2, Lexeme>) -> List<&2, Lexeme>:
1037    match value:
1038        case Null{}: source_text("null", acc)
1039        case Bool{truth}:
1040            match truth:
1041                case True{}: source_text("true", acc)
1042                case False{}: source_text("false", acc)
1043        case Number{lexeme, certificate}: source_text(lexeme, acc)
1044        case Str{text}: source_text("\"" ++ escape_string(text) ++ "\"", acc)
1045        case Arr{Nil{}}:
1046            match members:
1047                case False{}: Punctuation{'['} <> Punctuation{']'} <> acc
1048                case True{}: Punctuation{']'} <> acc
1049        case Arr{head <> tail}:
1050            match members:
1051                case False{}: Punctuation{'['} <> source(head, False{}, source(Arr{tail}, True{}, acc))
1052                case True{}: Punctuation{','} <> source(head, False{}, source(Arr{tail}, True{}, acc))
1053        case Obj{Nil{}}:
1054            match members:
1055                case False{}: Punctuation{'{'} <> Punctuation{'}'} <> acc
1056                case True{}: Punctuation{'}'} <> acc
1057        case Obj{(key, value) <> tail}:
1058            match members:
1059                case False{}: Punctuation{'{'} <> source_text("\"" ++ escape_string(key) ++ "\"", Punctuation{':'} <> source(value, False{}, source(Obj{tail}, True{}, acc)))
1060                case True{}: Punctuation{','} <> source_text("\"" ++ escape_string(key) ++ "\"", Punctuation{':'} <> source(value, False{}, source(Obj{tail}, True{}, acc)))
1061
1062type LexTree is Data:
1063    LexEmpty{}
1064    LexLeaf{lexeme: Lexeme}
1065    LexBranch{left: LexTree, right: LexTree}
1066
1067type Token is Type:
1068    Delimiter{character: Char}
1069    Atom{result: Result<&1, &1, Error, Value>}
1070
1071type TokenTree is Type:
1072    TokensEmpty{}
1073    TokenLeaf{token: Token}
1074    TokenBranch{left: TokenTree, right: TokenTree}
1075
1076def lex_leaves(items: List<&2, Lexeme>) -> List<&2, LexTree>:
1077    match items:
1078        case Nil{}: Nil{}
1079        case h <> t: LexLeaf{h} <> lex_leaves(t)
1080
1081def lex_pairs(trees: List<&2, LexTree>) -> List<&2, LexTree>:
1082    match trees:
1083        case Nil{}: Nil{}
1084        case h <> Nil{}: h <> Nil{}
1085        case a <> b <> t: LexBranch{a, b} <> lex_pairs(t)
1086
1087def lex_join(trees: List<&2, LexTree>) -> LexTree:
1088    match trees:
1089        case Nil{}: LexEmpty{}
1090        case head <> tail: LexBranch{head, lex_join(tail)}
1091
1092def lex_balance(fuel: Nat, trees: List<&2, LexTree>) -> LexTree:
1093    match fuel:
1094        case 0n: lex_join(trees)
1095        case 1n+p:
1096            match trees:
1097                case Nil{}: LexEmpty{}
1098                case h <> Nil{}: h
1099                case a <> b <> t: lex_balance(p, lex_pairs(a <> b <> t))
1100
1101def lex_tree(+items: List<&2, Lexeme>) -> LexTree:
1102    lex_balance(1n+List.length(&2, Lexeme, items), lex_leaves(items))
1103
1104def decode_lexeme(lexeme: Lexeme) -> Token:
1105    match lexeme:
1106        case Punctuation{c}: Delimiter{c}
1107        case Payload{text}: Atom{decode_payload(text)}
1108
1109def decode_tree(tree: LexTree) -> TokenTree:
1110    match tree:
1111        case LexEmpty{}: TokensEmpty{}
1112        case LexLeaf{lexeme}: TokenLeaf{decode_lexeme(lexeme)}
1113        case LexBranch{left, right}:
1114            l r = decode_tree(left) decode_tree(right)
1115            TokenBranch{l, r}
1116
1117def token_list(tree: TokenTree, tail: List<Token>) -> List<Token>:
1118    match tree:
1119        case TokensEmpty{}: tail
1120        case TokenLeaf{token}: token <> tail
1121        case TokenBranch{left, right}: token_list(left, token_list(right, tail))
1122
1123type Assembly is Type:
1124    NeedValue{kont: ParserKont}
1125    ArrayFirst{kont: ParserKont}
1126    ArrayNext{acc: List<&2, Value>, kont: ParserKont}
1127    ArrayComma{acc: List<&2, Value>, kont: ParserKont}
1128    ObjectFirst{kont: ParserKont}
1129    ObjectNext{acc: List<&2, Sigma<&2, &2, String, key => Value>>, kont: ParserKont}
1130    NeedColon{key: String, acc: List<&2, Sigma<&2, &2, String, key => Value>>, kont: ParserKont}
1131    ObjectComma{acc: List<&2, Sigma<&2, &2, String, key => Value>>, kont: ParserKont}
1132    Assembled{value: Value}
1133    AssemblyError{}
1134
1135def assembly_resume(kont: ParserKont, value: Value) -> Assembly:
1136    match kont:
1137        case Top{}: Assembled{value}
1138        case InArray{acc, parent}: ArrayComma{value <> acc, parent}
1139        case InObject{key, acc, parent}: ObjectComma{(key, value) <> acc, parent}
1140
1141def assembly_atom(result: Result<&1, &1, Error, Value>, kont: ParserKont) -> Assembly:
1142    match result:
1143        case Fail{_}: AssemblyError{}
1144        case Done{value}: assembly_resume(kont, value)
1145
1146def assembly_value(token: Token, kont: ParserKont) -> Assembly:
1147    match token:
1148        case Atom{result}: assembly_atom(result, kont)
1149        case Delimiter{'['}: ArrayFirst{kont}
1150        case Delimiter{'{'}: ObjectFirst{kont}
1151        case _: AssemblyError{}
1152
1153def assembly_key_value(result: Result<&1, &1, Error, Value>,
1154                       acc: List<&2, Sigma<&2, &2, String, key => Value>>, kont: ParserKont) -> Assembly:
1155    match result:
1156        case Done{Str{key}}: NeedColon{key, acc, kont}
1157        case _: AssemblyError{}
1158
1159def assembly_key(token: Token,
1160                 acc: List<&2, Sigma<&2, &2, String, key => Value>>, kont: ParserKont) -> Assembly:
1161    match token:
1162        case Atom{result}: assembly_key_value(result, acc, kont)
1163        case _: AssemblyError{}
1164
1165def assembly_step(state: Assembly, token: Token) -> Assembly:
1166    match state:
1167        case NeedValue{kont}: assembly_value(token, kont)
1168        case ArrayFirst{kont}:
1169            match token:
1170                case Delimiter{']'}: assembly_resume(kont, Arr{Nil{}})
1171                case _: assembly_value(token, InArray{Nil{}, kont})
1172        case ArrayNext{acc, kont}: assembly_value(token, InArray{acc, kont})
1173        case ArrayComma{acc, kont}:
1174            match token:
1175                case Delimiter{','}: ArrayNext{acc, kont}
1176                case Delimiter{']'}: assembly_resume(kont, Arr{List.reverse(&2, Value, acc)})
1177                case _: AssemblyError{}
1178        case ObjectFirst{kont}:
1179            match token:
1180                case Delimiter{'}'}: assembly_resume(kont, Obj{Nil{}})
1181                case _: assembly_key(token, Nil{}, kont)
1182        case ObjectNext{acc, kont}: assembly_key(token, acc, kont)
1183        case NeedColon{key, acc, kont}:
1184            match token:
1185                case Delimiter{':'}: NeedValue{InObject{key, acc, kont}}
1186                case _: AssemblyError{}
1187        case ObjectComma{acc, kont}:
1188            match token:
1189                case Delimiter{','}: ObjectNext{acc, kont}
1190                case Delimiter{'}'}: assembly_resume(kont, Obj{List.reverse(&2, Sigma<&2, &2, String, key => Value>, acc)})
1191                case _: AssemblyError{}
1192        case _: AssemblyError{}
1193
1194def assembly_finish(state: Assembly) -> Result<&1, &1, Error, Value>:
1195    match state:
1196        case Assembled{value}: Done{value}
1197        case _: Fail{Error{}}
1198
1199def assemble(tokens: List<Token>, state: Assembly) -> Result<&1, &1, Error, Value>:
1200    match tokens:
1201        case Nil{}: assembly_finish(state)
1202        case token <> tail: assemble(tail, assembly_step(state, token))
1203
1204def parse_normalized(text: String) -> Result<&1, &1, Error, Value>:
1205    assemble(token_list(decode_tree(lex_tree(lex_scan(text, Outside{}, SNil{}, Nil{}))), Nil{}), NeedValue{Top{}})
1206
1207# Call as parse!(text) to place the complete parse on Bend's GPU scheduler

1208# when one is available. The ordinary call remains useful on small inputs.

1209def parse(+text: String) -> Result<&1, &1, Error, Value>:
1210    parse_normalized(text)
1211
1212# Smart constructor. Validation evidence is checked by Bend and is not an

1213# unchecked assertion supplied by callers.

1214def number(+text: String) -> Result<&1, &1, Error, Value>:
1215    finish(number_lexeme(text, SNil{}, number_valid(text), {==}))
1216
1217# Independent documents form a fork/join tree. Keep sibling subtrees similar

1218# in total input size to distribute work across GPU lanes (or CPU workers).

1219type Batch is Data:
1220    Document{text: String}
1221    Documents{left: Batch, right: Batch}
1222
1223type BatchResult is Type:
1224    DocumentResult{result: Result<&1, &1, Error, Value>}
1225    DocumentResults{left: BatchResult, right: BatchResult}
1226
1227def parse_batch(batch: Batch) -> BatchResult:
1228    match batch:
1229        case Document{text}:
1230            DocumentResult{parse(text)}
1231        case Documents{left, right}:
1232            l r = parse_batch(left) parse_batch(right)
1233            DocumentResults{l, r}
1234
1235# The ! entry points request GPU execution; Bend provides the CPU fallback.

1236# A single document has sequential grammar dependencies. For parallel work,

1237# use parse_batch_gpu with independent documents.

1238def parse_gpu(text: String) -> Result<&1, &1, Error, Value>:
1239    parse!(text)
1240
1241def parse_batch_gpu(batch: Batch) -> BatchResult:
1242    parse_batch!(batch)
1243
1244# Build a balanced fork tree from documents in source order. Pairing adjacent

1245# trees on each pass keeps the depth logarithmic without copying input text.

1246# For best lane balance, supply documents of similar lengths/complexity.

1247def batch_leaves(texts: List<&2, String>) -> List<&2, Batch>:
1248    match texts:
1249        case Nil{}:
1250            Nil{}
1251        case text <> tail:
1252            Document{text} <> batch_leaves(tail)
1253
1254def batch_pairs(trees: List<&2, Batch>) -> List<&2, Batch>:
1255    match trees:
1256        case Nil{}:
1257            Nil{}
1258        case tree <> Nil{}:
1259            tree <> Nil{}
1260        case left <> right <> tail:
1261            Documents{left, right} <> batch_pairs(tail)
1262
1263def batch_build(fuel: Nat, trees: List<&2, Batch>) -> Maybe<&2, Batch>:
1264    match fuel:
1265        case 0n:
1266            List.head(&2, Batch, trees)
1267        case 1n+p:
1268            match trees:
1269                case Nil{}:
1270                    None{}
1271                case tree <> Nil{}:
1272                    Some{tree}
1273                case left <> right <> tail:
1274                    batch_build(p, batch_pairs(left <> right <> tail))
1275
1276def batch_from_list(+texts: List<&2, String>) -> Maybe<&2, Batch>:
1277    batch_build(List.length(&2, String, texts), batch_leaves(texts))
1278
1279def parse_optional_batch_gpu(batch: Maybe<&2, Batch>) -> Maybe<&1, BatchResult>:
1280    match batch:
1281        case None{}:
1282            None{}
1283        case Some{tree}:
1284            Some{parse_batch!(tree)}
1285
1286# Build the fork tree before entering the device. None represents an empty

1287# input list; each document's parse failure remains at its own result leaf.

1288def parse_many_gpu(texts: List<&2, String>) -> Maybe<&1, BatchResult>:
1289    parse_optional_batch_gpu(batch_from_list(texts))