def trailing_space

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

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

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