def lex_number_payload

qasim-bend-kit@0.1.0.2 · proof/JSON_NumberLexProof.bend:282

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

282def lex_number_payload(+text: String,
283                       +evidence: {J.number_valid(text) == True{} : Bool}) -> {J.lex_scan(text, J.Outside{}, SNil{}, Nil{}) == (J.Payload{text} <> Nil{}) : List<&2, J.Lexeme>}:
284    match text:
285        case SNil{}:
286            Empty.absurd({J.lex_scan(SNil{}, J.Outside{}, SNil{}, Nil{}) == (J.Payload{SNil{}} <> Nil{}) : List<&2, J.Lexeme>},
287                false_true(Equal.trans(Bool, False{}, J.number_valid(SNil{}), True{}, {==}, evidence)))
288        case SCon{+head, +tail}:
289            Equal.trans(List<&2, J.Lexeme>,
290                J.lex_scan(text, J.Outside{}, SNil{}, Nil{}),
291                J.lexemes(text, J.Outside{}, SNil{}, Nil{}, J.LexRaw{}),
292                J.Payload{text} <> Nil{},
293                Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, SNil{}, Nil{}, action),
294                    J.lex_seed_action(text, J.Outside{}), J.LexRaw{},
295                    number_char_action(head, J.number_char(head), {==}, tail, J.NumberStart{}, evidence)),
296                Equal.trans(List<&2, J.Lexeme>,
297                    J.lexemes(text, J.Outside{}, SNil{}, Nil{}, J.LexRaw{}),
298                    J.lex_scan(tail, J.Outside{}, SCon{head, SNil{}}, Nil{}),
299                    J.Payload{text} <> Nil{},
300                    {==},
301                    Equal.trans(List<&2, J.Lexeme>,
302                        J.lex_scan(tail, J.Outside{}, SCon{head, SNil{}}, Nil{}),
303                        J.Payload{SCon{head, SNil{}} ++ tail} <> Nil{},
304                        J.Payload{text} <> Nil{},
305                        lex_number_tail(tail, J.number_next(J.NumberStart{}, head), head, SNil{}, head, SNil{}, {==},
306                            number_valid_cons(head, tail, J.NumberStart{}, evidence)),
307                        Equal.cong(String, List<&2, J.Lexeme>, s => J.Payload{s} <> Nil{},
308                            SCon{head, SNil{}} ++ tail, text, {==}))))