def lex_simple_array_after_separator_end
qasim-bend-kit@0.1.0.2 · proof/JSON_SourceProof.bend:1273
import qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend as JSONSourceProof
import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J
import qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend as W
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))))