def number_end

qasim-bend-kit@0.1.0.2 · proof/JSON_RenderLexProof.bend:147

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_NumberLexProof.bend as Num

147def number_end(+text: String,
148               +acc: List<&2, J.Lexeme>,
149               +evidence: {J.number_valid(text) == True{} : Bool}) -> {J.lex_scan(text, J.Outside{}, SNil{}, acc) == (List.reverse(&2, J.Lexeme, J.Payload{text} <> acc)) : List<&2, J.Lexeme>}:
150    match text:
151        case SNil{}:
152            Empty.absurd({J.lex_scan(SNil{}, J.Outside{}, SNil{}, acc) == (List.reverse(&2, J.Lexeme, J.Payload{SNil{}} <> acc)) : List<&2, J.Lexeme>},
153                Num.false_true(Equal.trans(Bool, False{}, J.number_valid(SNil{}), True{}, {==}, evidence)))
154        case SCon{+head, +tail}:
155            Equal.trans(List<&2, J.Lexeme>,
156                J.lex_scan(text, J.Outside{}, SNil{}, acc),
157                J.lexemes(text, J.Outside{}, SNil{}, acc, J.LexRaw{}),
158                List.reverse(&2, J.Lexeme, J.Payload{text} <> acc),
159                Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, SNil{}, acc, action),
160                    J.lex_seed_action(text, J.Outside{}), J.LexRaw{},
161                    Num.number_char_action(head, J.number_char(head), {==}, tail, J.NumberStart{}, evidence)),
162                Equal.trans(List<&2, J.Lexeme>,
163                    J.lexemes(text, J.Outside{}, SNil{}, acc, J.LexRaw{}),
164                    J.lex_scan(tail, J.Outside{}, SCon{head, SNil{}}, acc),
165                    List.reverse(&2, J.Lexeme, J.Payload{text} <> acc),
166                    {==},
167                    Equal.trans(List<&2, J.Lexeme>,
168                        J.lex_scan(tail, J.Outside{}, SCon{head, SNil{}}, acc),
169                        List.reverse(&2, J.Lexeme, J.Payload{SCon{head, SNil{}} ++ tail} <> acc),
170                        List.reverse(&2, J.Lexeme, J.Payload{text} <> acc),
171                        number_tail_acc(tail, J.number_next(J.NumberStart{}, head), head, SNil{}, head, SNil{}, acc, {==},
172                            Num.number_valid_cons(head, tail, J.NumberStart{}, evidence)),
173                        Equal.cong(String, List<&2, J.Lexeme>, s => List.reverse(&2, J.Lexeme, J.Payload{s} <> acc),
174                            SCon{head, SNil{}} ++ tail, text, {==}))))