proof/JSON_LexWhitespaceProof.bend
qasim-bend-kit@0.1.0.2 · 597 lines · 33 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_StringProof.bend as S
4
5def after_mode(action: J.LexAction, mode: J.LexMode) -> J.LexMode:
6 match action:
7 case J.LexBackslash{}: J.Escaped{}
8 case J.LexEscapedChar{}: J.Quoted{}
9 case J.LexStringEnd{}: J.Outside{}
10 case J.LexStringChar{}: J.Quoted{}
11 case J.LexQuote{}: J.Quoted{}
12 case J.LexWhitespace{}: J.Outside{}
13 case J.LexPunctuation{_}: J.Outside{}
14 case J.LexRaw{}: J.Outside{}
15 case J.LexStop{}: mode
16
17def after_reversed(action: J.LexAction, head: Char, reversed: String) -> String:
18 match action:
19 case J.LexBackslash{}: SCon{'\\', reversed}
20 case J.LexEscapedChar{}: SCon{head, reversed}
21 case J.LexStringEnd{}: SNil{}
22 case J.LexStringChar{}: SCon{head, reversed}
23 case J.LexQuote{}: SCon{'"', SNil{}}
24 case J.LexWhitespace{}: SNil{}
25 case J.LexPunctuation{_}: SNil{}
26 case J.LexRaw{}: SCon{head, reversed}
27 case J.LexStop{}: SCon{head, reversed}
28
29def after_acc(action: J.LexAction,
30 head: Char,
31 reversed: String,
32 acc: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>:
33 match action:
34 case J.LexBackslash{}: acc
35 case J.LexEscapedChar{}: acc
36 case J.LexStringEnd{}: J.Payload{String.reverse(SCon{'"', reversed})} <> acc
37 case J.LexStringChar{}: acc
38 case J.LexQuote{}: J.flush_lexeme(reversed, acc)
39 case J.LexWhitespace{}: J.flush_lexeme(reversed, acc)
40 case J.LexPunctuation{character}: J.Punctuation{character} <> J.flush_lexeme(reversed, acc)
41 case J.LexRaw{}: acc
42 case J.LexStop{}: acc
43
44def lexemes_step(+head: Char,
45 +tail: String,
46 +mode: J.LexMode,
47 +reversed: String,
48 +acc: List<&2, J.Lexeme>,
49 action: J.LexAction) -> {J.lexemes(SCon{head, tail}, mode, reversed, acc, action) == J.lex_scan(tail, after_mode(action, mode), after_reversed(action, head, reversed), after_acc(action, head, reversed, acc)) : List<&2, J.Lexeme>}:
50 match action:
51 case J.LexStop{}: {==}
52 case J.LexEscapedChar{}: {==}
53 case J.LexBackslash{}: {==}
54 case J.LexStringEnd{}: {==}
55 case J.LexStringChar{}: {==}
56 case J.LexQuote{}: {==}
57 case J.LexWhitespace{}: {==}
58 case J.LexPunctuation{character}: {==}
59 case J.LexRaw{}: {==}
60
61def lex_scan_step(+head: Char,
62 +tail: String,
63 +mode: J.LexMode,
64 +reversed: String,
65 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(SCon{head, tail}, mode, reversed, acc) == J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)) : List<&2, J.Lexeme>}:
66 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail}, mode, reversed, acc),
67 J.lexemes(SCon{head, tail}, mode, reversed, acc, J.lex_seed_action(SCon{head, tail}, mode)),
68 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
69 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
70 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
71 {==}, lexemes_step(head, tail, mode, reversed, acc, J.lex_seed_action(SCon{head, tail}, mode)))
72
73def prefix_mode(text: String, +mode: J.LexMode) -> J.LexMode:
74 match text:
75 case SNil{}: mode
76 case SCon{+head, +tail}:
77 prefix_mode(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode))
78
79def prefix_reversed(text: String, +mode: J.LexMode, +reversed: String) -> String:
80 match text:
81 case SNil{}: reversed
82 case SCon{+head, +tail}:
83 prefix_reversed(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
84 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed))
85
86def prefix_acc(text: String,
87 +mode: J.LexMode,
88 +reversed: String,
89 +acc: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>:
90 match text:
91 case SNil{}: acc
92 case SCon{+head, +tail}:
93 prefix_acc(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
94 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
95 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc))
96
97def prefix_mode_append(+text: String,
98 +suffix: String,
99 +mode: J.LexMode) -> {prefix_mode(text ++ suffix, mode) == prefix_mode(suffix, prefix_mode(text, mode)) : J.LexMode}:
100 match text:
101 case SNil{}: {==}
102 case SCon{head, tail}:
103 prefix_mode_append(tail, suffix, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode))
104
105def prefix_reversed_append(+text: String,
106 +suffix: String,
107 +mode: J.LexMode,
108 +reversed: String) -> {prefix_reversed(text ++ suffix, mode, reversed) == prefix_reversed(suffix, prefix_mode(text, mode), prefix_reversed(text, mode, reversed)) : String}:
109 match text:
110 case SNil{}: {==}
111 case SCon{head, tail}:
112 prefix_reversed_append(tail, suffix, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
113 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed))
114
115def prefix_acc_append(+text: String,
116 +suffix: String,
117 +mode: J.LexMode,
118 +reversed: String,
119 +acc: List<&2, J.Lexeme>) -> {prefix_acc(text ++ suffix, mode, reversed, acc) == prefix_acc(suffix, prefix_mode(text, mode), prefix_reversed(text, mode, reversed), prefix_acc(text, mode, reversed, acc)) : List<&2, J.Lexeme>}:
120 match text:
121 case SNil{}: {==}
122 case SCon{head, tail}:
123 prefix_acc_append(tail, suffix, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
124 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
125 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc))
126
127def lex_scan_append(+text: String,
128 +suffix: String,
129 +mode: J.LexMode,
130 +reversed: String,
131 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(text ++ suffix, mode, reversed, acc) == J.lex_scan(suffix, prefix_mode(text, mode), prefix_reversed(text, mode, reversed), prefix_acc(text, mode, reversed, acc)) : List<&2, J.Lexeme>}:
132 match text:
133 case SNil{}: {==}
134 case SCon{head, tail}:
135 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ suffix, mode, reversed, acc),
136 J.lex_scan(tail ++ suffix, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
137 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
138 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
139 J.lex_scan(suffix, prefix_mode(SCon{head, tail}, mode), prefix_reversed(SCon{head, tail}, mode, reversed),
140 prefix_acc(SCon{head, tail}, mode, reversed, acc)),
141 lex_scan_step(head, tail ++ suffix, mode, reversed, acc),
142 lex_scan_append(tail, suffix, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
143 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
144 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)))
145
146def lex_scan_context(+text: String,
147 +mode1: J.LexMode,
148 +reversed1: String,
149 +acc1: List<&2, J.Lexeme>,
150 +mode2: J.LexMode,
151 +reversed2: String,
152 +acc2: List<&2, J.Lexeme>,
153 mode_eq: {mode1 == mode2 : J.LexMode},
154 reversed_eq: {reversed1 == reversed2 : String},
155 acc_eq: {acc1 == acc2 : List<&2, J.Lexeme>}) -> {J.lex_scan(text, mode1, reversed1, acc1) == J.lex_scan(text, mode2, reversed2, acc2) : List<&2, J.Lexeme>}:
156 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, mode1, reversed1, acc1),
157 J.lex_scan(text, mode2, reversed1, acc1), J.lex_scan(text, mode2, reversed2, acc2),
158 Equal.cong(J.LexMode, List<&2, J.Lexeme>, mode => J.lex_scan(text, mode, reversed1, acc1), mode1, mode2, mode_eq),
159 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, mode2, reversed1, acc1),
160 J.lex_scan(text, mode2, reversed2, acc1), J.lex_scan(text, mode2, reversed2, acc2),
161 Equal.cong(String, List<&2, J.Lexeme>, reversed => J.lex_scan(text, mode2, reversed, acc1),
162 reversed1, reversed2, reversed_eq),
163 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, acc => J.lex_scan(text, mode2, reversed2, acc),
164 acc1, acc2, acc_eq)))
165
166def scan_punctuation_char(+character: Char,
167 +tail: String,
168 +reversed: String,
169 +acc: List<&2, J.Lexeme>,
170 action: {J.lex_seed_action(SCon{character, tail}, J.Outside{}) == J.LexPunctuation{character} : J.LexAction}) -> {J.lex_scan(SCon{character, tail}, J.Outside{}, reversed, acc) == J.lex_scan(tail, J.Outside{}, SNil{}, J.Punctuation{character} <> J.flush_lexeme(reversed, acc)) : List<&2, J.Lexeme>}:
171 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{character, tail}, J.Outside{}, reversed, acc),
172 J.lex_scan(tail, after_mode(J.LexPunctuation{character}, J.Outside{}),
173 after_reversed(J.LexPunctuation{character}, character, reversed),
174 after_acc(J.LexPunctuation{character}, character, reversed, acc)),
175 J.lex_scan(tail, J.Outside{}, SNil{}, J.Punctuation{character} <> J.flush_lexeme(reversed, acc)),
176 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{character, tail}, J.Outside{}, reversed, acc),
177 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{character, tail}, J.Outside{}), J.Outside{}),
178 after_reversed(J.lex_seed_action(SCon{character, tail}, J.Outside{}), character, reversed),
179 after_acc(J.lex_seed_action(SCon{character, tail}, J.Outside{}), character, reversed, acc)),
180 J.lex_scan(tail, after_mode(J.LexPunctuation{character}, J.Outside{}),
181 after_reversed(J.LexPunctuation{character}, character, reversed),
182 after_acc(J.LexPunctuation{character}, character, reversed, acc)),
183 lex_scan_step(character, tail, J.Outside{}, reversed, acc),
184 Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lex_scan(tail, after_mode(action, J.Outside{}),
185 after_reversed(action, character, reversed), after_acc(action, character, reversed, acc)),
186 J.lex_seed_action(SCon{character, tail}, J.Outside{}), J.LexPunctuation{character}, action)),
187 {==})
188
189def raw_string_seed(+character: Char,
190 +tail: String,
191 classifier: {J.Raw{} == J.escape_class(character) : J.EscapeClass}) -> {J.lex_seed_action(SCon{character, tail}, J.Quoted{}) == J.LexStringChar{} : J.LexAction}:
192 Equal.trans(J.LexAction, J.lex_seed_action(SCon{character, tail}, J.Quoted{}),
193 J.quote_lex_action(J.quote_action_from_class(J.escape_class(character))), J.LexStringChar{},
194 {==},
195 Equal.cong(J.EscapeClass, J.LexAction, class => J.quote_lex_action(J.quote_action_from_class(class)),
196 J.escape_class(character), J.Raw{}, Equal.sym(J.EscapeClass, J.Raw{}, J.escape_class(character), classifier)))
197
198def scan_raw_string_char(+character: Char,
199 +tail: String,
200 +reversed: String,
201 +acc: List<&2, J.Lexeme>,
202 classifier: {J.Raw{} == J.escape_class(character) : J.EscapeClass}) -> {J.lex_scan(SCon{character, tail}, J.Quoted{}, reversed, acc) == J.lex_scan(tail, J.Quoted{}, SCon{character, reversed}, acc) : List<&2, J.Lexeme>}:
203 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{character, tail}, J.Quoted{}, reversed, acc),
204 J.lex_scan(tail, after_mode(J.LexStringChar{}, J.Quoted{}), after_reversed(J.LexStringChar{}, character, reversed), after_acc(J.LexStringChar{}, character, reversed, acc)),
205 J.lex_scan(tail, J.Quoted{}, SCon{character, reversed}, acc),
206 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{character, tail}, J.Quoted{}, reversed, acc),
207 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{character, tail}, J.Quoted{}), J.Quoted{}),
208 after_reversed(J.lex_seed_action(SCon{character, tail}, J.Quoted{}), character, reversed),
209 after_acc(J.lex_seed_action(SCon{character, tail}, J.Quoted{}), character, reversed, acc)),
210 J.lex_scan(tail, after_mode(J.LexStringChar{}, J.Quoted{}), after_reversed(J.LexStringChar{}, character, reversed), after_acc(J.LexStringChar{}, character, reversed, acc)),
211 lex_scan_step(character, tail, J.Quoted{}, reversed, acc),
212 Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lex_scan(tail, after_mode(action, J.Quoted{}), after_reversed(action, character, reversed), after_acc(action, character, reversed, acc)),
213 J.lex_seed_action(SCon{character, tail}, J.Quoted{}), J.LexStringChar{}, raw_string_seed(character, tail, classifier))),
214 {==})
215
216def scan_escape_char(+character: Char,
217 +tail: String,
218 +reversed: String,
219 +acc: List<&2, J.Lexeme>,
220 +class: J.EscapeClass,
221 classifier: {class == J.escape_class(character) : J.EscapeClass}) -> {J.lex_scan(J.escape_char_from_class(character, class) ++ tail, J.Quoted{}, reversed, acc) == J.lex_scan(tail, J.Quoted{}, String.reverse(J.escape_char_from_class(character, class)) ++ reversed, acc) : List<&2, J.Lexeme>}:
222 match class:
223 case J.Raw{}:
224 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(J.escape_char_from_class(character, J.Raw{}) ++ tail, J.Quoted{}, reversed, acc),
225 J.lex_scan(SCon{character, tail}, J.Quoted{}, reversed, acc),
226 J.lex_scan(tail, J.Quoted{}, SCon{character, reversed}, acc),
227 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Quoted{}, reversed, acc),
228 J.escape_char_from_class(character, J.Raw{}) ++ tail, SCon{character, tail}, {==}),
229 scan_raw_string_char(character, tail, reversed, acc, classifier))
230 case J.Backslash{}: {==}
231 case J.Quote{}: {==}
232 case J.Control0{}: {==}
233 case J.Control1{}: {==}
234 case J.Control2{}: {==}
235 case J.Control3{}: {==}
236 case J.Control4{}: {==}
237 case J.Control5{}: {==}
238 case J.Control6{}: {==}
239 case J.Control7{}: {==}
240 case J.Control8{}: {==}
241 case J.Control9{}: {==}
242 case J.Control10{}: {==}
243 case J.Control11{}: {==}
244 case J.Control12{}: {==}
245 case J.Control13{}: {==}
246 case J.Control14{}: {==}
247 case J.Control15{}: {==}
248 case J.Control16{}: {==}
249 case J.Control17{}: {==}
250 case J.Control18{}: {==}
251 case J.Control19{}: {==}
252 case J.Control20{}: {==}
253 case J.Control21{}: {==}
254 case J.Control22{}: {==}
255 case J.Control23{}: {==}
256 case J.Control24{}: {==}
257 case J.Control25{}: {==}
258 case J.Control26{}: {==}
259 case J.Control27{}: {==}
260 case J.Control28{}: {==}
261 case J.Control29{}: {==}
262 case J.Control30{}: {==}
263 case J.Control31{}: {==}
264
265def escape_reverse(text: String, reversed: String) -> String:
266 match text:
267 case SNil{}: reversed
268 case SCon{head, tail}:
269 escape_reverse(tail, String.reverse(J.escape_char(head)) ++ reversed)
270
271def escape_reverse_shape(+text: String,
272 +reversed: String) -> {String.reverse(escape_reverse(text, reversed)) == String.reverse(reversed) ++ J.escape_string(text) : String}:
273 match text:
274 case SNil{}: Equal.sym(String, String.reverse(reversed) ++ J.escape_string(SNil{}), String.reverse(reversed), S.append_nil(String.reverse(reversed)))
275 case SCon{head, tail}:
276 Equal.trans(String,
277 String.reverse(escape_reverse(tail, String.reverse(J.escape_char(head)) ++ reversed)),
278 String.reverse(String.reverse(J.escape_char(head)) ++ reversed) ++ J.escape_string(tail),
279 String.reverse(reversed) ++ J.escape_string(SCon{head, tail}),
280 escape_reverse_shape(tail, String.reverse(J.escape_char(head)) ++ reversed),
281 Equal.trans(String,
282 String.reverse(String.reverse(J.escape_char(head)) ++ reversed) ++ J.escape_string(tail),
283 (String.reverse(reversed) ++ String.reverse(String.reverse(J.escape_char(head)))) ++ J.escape_string(tail),
284 String.reverse(reversed) ++ (J.escape_char(head) ++ J.escape_string(tail)),
285 Equal.cong(String, String, value => value ++ J.escape_string(tail),
286 String.reverse(String.reverse(J.escape_char(head)) ++ reversed),
287 String.reverse(reversed) ++ String.reverse(String.reverse(J.escape_char(head))),
288 S.reverse_append(String.reverse(J.escape_char(head)), reversed)),
289 Equal.trans(String,
290 (String.reverse(reversed) ++ String.reverse(String.reverse(J.escape_char(head)))) ++ J.escape_string(tail),
291 String.reverse(reversed) ++ (String.reverse(String.reverse(J.escape_char(head))) ++ J.escape_string(tail)),
292 String.reverse(reversed) ++ (J.escape_char(head) ++ J.escape_string(tail)),
293 S.append_assoc(String.reverse(reversed), String.reverse(String.reverse(J.escape_char(head))), J.escape_string(tail)),
294 Equal.cong(String, String, value => String.reverse(reversed) ++ (value ++ J.escape_string(tail)),
295 String.reverse(String.reverse(J.escape_char(head))), J.escape_char(head), S.reverse_twice(J.escape_char(head))))))
296
297def scan_escape_string(+text: String,
298 +suffix: String,
299 +reversed: String,
300 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(J.escape_string(text) ++ suffix, J.Quoted{}, reversed, acc) == J.lex_scan(suffix, J.Quoted{}, escape_reverse(text, reversed), acc) : List<&2, J.Lexeme>}:
301 match text:
302 case SNil{}: {==}
303 case SCon{+head, +tail}:
304 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(J.escape_string(text) ++ suffix, J.Quoted{}, reversed, acc),
305 J.lex_scan(J.escape_char(head) ++ (J.escape_string(tail) ++ suffix), J.Quoted{}, reversed, acc),
306 J.lex_scan(suffix, J.Quoted{}, escape_reverse(text, reversed), acc),
307 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source, J.Quoted{}, reversed, acc),
308 J.escape_string(text) ++ suffix, J.escape_char(head) ++ (J.escape_string(tail) ++ suffix),
309 S.append_assoc(J.escape_char(head), J.escape_string(tail), suffix)),
310 Equal.trans(List<&2, J.Lexeme>,
311 J.lex_scan(J.escape_char(head) ++ (J.escape_string(tail) ++ suffix), J.Quoted{}, reversed, acc),
312 J.lex_scan(J.escape_string(tail) ++ suffix, J.Quoted{}, String.reverse(J.escape_char(head)) ++ reversed, acc),
313 J.lex_scan(suffix, J.Quoted{}, escape_reverse(text, reversed), acc),
314 scan_escape_char(head, J.escape_string(tail) ++ suffix, reversed, acc, J.escape_class(head), {==}),
315 scan_escape_string(tail, suffix, String.reverse(J.escape_char(head)) ++ reversed, acc)))
316
317def quoted_buffer_payload(+text: String) -> {String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})}) == SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}} : String}:
318 Equal.trans(String,
319 String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})}),
320 String.reverse(escape_reverse(text, SCon{'"', SNil{}})) ++ SCon{'"', SNil{}},
321 SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}},
322 S.reverse_cons('"', escape_reverse(text, SCon{'"', SNil{}})),
323 Equal.trans(String,
324 String.reverse(escape_reverse(text, SCon{'"', SNil{}})) ++ SCon{'"', SNil{}},
325 (SCon{'"', SNil{}} ++ J.escape_string(text)) ++ SCon{'"', SNil{}},
326 SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}},
327 Equal.cong(String, String, value => value ++ SCon{'"', SNil{}},
328 String.reverse(escape_reverse(text, SCon{'"', SNil{}})),
329 SCon{'"', SNil{}} ++ J.escape_string(text),
330 escape_reverse_shape(text, SCon{'"', SNil{}})),
331 S.append_assoc(SCon{'"', SNil{}}, J.escape_string(text), SCon{'"', SNil{}})))
332
333def lex_rendered_string(+text: String) -> {J.lex_scan(SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, J.Outside{}, SNil{}, Nil{}) == J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> Nil{} : List<&2, J.Lexeme>}:
334 Equal.trans(List<&2, J.Lexeme>,
335 J.lex_scan(SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, J.Outside{}, SNil{}, Nil{}),
336 J.lex_scan(J.escape_string(text) ++ SCon{'"', SNil{}}, J.Quoted{}, SCon{'"', SNil{}}, Nil{}),
337 J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> Nil{},
338 lex_scan_step('"', J.escape_string(text) ++ SCon{'"', SNil{}}, J.Outside{}, SNil{}, Nil{}),
339 Equal.trans(List<&2, J.Lexeme>,
340 J.lex_scan(J.escape_string(text) ++ SCon{'"', SNil{}}, J.Quoted{}, SCon{'"', SNil{}}, Nil{}),
341 J.lex_scan(SCon{'"', SNil{}}, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), Nil{}),
342 J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> Nil{},
343 scan_escape_string(text, SCon{'"', SNil{}}, SCon{'"', SNil{}}, Nil{}),
344 Equal.trans(List<&2, J.Lexeme>,
345 J.lex_scan(SCon{'"', SNil{}}, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), Nil{}),
346 J.Payload{String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})})} <> Nil{},
347 J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> Nil{},
348 lex_scan_step('"', SNil{}, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), Nil{}),
349 Equal.cong(String, List<&2, J.Lexeme>, payload => J.Payload{payload} <> Nil{},
350 String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})}),
351 SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, quoted_buffer_payload(text)))))
352
353def lex_rendered_string_suffix(+text: String,
354 +suffix: String,
355 +acc: List<&2, J.Lexeme>) -> {J.lex_scan((SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ suffix, J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc) : List<&2, J.Lexeme>}:
356 Equal.trans(List<&2, J.Lexeme>,
357 J.lex_scan((SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ suffix, J.Outside{}, SNil{}, acc),
358 J.lex_scan(SCon{'"', (J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix}, J.Outside{}, SNil{}, acc),
359 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc),
360 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source, J.Outside{}, SNil{}, acc),
361 (SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ suffix,
362 SCon{'"', (J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix}, {==}),
363 Equal.trans(List<&2, J.Lexeme>,
364 J.lex_scan(SCon{'"', (J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix}, J.Outside{}, SNil{}, acc),
365 J.lex_scan((J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix, J.Quoted{}, SCon{'"', SNil{}}, acc),
366 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc),
367 lex_scan_step('"', (J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix, J.Outside{}, SNil{}, acc),
368 Equal.trans(List<&2, J.Lexeme>,
369 J.lex_scan((J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix, J.Quoted{}, SCon{'"', SNil{}}, acc),
370 J.lex_scan(J.escape_string(text) ++ (SCon{'"', SNil{}} ++ suffix), J.Quoted{}, SCon{'"', SNil{}}, acc),
371 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc),
372 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source, J.Quoted{}, SCon{'"', SNil{}}, acc),
373 (J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix,
374 J.escape_string(text) ++ (SCon{'"', SNil{}} ++ suffix),
375 S.append_assoc(J.escape_string(text), SCon{'"', SNil{}}, suffix)),
376 Equal.trans(List<&2, J.Lexeme>,
377 J.lex_scan(J.escape_string(text) ++ (SCon{'"', SNil{}} ++ suffix), J.Quoted{}, SCon{'"', SNil{}}, acc),
378 J.lex_scan(SCon{'"', SNil{}} ++ suffix, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), acc),
379 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc),
380 scan_escape_string(text, SCon{'"', SNil{}} ++ suffix, SCon{'"', SNil{}}, acc),
381 Equal.trans(List<&2, J.Lexeme>,
382 J.lex_scan(SCon{'"', SNil{}} ++ suffix, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), acc),
383 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})})} <> acc),
384 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc),
385 lex_scan_step('"', suffix, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), acc),
386 Equal.cong(String, List<&2, J.Lexeme>, payload => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{payload} <> acc),
387 String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})}),
388 SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, quoted_buffer_payload(text)))))))
389
390def lex_string_before_punctuation(+text: String,
391 +punctuation: Char,
392 +suffix: String,
393 +acc: List<&2, J.Lexeme>,
394 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan((SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, (J.Punctuation{punctuation} <> J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc)) : List<&2, J.Lexeme>}:
395 Equal.trans(List<&2, J.Lexeme>,
396 J.lex_scan((SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
397 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc),
398 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc),
399 lex_rendered_string_suffix(text, SCon{punctuation, SNil{}} ++ suffix, acc),
400 scan_punctuation_char(punctuation, suffix, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc, action))
401
402def lex_null_before_punctuation(+punctuation: Char,
403 +suffix: String,
404 +acc: List<&2, J.Lexeme>,
405 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan("null" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{"null"} <> acc) : List<&2, J.Lexeme>}:
406 Equal.trans(List<&2, J.Lexeme>,
407 J.lex_scan("null" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
408 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, "llun", acc),
409 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{"null"} <> acc),
410 {==},
411 scan_punctuation_char(punctuation, suffix, "llun", acc, action))
412
413def lex_true_before_punctuation(+punctuation: Char,
414 +suffix: String,
415 +acc: List<&2, J.Lexeme>,
416 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan("true" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{"true"} <> acc) : List<&2, J.Lexeme>}:
417 Equal.trans(List<&2, J.Lexeme>,
418 J.lex_scan("true" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
419 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, "eurt", acc),
420 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{"true"} <> acc),
421 {==},
422 scan_punctuation_char(punctuation, suffix, "eurt", acc, action))
423
424def lex_false_before_punctuation(+punctuation: Char,
425 +suffix: String,
426 +acc: List<&2, J.Lexeme>,
427 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan("false" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{"false"} <> acc) : List<&2, J.Lexeme>}:
428 Equal.trans(List<&2, J.Lexeme>,
429 J.lex_scan("false" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
430 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, "eslaf", acc),
431 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{"false"} <> acc),
432 {==},
433 scan_punctuation_char(punctuation, suffix, "eslaf", acc, action))
434
435def lex_empty_array_before_punctuation(+punctuation: Char,
436 +suffix: String,
437 +acc: List<&2, J.Lexeme>,
438 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan("[]" ++ (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>}:
439 Equal.trans(List<&2, J.Lexeme>, J.lex_scan("[]" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
440 J.lex_scan(SCon{']', SCon{punctuation, SNil{}} ++ suffix}, J.Outside{}, SNil{}, J.Punctuation{'['} <> acc),
441 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> J.Punctuation{'['} <> acc),
442 scan_punctuation_char('[', SCon{']', SCon{punctuation, SNil{}} ++ suffix}, SNil{}, acc, {==}),
443 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{']', SCon{punctuation, SNil{}} ++ suffix}, J.Outside{}, SNil{}, J.Punctuation{'['} <> acc),
444 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{']'} <> J.Punctuation{'['} <> acc),
445 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> J.Punctuation{'['} <> acc),
446 scan_punctuation_char(']', SCon{punctuation, SNil{}} ++ suffix, SNil{}, J.Punctuation{'['} <> acc, {==}),
447 scan_punctuation_char(punctuation, suffix, SNil{}, J.Punctuation{']'} <> J.Punctuation{'['} <> acc, action)))
448
449def lex_empty_object_before_punctuation(+punctuation: Char,
450 +suffix: String,
451 +acc: List<&2, J.Lexeme>,
452 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan("{}" ++ (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>}:
453 Equal.trans(List<&2, J.Lexeme>, J.lex_scan("{}" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
454 J.lex_scan(SCon{'}', SCon{punctuation, SNil{}} ++ suffix}, J.Outside{}, SNil{}, J.Punctuation{'{'} <> acc),
455 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{'}'} <> J.Punctuation{'{'} <> acc),
456 scan_punctuation_char('{', SCon{'}', SCon{punctuation, SNil{}} ++ suffix}, SNil{}, acc, {==}),
457 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{'}', SCon{punctuation, SNil{}} ++ suffix}, J.Outside{}, SNil{}, J.Punctuation{'{'} <> acc),
458 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{'}'} <> J.Punctuation{'{'} <> acc),
459 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{'}'} <> J.Punctuation{'{'} <> acc),
460 scan_punctuation_char('}', SCon{punctuation, SNil{}} ++ suffix, SNil{}, J.Punctuation{'{'} <> acc, {==}),
461 scan_punctuation_char(punctuation, suffix, SNil{}, J.Punctuation{'}'} <> J.Punctuation{'{'} <> acc, action)))
462
463def trailing_space(+text: String,
464 +mode: J.LexMode,
465 +reversed: String,
466 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(text ++ " ", mode, reversed, acc) == J.lex_scan(text, mode, reversed, acc) : List<&2, J.Lexeme>}:
467 match text:
468 case SNil{}:
469 match mode:
470 case J.Outside{}: {==}
471 case J.Quoted{}: {==}
472 case J.Escaped{}: {==}
473 case SCon{head, tail}:
474 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ " ", mode, reversed, acc),
475 J.lex_scan(tail ++ " ", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
476 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
477 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
478 J.lex_scan(SCon{head, tail}, mode, reversed, acc),
479 lex_scan_step(head, tail ++ " ", mode, reversed, acc),
480 Equal.trans(List<&2, J.Lexeme>,
481 J.lex_scan(tail ++ " ", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
482 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
483 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
484 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
485 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
486 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
487 J.lex_scan(SCon{head, tail}, mode, reversed, acc),
488 trailing_space(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
489 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
490 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
491 Equal.sym(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail}, mode, reversed, acc),
492 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
493 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
494 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
495 lex_scan_step(head, tail, mode, reversed, acc))))
496
497def trailing_tab(+text: String,
498 +mode: J.LexMode,
499 +reversed: String,
500 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(text ++ "\t", mode, reversed, acc) == J.lex_scan(text, mode, reversed, acc) : List<&2, J.Lexeme>}:
501 match text:
502 case SNil{}:
503 match mode:
504 case J.Outside{}: {==}
505 case J.Quoted{}: {==}
506 case J.Escaped{}: {==}
507 case SCon{head, tail}:
508 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ "\t", mode, reversed, acc),
509 J.lex_scan(tail ++ "\t", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
510 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
511 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
512 J.lex_scan(SCon{head, tail}, mode, reversed, acc),
513 lex_scan_step(head, tail ++ "\t", mode, reversed, acc),
514 Equal.trans(List<&2, J.Lexeme>,
515 J.lex_scan(tail ++ "\t", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
516 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
517 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
518 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
519 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
520 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
521 J.lex_scan(SCon{head, tail}, mode, reversed, acc),
522 trailing_tab(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
523 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
524 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
525 Equal.sym(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail}, mode, reversed, acc),
526 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
527 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
528 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
529 lex_scan_step(head, tail, mode, reversed, acc))))
530
531def trailing_return(+text: String,
532 +mode: J.LexMode,
533 +reversed: String,
534 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(text ++ "\r", mode, reversed, acc) == J.lex_scan(text, mode, reversed, acc) : List<&2, J.Lexeme>}:
535 match text:
536 case SNil{}:
537 match mode:
538 case J.Outside{}: {==}
539 case J.Quoted{}: {==}
540 case J.Escaped{}: {==}
541 case SCon{head, tail}:
542 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ "\r", mode, reversed, acc),
543 J.lex_scan(tail ++ "\r", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
544 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
545 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
546 J.lex_scan(SCon{head, tail}, mode, reversed, acc),
547 lex_scan_step(head, tail ++ "\r", mode, reversed, acc),
548 Equal.trans(List<&2, J.Lexeme>,
549 J.lex_scan(tail ++ "\r", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
550 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
551 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
552 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
553 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
554 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
555 J.lex_scan(SCon{head, tail}, mode, reversed, acc),
556 trailing_return(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
557 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
558 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
559 Equal.sym(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail}, mode, reversed, acc),
560 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
561 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
562 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
563 lex_scan_step(head, tail, mode, reversed, acc))))
564
565def trailing_newline(+text: String,
566 +mode: J.LexMode,
567 +reversed: String,
568 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(text ++ "\n", mode, reversed, acc) == J.lex_scan(text, mode, reversed, acc) : List<&2, J.Lexeme>}:
569 match text:
570 case SNil{}:
571 match mode:
572 case J.Outside{}: {==}
573 case J.Quoted{}: {==}
574 case J.Escaped{}: {==}
575 case SCon{head, tail}:
576 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ "\n", mode, reversed, acc),
577 J.lex_scan(tail ++ "\n", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
578 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
579 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
580 J.lex_scan(SCon{head, tail}, mode, reversed, acc),
581 lex_scan_step(head, tail ++ "\n", mode, reversed, acc),
582 Equal.trans(List<&2, J.Lexeme>,
583 J.lex_scan(tail ++ "\n", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
584 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
585 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
586 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
587 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
588 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
589 J.lex_scan(SCon{head, tail}, mode, reversed, acc),
590 trailing_newline(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
591 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
592 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
593 Equal.sym(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail}, mode, reversed, acc),
594 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
595 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
596 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
597 lex_scan_step(head, tail, mode, reversed, acc))))