1	import Base
2	
3	# Decimal numbers remain text; objects retain ordering and unknown fields.
4	type Member<a, -A: Kind(a)> is Kind(a):
5	  Field{key: String, value: A}
6	
7	type Json is Data:
8	  Null{}
9	  Boolean{value: Bool}
10	  Number{text: String}
11	  Text{value: String}
12	  Array{items: List<&2, Json>}
13	  Object{fields: List<&2, Member<&2, Json>>}
14	
15	def hex(n: U32) -> String:
16	  String.take(String.drop("0123456789abcdef", U32.to_nat(n)), 1n)
17	
18	def escape_code(control: Bool, +c: U32) -> String:
19	  match control:
20	    case True{}:
21	      "\\u00" ++ hex((c / 16 : U32)) ++ hex((c % 16 : U32))
22	    case False{}:
23	      SCon{Chr{c}, SNil{}}
24	
25	def escape_char(+c: U32) -> String:
26	  escape_code((c < 32 : U32), c)
27	
28	def escape_go(s: String, acc: String) -> String:
29	  match s:
30	    case SNil{}: String.reverse(acc)
31	    case SCon{'"', rest}: escape_go(rest, "\"\\" ++ acc)
32	    case SCon{'\\', rest}: escape_go(rest, "\\\\" ++ acc)
33	    case SCon{Chr{c}, rest}: escape_go(rest, String.reverse(escape_char(c)) ++ acc)
34	
35	def escape(s: String) -> String:
36	  escape_go(s, "")
37	
38	def quote(s: String) -> String:
39	  "\"" ++ escape(s) ++ "\""
40	
41	def comma(empty: Bool) -> String:
42	  match empty:
43	    case True{}:
44	      ""
45	    case False{}:
46	      ","
47	
48	@unsafe
49	def stringify(value: Json) -> String:
50	  match value:
51	    case Null{}:
52	      "null"
53	    case Boolean{True{}}:
54	      "true"
55	    case Boolean{False{}}:
56	      "false"
57	    case Number{text}:
58	      text
59	    case Text{value}:
60	      quote(value)
61	    case Array{Nil{}}:
62	      "[]"
63	    case Array{Con{head, +tail}}:
64	      "[" ++ stringify(head) ++ comma(List.is_empty(&2, Json, tail)) ++ String.drop(stringify(Array{tail}), 1n)
65	    case Object{Nil{}}:
66	      "{}"
67	    case Object{Con{Field{key, value}, +tail}}:
68	      "{" ++ quote(key) ++ ":" ++ stringify(value) ++ comma(List.is_empty(&2, Member<&2, Json>, tail)) ++ String.drop(stringify(Object{tail}), 1n)
69	
70	def choose(found: Bool, value: Json, other: Maybe<&2, Json>) -> Maybe<&2, Json>:
71	  match found:
72	    case True{}:
73	      Some{value}
74	    case False{}:
75	      other
76	
77	def get_fields(fields: List<&2, Member<&2, Json>>, +key: String) -> Maybe<&2, Json>:
78	  match fields:
79	    case Nil{}:
80	      None{}
81	    case Con{Field{name, value}, tail}:
82	      choose(String.eq(name, key), value, get_fields(tail, key))
83	
84	def get(value: Json, key: String) -> Maybe<&2, Json>:
85	  match value:
86	    case Object{fields}:
87	      get_fields(fields, key)
88	    case _:
89	      None{}
90	
91	def text(value: Maybe<&2, Json>) -> String:
92	  match value:
93	    case Some{Text{s}}:
94	      s
95	    case _:
96	      ""
97	
98	type Token is Data:
99	  Atom{value: Json}
100	  OpenArray{}
101	  CloseArray{}
102	  OpenObject{}
103	  CloseObject{}
104	  Colon{}
105	  Comma{}
106	
107	def select_u32(ok: Bool, yes: U32, no: U32) -> U32:
108	  match ok:
109	    case True{}: yes
110	    case False{}: no
111	
112	def hex_digit(ch: Char) -> U32:
113	  +c = Char.to_u32(ch)
114	  select_u32((c >= 48 : U32) && (c <= 57 : U32), (c - 48 : U32),
115	    select_u32((c >= 97 : U32) && (c <= 102 : U32), (c - 87 : U32),
116	      select_u32((c >= 65 : U32) && (c <= 70 : U32), (c - 55 : U32), 256)))
117	
118	def checked_char(ok: Bool, code: U32) -> Result<&1, &1, String, Char>:
119	  match ok:
120	    case True{}: Done{Chr{code}}
121	    case False{}: Fail{"invalid JSON Unicode escape"}
122	
123	def hex_checked(ok: Bool, code: U32) -> Result<&1, &1, String, U32>:
124	  match ok:
125	    case True{}: Done{code}
126	    case False{}: Fail{"invalid JSON Unicode escape"}
127	
128	def hex4(+a: U32, +b: U32, +c: U32, +d: U32) -> Result<&1, &1, String, U32>:
129	  hex_checked((a < 16 : U32) && (b < 16 : U32) && (c < 16 : U32) && (d < 16 : U32), (a * 4096 + b * 256 + c * 16 + d : U32))
130	
131	def unicode_escape(high: Bool, +code: U32, rest: String) -> Result<&1, &1, String, Char & String>:
132	  match high:
133	    case True{}:
134	      match rest:
135	        case SCon{'\\', SCon{'u', SCon{a, SCon{b, SCon{c, SCon{d, tail}}}}}}:
136	          do Result<&1, &1, String, Char & String>:
137	            +low : U32 <- hex4(hex_digit(a), hex_digit(b), hex_digit(c), hex_digit(d))
138	            ch : Char <- checked_char((low >= 56320 : U32) && (low <= 57343 : U32), (65536 + (code - 55296) * 1024 + low - 56320 : U32))
139	            return (ch, tail)
140	        case _: Fail{"unpaired JSON surrogate"}
141	    case False{}:
142	      do Result<&1, &1, String, Char & String>:
143	        ch : Char <- checked_char((code < 55296 : U32) || (code > 57343 : U32), code)
144	        return (ch, rest)
145	
146	def unicode_escape_code(result: Result<&1, &1, String, U32>, rest: String) -> Result<&1, &1, String, Char & String>:
147	  match result:
148	    case Fail{e}: Fail{e}
149	    case Done{+code}: unicode_escape((code >= 55296 : U32) && (code <= 56319 : U32), code, rest)
150	
151	def unescape(s: String) -> Result<&1, &1, String, Char & String>:
152	  match s:
153	    case SCon{'"', rest}: Done{('"', rest)}
154	    case SCon{'\\', rest}: Done{('\\', rest)}
155	    case SCon{'/', rest}: Done{('/', rest)}
156	    case SCon{'b', rest}: Done{(Chr{8}, rest)}
157	    case SCon{'f', rest}: Done{(Chr{12}, rest)}
158	    case SCon{'n', rest}: Done{('\n', rest)}
159	    case SCon{'r', rest}: Done{('\r', rest)}
160	    case SCon{'t', rest}: Done{('\t', rest)}
161	    case SCon{'u', SCon{a, SCon{b, SCon{c, SCon{d, rest}}}}}:
162	      unicode_escape_code(hex4(hex_digit(a), hex_digit(b), hex_digit(c), hex_digit(d)), rest)
163	    case _: Fail{"invalid JSON escape"}
164	
165	def string_char(ok: Bool, ch: Char, rest: String, acc: String,
166	                next: String -> String -> Result<&1, &1, String, String & String>) -> Result<&1, &1, String, String & String>:
167	  match ok:
168	    case True{}: next(rest, SCon{ch, acc})
169	    case False{}: Fail{"unescaped control character"}
170	
171	def string_escape(result: Result<&1, &1, String, Char & String>, acc: String,
172	                  next: String -> String -> Result<&1, &1, String, String & String>) -> Result<&1, &1, String, String & String>:
173	  match result:
174	    case Fail{e}: Fail{e}
175	    case Done{(ch, rest)}: next(rest, SCon{ch, acc})
176	
177	def string_read(fuel: Nat, s: String, acc: String) -> Result<&1, &1, String, String & String>:
178	  match fuel:
179	    case 0n: Fail{"JSON string limit"}
180	    case 1n+n:
181	      match s:
182	        case SNil{}: Fail{"unterminated JSON string"}
183	        case SCon{'"', rest}: Done{(String.reverse(acc), rest)}
184	        case SCon{'\\', rest}:
185	          string_escape(unescape(rest), acc, r => a => string_read(n, r, a))
186	        case SCon{Chr{+c}, rest}:
187	          string_char((c >= 32 : U32), Chr{c}, rest, acc, r => a => string_read(n, r, a))
188	
189	# Number states avoid matching U32 bit constructors in the parser.
190	type NumberState is Data:
191	  Start{}
192	  Minus{}
193	  Zero{}
194	  Integer{}
195	  Dot{}
196	  Fraction{}
197	  Exponent{}
198	  Sign{}
199	  Digits{}
200	  Bad{}
201	
202	def select_state(ok: Bool, yes: NumberState, no: NumberState) -> NumberState:
203	  match ok:
204	    case True{}: yes
205	    case False{}: no
206	
207	def number_state(state: NumberState, +ch: Char) -> NumberState:
208	  match state:
209	    case Start{}: select_state(Char.is_eq(ch, '-'), Minus{}, select_state(Char.is_eq(ch, '0'), Zero{}, select_state(Char.is_digit(ch), Integer{}, Bad{})))
210	    case Minus{}: select_state(Char.is_eq(ch, '0'), Zero{}, select_state(Char.is_digit(ch), Integer{}, Bad{}))
211	    case Zero{}: select_state(Char.is_eq(ch, '.'), Dot{}, select_state(Char.is_eq(ch, 'e') || Char.is_eq(ch, 'E'), Exponent{}, Bad{}))
212	    case Integer{}: select_state(Char.is_digit(ch), Integer{}, select_state(Char.is_eq(ch, '.'), Dot{}, select_state(Char.is_eq(ch, 'e') || Char.is_eq(ch, 'E'), Exponent{}, Bad{})))
213	    case Dot{}: select_state(Char.is_digit(ch), Fraction{}, Bad{})
214	    case Fraction{}: select_state(Char.is_digit(ch), Fraction{}, select_state(Char.is_eq(ch, 'e') || Char.is_eq(ch, 'E'), Exponent{}, Bad{}))
215	    case Exponent{}: select_state(Char.is_eq(ch, '+') || Char.is_eq(ch, '-'), Sign{}, select_state(Char.is_digit(ch), Digits{}, Bad{}))
216	    case Sign{}: select_state(Char.is_digit(ch), Digits{}, Bad{})
217	    case Digits{}: select_state(Char.is_digit(ch), Digits{}, Bad{})
218	    case Bad{}: Bad{}
219	
220	def number_end(state: NumberState) -> Bool:
221	  match state:
222	    case Zero{}: True{}
223	    case Integer{}: True{}
224	    case Fraction{}: True{}
225	    case Digits{}: True{}
226	    case _: False{}
227	
228	def number_valid(s: String, state: NumberState) -> Bool:
229	  match s:
230	    case SNil{}: number_end(state)
231	    case SCon{ch, rest}: number_valid(rest, number_state(state, ch))
232	
233	def primitive(ok: Bool, raw: String) -> Result<&1, &1, String, Token>:
234	  match ok:
235	    case True{}: Done{Atom{Number{raw}}}
236	    case False{}: Fail{"invalid JSON literal"}
237	
238	def literal_known(is_null: Bool, is_true: Bool, is_false: Bool, +raw: String) -> Result<&1, &1, String, Token>:
239	  match is_null is_true is_false:
240	    case True{} _ _: Done{Atom{Null{}}}
241	    case _ True{} _: Done{Atom{Boolean{True{}}}}
242	    case _ _ True{}: Done{Atom{Boolean{False{}}}}
243	    case _ _ _: primitive(number_valid(raw, Start{}), raw)
244	
245	def literal(+raw: String) -> Result<&1, &1, String, Token>:
246	  literal_known(String.eq(raw, "null"), String.eq(raw, "true"), String.eq(raw, "false"), raw)
247	
248	def delimiter(+c: Char) -> Bool:
249	  Char.is_eq(c, ' ') || Char.is_eq(c, '\n') || Char.is_eq(c, '\r') || Char.is_eq(c, '\t') || Char.is_eq(c, ',') || Char.is_eq(c, ']') || Char.is_eq(c, '}')
250	
251	def word_step(stop: Bool, c: Char, rest: String, acc: String,
252	              next: String -> String -> String & String) -> String & String:
253	  match stop:
254	    case True{}: (String.reverse(acc), SCon{c, rest})
255	    case False{}: next(rest, SCon{c, acc})
256	
257	def word(s: String, acc: String) -> String & String:
258	  match s:
259	    case SNil{}: (String.reverse(acc), "")
260	    case SCon{+c, +rest}: word_step(delimiter(c), c, rest, acc, r => a => word(rest, a))
261	
262	def lex_string(result: Result<&1, &1, String, String & String>,
263	               next: String -> Maybe<&2, Token> -> Result<&1, &1, String, List<&2, Token>>) -> Result<&1, &1, String, List<&2, Token>>:
264	  match result:
265	    case Fail{e}: Fail{e}
266	    case Done{(s, rest)}: next(rest, Some{Atom{Text{s}}})
267	
268	def lex_word(pair: String & String,
269	             next: String -> Maybe<&2, Token> -> Result<&1, &1, String, List<&2, Token>>) -> Result<&1, &1, String, List<&2, Token>>:
270	  (raw, rest) = pair
271	  do Result<&1, &1, String, List<&2, Token>>:
272	    token : Token <- literal(raw)
273	    next(rest, Some{token})
274	
275	type LexKind is Data:
276	  Space{}
277	  LArray{}
278	  RArray{}
279	  LObject{}
280	  RObject{}
281	  LColon{}
282	  LComma{}
283	  Quote{}
284	  Other{}
285	
286	def select_lex(ok: Bool, yes: LexKind, no: LexKind) -> LexKind:
287	  match ok:
288	    case True{}: yes
289	    case False{}: no
290	
291	def lex_kind(+c: Char) -> LexKind:
292	  select_lex(Char.is_eq(c, ' ') || Char.is_eq(c, '\n') || Char.is_eq(c, '\r') || Char.is_eq(c, '\t'), Space{},
293	    select_lex(Char.is_eq(c, '['), LArray{}, select_lex(Char.is_eq(c, ']'), RArray{},
294	    select_lex(Char.is_eq(c, '{'), LObject{}, select_lex(Char.is_eq(c, '}'), RObject{},
295	    select_lex(Char.is_eq(c, ':'), LColon{}, select_lex(Char.is_eq(c, ','), LComma{},
296	    select_lex(Char.is_eq(c, '"'), Quote{}, Other{}))))))))
297	
298	def lex_step(kind: LexKind, c: Char, +rest: String,
299	             next: String -> Maybe<&2, Token> -> Result<&1, &1, String, List<&2, Token>>) -> Result<&1, &1, String, List<&2, Token>>:
300	  match kind:
301	    case Space{}: next(rest, None{})
302	    case LArray{}: next(rest, Some{OpenArray{}})
303	    case RArray{}: next(rest, Some{CloseArray{}})
304	    case LObject{}: next(rest, Some{OpenObject{}})
305	    case RObject{}: next(rest, Some{CloseObject{}})
306	    case LColon{}: next(rest, Some{Colon{}})
307	    case LComma{}: next(rest, Some{Comma{}})
308	    case Quote{}: lex_string(string_read(1n+String.length(rest), rest, ""), next)
309	    case Other{}: lex_word(word(SCon{c, rest}, ""), next)
310	
311	def lex_acc(token: Maybe<&2, Token>, acc: List<&2, Token>) -> List<&2, Token>:
312	  match token:
313	    case None{}: acc
314	    case Some{t}: Con{t, acc}
315	
316	def lex(fuel: Nat, s: String, acc: List<&2, Token>) -> Result<&1, &1, String, List<&2, Token>>:
317	  match fuel:
318	    case 0n: Fail{"JSON token limit"}
319	    case 1n+n:
320	      match s:
321	        case SNil{}: Done{List.reverse(&2, Token, acc)}
322	        case SCon{+c, rest}: lex_step(lex_kind(c), c, rest, r => t => lex(n, r, lex_acc(t, acc)))
323	
324	type Parse is Type:
325	  Parsed{value: Json, rest: List<&2, Token>}
326	  Invalid{message: String}
327	
328	type Mode is Data:
329	  Value{}
330	  Elements{acc: List<&2, Json>, empty: Bool}
331	  Fields{acc: List<&2, Member<&2, Json>>, empty: Bool}
332	
333	def array_end(ok: Bool, acc: List<&2, Json>, rest: List<&2, Token>) -> Parse:
334	  match ok:
335	    case True{}: Parsed{Array{List.reverse(&2, Json, acc)}, rest}
336	    case False{}: Invalid{"trailing array comma"}
337	
338	def object_end(ok: Bool, acc: List<&2, Member<&2, Json>>, rest: List<&2, Token>) -> Parse:
339	  match ok:
340	    case True{}: Parsed{Object{List.reverse(&2, Member<&2, Json>, acc)}, rest}
341	    case False{}: Invalid{"trailing object comma"}
342	
343	def array_after(result: Parse, acc: List<&2, Json>, next: Mode -> List<&2, Token> -> Parse) -> Parse:
344	  match result:
345	    case Invalid{e}: Invalid{e}
346	    case Parsed{value, Con{Comma{}, rest}}: next(Elements{Con{value, acc}, False{}}, rest)
347	    case Parsed{value, Con{CloseArray{}, rest}}: array_end(True{}, Con{value, acc}, rest)
348	    case Parsed{value, rest}: Invalid{"expected array comma or closing bracket"}
349	
350	def object_after(result: Parse, key: String, acc: List<&2, Member<&2, Json>>, next: Mode -> List<&2, Token> -> Parse) -> Parse:
351	  match result:
352	    case Invalid{e}: Invalid{e}
353	    case Parsed{value, Con{Comma{}, rest}}: next(Fields{Con{Field{key, value}, acc}, False{}}, rest)
354	    case Parsed{value, Con{CloseObject{}, rest}}: object_end(True{}, Con{Field{key, value}, acc}, rest)
355	    case Parsed{value, rest}: Invalid{"expected object comma or closing brace"}
356	
357	def parse(fuel: Nat, mode: Mode, tokens: List<&2, Token>) -> Parse:
358	  match fuel:
359	    case 0n: Invalid{"JSON nesting or token limit"}
360	    case 1n+ +n:
361	      match mode tokens:
362	        case Value{} Con{Atom{value}, rest}: Parsed{value, rest}
363	        case Value{} Con{OpenArray{}, rest}: parse(n, Elements{Nil{}, True{}}, rest)
364	        case Value{} Con{OpenObject{}, rest}: parse(n, Fields{Nil{}, True{}}, rest)
365	        case Elements{acc, empty} Con{CloseArray{}, rest}: array_end(empty, acc, rest)
366	        case Elements{acc, empty} ts: array_after(parse(n, Value{}, ts), acc, m => t => parse(n, m, t))
367	        case Fields{acc, empty} Con{CloseObject{}, rest}: object_end(empty, acc, rest)
368	        case Fields{acc, empty} Con{Atom{Text{key}}, Con{Colon{}, rest}}:
369	          object_after(parse(n, Value{}, rest), key, acc, m => t => parse(n, m, t))
370	        case _ _: Invalid{"expected JSON value or object key"}
371	
372	def finish(result: Parse) -> Result<&1, &1, String, Json>:
373	  match result:
374	    case Invalid{e}: Fail{e}
375	    case Parsed{value, Nil{}}: Done{value}
376	    case Parsed{value, rest}: Fail{"trailing JSON tokens"}
377	
378	def depth_guard(ok: Bool, depth: U32, next: U32 -> Bool) -> Bool:
379	  match ok:
380	    case True{}: next(depth)
381	    case False{}: False{}
382	
383	def depth_step(token: Token, +depth: U32, next: U32 -> Bool) -> Bool:
384	  match token:
385	    case OpenArray{}: depth_guard((depth < 64 : U32), (depth + 1 : U32), next)
386	    case OpenObject{}: depth_guard((depth < 64 : U32), (depth + 1 : U32), next)
387	    case CloseArray{}: depth_guard((depth > 0 : U32), (depth - 1 : U32), next)
388	    case CloseObject{}: depth_guard((depth > 0 : U32), (depth - 1 : U32), next)
389	    case _: next(depth)
390	
391	def depth_valid(tokens: List<&2, Token>, depth: U32) -> Bool:
392	  match tokens:
393	    case Nil{}: U32.is_eq(depth, 0)
394	    case Con{token, rest}: depth_step(token, depth, d => depth_valid(rest, d))
395	
396	def token_count(tokens: List<&2, Token>, count: U32) -> U32:
397	  match tokens:
398	    case Nil{}: count
399	    case Con{token, rest}: token_count(rest, (count + 1 : U32))
400	
401	def parse_checked(ok: Bool, count: U32, tokens: List<&2, Token>) -> Result<&1, &1, String, Json>:
402	  match ok:
403	    case False{}: Fail{"JSON exceeds 64 nesting levels or 65536 tokens, or has unmatched brackets"}
404	    case True{}: finish(parse(1n+U32.to_nat(count), Value{}, tokens))
405	
406	def parse_tokens(+tokens: List<&2, Token>) -> Result<&1, &1, String, Json>:
407	  +count = token_count(tokens, 0)
408	  parse_checked(depth_valid(tokens, 0) && (count <= 65536 : U32), count, tokens)
409	
410	def read(+s: String) -> Result<&1, &1, String, Json>:
411	  do Result<&1, &1, String, Json>:
412	    tokens : List<&2, Token> <- lex(1n+String.length(s), s, Nil{})
413	    parse_tokens(tokens)