1	import 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.
7	def BoolType() -> Data:
8	    Bool
9	
10	type NumberCert<-s: String> is Data:
11	    Certified{witness: NumberProof(s)}
12	
13	type 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	
21	type Error is Data:
22	    Error{}
23	
24	type Parsed is Type:
25	    Parsed{value: Value, rest: String}
26	
27	type StringScan is Data:
28	    StringScan{value: String, rest: String}
29	
30	type 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	
38	type NumberState is Data:
39	    NumberStart{}
40	    NumberMinus{}
41	    NumberZero{}
42	    NumberInteger{}
43	    NumberDot{}
44	    NumberFraction{}
45	    NumberExponent{}
46	    NumberExponentSign{}
47	    NumberExponentDigits{}
48	    NumberInvalid{}
49	
50	def 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	
67	def 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	
103	def 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	
141	type 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	
178	def 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	
216	type QuoteAction is Data:
217	    QuoteBackslash{}
218	    QuoteEnd{}
219	    QuotePlain{}
220	
221	def quote_action_from_class(class: EscapeClass) -> QuoteAction:
222	    match class:
223	        case Backslash{}: QuoteBackslash{}
224	        case Quote{}: QuoteEnd{}
225	        case _: QuotePlain{}
226	
227	def quote_action(character: Char) -> QuoteAction:
228	    quote_action_from_class(escape_class(character))
229	
230	def quote_lex_action(action: QuoteAction) -> LexAction:
231	    match action:
232	        case QuoteBackslash{}: LexBackslash{}
233	        case QuoteEnd{}: LexStringEnd{}
234	        case QuotePlain{}: LexStringChar{}
235	
236	def 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	
274	def escape_char(+character: Char) -> String:
275	    escape_char_from_class(character, escape_class(character))
276	
277	def 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.
286	def render_object_field(prefix: String, key: String, value_text: String) -> String:
287	    (prefix ++ ("\"" ++ escape_string(key) ++ "\":")) ++ value_text
288	
289	def 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	
315	def 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.
321	type HexScan is Data:
322	    HexScan{code: U32, rest: String}
323	
324	def 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	
350	def 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	
405	def 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	
415	def 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	
486	def scan_string(+s: String) -> Result<&1, &1, Error, StringScan>:
487	    scan_string_machine((String.length(s) * 2n + 16n : Nat), ScanText{s, SNil{}})
488	
489	def 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	
512	type NumberChar is Data:
513	    NMinus{}
514	    NPlus{}
515	    NDot{}
516	    NExp{}
517	    NZero{}
518	    NDigit{}
519	    NOther{}
520	
521	def 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	
540	def 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	
569	def number_next(state: NumberState, c: Char) -> NumberState:
570	    match state:
571	        case NumberInvalid{}: NumberInvalid{}
572	        case _: number_step(number_char(c), state)
573	
574	def 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	
587	def 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	
596	def number_valid(+s: String) -> BoolType():
597	    number_valid_end(number_valid_step(s, NumberStart{}))
598	
599	def NumberProofFrom(valid: BoolType()) -> Data:
600	    match valid:
601	        case True{}:
602	            Unit
603	        case False{}:
604	            Empty
605	
606	def NumberProof(s: String) -> Data:
607	    NumberProofFrom(number_valid(s))
608	
609	def 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	
616	def 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	
623	def 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	
630	def 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	
639	def 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	
644	def 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	
654	def 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	
659	def parse_number(s: String) -> Result<&1, &1, Error, Parsed>:
660	    from_number_scan(scan_number(s, SNil{}))
661	
662	def 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.
671	type 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	
676	type 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	
688	def 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	
697	def 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	
818	def parse_value(+s: String) -> Result<&1, &1, Error, Parsed>:
819	    parse_machine((String.length(s) * 8n + 16n : Nat), ParseValue{whitespace(s), Top{}})
820	
821	def 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	
828	def finish_rest(value: Value, rest: String) -> Result<&1, &1, Error, Value>:
829	    finish_rest_clean(value, whitespace(rest))
830	
831	def 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.
842	type FastString is Data:
843	    Decoded{text: String}
844	    InvalidString{}
845	    UnicodeFallback{}
846	
847	def 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	
853	def fast_raw(control: BoolType(), result: FastString, character: Char) -> FastString:
854	    match control:
855	        case True{}: InvalidString{}
856	        case False{}: fast_push(result, character)
857	
858	def 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	
907	def 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	
913	def 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	
921	def 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	
928	def 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.
934	type Lexeme is Data:
935	    Punctuation{character: Char}
936	    Payload{text: String}
937	
938	def 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	
943	type LexMode is Data:
944	    Outside{}
945	    Quoted{}
946	    Escaped{}
947	
948	type LexAction is Data:
949	    LexStop{}
950	    LexEscapedChar{}
951	    LexBackslash{}
952	    LexStringEnd{}
953	    LexStringChar{}
954	    LexQuote{}
955	    LexWhitespace{}
956	    LexPunctuation{character: Char}
957	    LexRaw{}
958	
959	def 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	
974	def lex_outside_action(character: Char, number_kind: NumberChar) -> LexAction:
975	    match number_kind:
976	        case NOther{}: lex_outside_other(character)
977	        case _: LexRaw{}
978	
979	def 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	
985	def 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	
990	def 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	
996	def 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	
1025	def 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.
1033	def source_text(text: String, acc: List<&2, Lexeme>) -> List<&2, Lexeme>:
1034	    Payload{text} <> acc
1035	
1036	def 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	
1062	type LexTree is Data:
1063	    LexEmpty{}
1064	    LexLeaf{lexeme: Lexeme}
1065	    LexBranch{left: LexTree, right: LexTree}
1066	
1067	type Token is Type:
1068	    Delimiter{character: Char}
1069	    Atom{result: Result<&1, &1, Error, Value>}
1070	
1071	type TokenTree is Type:
1072	    TokensEmpty{}
1073	    TokenLeaf{token: Token}
1074	    TokenBranch{left: TokenTree, right: TokenTree}
1075	
1076	def 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	
1081	def 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	
1087	def lex_join(trees: List<&2, LexTree>) -> LexTree:
1088	    match trees:
1089	        case Nil{}: LexEmpty{}
1090	        case head <> tail: LexBranch{head, lex_join(tail)}
1091	
1092	def 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	
1101	def lex_tree(+items: List<&2, Lexeme>) -> LexTree:
1102	    lex_balance(1n+List.length(&2, Lexeme, items), lex_leaves(items))
1103	
1104	def decode_lexeme(lexeme: Lexeme) -> Token:
1105	    match lexeme:
1106	        case Punctuation{c}: Delimiter{c}
1107	        case Payload{text}: Atom{decode_payload(text)}
1108	
1109	def 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	
1117	def 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	
1123	type 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	
1135	def 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	
1141	def 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	
1146	def 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	
1153	def 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	
1159	def 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	
1165	def 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	
1194	def assembly_finish(state: Assembly) -> Result<&1, &1, Error, Value>:
1195	    match state:
1196	        case Assembled{value}: Done{value}
1197	        case _: Fail{Error{}}
1198	
1199	def 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	
1204	def 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.
1209	def 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.
1214	def 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).
1219	type Batch is Data:
1220	    Document{text: String}
1221	    Documents{left: Batch, right: Batch}
1222	
1223	type BatchResult is Type:
1224	    DocumentResult{result: Result<&1, &1, Error, Value>}
1225	    DocumentResults{left: BatchResult, right: BatchResult}
1226	
1227	def 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.
1238	def parse_gpu(text: String) -> Result<&1, &1, Error, Value>:
1239	    parse!(text)
1240	
1241	def 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.
1247	def 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	
1254	def 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	
1263	def 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	
1276	def batch_from_list(+texts: List<&2, String>) -> Maybe<&2, Batch>:
1277	    batch_build(List.length(&2, String, texts), batch_leaves(texts))
1278	
1279	def 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.
1288	def parse_many_gpu(texts: List<&2, String>) -> Maybe<&1, BatchResult>:
1289	    parse_optional_batch_gpu(batch_from_list(texts))