proof/JSON_SourceProof.bend
qasim-bend-kit@0.1.0.2 · 1,515 lines · 82 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J
3import qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend as A
4import qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend as P
5import qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend as S
6import qasim-bend-kit@0.1.0.2/proof/JSON_ParallelProof.bend as Par
7import qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend as Num
8import qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend as W
9import qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend as LP
10
11def token_source(xs: List<&2, J.Lexeme>, tail: List<J.Token>) -> List<J.Token>:
12 match xs:
13 case Nil{}: tail
14 case h <> t: J.decode_lexeme(h) <> token_source(t, tail)
15
16def token_source_flat(+xs: List<&2, J.Lexeme>,
17 -tail: List<J.Token>) -> {token_source(xs, tail) == Par.flat(xs, tail) : List<J.Token>}:
18 match xs:
19 case Nil{}: {==}
20 case head <> rest:
21 Equal.cong(List<J.Token>, List<J.Token>, tokens => J.decode_lexeme(head) <> tokens,
22 token_source(rest, tail), Par.flat(rest, tail), token_source_flat(rest, tail))
23
24def is_members(mode: A.Mode) -> Bool:
25 match mode:
26 case A.Whole{}: False{}
27 case A.Members{}: True{}
28
29def token_string(text: String) -> J.Token:
30 J.Atom{Done{J.Str{text}}}
31
32def nested_render_append(+outer: J.Value,
33 +inner: J.Value,
34 +inner_members: Bool,
35 +prefix: String,
36 +suffix: String,
37 +outer_append: {J.render(outer, False{}, J.render(inner, inner_members, prefix)) ++ suffix == J.render(outer, False{}, J.render(inner, inner_members, prefix) ++ suffix) : String},
38 +inner_append: {J.render(inner, inner_members, prefix) ++ suffix == J.render(inner, inner_members, prefix ++ suffix) : String}) -> {J.render(outer, False{}, J.render(inner, inner_members, prefix)) ++ suffix == J.render(outer, False{}, J.render(inner, inner_members, prefix ++ suffix)) : String}:
39 Equal.trans(String,
40 J.render(outer, False{}, J.render(inner, inner_members, prefix)) ++ suffix,
41 J.render(outer, False{}, J.render(inner, inner_members, prefix) ++ suffix),
42 J.render(outer, False{}, J.render(inner, inner_members, prefix ++ suffix)),
43 outer_append,
44 Equal.cong(String, String, text => J.render(outer, False{}, text),
45 J.render(inner, inner_members, prefix) ++ suffix,
46 J.render(inner, inner_members, prefix ++ suffix),
47 inner_append))
48
49
50def render_object_field_append(+prefix: String,
51 +key: String,
52 +text: String,
53 +suffix: String) -> {J.render_object_field(prefix, key, text) ++ suffix == J.render_object_field(prefix, key, text ++ suffix) : String}:
54 S.append_assoc(prefix ++ ("\"" ++ J.escape_string(key) ++ "\":"), text, suffix)
55
56def render_append(+value: J.Value,
57 +members: Bool,
58 +prefix: String,
59 +suffix: String) -> {J.render(value, members, prefix) ++ suffix == J.render(value, members, prefix ++ suffix) : String}:
60 match value:
61 case J.Null{}: S.append_assoc("null", prefix, suffix)
62 case J.Bool{truth}:
63 match truth:
64 case True{}: S.append_assoc("true", prefix, suffix)
65 case False{}: S.append_assoc("false", prefix, suffix)
66 case J.Number{lexeme, certificate}: S.append_assoc(lexeme, prefix, suffix)
67 case J.Str{text}:
68 Equal.cong(String, String, rest => SCon{'"', rest},
69 (J.escape_string(text) ++ (SCon{'"', SNil{}} ++ prefix)) ++ suffix,
70 J.escape_string(text) ++ (SCon{'"', SNil{}} ++ (prefix ++ suffix)),
71 Equal.trans(String,
72 (J.escape_string(text) ++ (SCon{'"', SNil{}} ++ prefix)) ++ suffix,
73 J.escape_string(text) ++ ((SCon{'"', SNil{}} ++ prefix) ++ suffix),
74 J.escape_string(text) ++ (SCon{'"', SNil{}} ++ (prefix ++ suffix)),
75 S.append_assoc(J.escape_string(text), SCon{'"', SNil{}} ++ prefix, suffix),
76 Equal.cong(String, String, value => J.escape_string(text) ++ value,
77 (SCon{'"', SNil{}} ++ prefix) ++ suffix,
78 SCon{'"', SNil{}} ++ (prefix ++ suffix),
79 S.append_assoc(SCon{'"', SNil{}}, prefix, suffix))))
80 case J.Arr{Nil{}}:
81 match members:
82 case False{}: S.append_assoc("[]", prefix, suffix)
83 case True{}: S.append_assoc("]", prefix, suffix)
84 case J.Arr{head <> tail}:
85 match members:
86 case False{}:
87 Equal.trans(String, ("[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix))) ++ suffix,
88 "[" ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix),
89 "[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)),
90 S.append_assoc("[", J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)), suffix),
91 Equal.trans(String, "[" ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix),
92 "[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix),
93 "[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)),
94 Equal.cong(String, String, text => "[" ++ text,
95 J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix,
96 J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix),
97 render_append(head, False{}, J.render(J.Arr{tail}, True{}, prefix), suffix)),
98 Equal.cong(String, String, text => "[" ++ J.render(head, False{}, text),
99 J.render(J.Arr{tail}, True{}, prefix) ++ suffix,
100 J.render(J.Arr{tail}, True{}, prefix ++ suffix),
101 render_append(J.Arr{tail}, True{}, prefix, suffix))))
102 case True{}:
103 Equal.trans(String, ("," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix))) ++ suffix,
104 "," ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix),
105 "," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)),
106 S.append_assoc(",", J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)), suffix),
107 Equal.trans(String, "," ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix),
108 "," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix),
109 "," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)),
110 Equal.cong(String, String, text => "," ++ text,
111 J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix,
112 J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix),
113 render_append(head, False{}, J.render(J.Arr{tail}, True{}, prefix), suffix)),
114 Equal.cong(String, String, text => "," ++ J.render(head, False{}, text),
115 J.render(J.Arr{tail}, True{}, prefix) ++ suffix,
116 J.render(J.Arr{tail}, True{}, prefix ++ suffix),
117 render_append(J.Arr{tail}, True{}, prefix, suffix))))
118 case J.Obj{Nil{}}:
119 match members:
120 case False{}: S.append_assoc("{}", prefix, suffix)
121 case True{}: S.append_assoc("}", prefix, suffix)
122 case J.Obj{(key, field_value) <> tail}:
123 match members:
124 case False{}:
125 Equal.trans(String,
126 J.render_object_field("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix))) ++ suffix,
127 J.render_object_field("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix),
128 J.render_object_field("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix))),
129 render_object_field_append("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)), suffix),
130 Equal.cong(String, String, text => J.render_object_field("{", key, text),
131 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix,
132 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix)),
133 nested_render_append(field_value, J.Obj{tail}, True{}, prefix, suffix,
134 render_append(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix), suffix),
135 render_append(J.Obj{tail}, True{}, prefix, suffix))))
136 case True{}:
137 Equal.trans(String,
138 J.render_object_field(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix))) ++ suffix,
139 J.render_object_field(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix),
140 J.render_object_field(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix))),
141 render_object_field_append(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)), suffix),
142 Equal.cong(String, String, text => J.render_object_field(",", key, text),
143 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix,
144 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix)),
145 nested_render_append(field_value, J.Obj{tail}, True{}, prefix, suffix,
146 render_append(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix), suffix),
147 render_append(J.Obj{tail}, True{}, prefix, suffix))))
148
149def render_array_singleton_suffix(+head: J.Value,
150 +suffix: String) -> {J.render(J.Arr{head <> Nil{}}, False{}, suffix) == "[" ++ (J.render(head, False{}, SNil{}) ++ ("]" ++ suffix)) : String}:
151 Equal.cong(String, String, text => "[" ++ text,
152 J.render(head, False{}, J.render(J.Arr{Nil{}}, True{}, suffix)),
153 J.render(head, False{}, SNil{}) ++ ("]" ++ suffix),
154 Equal.trans(String,
155 J.render(head, False{}, J.render(J.Arr{Nil{}}, True{}, suffix)),
156 J.render(head, False{}, "]") ++ suffix,
157 J.render(head, False{}, SNil{}) ++ ("]" ++ suffix),
158 Equal.sym(String, J.render(head, False{}, "]") ++ suffix,
159 J.render(head, False{}, J.render(J.Arr{Nil{}}, True{}, suffix)),
160 nested_render_append(head, J.Arr{Nil{}}, True{}, SNil{}, suffix,
161 render_append(head, False{}, "]", suffix),
162 render_append(J.Arr{Nil{}}, True{}, SNil{}, suffix))),
163 Equal.trans(String,
164 J.render(head, False{}, "]") ++ suffix,
165 (J.render(head, False{}, SNil{}) ++ "]") ++ suffix,
166 J.render(head, False{}, SNil{}) ++ ("]" ++ suffix),
167 Equal.cong(String, String, text => text ++ suffix,
168 J.render(head, False{}, "]"), J.render(head, False{}, SNil{}) ++ "]",
169 Equal.sym(String, J.render(head, False{}, SNil{}) ++ "]",
170 J.render(head, False{}, "]"), render_append(head, False{}, SNil{}, "]"))),
171 S.append_assoc(J.render(head, False{}, SNil{}), "]", suffix))))
172
173def lex_source_number_before_punctuation(+text: String,
174 +certificate: J.NumberCert<text>,
175 +punctuation: Char,
176 +suffix: String,
177 +acc: List<&2, J.Lexeme>,
178 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(J.Number{text, certificate}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{text} <> acc) : List<&2, J.Lexeme>}:
179 Equal.trans(List<&2, J.Lexeme>,
180 J.lex_scan(J.render(J.Number{text, certificate}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
181 J.lex_scan(text ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
182 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{text} <> acc),
183 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
184 J.render(J.Number{text, certificate}, False{}, SNil{}), text,
185 S.append_nil(text)),
186 Num.lex_certified_number_before_punctuation(text, certificate, punctuation, suffix, acc, action))
187
188
189type AtomicValue is Data:
190 AtomicNull{}
191 AtomicTrue{}
192 AtomicFalse{}
193 AtomicNumber{text: String, certificate: J.NumberCert<text>}
194 AtomicString{text: String}
195
196type SimpleValue is Data:
197 SimpleAtom{atom: AtomicValue}
198 SimpleEmptyArray{}
199 SimpleEmptyObject{}
200
201def atomic_value(atom: AtomicValue) -> J.Value:
202 match atom:
203 case AtomicNull{}: J.Null{}
204 case AtomicTrue{}: J.Bool{True{}}
205 case AtomicFalse{}: J.Bool{False{}}
206 case AtomicNumber{text, certificate}: J.Number{text, certificate}
207 case AtomicString{text}: J.Str{text}
208
209def simple_value(simple: SimpleValue) -> J.Value:
210 match simple:
211 case SimpleAtom{atom}: atomic_value(atom)
212 case SimpleEmptyArray{}: J.Arr{Nil{}}
213 case SimpleEmptyObject{}: J.Obj{Nil{}}
214
215type RenderMode is Data:
216 RenderWhole{}
217 RenderMembers{}
218 RenderAfterSeparator{}
219
220type JsonPunctuation is Data:
221 ArrayEnd{}
222 ObjectEnd{}
223 MemberComma{}
224 KeyColon{}
225
226def punctuation_char(mark: JsonPunctuation) -> Char:
227 match mark:
228 case ArrayEnd{}: ']'
229 case ObjectEnd{}: '}'
230 case MemberComma{}: ','
231 case KeyColon{}: ':'
232
233def punctuation_action(mark: JsonPunctuation,
234 suffix: String) -> {J.lex_seed_action(SCon{punctuation_char(mark), suffix}, J.Outside{}) == J.LexPunctuation{punctuation_char(mark)} : J.LexAction}:
235 match mark:
236 case ArrayEnd{}: {==}
237 case ObjectEnd{}: {==}
238 case MemberComma{}: {==}
239 case KeyColon{}: {==}
240
241def render_after_separator(value: J.Value, suffix: String) -> String:
242 match value:
243 case J.Arr{Nil{}}: "]" ++ suffix
244 case J.Arr{head <> tail}: J.render(head, False{}, J.render(J.Arr{tail}, True{}, suffix))
245 case J.Obj{Nil{}}: "}" ++ suffix
246 case J.Obj{(key, field_value) <> tail}:
247 J.render_object_field(SNil{}, key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, suffix)))
248 case _: J.render(value, False{}, suffix)
249
250def render_task(value: J.Value, mode: RenderMode, suffix: String) -> String:
251 match mode:
252 case RenderWhole{}: J.render(value, False{}, suffix)
253 case RenderMembers{}: J.render(value, True{}, suffix)
254 case RenderAfterSeparator{}: render_after_separator(value, suffix)
255
256def source_after_separator(value: J.Value, suffix: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>:
257 match value:
258 case J.Arr{Nil{}}: J.Punctuation{']'} <> suffix
259 case J.Arr{head <> tail}: J.source(head, False{}, J.source(J.Arr{tail}, True{}, suffix))
260 case J.Obj{Nil{}}: J.Punctuation{'}'} <> suffix
261 case J.Obj{(key, field_value) <> tail}:
262 J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, suffix)))
263 case _: J.source(value, False{}, suffix)
264
265def source_task(value: J.Value, mode: RenderMode, suffix: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>:
266 match mode:
267 case RenderWhole{}: J.source(value, False{}, suffix)
268 case RenderMembers{}: J.source(value, True{}, suffix)
269 case RenderAfterSeparator{}: source_after_separator(value, suffix)
270
271def reverse_source_task(value: J.Value, mode: RenderMode) -> List<&2, J.Lexeme>:
272 List.reverse(&2, J.Lexeme, source_task(value, mode, Nil{}))
273
274def source_text_append(+text: String,
275 +first: List<&2, J.Lexeme>,
276 +second: List<&2, J.Lexeme>) -> {J.source_text(text, List.append(&2, J.Lexeme, first, second)) == List.append(&2, J.Lexeme, J.source_text(text, first), second) : List<&2, J.Lexeme>}:
277 {==}
278
279def source_append(+value: J.Value,
280 +members: Bool,
281 +first: List<&2, J.Lexeme>,
282 +second: List<&2, J.Lexeme>) -> {J.source(value, members, List.append(&2, J.Lexeme, first, second)) == List.append(&2, J.Lexeme, J.source(value, members, first), second) : List<&2, J.Lexeme>}:
283 match value:
284 case J.Null{}: source_text_append("null", first, second)
285 case J.Bool{truth}:
286 match truth:
287 case True{}: source_text_append("true", first, second)
288 case False{}: source_text_append("false", first, second)
289 case J.Number{lexeme, certificate}: source_text_append(lexeme, first, second)
290 case J.Str{text}: source_text_append("\"" ++ J.escape_string(text) ++ "\"", first, second)
291 case J.Arr{Nil{}}:
292 match members:
293 case False{}: {==}
294 case True{}: {==}
295 case J.Arr{head <> tail}:
296 match members:
297 case False{}:
298 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{'['} <> xs,
299 J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
300 List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second),
301 Equal.trans(List<&2, J.Lexeme>,
302 J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
303 J.source(head, False{}, List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second)),
304 List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second),
305 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(head, False{}, xs),
306 J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second)),
307 List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second),
308 source_append(J.Arr{tail}, True{}, first, second)),
309 source_append(head, False{}, J.source(J.Arr{tail}, True{}, first), second)))
310 case True{}:
311 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{','} <> xs,
312 J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
313 List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second),
314 Equal.trans(List<&2, J.Lexeme>,
315 J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
316 J.source(head, False{}, List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second)),
317 List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second),
318 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(head, False{}, xs),
319 J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second)),
320 List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second),
321 source_append(J.Arr{tail}, True{}, first, second)),
322 source_append(head, False{}, J.source(J.Arr{tail}, True{}, first), second)))
323 case J.Obj{Nil{}}:
324 match members:
325 case False{}: {==}
326 case True{}: {==}
327 case J.Obj{(key, field_value) <> tail}:
328 match members:
329 case False{}:
330 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{'{'} <> xs,
331 J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)))),
332 List.append(&2, J.Lexeme, J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first))), second),
333 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> xs),
334 J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
335 List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second),
336 Equal.trans(List<&2, J.Lexeme>,
337 J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
338 J.source(field_value, False{}, List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second)),
339 List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second),
340 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(field_value, False{}, xs),
341 J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)),
342 List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second),
343 source_append(J.Obj{tail}, True{}, first, second)),
344 source_append(field_value, False{}, J.source(J.Obj{tail}, True{}, first), second))))
345 case True{}:
346 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{','} <> xs,
347 J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)))),
348 List.append(&2, J.Lexeme, J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first))), second),
349 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> xs),
350 J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
351 List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second),
352 Equal.trans(List<&2, J.Lexeme>,
353 J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
354 J.source(field_value, False{}, List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second)),
355 List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second),
356 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(field_value, False{}, xs),
357 J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)),
358 List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second),
359 source_append(J.Obj{tail}, True{}, first, second)),
360 source_append(field_value, False{}, J.source(J.Obj{tail}, True{}, first), second))))
361
362def reverse_source_suffix(+value: J.Value,
363 +members: Bool,
364 +suffix: List<&2, J.Lexeme>) -> {List.reverse(&2, J.Lexeme, J.source(value, members, suffix)) == List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, suffix), List.reverse(&2, J.Lexeme, J.source(value, members, Nil{}))) : List<&2, J.Lexeme>}:
365 Equal.trans(List<&2, J.Lexeme>,
366 List.reverse(&2, J.Lexeme, J.source(value, members, suffix)),
367 List.reverse(&2, J.Lexeme, List.append(&2, J.Lexeme, J.source(value, members, Nil{}), suffix)),
368 List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, suffix),
369 List.reverse(&2, J.Lexeme, J.source(value, members, Nil{}))),
370 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items),
371 J.source(value, members, suffix),
372 List.append(&2, J.Lexeme, J.source(value, members, Nil{}), suffix),
373 source_append(value, members, Nil{}, suffix)),
374 LP.reverse_append(J.Lexeme, J.source(value, members, Nil{}), suffix))
375
376def reverse_source_text(+text: String,
377 +suffix: List<&2, J.Lexeme>) -> {List.reverse(&2, J.Lexeme, J.source_text(text, suffix)) == List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, suffix), J.Payload{text} <> Nil{}) : List<&2, J.Lexeme>}:
378 LP.reverse_cons(J.Lexeme, J.Payload{text}, suffix)
379
380def reverse_source_colon_value_tail(+value: J.Value,
381 +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>) -> {List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))) == List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})) : List<&2, J.Lexeme>}:
382 Equal.trans(List<&2, J.Lexeme>,
383 List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
384 List.append(&2, J.Lexeme,
385 List.reverse(&2, J.Lexeme, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
386 J.Punctuation{':'} <> Nil{}),
387 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
388 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})),
389 LP.reverse_cons(J.Lexeme, J.Punctuation{':'}, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
390 Equal.trans(List<&2, J.Lexeme>,
391 List.append(&2, J.Lexeme,
392 List.reverse(&2, J.Lexeme, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
393 J.Punctuation{':'} <> Nil{}),
394 List.append(&2, J.Lexeme,
395 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), reverse_source_task(value, RenderWhole{})),
396 J.Punctuation{':'} <> Nil{}),
397 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
398 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})),
399 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs =>
400 List.append(&2, J.Lexeme, xs, J.Punctuation{':'} <> Nil{}),
401 List.reverse(&2, J.Lexeme, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
402 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), reverse_source_task(value, RenderWhole{})),
403 reverse_source_suffix(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
404 LP.append_assoc(J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
405 reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})))
406
407def reverse_source_object_after_separator(+key: String,
408 +value: J.Value,
409 +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>) -> {reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})) : List<&2, J.Lexeme>}:
410 Equal.trans(List<&2, J.Lexeme>,
411 reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}),
412 List.append(&2, J.Lexeme,
413 List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
414 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
415 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
416 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}),
417 J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})),
418 reverse_source_text("\"" ++ J.escape_string(key) ++ "\"",
419 J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
420 Equal.trans(List<&2, J.Lexeme>,
421 List.append(&2, J.Lexeme,
422 List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
423 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
424 List.append(&2, J.Lexeme,
425 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
426 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})),
427 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
428 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
429 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}),
430 J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})),
431 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs =>
432 List.append(&2, J.Lexeme, xs, J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
433 List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
434 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
435 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})),
436 reverse_source_colon_value_tail(value, tail)),
437 Equal.trans(List<&2, J.Lexeme>,
438 List.append(&2, J.Lexeme,
439 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
440 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})),
441 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
442 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
443 List.append(&2, J.Lexeme,
444 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{}),
445 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})),
446 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
447 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}),
448 J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})),
449 LP.append_assoc(J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
450 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{}),
451 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
452 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs =>
453 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), xs),
454 List.append(&2, J.Lexeme,
455 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{}),
456 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
457 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}),
458 List.append(&2, J.Lexeme, J.Punctuation{':'} <> Nil{}, J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})),
459 LP.append_assoc(J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{},
460 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})))))
461
462def reverse_source_object_members_after_separator(+key: String,
463 +value: J.Value,
464 +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>) -> {reverse_source_task(J.Obj{(key, value) <> tail}, RenderMembers{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}) : List<&2, J.Lexeme>}:
465 Equal.trans(List<&2, J.Lexeme>,
466 reverse_source_task(J.Obj{(key, value) <> tail}, RenderMembers{}),
467 List.reverse(&2, J.Lexeme, J.Punctuation{','} <> source_after_separator(J.Obj{(key, value) <> tail}, Nil{})),
468 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}),
469 J.Punctuation{','} <> Nil{}),
470 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items),
471 J.source(J.Obj{(key, value) <> tail}, True{}, Nil{}),
472 J.Punctuation{','} <> source_after_separator(J.Obj{(key, value) <> tail}, Nil{}),
473 {==}),
474 LP.reverse_cons(J.Lexeme, J.Punctuation{','}, source_after_separator(J.Obj{(key, value) <> tail}, Nil{})))
475
476def reverse_source_array_whole(+head: J.Value,
477 +tail: List<&2, J.Value>) -> {reverse_source_task(J.Arr{head <> tail}, RenderWhole{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})) : List<&2, J.Lexeme>}:
478 Equal.trans(List<&2, J.Lexeme>,
479 reverse_source_task(J.Arr{head <> tail}, RenderWhole{}),
480 List.reverse(&2, J.Lexeme, List.append(&2, J.Lexeme,
481 J.Punctuation{'['} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{}))),
482 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
483 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
484 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items),
485 J.source(J.Arr{head <> tail}, False{}, Nil{}),
486 List.append(&2, J.Lexeme, J.Punctuation{'['} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})),
487 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.Punctuation{'['} <> items,
488 J.source(head, False{}, J.source(J.Arr{tail}, True{}, Nil{})),
489 List.append(&2, J.Lexeme, J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})),
490 source_append(head, False{}, Nil{}, J.source(J.Arr{tail}, True{}, Nil{})))),
491 Equal.trans(List<&2, J.Lexeme>,
492 List.reverse(&2, J.Lexeme, List.append(&2, J.Lexeme,
493 J.Punctuation{'['} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{}))),
494 List.append(&2, J.Lexeme,
495 List.reverse(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, Nil{})),
496 List.reverse(&2, J.Lexeme, J.Punctuation{'['} <> J.source(head, False{}, Nil{}))),
497 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
498 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
499 LP.reverse_append(J.Lexeme, J.Punctuation{'['} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})),
500 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), items),
501 List.reverse(&2, J.Lexeme, J.Punctuation{'['} <> J.source(head, False{}, Nil{})),
502 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{}),
503 LP.reverse_cons(J.Lexeme, J.Punctuation{'['}, J.source(head, False{}, Nil{})))))
504
505def reverse_source_array_members(+head: J.Value,
506 +tail: List<&2, J.Value>) -> {reverse_source_task(J.Arr{head <> tail}, RenderMembers{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{','} <> Nil{})) : List<&2, J.Lexeme>}:
507 Equal.trans(List<&2, J.Lexeme>,
508 reverse_source_task(J.Arr{head <> tail}, RenderMembers{}),
509 List.reverse(&2, J.Lexeme, List.append(&2, J.Lexeme,
510 J.Punctuation{','} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{}))),
511 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
512 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{','} <> Nil{})),
513 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items),
514 J.source(J.Arr{head <> tail}, True{}, Nil{}),
515 List.append(&2, J.Lexeme, J.Punctuation{','} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})),
516 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.Punctuation{','} <> items,
517 J.source(head, False{}, J.source(J.Arr{tail}, True{}, Nil{})),
518 List.append(&2, J.Lexeme, J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})),
519 source_append(head, False{}, Nil{}, J.source(J.Arr{tail}, True{}, Nil{})))),
520 Equal.trans(List<&2, J.Lexeme>,
521 List.reverse(&2, J.Lexeme, List.append(&2, J.Lexeme,
522 J.Punctuation{','} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{}))),
523 List.append(&2, J.Lexeme,
524 List.reverse(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, Nil{})),
525 List.reverse(&2, J.Lexeme, J.Punctuation{','} <> J.source(head, False{}, Nil{}))),
526 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
527 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{','} <> Nil{})),
528 LP.reverse_append(J.Lexeme, J.Punctuation{','} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})),
529 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), items),
530 List.reverse(&2, J.Lexeme, J.Punctuation{','} <> J.source(head, False{}, Nil{})),
531 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{','} <> Nil{}),
532 LP.reverse_cons(J.Lexeme, J.Punctuation{','}, J.source(head, False{}, Nil{})))))
533
534def reverse_source_array_after_separator(+head: J.Value,
535 +tail: List<&2, J.Value>) -> {reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})) : List<&2, J.Lexeme>}:
536 reverse_source_suffix(head, False{}, J.source(J.Arr{tail}, True{}, Nil{}))
537
538def reverse_source_array_after_separator_whole(+head: J.Value,
539 +tail: List<&2, J.Value>) -> {reverse_source_task(J.Arr{head <> tail}, RenderWhole{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}) : List<&2, J.Lexeme>}:
540 Equal.trans(List<&2, J.Lexeme>,
541 reverse_source_task(J.Arr{head <> tail}, RenderWhole{}),
542 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
543 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
544 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}),
545 reverse_source_array_whole(head, tail),
546 Equal.trans(List<&2, J.Lexeme>,
547 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
548 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
549 List.append(&2, J.Lexeme,
550 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})),
551 J.Punctuation{'['} <> Nil{}),
552 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}),
553 Equal.sym(List<&2, J.Lexeme>,
554 List.append(&2, J.Lexeme,
555 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})),
556 J.Punctuation{'['} <> Nil{}),
557 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
558 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
559 LP.append_assoc(J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
560 reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
561 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items =>
562 List.append(&2, J.Lexeme, items, J.Punctuation{'['} <> Nil{}),
563 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})),
564 reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}),
565 Equal.sym(List<&2, J.Lexeme>, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}),
566 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})),
567 reverse_source_array_after_separator(head, tail)))))
568
569def reverse_source_array_members_after_separator(+head: J.Value,
570 +tail: List<&2, J.Value>) -> {reverse_source_task(J.Arr{head <> tail}, RenderMembers{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}) : List<&2, J.Lexeme>}:
571 Equal.trans(List<&2, J.Lexeme>,
572 reverse_source_task(J.Arr{head <> tail}, RenderMembers{}),
573 List.reverse(&2, J.Lexeme, J.Punctuation{','} <> source_after_separator(J.Arr{head <> tail}, Nil{})),
574 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}),
575 J.Punctuation{','} <> Nil{}),
576 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items),
577 J.source(J.Arr{head <> tail}, True{}, Nil{}),
578 J.Punctuation{','} <> source_after_separator(J.Arr{head <> tail}, Nil{}),
579 {==}),
580 LP.reverse_cons(J.Lexeme, J.Punctuation{','}, source_after_separator(J.Arr{head <> tail}, Nil{})))
581
582def source_separator(value: J.Value) -> List<&2, J.Lexeme>:
583 match value:
584 case J.Arr{Nil{}}: Nil{}
585 case J.Arr{_ <> _}: J.Punctuation{','} <> Nil{}
586 case J.Obj{Nil{}}: Nil{}
587 case J.Obj{_ <> _}: J.Punctuation{','} <> Nil{}
588 case _: Nil{}
589
590def separator_text(value: J.Value) -> String:
591 match value:
592 case J.Arr{Nil{}}: SNil{}
593 case J.Arr{_ <> _}: ","
594 case J.Obj{Nil{}}: SNil{}
595 case J.Obj{_ <> _}: ","
596 case _: SNil{}
597
598def render_members_decompose(+value: J.Value,
599 +suffix: String) -> {J.render(value, True{}, suffix) == separator_text(value) ++ render_after_separator(value, suffix) : String}:
600 match value:
601 case J.Null{}: {==}
602 case J.Bool{truth}:
603 match truth:
604 case True{}: {==}
605 case False{}: {==}
606 case J.Number{lexeme, certificate}: {==}
607 case J.Str{text}: {==}
608 case J.Arr{Nil{}}: {==}
609 case J.Arr{head <> tail}: {==}
610 case J.Obj{Nil{}}: {==}
611 case J.Obj{(key, field_value) <> tail}: {==}
612
613def render_after_separator_array_decompose(+head: J.Value,
614 +tail: List<&2, J.Value>,
615 +suffix: String) -> {render_after_separator(J.Arr{head <> tail}, suffix) == J.render(head, False{}, SNil{}) ++ (separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix)) : String}:
616 Equal.trans(String,
617 render_after_separator(J.Arr{head <> tail}, suffix),
618 J.render(head, False{}, SNil{}) ++ J.render(J.Arr{tail}, True{}, suffix),
619 J.render(head, False{}, SNil{}) ++
620 (separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix)),
621 Equal.sym(String,
622 J.render(head, False{}, SNil{}) ++ J.render(J.Arr{tail}, True{}, suffix),
623 render_after_separator(J.Arr{head <> tail}, suffix),
624 render_append(head, False{}, SNil{}, J.render(J.Arr{tail}, True{}, suffix))),
625 Equal.cong(String, String, text => J.render(head, False{}, SNil{}) ++ text,
626 J.render(J.Arr{tail}, True{}, suffix),
627 separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix),
628 render_members_decompose(J.Arr{tail}, suffix)))
629
630def render_after_separator_object_decompose(+key: String,
631 +value: J.Value,
632 +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>, +suffix: String) -> {render_after_separator(J.Obj{(key, value) <> tail}, suffix) == J.render_object_field(SNil{}, key, J.render(value, False{}, SNil{}) ++ (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix))) : String}:
633 Equal.cong(String, String, text => J.render_object_field(SNil{}, key, text),
634 J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)),
635 J.render(value, False{}, SNil{}) ++
636 (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix)),
637 Equal.trans(String,
638 J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)),
639 J.render(value, False{}, SNil{}) ++ J.render(J.Obj{tail}, True{}, suffix),
640 J.render(value, False{}, SNil{}) ++
641 (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix)),
642 Equal.sym(String,
643 J.render(value, False{}, SNil{}) ++ J.render(J.Obj{tail}, True{}, suffix),
644 J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)),
645 render_append(value, False{}, SNil{}, J.render(J.Obj{tail}, True{}, suffix))),
646 Equal.cong(String, String, text => J.render(value, False{}, SNil{}) ++ text,
647 J.render(J.Obj{tail}, True{}, suffix),
648 separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix),
649 render_members_decompose(J.Obj{tail}, suffix))))
650
651def render_object_whole_decompose(+key: String,
652 +value: J.Value,
653 +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>, +suffix: String) -> {J.render(J.Obj{(key, value) <> tail}, False{}, suffix) == J.render_object_field("{", key, J.render(value, False{}, SNil{}) ++ (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix))) : String}:
654 Equal.cong(String, String, text => J.render_object_field("{", key, text),
655 J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)),
656 J.render(value, False{}, SNil{}) ++
657 (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix)),
658 Equal.trans(String,
659 J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)),
660 J.render(value, False{}, SNil{}) ++ J.render(J.Obj{tail}, True{}, suffix),
661 J.render(value, False{}, SNil{}) ++
662 (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix)),
663 Equal.sym(String,
664 J.render(value, False{}, SNil{}) ++ J.render(J.Obj{tail}, True{}, suffix),
665 J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)),
666 render_append(value, False{}, SNil{}, J.render(J.Obj{tail}, True{}, suffix))),
667 Equal.cong(String, String, text => J.render(value, False{}, SNil{}) ++ text,
668 J.render(J.Obj{tail}, True{}, suffix),
669 separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix),
670 render_members_decompose(J.Obj{tail}, suffix))))
671
672def render_array_whole_decompose(+head: J.Value,
673 +tail: List<&2, J.Value>,
674 +suffix: String) -> {J.render(J.Arr{head <> tail}, False{}, suffix) == "[" ++ (J.render(head, False{}, SNil{}) ++ (separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix))) : String}:
675 Equal.cong(String, String, text => "[" ++ text,
676 render_after_separator(J.Arr{head <> tail}, suffix),
677 J.render(head, False{}, SNil{}) ++
678 (separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix)),
679 render_after_separator_array_decompose(head, tail, suffix))
680
681def render_after_separator_append(+value: J.Value,
682 +prefix: String,
683 +suffix: String) -> {render_after_separator(value, prefix) ++ suffix == render_after_separator(value, prefix ++ suffix) : String}:
684 match value:
685 case J.Arr{Nil{}}: S.append_assoc("]", prefix, suffix)
686 case J.Arr{head <> tail}:
687 nested_render_append(head, J.Arr{tail}, True{}, prefix, suffix,
688 render_append(head, False{}, J.render(J.Arr{tail}, True{}, prefix), suffix),
689 render_append(J.Arr{tail}, True{}, prefix, suffix))
690 case J.Obj{Nil{}}: S.append_assoc("}", prefix, suffix)
691 case J.Obj{(key, field_value) <> tail}:
692 Equal.trans(String,
693 render_after_separator(J.Obj{(key, field_value) <> tail}, prefix) ++ suffix,
694 J.render_object_field(SNil{}, key,
695 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix),
696 render_after_separator(J.Obj{(key, field_value) <> tail}, prefix ++ suffix),
697 render_object_field_append(SNil{}, key,
698 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)), suffix),
699 Equal.cong(String, String, text => J.render_object_field(SNil{}, key, text),
700 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix,
701 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix)),
702 nested_render_append(field_value, J.Obj{tail}, True{}, prefix, suffix,
703 render_append(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix), suffix),
704 render_append(J.Obj{tail}, True{}, prefix, suffix))))
705 case J.Null{}: render_append(J.Null{}, False{}, prefix, suffix)
706 case J.Bool{truth}:
707 match truth:
708 case True{}: render_append(J.Bool{True{}}, False{}, prefix, suffix)
709 case False{}: render_append(J.Bool{False{}}, False{}, prefix, suffix)
710 case J.Number{lexeme, certificate}:
711 render_append(J.Number{lexeme, certificate}, False{}, prefix, suffix)
712 case J.Str{text}: render_append(J.Str{text}, False{}, prefix, suffix)
713
714def render_task_append(+value: J.Value,
715 +mode: RenderMode,
716 +prefix: String,
717 +suffix: String) -> {render_task(value, mode, prefix) ++ suffix == render_task(value, mode, prefix ++ suffix) : String}:
718 match mode:
719 case RenderWhole{}: render_append(value, False{}, prefix, suffix)
720 case RenderMembers{}: render_append(value, True{}, prefix, suffix)
721 case RenderAfterSeparator{}: render_after_separator_append(value, prefix, suffix)
722
723def render_after_separator_array_single(+head: J.Value,
724 +suffix: String) -> {render_after_separator(J.Arr{head <> Nil{}}, suffix) == render_task(head, RenderWhole{}, "]" ++ suffix) : String}:
725 Equal.trans(String,
726 render_after_separator(J.Arr{head <> Nil{}}, suffix),
727 J.render(head, False{}, SNil{}) ++ (separator_text(J.Arr{Nil{}}) ++ render_after_separator(J.Arr{Nil{}}, suffix)),
728 render_task(head, RenderWhole{}, "]" ++ suffix),
729 render_after_separator_array_decompose(head, Nil{}, suffix),
730 Equal.trans(String,
731 J.render(head, False{}, SNil{}) ++ (separator_text(J.Arr{Nil{}}) ++ render_after_separator(J.Arr{Nil{}}, suffix)),
732 J.render(head, False{}, SNil{}) ++ ("]" ++ suffix),
733 render_task(head, RenderWhole{}, "]" ++ suffix),
734 Equal.cong(String, String, text => J.render(head, False{}, SNil{}) ++ text,
735 separator_text(J.Arr{Nil{}}) ++ render_after_separator(J.Arr{Nil{}}, suffix), "]" ++ suffix, {==}),
736 render_task_append(head, RenderWhole{}, SNil{}, "]" ++ suffix)))
737
738def render_after_separator_array_many(+head: J.Value,
739 +next: J.Value,
740 +tail: List<&2, J.Value>,
741 +suffix: String) -> {render_after_separator(J.Arr{head <> next <> tail}, suffix) == render_task(head, RenderWhole{}, "," ++ render_after_separator(J.Arr{next <> tail}, suffix)) : String}:
742 Equal.trans(String,
743 render_after_separator(J.Arr{head <> next <> tail}, suffix),
744 J.render(head, False{}, SNil{}) ++
745 (separator_text(J.Arr{next <> tail}) ++ render_after_separator(J.Arr{next <> tail}, suffix)),
746 render_task(head, RenderWhole{}, "," ++ render_after_separator(J.Arr{next <> tail}, suffix)),
747 render_after_separator_array_decompose(head, next <> tail, suffix),
748 render_task_append(head, RenderWhole{}, SNil{}, "," ++ render_after_separator(J.Arr{next <> tail}, suffix)))
749
750
751
752
753def source_members_decompose(+value: J.Value,
754 +suffix: List<&2, J.Lexeme>) -> {J.source(value, True{}, suffix) == List.append(&2, J.Lexeme, source_separator(value), source_after_separator(value, suffix)) : List<&2, J.Lexeme>}:
755 match value:
756 case J.Null{}: {==}
757 case J.Bool{truth}:
758 match truth:
759 case True{}: {==}
760 case False{}: {==}
761 case J.Number{lexeme, certificate}: {==}
762 case J.Str{text}: {==}
763 case J.Arr{Nil{}}: {==}
764 case J.Arr{head <> tail}: {==}
765 case J.Obj{Nil{}}: {==}
766 case J.Obj{(key, field_value) <> tail}: {==}
767
768def atomic_source(atom: AtomicValue) -> List<&2, J.Lexeme>:
769 match atom:
770 case AtomicNull{}: J.Payload{"null"} <> Nil{}
771 case AtomicTrue{}: J.Payload{"true"} <> Nil{}
772 case AtomicFalse{}: J.Payload{"false"} <> Nil{}
773 case AtomicNumber{text, _}: J.Payload{text} <> Nil{}
774 case AtomicString{text}: J.Payload{"\"" ++ J.escape_string(text) ++ "\""} <> Nil{}
775
776def atomic_source_reverse(+atom: AtomicValue) -> {atomic_source(atom) == List.reverse(&2, J.Lexeme, J.source(atomic_value(atom), False{}, Nil{})) : List<&2, J.Lexeme>}:
777 match atom:
778 case AtomicNull{}: {==}
779 case AtomicTrue{}: {==}
780 case AtomicFalse{}: {==}
781 case AtomicNumber{text, certificate}: {==}
782 case AtomicString{text}: {==}
783
784def lex_atomic_source_before_punctuation(+atom: AtomicValue,
785 +punctuation: Char,
786 +suffix: String,
787 +acc: List<&2, J.Lexeme>,
788 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(atomic_value(atom), False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(atom), acc)) : List<&2, J.Lexeme>}:
789 match atom:
790 case AtomicNull{}:
791 Equal.trans(List<&2, J.Lexeme>,
792 J.lex_scan(J.render(J.Null{}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
793 J.lex_scan("null" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
794 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(AtomicNull{}), acc)),
795 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
796 J.render(J.Null{}, False{}, SNil{}), "null", S.append_nil("null")),
797 W.lex_null_before_punctuation(punctuation, suffix, acc, action))
798 case AtomicTrue{}:
799 Equal.trans(List<&2, J.Lexeme>,
800 J.lex_scan(J.render(J.Bool{True{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
801 J.lex_scan("true" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
802 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(AtomicTrue{}), acc)),
803 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
804 J.render(J.Bool{True{}}, False{}, SNil{}), "true", S.append_nil("true")),
805 W.lex_true_before_punctuation(punctuation, suffix, acc, action))
806 case AtomicFalse{}:
807 Equal.trans(List<&2, J.Lexeme>,
808 J.lex_scan(J.render(J.Bool{False{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
809 J.lex_scan("false" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
810 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(AtomicFalse{}), acc)),
811 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
812 J.render(J.Bool{False{}}, False{}, SNil{}), "false", S.append_nil("false")),
813 W.lex_false_before_punctuation(punctuation, suffix, acc, action))
814 case AtomicNumber{text, certificate}:
815 lex_source_number_before_punctuation(text, certificate, punctuation, suffix, acc, action)
816 case AtomicString{text}:
817 Equal.trans(List<&2, J.Lexeme>,
818 J.lex_scan(J.render(J.Str{text}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
819 J.lex_scan((SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
820 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(AtomicString{text}), acc)),
821 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
822 J.render(J.Str{text}, False{}, SNil{}), SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, {==}),
823 W.lex_string_before_punctuation(text, punctuation, suffix, acc, action))
824
825def lex_atomic_reverse_before_punctuation(+atom: AtomicValue,
826 +punctuation: Char,
827 +suffix: String,
828 +acc: List<&2, J.Lexeme>,
829 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(atomic_value(atom), False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, J.source(atomic_value(atom), False{}, Nil{})), acc)) : List<&2, J.Lexeme>}:
830 Equal.trans(List<&2, J.Lexeme>,
831 J.lex_scan(J.render(atomic_value(atom), False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
832 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(atom), acc)),
833 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, J.source(atomic_value(atom), False{}, Nil{})), acc)),
834 lex_atomic_source_before_punctuation(atom, punctuation, suffix, acc, action),
835 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, items, acc)),
836 atomic_source(atom),
837 List.reverse(&2, J.Lexeme, J.source(atomic_value(atom), False{}, Nil{})),
838 atomic_source_reverse(atom)))
839
840def lex_atomic_value_source(+atom: AtomicValue) -> {J.lex_scan(J.stringify(atomic_value(atom)), J.Outside{}, SNil{}, Nil{}) == J.source(atomic_value(atom), False{}, Nil{}) : List<&2, J.Lexeme>}:
841 match atom:
842 case AtomicNull{}: {==}
843 case AtomicTrue{}: {==}
844 case AtomicFalse{}: {==}
845 case AtomicNumber{text, certificate}:
846 Equal.trans(List<&2, J.Lexeme>,
847 J.lex_scan(J.stringify(J.Number{text, certificate}), J.Outside{}, SNil{}, Nil{}),
848 J.lex_scan(text, J.Outside{}, SNil{}, Nil{}),
849 J.source(J.Number{text, certificate}, False{}, Nil{}),
850 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source, J.Outside{}, SNil{}, Nil{}),
851 J.stringify(J.Number{text, certificate}), text, S.append_nil(text)),
852 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, J.Outside{}, SNil{}, Nil{}),
853 J.Payload{text} <> Nil{}, J.source(J.Number{text, certificate}, False{}, Nil{}),
854 Num.lex_number_payload(text, P.cert_valid(text, certificate)), {==}))
855 case AtomicString{text}:
856 W.lex_rendered_string(text)
857
858
859def lex_source_empty_array_before_punctuation(+punctuation: Char,
860 +suffix: String,
861 +acc: List<&2, J.Lexeme>,
862 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(J.Arr{Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> J.Punctuation{'['} <> acc) : List<&2, J.Lexeme>}:
863 Equal.trans(List<&2, J.Lexeme>,
864 J.lex_scan(J.render(J.Arr{Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
865 J.lex_scan("[]" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
866 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> J.Punctuation{'['} <> acc),
867 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
868 J.render(J.Arr{Nil{}}, False{}, SNil{}), "[]", S.append_nil("[]")),
869 W.lex_empty_array_before_punctuation(punctuation, suffix, acc, action))
870
871def lex_source_empty_object_before_punctuation(+punctuation: Char,
872 +suffix: String,
873 +acc: List<&2, J.Lexeme>,
874 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(J.Obj{Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{'}'} <> J.Punctuation{'{'} <> acc) : List<&2, J.Lexeme>}:
875 Equal.trans(List<&2, J.Lexeme>,
876 J.lex_scan(J.render(J.Obj{Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
877 J.lex_scan("{}" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
878 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{'}'} <> J.Punctuation{'{'} <> acc),
879 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
880 J.render(J.Obj{Nil{}}, False{}, SNil{}), "{}", S.append_nil("{}")),
881 W.lex_empty_object_before_punctuation(punctuation, suffix, acc, action))
882
883def lex_empty_array_reverse_before_punctuation(+punctuation: Char,
884 +suffix: String,
885 +acc: List<&2, J.Lexeme>,
886 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(J.Arr{Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, J.source(J.Arr{Nil{}}, False{}, Nil{})), acc)) : List<&2, J.Lexeme>}:
887 lex_source_empty_array_before_punctuation(punctuation, suffix, acc, action)
888
889def lex_empty_object_reverse_before_punctuation(+punctuation: Char,
890 +suffix: String,
891 +acc: List<&2, J.Lexeme>,
892 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(J.Obj{Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, J.source(J.Obj{Nil{}}, False{}, Nil{})), acc)) : List<&2, J.Lexeme>}:
893 lex_source_empty_object_before_punctuation(punctuation, suffix, acc, action)
894
895def lex_simple_before_punctuation(+simple: SimpleValue,
896 +punctuation: Char,
897 +suffix: String,
898 +acc: List<&2, J.Lexeme>,
899 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(simple_value(simple), False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, J.source(simple_value(simple), False{}, Nil{})), acc)) : List<&2, J.Lexeme>}:
900 match simple:
901 case SimpleAtom{atom}: lex_atomic_reverse_before_punctuation(atom, punctuation, suffix, acc, action)
902 case SimpleEmptyArray{}: lex_empty_array_reverse_before_punctuation(punctuation, suffix, acc, action)
903 case SimpleEmptyObject{}: lex_empty_object_reverse_before_punctuation(punctuation, suffix, acc, action)
904
905def lex_close_before_punctuation(+closing: Char,
906 +punctuation: Char,
907 +suffix: String,
908 +acc: List<&2, J.Lexeme>,
909 close_action: {J.lex_seed_action(SCon{closing, SCon{punctuation, SNil{}} ++ suffix}, J.Outside{}) == J.LexPunctuation{closing} : J.LexAction},
910 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(SCon{closing, SCon{punctuation, SNil{}} ++ suffix}, J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{closing} <> acc) : List<&2, J.Lexeme>}:
911 Equal.trans(List<&2, J.Lexeme>,
912 J.lex_scan(SCon{closing, SCon{punctuation, SNil{}} ++ suffix}, J.Outside{}, SNil{}, acc),
913 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{closing} <> acc),
914 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{closing} <> acc),
915 W.scan_punctuation_char(closing, SCon{punctuation, SNil{}} ++ suffix, SNil{}, acc, close_action),
916 W.scan_punctuation_char(punctuation, suffix, SNil{}, J.Punctuation{closing} <> acc, action))
917
918def lex_object_key_before_colon(+key: String,
919 +suffix: String,
920 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> acc) : List<&2, J.Lexeme>}:
921 W.lex_string_before_punctuation(key, ':', suffix, acc, {==})
922
923def atomic_task_render(atom: AtomicValue,
924 mode: RenderMode) -> {render_task(atomic_value(atom), mode, SNil{}) == J.render(atomic_value(atom), False{}, SNil{}) : String}:
925 match atom mode:
926 case AtomicNull{} RenderWhole{}: {==}
927 case AtomicTrue{} RenderWhole{}: {==}
928 case AtomicFalse{} RenderWhole{}: {==}
929 case AtomicNumber{text, certificate} RenderWhole{}: {==}
930 case AtomicString{text} RenderWhole{}: {==}
931 case AtomicNull{} RenderMembers{}: {==}
932 case AtomicTrue{} RenderMembers{}: {==}
933 case AtomicFalse{} RenderMembers{}: {==}
934 case AtomicNumber{text, certificate} RenderMembers{}: {==}
935 case AtomicString{text} RenderMembers{}: {==}
936 case AtomicNull{} RenderAfterSeparator{}: {==}
937 case AtomicTrue{} RenderAfterSeparator{}: {==}
938 case AtomicFalse{} RenderAfterSeparator{}: {==}
939 case AtomicNumber{text, certificate} RenderAfterSeparator{}: {==}
940 case AtomicString{text} RenderAfterSeparator{}: {==}
941
942def atomic_task_source(atom: AtomicValue,
943 mode: RenderMode) -> {reverse_source_task(atomic_value(atom), mode) == reverse_source_task(atomic_value(atom), RenderWhole{}) : List<&2, J.Lexeme>}:
944 match atom mode:
945 case AtomicNull{} RenderWhole{}: {==}
946 case AtomicTrue{} RenderWhole{}: {==}
947 case AtomicFalse{} RenderWhole{}: {==}
948 case AtomicNumber{text, certificate} RenderWhole{}: {==}
949 case AtomicString{text} RenderWhole{}: {==}
950 case AtomicNull{} RenderMembers{}: {==}
951 case AtomicTrue{} RenderMembers{}: {==}
952 case AtomicFalse{} RenderMembers{}: {==}
953 case AtomicNumber{text, certificate} RenderMembers{}: {==}
954 case AtomicString{text} RenderMembers{}: {==}
955 case AtomicNull{} RenderAfterSeparator{}: {==}
956 case AtomicTrue{} RenderAfterSeparator{}: {==}
957 case AtomicFalse{} RenderAfterSeparator{}: {==}
958 case AtomicNumber{text, certificate} RenderAfterSeparator{}: {==}
959 case AtomicString{text} RenderAfterSeparator{}: {==}
960
961def lex_atomic_task_before_punctuation(+atom: AtomicValue,
962 +mode: RenderMode,
963 +punctuation: Char,
964 +suffix: String,
965 +acc: List<&2, J.Lexeme>,
966 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(render_task(atomic_value(atom), mode, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, reverse_source_task(atomic_value(atom), mode), acc)) : List<&2, J.Lexeme>}:
967 Equal.trans(List<&2, J.Lexeme>,
968 J.lex_scan(render_task(atomic_value(atom), mode, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix),
969 J.Outside{}, SNil{}, acc),
970 J.lex_scan(J.render(atomic_value(atom), False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix),
971 J.Outside{}, SNil{}, acc),
972 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <>
973 List.append(&2, J.Lexeme, reverse_source_task(atomic_value(atom), mode), acc)),
974 Equal.cong(String, List<&2, J.Lexeme>, text =>
975 J.lex_scan(text ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
976 render_task(atomic_value(atom), mode, SNil{}), J.render(atomic_value(atom), False{}, SNil{}),
977 atomic_task_render(atom, mode)),
978 Equal.trans(List<&2, J.Lexeme>,
979 J.lex_scan(J.render(atomic_value(atom), False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix),
980 J.Outside{}, SNil{}, acc),
981 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <>
982 List.append(&2, J.Lexeme, reverse_source_task(atomic_value(atom), RenderWhole{}), acc)),
983 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <>
984 List.append(&2, J.Lexeme, reverse_source_task(atomic_value(atom), mode), acc)),
985 lex_atomic_reverse_before_punctuation(atom, punctuation, suffix, acc, action),
986 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items =>
987 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <>
988 List.append(&2, J.Lexeme, items, acc)),
989 reverse_source_task(atomic_value(atom), RenderWhole{}),
990 reverse_source_task(atomic_value(atom), mode),
991 Equal.sym(List<&2, J.Lexeme>, reverse_source_task(atomic_value(atom), mode),
992 reverse_source_task(atomic_value(atom), RenderWhole{}), atomic_task_source(atom, mode)))))
993
994def lex_simple_task_before_punctuation(+simple: SimpleValue,
995 +mode: RenderMode,
996 +punctuation: Char,
997 +suffix: String,
998 +acc: List<&2, J.Lexeme>,
999 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(render_task(simple_value(simple), mode, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(simple), mode), acc)) : List<&2, J.Lexeme>}:
1000 match simple mode:
1001 case SimpleAtom{atom} RenderWhole{}:
1002 lex_atomic_task_before_punctuation(atom, RenderWhole{}, punctuation, suffix, acc, action)
1003 case SimpleAtom{atom} RenderMembers{}:
1004 lex_atomic_task_before_punctuation(atom, RenderMembers{}, punctuation, suffix, acc, action)
1005 case SimpleAtom{atom} RenderAfterSeparator{}:
1006 lex_atomic_task_before_punctuation(atom, RenderAfterSeparator{}, punctuation, suffix, acc, action)
1007 case SimpleEmptyArray{} RenderWhole{}:
1008 lex_empty_array_reverse_before_punctuation(punctuation, suffix, acc, action)
1009 case SimpleEmptyArray{} RenderMembers{}:
1010 lex_close_before_punctuation(']', punctuation, suffix, acc, {==}, action)
1011 case SimpleEmptyArray{} RenderAfterSeparator{}:
1012 lex_close_before_punctuation(']', punctuation, suffix, acc, {==}, action)
1013 case SimpleEmptyObject{} RenderWhole{}:
1014 lex_empty_object_reverse_before_punctuation(punctuation, suffix, acc, action)
1015 case SimpleEmptyObject{} RenderMembers{}:
1016 lex_close_before_punctuation('}', punctuation, suffix, acc, {==}, action)
1017 case SimpleEmptyObject{} RenderAfterSeparator{}:
1018 lex_close_before_punctuation('}', punctuation, suffix, acc, {==}, action)
1019
1020def lex_simple_task_suffix_before_punctuation(+simple: SimpleValue,
1021 +mode: RenderMode,
1022 +punctuation: Char,
1023 +suffix: String,
1024 +acc: List<&2, J.Lexeme>,
1025 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(render_task(simple_value(simple), mode, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(simple), mode), acc)) : List<&2, J.Lexeme>}:
1026 Equal.trans(List<&2, J.Lexeme>,
1027 J.lex_scan(render_task(simple_value(simple), mode, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
1028 J.lex_scan(render_task(simple_value(simple), mode, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
1029 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <>
1030 List.append(&2, J.Lexeme, reverse_source_task(simple_value(simple), mode), acc)),
1031 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, acc),
1032 render_task(simple_value(simple), mode, SCon{punctuation, SNil{}} ++ suffix),
1033 render_task(simple_value(simple), mode, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix),
1034 Equal.sym(String,
1035 render_task(simple_value(simple), mode, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix),
1036 render_task(simple_value(simple), mode, SCon{punctuation, SNil{}} ++ suffix),
1037 render_task_append(simple_value(simple), mode, SNil{}, SCon{punctuation, SNil{}} ++ suffix))),
1038 lex_simple_task_before_punctuation(simple, mode, punctuation, suffix, acc, action))
1039
1040def lex_array_singleton_value_before_punctuation(+head: J.Value,
1041 +punctuation: Char,
1042 +suffix: String,
1043 +acc: List<&2, J.Lexeme>,
1044 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction},
1045 head_lex: {J.lex_scan(J.render(head, False{}, SNil{}) ++ (SCon{']', SCon{punctuation, SNil{}} ++ suffix}), J.Outside{}, SNil{}, J.Punctuation{'['} <> acc) == J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> acc)) : List<&2, J.Lexeme>}) -> {J.lex_scan(J.render(J.Arr{head <> Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> acc)) : List<&2, J.Lexeme>}:
1046 Equal.trans(List<&2, J.Lexeme>,
1047 J.lex_scan(J.render(J.Arr{head <> Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
1048 J.lex_scan("[" ++ (J.render(head, False{}, SNil{}) ++ ("]" ++ (SCon{punctuation, SNil{}} ++ suffix))), J.Outside{}, SNil{}, acc),
1049 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <>
1050 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> acc)),
1051 Equal.trans(List<&2, J.Lexeme>,
1052 J.lex_scan(J.render(J.Arr{head <> Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
1053 J.lex_scan(J.render(J.Arr{head <> Nil{}}, False{}, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
1054 J.lex_scan("[" ++ (J.render(head, False{}, SNil{}) ++ ("]" ++ (SCon{punctuation, SNil{}} ++ suffix))), J.Outside{}, SNil{}, acc),
1055 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, acc),
1056 J.render(J.Arr{head <> Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix),
1057 J.render(J.Arr{head <> Nil{}}, False{}, SCon{punctuation, SNil{}} ++ suffix),
1058 render_append(J.Arr{head <> Nil{}}, False{}, SNil{}, SCon{punctuation, SNil{}} ++ suffix)),
1059 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, acc),
1060 J.render(J.Arr{head <> Nil{}}, False{}, SCon{punctuation, SNil{}} ++ suffix),
1061 "[" ++ (J.render(head, False{}, SNil{}) ++ ("]" ++ (SCon{punctuation, SNil{}} ++ suffix))),
1062 render_array_singleton_suffix(head, SCon{punctuation, SNil{}} ++ suffix))),
1063 Equal.trans(List<&2, J.Lexeme>,
1064 J.lex_scan("[" ++ (J.render(head, False{}, SNil{}) ++ ("]" ++ (SCon{punctuation, SNil{}} ++ suffix))), J.Outside{}, SNil{}, acc),
1065 J.lex_scan(J.render(head, False{}, SNil{}) ++ (SCon{']', SCon{punctuation, SNil{}} ++ suffix}), J.Outside{}, SNil{}, J.Punctuation{'['} <> acc),
1066 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <>
1067 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> acc)),
1068 W.scan_punctuation_char('[', J.render(head, False{}, SNil{}) ++ ("]" ++ (SCon{punctuation, SNil{}} ++ suffix)), SNil{}, acc, {==}),
1069 Equal.trans(List<&2, J.Lexeme>,
1070 J.lex_scan(J.render(head, False{}, SNil{}) ++ (SCon{']', SCon{punctuation, SNil{}} ++ suffix}), J.Outside{}, SNil{}, J.Punctuation{'['} <> acc),
1071 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{']'} <>
1072 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> acc)),
1073 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <>
1074 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> acc)),
1075 head_lex,
1076 W.scan_punctuation_char(punctuation, suffix, SNil{}, J.Punctuation{']'} <>
1077 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> acc), action))))
1078
1079def lex_array_singleton_before_punctuation(+head: SimpleValue,
1080 +punctuation: Char,
1081 +suffix: String,
1082 +acc: List<&2, J.Lexeme>,
1083 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(J.Arr{simple_value(head) <> Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), J.Punctuation{'['} <> acc)) : List<&2, J.Lexeme>}:
1084 lex_array_singleton_value_before_punctuation(simple_value(head), punctuation, suffix, acc, action,
1085 lex_simple_task_before_punctuation(head, RenderWhole{}, ']', SCon{punctuation, SNil{}} ++ suffix,
1086 J.Punctuation{'['} <> acc, {==}))
1087
1088def lex_array_after_separator_single(+head: J.Value,
1089 +punctuation: Char,
1090 +suffix: String,
1091 +acc: List<&2, J.Lexeme>,
1092 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction},
1093 head_lex: {J.lex_scan(render_task(head, RenderWhole{}, "]" ++ (SCon{punctuation, SNil{}} ++ suffix)), J.Outside{}, SNil{}, acc) == J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) : List<&2,
1094 J.Lexeme>}) -> {J.lex_scan(render_after_separator(J.Arr{head <> Nil{}}, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) : List<&2, J.Lexeme>}:
1095 Equal.trans(List<&2, J.Lexeme>,
1096 J.lex_scan(render_after_separator(J.Arr{head <> Nil{}}, SCon{punctuation, SNil{}} ++ suffix),
1097 J.Outside{}, SNil{}, acc),
1098 J.lex_scan(render_task(head, RenderWhole{}, "]" ++ (SCon{punctuation, SNil{}} ++ suffix)),
1099 J.Outside{}, SNil{}, acc),
1100 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <>
1101 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1102 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, acc),
1103 render_after_separator(J.Arr{head <> Nil{}}, SCon{punctuation, SNil{}} ++ suffix),
1104 render_task(head, RenderWhole{}, "]" ++ (SCon{punctuation, SNil{}} ++ suffix)),
1105 render_after_separator_array_single(head, SCon{punctuation, SNil{}} ++ suffix)),
1106 Equal.trans(List<&2, J.Lexeme>,
1107 J.lex_scan(render_task(head, RenderWhole{}, "]" ++ (SCon{punctuation, SNil{}} ++ suffix)),
1108 J.Outside{}, SNil{}, acc),
1109 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{']'} <>
1110 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1111 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <>
1112 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1113 head_lex,
1114 W.scan_punctuation_char(punctuation, suffix, SNil{}, J.Punctuation{']'} <>
1115 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc), action)))
1116
1117def lex_array_after_separator_single_source(+head: J.Value,
1118 +punctuation: Char,
1119 +suffix: String,
1120 +acc: List<&2, J.Lexeme>,
1121 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction},
1122 head_lex: {J.lex_scan(render_task(head, RenderWhole{}, "]" ++ (SCon{punctuation, SNil{}} ++ suffix)), J.Outside{}, SNil{}, acc) == J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) : List<&2,
1123 J.Lexeme>}) -> {J.lex_scan(render_after_separator(J.Arr{head <> Nil{}}, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> Nil{}}, RenderAfterSeparator{}), acc)) : List<&2, J.Lexeme>}:
1124 Equal.trans(List<&2, J.Lexeme>,
1125 J.lex_scan(render_after_separator(J.Arr{head <> Nil{}}, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
1126 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <>
1127 J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1128 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <>
1129 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> Nil{}}, RenderAfterSeparator{}), acc)),
1130 lex_array_after_separator_single(head, punctuation, suffix, acc, action, head_lex),
1131 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.lex_scan(suffix, J.Outside{}, SNil{},
1132 J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, items, acc)),
1133 J.Punctuation{']'} <> reverse_source_task(head, RenderWhole{}),
1134 reverse_source_task(J.Arr{head <> Nil{}}, RenderAfterSeparator{}),
1135 Equal.sym(List<&2, J.Lexeme>, reverse_source_task(J.Arr{head <> Nil{}}, RenderAfterSeparator{}),
1136 J.Punctuation{']'} <> reverse_source_task(head, RenderWhole{}),
1137 reverse_source_array_after_separator(head, Nil{}))))
1138
1139def reverse_array_after_separator_acc_many(+head: J.Value,
1140 +next: J.Value,
1141 +tail: List<&2, J.Value>,
1142 +acc: List<&2, J.Lexeme>) -> {List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc) : List<&2, J.Lexeme>}:
1143 Equal.trans(List<&2, J.Lexeme>,
1144 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}),
1145 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1146 List.append(&2, J.Lexeme,
1147 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}),
1148 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1149 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc),
1150 Equal.sym(List<&2, J.Lexeme>,
1151 List.append(&2, J.Lexeme,
1152 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}),
1153 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1154 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}),
1155 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1156 LP.append_assoc(J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}),
1157 J.Punctuation{','} <> Nil{}, List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc))),
1158 Equal.trans(List<&2, J.Lexeme>,
1159 List.append(&2, J.Lexeme,
1160 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}),
1161 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1162 List.append(&2, J.Lexeme,
1163 reverse_source_task(J.Arr{next <> tail}, RenderMembers{}),
1164 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1165 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc),
1166 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs =>
1167 List.append(&2, J.Lexeme, xs, List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1168 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}),
1169 reverse_source_task(J.Arr{next <> tail}, RenderMembers{}),
1170 Equal.sym(List<&2, J.Lexeme>, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}),
1171 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}),
1172 reverse_source_array_members_after_separator(next, tail))),
1173 Equal.trans(List<&2, J.Lexeme>,
1174 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}),
1175 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1176 List.append(&2, J.Lexeme,
1177 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})), acc),
1178 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc),
1179 Equal.sym(List<&2, J.Lexeme>,
1180 List.append(&2, J.Lexeme,
1181 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})), acc),
1182 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}),
1183 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1184 LP.append_assoc(J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}),
1185 reverse_source_task(head, RenderWhole{}), acc)),
1186 Equal.sym(List<&2, J.Lexeme>,
1187 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc),
1188 List.append(&2, J.Lexeme,
1189 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})), acc),
1190 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => List.append(&2, J.Lexeme, xs, acc),
1191 reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}),
1192 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})),
1193 reverse_source_array_after_separator(head, next <> tail))))))
1194
1195def lex_array_after_separator_many(+head: J.Value,
1196 +next: J.Value,
1197 +tail: List<&2, J.Value>,
1198 +punctuation: Char,
1199 +suffix: String,
1200 +acc: List<&2, J.Lexeme>,
1201 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction},
1202 head_lex: {J.lex_scan(render_task(head, RenderWhole{}, "," ++ render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix)), J.Outside{}, SNil{}, acc) == J.lex_scan(render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) : List<&2, J.Lexeme>},
1203 tail_lex: {J.lex_scan(render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc))) : List<&2, J.Lexeme>}) -> {J.lex_scan(render_after_separator(J.Arr{head <> next <> tail}, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc)) : List<&2, J.Lexeme>}:
1204 Equal.trans(List<&2, J.Lexeme>,
1205 J.lex_scan(render_after_separator(J.Arr{head <> next <> tail}, SCon{punctuation, SNil{}} ++ suffix),
1206 J.Outside{}, SNil{}, acc),
1207 J.lex_scan(render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix),
1208 J.Outside{}, SNil{}, J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1209 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <>
1210 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc)),
1211 Equal.trans(List<&2, J.Lexeme>,
1212 J.lex_scan(render_after_separator(J.Arr{head <> next <> tail}, SCon{punctuation, SNil{}} ++ suffix),
1213 J.Outside{}, SNil{}, acc),
1214 J.lex_scan(render_task(head, RenderWhole{}, "," ++ render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix)),
1215 J.Outside{}, SNil{}, acc),
1216 J.lex_scan(render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix),
1217 J.Outside{}, SNil{}, J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1218 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, acc),
1219 render_after_separator(J.Arr{head <> next <> tail}, SCon{punctuation, SNil{}} ++ suffix),
1220 render_task(head, RenderWhole{}, "," ++ render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix)),
1221 render_after_separator_array_many(head, next, tail, SCon{punctuation, SNil{}} ++ suffix)),
1222 head_lex),
1223 Equal.trans(List<&2, J.Lexeme>,
1224 J.lex_scan(render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix),
1225 J.Outside{}, SNil{}, J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1226 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <>
1227 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}),
1228 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc))),
1229 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <>
1230 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc)),
1231 tail_lex,
1232 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> items),
1233 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}),
1234 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
1235 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc),
1236 reverse_array_after_separator_acc_many(head, next, tail, acc))))
1237
1238def lex_array_after_separator_two_simple(+first: SimpleValue,
1239 +second: SimpleValue,
1240 +mark: JsonPunctuation,
1241 +suffix: String,
1242 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(render_after_separator(J.Arr{simple_value(first) <> simple_value(second) <> Nil{}}, SCon{punctuation_char(mark), SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation_char(mark)} <> List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_value(first) <> simple_value(second) <> Nil{}}, RenderAfterSeparator{}), acc)) : List<&2, J.Lexeme>}:
1243 lex_array_after_separator_many(simple_value(first), simple_value(second), Nil{}, punctuation_char(mark), suffix, acc, punctuation_action(mark, suffix),
1244 lex_simple_task_suffix_before_punctuation(first, RenderWhole{}, ',', render_after_separator(J.Arr{simple_value(second) <> Nil{}}, SCon{punctuation_char(mark), SNil{}} ++ suffix), acc, {==}),
1245 Equal.trans(List<&2, J.Lexeme>,
1246 J.lex_scan(render_after_separator(J.Arr{simple_value(second) <> Nil{}}, SCon{punctuation_char(mark), SNil{}} ++ suffix),
1247 J.Outside{}, SNil{}, J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(first), RenderWhole{}), acc)),
1248 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation_char(mark)} <> J.Punctuation{']'} <>
1249 List.append(&2, J.Lexeme, reverse_source_task(simple_value(second), RenderWhole{}),
1250 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(first), RenderWhole{}), acc))),
1251 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation_char(mark)} <>
1252 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_value(second) <> Nil{}}, RenderAfterSeparator{}),
1253 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(first), RenderWhole{}), acc))),
1254 lex_array_after_separator_single(simple_value(second), punctuation_char(mark), suffix,
1255 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(first), RenderWhole{}), acc), punctuation_action(mark, suffix),
1256 lex_simple_task_suffix_before_punctuation(second, RenderWhole{}, ']', SCon{punctuation_char(mark), SNil{}} ++ suffix,
1257 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(first), RenderWhole{}), acc), {==})),
1258 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items =>
1259 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation_char(mark)} <>
1260 List.append(&2, J.Lexeme, items, J.Punctuation{','} <>
1261 List.append(&2, J.Lexeme, reverse_source_task(simple_value(first), RenderWhole{}), acc))),
1262 J.Punctuation{']'} <> reverse_source_task(simple_value(second), RenderWhole{}),
1263 reverse_source_task(J.Arr{simple_value(second) <> Nil{}}, RenderAfterSeparator{}),
1264 Equal.sym(List<&2, J.Lexeme>, reverse_source_task(J.Arr{simple_value(second) <> Nil{}}, RenderAfterSeparator{}),
1265 J.Punctuation{']'} <> reverse_source_task(simple_value(second), RenderWhole{}),
1266 reverse_source_array_after_separator(simple_value(second), Nil{})))))
1267
1268def simple_values(values: List<&2, SimpleValue>) -> List<&2, J.Value>:
1269 match values:
1270 case Nil{}: Nil{}
1271 case head <> tail: simple_value(head) <> simple_values(tail)
1272
1273def lex_simple_array_after_separator_end(+values: List<&2, SimpleValue>,
1274 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(render_after_separator(J.Arr{simple_values(values)}, SNil{}), J.Outside{}, SNil{}, acc) == J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), acc)) : List<&2, J.Lexeme>}:
1275 match values:
1276 case Nil{}:
1277 W.scan_punctuation_char(']', SNil{}, SNil{}, acc, {==})
1278 case head <> Nil{}:
1279 Equal.trans(List<&2, J.Lexeme>,
1280 J.lex_scan(render_after_separator(J.Arr{simple_value(head) <> Nil{}}, SNil{}), J.Outside{}, SNil{}, acc),
1281 J.lex_scan(render_task(simple_value(head), RenderWhole{}, "]"), J.Outside{}, SNil{}, acc),
1282 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme,
1283 reverse_source_task(J.Arr{simple_value(head) <> Nil{}}, RenderAfterSeparator{}), acc)),
1284 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, acc),
1285 render_after_separator(J.Arr{simple_value(head) <> Nil{}}, SNil{}),
1286 render_task(simple_value(head), RenderWhole{}, "]"),
1287 render_after_separator_array_single(simple_value(head), SNil{})),
1288 Equal.trans(List<&2, J.Lexeme>,
1289 J.lex_scan(render_task(simple_value(head), RenderWhole{}, "]"), J.Outside{}, SNil{}, acc),
1290 J.lex_scan(SNil{}, J.Outside{}, SNil{}, J.Punctuation{']'} <>
1291 List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc)),
1292 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme,
1293 reverse_source_task(J.Arr{simple_value(head) <> Nil{}}, RenderAfterSeparator{}), acc)),
1294 lex_simple_task_suffix_before_punctuation(head, RenderWhole{}, ']', SNil{}, acc, {==}),
1295 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items =>
1296 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme, items, acc)),
1297 J.Punctuation{']'} <> reverse_source_task(simple_value(head), RenderWhole{}),
1298 reverse_source_task(J.Arr{simple_value(head) <> Nil{}}, RenderAfterSeparator{}),
1299 Equal.sym(List<&2, J.Lexeme>, reverse_source_task(J.Arr{simple_value(head) <> Nil{}}, RenderAfterSeparator{}),
1300 J.Punctuation{']'} <> reverse_source_task(simple_value(head), RenderWhole{}),
1301 reverse_source_array_after_separator(simple_value(head), Nil{})))))
1302 case head <> next <> tail:
1303 Equal.trans(List<&2, J.Lexeme>,
1304 J.lex_scan(render_after_separator(J.Arr{simple_value(head) <> simple_value(next) <> simple_values(tail)}, SNil{}), J.Outside{}, SNil{}, acc),
1305 J.lex_scan(render_after_separator(J.Arr{simple_value(next) <> simple_values(tail)}, SNil{}), J.Outside{}, SNil{},
1306 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc)),
1307 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme,
1308 reverse_source_task(J.Arr{simple_value(head) <> simple_value(next) <> simple_values(tail)}, RenderAfterSeparator{}), acc)),
1309 Equal.trans(List<&2, J.Lexeme>,
1310 J.lex_scan(render_after_separator(J.Arr{simple_value(head) <> simple_value(next) <> simple_values(tail)}, SNil{}), J.Outside{}, SNil{}, acc),
1311 J.lex_scan(render_task(simple_value(head), RenderWhole{}, "," ++ render_after_separator(J.Arr{simple_value(next) <> simple_values(tail)}, SNil{})),
1312 J.Outside{}, SNil{}, acc),
1313 J.lex_scan(render_after_separator(J.Arr{simple_value(next) <> simple_values(tail)}, SNil{}), J.Outside{}, SNil{},
1314 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc)),
1315 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, acc),
1316 render_after_separator(J.Arr{simple_value(head) <> simple_value(next) <> simple_values(tail)}, SNil{}),
1317 render_task(simple_value(head), RenderWhole{}, "," ++ render_after_separator(J.Arr{simple_value(next) <> simple_values(tail)}, SNil{})),
1318 render_after_separator_array_many(simple_value(head), simple_value(next), simple_values(tail), SNil{})),
1319 lex_simple_task_suffix_before_punctuation(head, RenderWhole{}, ',',
1320 render_after_separator(J.Arr{simple_value(next) <> simple_values(tail)}, SNil{}), acc, {==})),
1321 Equal.trans(List<&2, J.Lexeme>,
1322 J.lex_scan(render_after_separator(J.Arr{simple_value(next) <> simple_values(tail)}, SNil{}), J.Outside{}, SNil{},
1323 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc)),
1324 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme,
1325 reverse_source_task(J.Arr{simple_value(next) <> simple_values(tail)}, RenderAfterSeparator{}),
1326 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc))),
1327 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme,
1328 reverse_source_task(J.Arr{simple_value(head) <> simple_value(next) <> simple_values(tail)}, RenderAfterSeparator{}), acc)),
1329 lex_simple_array_after_separator_end(next <> tail,
1330 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc)),
1331 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.lex_scan(SNil{}, J.Outside{}, SNil{}, items),
1332 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_value(next) <> simple_values(tail)}, RenderAfterSeparator{}),
1333 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc)),
1334 List.append(&2, J.Lexeme,
1335 reverse_source_task(J.Arr{simple_value(head) <> simple_value(next) <> simple_values(tail)}, RenderAfterSeparator{}), acc),
1336 reverse_array_after_separator_acc_many(simple_value(head), simple_value(next), simple_values(tail), acc))))
1337
1338def reverse_source_array_after_separator_whole_list(+values: List<&2, J.Value>) -> {reverse_source_task(J.Arr{values}, RenderWhole{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{values}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}) : List<&2, J.Lexeme>}:
1339 match values:
1340 case Nil{}: {==}
1341 case head <> tail: reverse_source_array_after_separator_whole(head, tail)
1342
1343def render_array_whole_after_separator(+values: List<&2, J.Value>,
1344 +suffix: String) -> {J.render(J.Arr{values}, False{}, suffix) == "[" ++ render_after_separator(J.Arr{values}, suffix) : String}:
1345 match values:
1346 case Nil{}: {==}
1347 case head <> tail: {==}
1348
1349def lex_simple_array_whole(+values: List<&2, SimpleValue>) -> {J.lex_scan(J.render(J.Arr{simple_values(values)}, False{}, SNil{}), J.Outside{}, SNil{}, Nil{}) == J.source(J.Arr{simple_values(values)}, False{}, Nil{}) : List<&2, J.Lexeme>}:
1350 Equal.trans(List<&2, J.Lexeme>,
1351 J.lex_scan(J.render(J.Arr{simple_values(values)}, False{}, SNil{}), J.Outside{}, SNil{}, Nil{}),
1352 J.lex_scan(render_after_separator(J.Arr{simple_values(values)}, SNil{}), J.Outside{}, SNil{}, J.Punctuation{'['} <> Nil{}),
1353 J.source(J.Arr{simple_values(values)}, False{}, Nil{}),
1354 Equal.trans(List<&2, J.Lexeme>,
1355 J.lex_scan(J.render(J.Arr{simple_values(values)}, False{}, SNil{}), J.Outside{}, SNil{}, Nil{}),
1356 J.lex_scan("[" ++ render_after_separator(J.Arr{simple_values(values)}, SNil{}), J.Outside{}, SNil{}, Nil{}),
1357 J.lex_scan(render_after_separator(J.Arr{simple_values(values)}, SNil{}), J.Outside{}, SNil{}, J.Punctuation{'['} <> Nil{}),
1358 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, Nil{}),
1359 J.render(J.Arr{simple_values(values)}, False{}, SNil{}),
1360 "[" ++ render_after_separator(J.Arr{simple_values(values)}, SNil{}),
1361 render_array_whole_after_separator(simple_values(values), SNil{})),
1362 W.scan_punctuation_char('[', render_after_separator(J.Arr{simple_values(values)}, SNil{}), SNil{}, Nil{}, {==})),
1363 Equal.trans(List<&2, J.Lexeme>,
1364 J.lex_scan(render_after_separator(J.Arr{simple_values(values)}, SNil{}), J.Outside{}, SNil{}, J.Punctuation{'['} <> Nil{}),
1365 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme,
1366 reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{})),
1367 J.source(J.Arr{simple_values(values)}, False{}, Nil{}),
1368 lex_simple_array_after_separator_end(values, J.Punctuation{'['} <> Nil{}),
1369 Equal.trans(List<&2, J.Lexeme>,
1370 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme,
1371 reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{})),
1372 J.lex_scan(SNil{}, J.Outside{}, SNil{}, reverse_source_task(J.Arr{simple_values(values)}, RenderWhole{})),
1373 J.source(J.Arr{simple_values(values)}, False{}, Nil{}),
1374 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.lex_scan(SNil{}, J.Outside{}, SNil{}, items),
1375 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}),
1376 reverse_source_task(J.Arr{simple_values(values)}, RenderWhole{}),
1377 Equal.sym(List<&2, J.Lexeme>, reverse_source_task(J.Arr{simple_values(values)}, RenderWhole{}),
1378 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}),
1379 reverse_source_array_after_separator_whole_list(simple_values(values)))),
1380 LP.reverse_twice(J.Lexeme, J.source(J.Arr{simple_values(values)}, False{}, Nil{})))))
1381
1382def lex_simple_array_after_separator(+values: List<&2, SimpleValue>,
1383 +mark: JsonPunctuation,
1384 +suffix: String,
1385 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(render_after_separator(J.Arr{simple_values(values)}, SCon{punctuation_char(mark), SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation_char(mark)} <> List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), acc)) : List<&2, J.Lexeme>}:
1386 match values:
1387 case Nil{}:
1388 lex_close_before_punctuation(']', punctuation_char(mark), suffix, acc, {==}, punctuation_action(mark, suffix))
1389 case head <> Nil{}:
1390 lex_array_after_separator_single_source(simple_value(head), punctuation_char(mark), suffix, acc,
1391 punctuation_action(mark, suffix),
1392 lex_simple_task_suffix_before_punctuation(head, RenderWhole{}, ']', SCon{punctuation_char(mark), SNil{}} ++ suffix, acc, {==}))
1393 case head <> next <> tail:
1394 lex_array_after_separator_many(simple_value(head), simple_value(next), simple_values(tail),
1395 punctuation_char(mark), suffix, acc, punctuation_action(mark, suffix),
1396 lex_simple_task_suffix_before_punctuation(head, RenderWhole{}, ',',
1397 render_after_separator(J.Arr{simple_value(next) <> simple_values(tail)}, SCon{punctuation_char(mark), SNil{}} ++ suffix),
1398 acc, {==}),
1399 lex_simple_array_after_separator(next <> tail, mark, suffix,
1400 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc)))
1401
1402def source_token_string(+text: String,
1403 +suffix: List<&2, J.Lexeme>,
1404 -tail: List<J.Token>) -> {token_source(J.source_text("\"" ++ J.escape_string(text) ++ "\"", suffix), tail) == token_string(text) <> token_source(suffix, tail) : List<J.Token>}:
1405 Equal.cong(Result<&1, &1, J.Error, J.Value>, List<J.Token>, result => J.Atom{result} <> token_source(suffix, tail),
1406 J.decode_payload("\"" ++ J.escape_string(text) ++ "\""), Done{J.Str{text}}, S.string_payload(text))
1407
1408def source_object_key_prefix(+delimiter: Char,
1409 +key: String,
1410 +suffix: List<&2, J.Lexeme>,
1411 -tail: List<J.Token>) -> {token_source(J.Punctuation{delimiter} <> J.source_text("\"" ++ J.escape_string(key) ++ "\"", suffix), tail) == J.Delimiter{delimiter} <> token_string(key) <> token_source(suffix, tail) : List<J.Token>}:
1412 Equal.trans(List<J.Token>,
1413 token_source(J.Punctuation{delimiter} <> J.source_text("\"" ++ J.escape_string(key) ++ "\"", suffix), tail),
1414 J.Delimiter{delimiter} <> token_source(J.source_text("\"" ++ J.escape_string(key) ++ "\"", suffix), tail),
1415 J.Delimiter{delimiter} <> token_string(key) <> token_source(suffix, tail),
1416 {==},
1417 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{delimiter} <> xs,
1418 token_source(J.source_text("\"" ++ J.escape_string(key) ++ "\"", suffix), tail),
1419 token_string(key) <> token_source(suffix, tail), source_token_string(key, suffix, tail)))
1420
1421def to_bool(mode: A.Mode) -> Bool:
1422 match mode:
1423 case A.Whole{}: False{}
1424 case A.Members{}: True{}
1425
1426def canonical(value: J.Value, mode: A.Mode, tail: List<J.Token>) -> List<J.Token>:
1427 A.tokens(value, mode, tail)
1428
1429def canonical_tokens(+value: J.Value,
1430 +mode: A.Mode,
1431 -tail: List<J.Token>) -> {canonical(value, mode, tail) == A.tokens(value, mode, tail) : List<J.Token>}:
1432 {==}
1433
1434def source_tokens(+value: J.Value,
1435 +mode: A.Mode,
1436 +suffix: List<&2, J.Lexeme>,
1437 -tail: List<J.Token>) -> {token_source(J.source(value, to_bool(mode), suffix), tail) == canonical(value, mode, token_source(suffix, tail)) : List<J.Token>}:
1438 match value:
1439 case J.Null{}: {==}
1440 case J.Bool{truth}:
1441 match truth:
1442 case True{}: {==}
1443 case False{}: {==}
1444 case J.Number{lexeme, certificate}: {==}
1445 case J.Str{text}: {==}
1446 case J.Arr{values}:
1447 match values:
1448 case Nil{}:
1449 match mode:
1450 case A.Whole{}: {==}
1451 case A.Members{}: {==}
1452 case head <> rest:
1453 match mode:
1454 case A.Whole{}:
1455 Equal.trans(List<J.Token>, token_source(J.source(J.Arr{head <> rest}, False{}, suffix), tail),
1456 J.Delimiter{'['} <> canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)),
1457 canonical(J.Arr{head <> rest}, A.Whole{}, token_source(suffix, tail)),
1458 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{'['} <> xs,
1459 token_source(J.source(head, False{}, J.source(J.Arr{rest}, True{}, suffix)), tail),
1460 canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)),
1461 source_tokens(head, A.Whole{}, J.source(J.Arr{rest}, True{}, suffix), tail)),
1462 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{'['} <> canonical(head, A.Whole{}, xs),
1463 token_source(J.source(J.Arr{rest}, True{}, suffix), tail), canonical(J.Arr{rest}, A.Members{}, token_source(suffix, tail)),
1464 source_tokens(J.Arr{rest}, A.Members{}, suffix, tail)))
1465 case A.Members{}:
1466 Equal.trans(List<J.Token>, token_source(J.source(J.Arr{head <> rest}, True{}, suffix), tail),
1467 J.Delimiter{','} <> canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)),
1468 canonical(J.Arr{head <> rest}, A.Members{}, token_source(suffix, tail)),
1469 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{','} <> xs,
1470 token_source(J.source(head, False{}, J.source(J.Arr{rest}, True{}, suffix)), tail),
1471 canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)),
1472 source_tokens(head, A.Whole{}, J.source(J.Arr{rest}, True{}, suffix), tail)),
1473 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{','} <> canonical(head, A.Whole{}, xs),
1474 token_source(J.source(J.Arr{rest}, True{}, suffix), tail), canonical(J.Arr{rest}, A.Members{}, token_source(suffix, tail)),
1475 source_tokens(J.Arr{rest}, A.Members{}, suffix, tail)))
1476 case J.Obj{fields}:
1477 match fields:
1478 case Nil{}:
1479 match mode:
1480 case A.Whole{}: {==}
1481 case A.Members{}: {==}
1482 case (key, field_value) <> rest:
1483 match mode:
1484 case A.Whole{}:
1485 Equal.trans(List<J.Token>, token_source(J.source(J.Obj{(key, field_value) <> rest}, False{}, suffix), tail),
1486 J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1487 canonical(J.Obj{(key, field_value) <> rest}, A.Whole{}, token_source(suffix, tail)),
1488 source_object_key_prefix('{', key, J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1489 Equal.trans(List<J.Token>,
1490 J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1491 J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)),
1492 canonical(J.Obj{(key, field_value) <> rest}, A.Whole{}, token_source(suffix, tail)),
1493 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> xs,
1494 token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1495 canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)),
1496 source_tokens(field_value, A.Whole{}, J.source(J.Obj{rest}, True{}, suffix), tail)),
1497 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, xs),
1498 token_source(J.source(J.Obj{rest}, True{}, suffix), tail), canonical(J.Obj{rest}, A.Members{}, token_source(suffix, tail)),
1499 source_tokens(J.Obj{rest}, A.Members{}, suffix, tail))))
1500 case A.Members{}:
1501 Equal.trans(List<J.Token>, token_source(J.source(J.Obj{(key, field_value) <> rest}, True{}, suffix), tail),
1502 J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1503 canonical(J.Obj{(key, field_value) <> rest}, A.Members{}, token_source(suffix, tail)),
1504 source_object_key_prefix(',', key, J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1505 Equal.trans(List<J.Token>,
1506 J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1507 J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)),
1508 canonical(J.Obj{(key, field_value) <> rest}, A.Members{}, token_source(suffix, tail)),
1509 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> xs,
1510 token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1511 canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)),
1512 source_tokens(field_value, A.Whole{}, J.source(J.Obj{rest}, True{}, suffix), tail)),
1513 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, xs),
1514 token_source(J.source(J.Obj{rest}, True{}, suffix), tail), canonical(J.Obj{rest}, A.Members{}, token_source(suffix, tail)),
1515 source_tokens(J.Obj{rest}, A.Members{}, suffix, tail))))