def lex_scan_append

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

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

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