def trailing_newline

qasim-bend-kit@0.1.0.2 · proof/JSON_LexWhitespaceProof.bend:565

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J

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))))