proof/JSON_NumberLexProof.bend source
proof/JSON_NumberLexProof.bend on the hub · documented module
import Base import ../libs/JSON.bend as J import ./JSON_PrimitiveProof.bend as P import ./JSON_StringProof.bend as S import ./JSON_LexWhitespaceProof.bend as W def false_true(e: {False{} == True{} : Bool}) -> Empty: %e : P.false_type(_) Unit{} def number_valid_cons(+character: Char, +tail: String, +state: J.NumberState, evidence: {J.number_valid_end(J.number_valid_step(SCon{character, tail}, state)) == True{} : Bool}) -> {J.number_valid_end(J.number_valid_step(tail, J.number_next(state, character))) == True{} : Bool}: match state: case J.NumberInvalid{}: Empty.absurd({J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})) == True{} : Bool}, false_true(evidence)) case J.NumberStart{}: Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberStart{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberStart{})), True{}, {==}, evidence) case J.NumberMinus{}: Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberMinus{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberMinus{})), True{}, {==}, evidence) case J.NumberZero{}: Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberZero{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberZero{})), True{}, {==}, evidence) case J.NumberInteger{}: Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberInteger{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberInteger{})), True{}, {==}, evidence) case J.NumberDot{}: Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberDot{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberDot{})), True{}, {==}, evidence) case J.NumberFraction{}: Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberFraction{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberFraction{})), True{}, {==}, evidence) case J.NumberExponent{}: Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberExponent{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberExponent{})), True{}, {==}, evidence) case J.NumberExponentSign{}: Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberExponentSign{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberExponentSign{})), True{}, {==}, evidence) case J.NumberExponentDigits{}: Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberExponentDigits{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberExponentDigits{})), True{}, {==}, evidence) def number_other_invalid(state: J.NumberState) -> {J.number_step(J.NOther{}, state) == J.NumberInvalid{} : J.NumberState}: match state: case J.NumberStart{}: {==} case J.NumberMinus{}: {==} case J.NumberZero{}: {==} case J.NumberInteger{}: {==} case J.NumberDot{}: {==} case J.NumberFraction{}: {==} case J.NumberExponent{}: {==} case J.NumberExponentSign{}: {==} case J.NumberExponentDigits{}: {==} case J.NumberInvalid{}: {==} def number_next_other(+character: Char, +state: J.NumberState, evidence: {J.number_char(character) == J.NOther{} : J.NumberChar}) -> {J.number_next(state, character) == J.NumberInvalid{} : J.NumberState}: match state: case J.NumberInvalid{}: {==} case J.NumberStart{}: Equal.trans(J.NumberState, J.number_next(J.NumberStart{}, character), J.number_step(J.NOther{}, J.NumberStart{}), J.NumberInvalid{}, Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberStart{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberStart{})) case J.NumberMinus{}: Equal.trans(J.NumberState, J.number_next(J.NumberMinus{}, character), J.number_step(J.NOther{}, J.NumberMinus{}), J.NumberInvalid{}, Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberMinus{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberMinus{})) case J.NumberZero{}: Equal.trans(J.NumberState, J.number_next(J.NumberZero{}, character), J.number_step(J.NOther{}, J.NumberZero{}), J.NumberInvalid{}, Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberZero{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberZero{})) case J.NumberInteger{}: Equal.trans(J.NumberState, J.number_next(J.NumberInteger{}, character), J.number_step(J.NOther{}, J.NumberInteger{}), J.NumberInvalid{}, Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberInteger{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberInteger{})) case J.NumberDot{}: Equal.trans(J.NumberState, J.number_next(J.NumberDot{}, character), J.number_step(J.NOther{}, J.NumberDot{}), J.NumberInvalid{}, Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberDot{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberDot{})) case J.NumberFraction{}: Equal.trans(J.NumberState, J.number_next(J.NumberFraction{}, character), J.number_step(J.NOther{}, J.NumberFraction{}), J.NumberInvalid{}, Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberFraction{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberFraction{})) case J.NumberExponent{}: Equal.trans(J.NumberState, J.number_next(J.NumberExponent{}, character), J.number_step(J.NOther{}, J.NumberExponent{}), J.NumberInvalid{}, Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberExponent{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberExponent{})) case J.NumberExponentSign{}: Equal.trans(J.NumberState, J.number_next(J.NumberExponentSign{}, character), J.number_step(J.NOther{}, J.NumberExponentSign{}), J.NumberInvalid{}, Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberExponentSign{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberExponentSign{})) case J.NumberExponentDigits{}: Equal.trans(J.NumberState, J.number_next(J.NumberExponentDigits{}, character), J.number_step(J.NOther{}, J.NumberExponentDigits{}), J.NumberInvalid{}, Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberExponentDigits{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberExponentDigits{})) def invalid_valid_tail(+tail: String, +state: J.NumberState, +character: Char, other: {J.number_char(character) == J.NOther{} : J.NumberChar}, evidence: {J.number_valid_end(J.number_valid_step(SCon{character, tail}, state)) == True{} : Bool}) -> Empty: false_true(Equal.trans(Bool, False{}, J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})), True{}, Equal.sym(Bool, J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})), False{}, P.invalid_end(tail)), Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})), J.number_valid_end(J.number_valid_step(tail, J.number_next(state, character))), True{}, Equal.sym(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(state, character))), J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})), Equal.cong(J.NumberState, Bool, s => J.number_valid_end(J.number_valid_step(tail, s)), J.number_next(state, character), J.NumberInvalid{}, number_next_other(character, state, other))), number_valid_cons(character, tail, state, evidence)))) def plain_lexemes(+text: String, reversed: String, acc: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>: match text: case SNil{}: List.reverse(&2, J.Lexeme, J.flush_lexeme(reversed, acc)) case SCon{head, tail}: plain_lexemes(tail, SCon{head, reversed}, acc) def number_char_action(+character: Char, +class: J.NumberChar, class_eq: {J.number_char(character) == class : J.NumberChar}, +tail: String, +state: J.NumberState, evidence: {J.number_valid_end(J.number_valid_step(SCon{character, tail}, state)) == True{} : Bool}) -> {J.lex_outside_action(character, class) == J.LexRaw{} : J.LexAction}: match class: case J.NOther{}: Empty.absurd({J.lex_outside_action(character, J.NOther{}) == J.LexRaw{} : J.LexAction}, invalid_valid_tail(tail, state, character, class_eq, evidence)) case J.NMinus{}: {==} case J.NPlus{}: {==} case J.NDot{}: {==} case J.NExp{}: {==} case J.NZero{}: {==} case J.NDigit{}: {==} def number_prefix_mode(+text: String, +state: J.NumberState, +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {W.prefix_mode(text, J.Outside{}) == J.Outside{} : J.LexMode}: match text: case SNil{}: {==} case SCon{+head, +tail}: Equal.trans(J.LexMode, W.prefix_mode(SCon{head, tail}, J.Outside{}), W.prefix_mode(tail, W.after_mode(J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.Outside{})), J.Outside{}, {==}, Equal.trans(J.LexMode, W.prefix_mode(tail, W.after_mode(J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.Outside{})), W.prefix_mode(tail, J.Outside{}), J.Outside{}, Equal.cong(J.LexAction, J.LexMode, action => W.prefix_mode(tail, W.after_mode(action, J.Outside{})), J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.LexRaw{}, number_char_action(head, J.number_char(head), {==}, tail, state, evidence)), number_prefix_mode(tail, J.number_next(state, head), number_valid_cons(head, tail, state, evidence)))) def number_prefix_acc(+text: String, +state: J.NumberState, +reversed: String, +acc: List<&2, J.Lexeme>, +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {W.prefix_acc(text, J.Outside{}, reversed, acc) == acc : List<&2, J.Lexeme>}: match text: case SNil{}: {==} case SCon{+head, +tail}: Equal.trans(List<&2, J.Lexeme>, W.prefix_acc(SCon{head, tail}, J.Outside{}, reversed, acc), W.prefix_acc(tail, J.Outside{}, SCon{head, reversed}, acc), acc, Equal.trans(List<&2, J.Lexeme>, W.prefix_acc(SCon{head, tail}, J.Outside{}, reversed, acc), W.prefix_acc(tail, W.after_mode(J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.Outside{}), W.after_reversed(J.lex_seed_action(SCon{head, tail}, J.Outside{}), head, reversed), W.after_acc(J.lex_seed_action(SCon{head, tail}, J.Outside{}), head, reversed, acc)), W.prefix_acc(tail, J.Outside{}, SCon{head, reversed}, acc), {==}, Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => W.prefix_acc(tail, W.after_mode(action, J.Outside{}), W.after_reversed(action, head, reversed), W.after_acc(action, head, reversed, acc)), J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.LexRaw{}, number_char_action(head, J.number_char(head), {==}, tail, state, evidence))), number_prefix_acc(tail, J.number_next(state, head), SCon{head, reversed}, acc, number_valid_cons(head, tail, state, evidence))) def number_prefix_reversed(+text: String, +state: J.NumberState, +reversed: String, +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {W.prefix_reversed(text, J.Outside{}, reversed) == String.reverse(text) ++ reversed : String}: match text: case SNil{}: {==} case SCon{+head, +tail}: Equal.trans(String, W.prefix_reversed(SCon{head, tail}, J.Outside{}, reversed), W.prefix_reversed(tail, J.Outside{}, SCon{head, reversed}), String.reverse(SCon{head, tail}) ++ reversed, Equal.trans(String, W.prefix_reversed(SCon{head, tail}, J.Outside{}, reversed), W.prefix_reversed(tail, W.after_mode(J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.Outside{}), W.after_reversed(J.lex_seed_action(SCon{head, tail}, J.Outside{}), head, reversed)), W.prefix_reversed(tail, J.Outside{}, SCon{head, reversed}), {==}, Equal.cong(J.LexAction, String, action => W.prefix_reversed(tail, W.after_mode(action, J.Outside{}), W.after_reversed(action, head, reversed)), J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.LexRaw{}, number_char_action(head, J.number_char(head), {==}, tail, state, evidence))), Equal.trans(String, W.prefix_reversed(tail, J.Outside{}, SCon{head, reversed}), String.reverse(tail) ++ SCon{head, reversed}, String.reverse(SCon{head, tail}) ++ reversed, number_prefix_reversed(tail, J.number_next(state, head), SCon{head, reversed}, number_valid_cons(head, tail, state, evidence)), Equal.trans(String, String.reverse(tail) ++ SCon{head, reversed}, (String.reverse(tail) ++ SCon{head, SNil{}}) ++ reversed, String.reverse(SCon{head, tail}) ++ reversed, Equal.sym(String, (String.reverse(tail) ++ SCon{head, SNil{}}) ++ reversed, String.reverse(tail) ++ SCon{head, reversed}, S.append_assoc(String.reverse(tail), SCon{head, SNil{}}, reversed)), Equal.cong(String, String, value => value ++ reversed, String.reverse(tail) ++ SCon{head, SNil{}}, String.reverse(SCon{head, tail}), Equal.sym(String, String.reverse(SCon{head, tail}), String.reverse(tail) ++ SCon{head, SNil{}}, S.reverse_cons(head, tail)))))) def lex_number_valid(+text: String, +state: J.NumberState, +reversed: String, +acc: List<&2, J.Lexeme>, +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {J.lex_scan(text, J.Outside{}, reversed, acc) == plain_lexemes(text, reversed, acc) : List<&2, J.Lexeme>}: match text: case SNil{}: {==} case SCon{+head, +tail}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, J.Outside{}, reversed, acc), J.lexemes(text, J.Outside{}, reversed, acc, J.LexRaw{}), plain_lexemes(text, reversed, acc), Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, reversed, acc, action), J.lex_seed_action(text, J.Outside{}), J.LexRaw{}, number_char_action(head, J.number_char(head), {==}, tail, state, evidence)), Equal.trans(List<&2, J.Lexeme>, J.lexemes(text, J.Outside{}, reversed, acc, J.LexRaw{}), J.lexemes(tail, J.Outside{}, SCon{head, reversed}, acc, J.lex_seed_action(tail, J.Outside{})), plain_lexemes(text, reversed, acc), {==}, lex_number_valid(tail, J.number_next(state, head), SCon{head, reversed}, acc, number_valid_cons(head, tail, state, evidence)))) def lex_number_tail(+text: String, +state: J.NumberState, +rev_head: Char, +rev_tail: String, +first: Char, +prefix_tail: String, +reverse_prefix: {String.reverse(SCon{rev_head, rev_tail}) == SCon{first, prefix_tail} : String}, +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {J.lex_scan(text, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}) == (J.Payload{SCon{first, prefix_tail} ++ text} <> Nil{}) : List<&2, J.Lexeme>}: match text: case SNil{}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SNil{}, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}), J.Payload{String.reverse(SCon{rev_head, rev_tail})} <> Nil{}, J.Payload{SCon{first, prefix_tail} ++ SNil{}} <> Nil{}, {==}, Equal.trans(List<&2, J.Lexeme>, J.Payload{String.reverse(SCon{rev_head, rev_tail})} <> Nil{}, J.Payload{SCon{first, prefix_tail}} <> Nil{}, J.Payload{SCon{first, prefix_tail} ++ SNil{}} <> Nil{}, Equal.cong(String, List<&2, J.Lexeme>, s => J.Payload{s} <> Nil{}, String.reverse(SCon{rev_head, rev_tail}), SCon{first, prefix_tail}, reverse_prefix), Equal.cong(String, List<&2, J.Lexeme>, s => J.Payload{s} <> Nil{}, SCon{first, prefix_tail}, SCon{first, prefix_tail} ++ SNil{}, Equal.sym(String, SCon{first, prefix_tail} ++ SNil{}, SCon{first, prefix_tail}, S.append_nil(SCon{first, prefix_tail}))))) case SCon{+head, +tail}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}), J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}, J.LexRaw{}), J.Payload{SCon{first, prefix_tail} ++ text} <> Nil{}, Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}, action), J.lex_seed_action(text, J.Outside{}), J.LexRaw{}, number_char_action(head, J.number_char(head), {==}, tail, state, evidence)), Equal.trans(List<&2, J.Lexeme>, J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}, J.LexRaw{}), J.lex_scan(tail, J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, Nil{}), J.Payload{SCon{first, prefix_tail} ++ text} <> Nil{}, {==}, Equal.trans(List<&2, J.Lexeme>, J.lex_scan(tail, J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, Nil{}), J.Payload{(SCon{first, prefix_tail} ++ SCon{head, SNil{}}) ++ tail} <> Nil{}, J.Payload{SCon{first, prefix_tail} ++ text} <> Nil{}, lex_number_tail(tail, J.number_next(state, head), head, SCon{rev_head, rev_tail}, first, prefix_tail ++ SCon{head, SNil{}}, Equal.trans(String, String.reverse(SCon{head, SCon{rev_head, rev_tail}}), String.reverse(SCon{rev_head, rev_tail}) ++ SCon{head, SNil{}}, SCon{first, prefix_tail} ++ SCon{head, SNil{}}, S.reverse_cons(head, SCon{rev_head, rev_tail}), Equal.cong(String, String, x => x ++ SCon{head, SNil{}}, String.reverse(SCon{rev_head, rev_tail}), SCon{first, prefix_tail}, reverse_prefix)), number_valid_cons(head, tail, state, evidence)), Equal.cong(String, List<&2, J.Lexeme>, s => J.Payload{s} <> Nil{}, (SCon{first, prefix_tail} ++ SCon{head, SNil{}}) ++ tail, SCon{first, prefix_tail} ++ text, S.append_assoc(SCon{first, prefix_tail}, SCon{head, SNil{}}, tail))))) def lex_number_payload(+text: String, +evidence: {J.number_valid(text) == True{} : Bool}) -> {J.lex_scan(text, J.Outside{}, SNil{}, Nil{}) == (J.Payload{text} <> Nil{}) : List<&2, J.Lexeme>}: match text: case SNil{}: Empty.absurd({J.lex_scan(SNil{}, J.Outside{}, SNil{}, Nil{}) == (J.Payload{SNil{}} <> Nil{}) : List<&2, J.Lexeme>}, false_true(Equal.trans(Bool, False{}, J.number_valid(SNil{}), True{}, {==}, evidence))) case SCon{+head, +tail}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, J.Outside{}, SNil{}, Nil{}), J.lexemes(text, J.Outside{}, SNil{}, Nil{}, J.LexRaw{}), J.Payload{text} <> Nil{}, Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, SNil{}, Nil{}, action), J.lex_seed_action(text, J.Outside{}), J.LexRaw{}, number_char_action(head, J.number_char(head), {==}, tail, J.NumberStart{}, evidence)), Equal.trans(List<&2, J.Lexeme>, J.lexemes(text, J.Outside{}, SNil{}, Nil{}, J.LexRaw{}), J.lex_scan(tail, J.Outside{}, SCon{head, SNil{}}, Nil{}), J.Payload{text} <> Nil{}, {==}, Equal.trans(List<&2, J.Lexeme>, J.lex_scan(tail, J.Outside{}, SCon{head, SNil{}}, Nil{}), J.Payload{SCon{head, SNil{}} ++ tail} <> Nil{}, J.Payload{text} <> Nil{}, lex_number_tail(tail, J.number_next(J.NumberStart{}, head), head, SNil{}, head, SNil{}, {==}, number_valid_cons(head, tail, J.NumberStart{}, evidence)), Equal.cong(String, List<&2, J.Lexeme>, s => J.Payload{s} <> Nil{}, SCon{head, SNil{}} ++ tail, text, {==})))) def lex_number_delimited_tail(+text: String, +state: J.NumberState, +rev_head: Char, +rev_tail: String, +payload: String, +punctuation: Char, +suffix: String, +acc: List<&2, J.Lexeme>, reverse_buffer: {String.reverse(SCon{rev_head, rev_tail}) == payload : String}, action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}, +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {J.lex_scan(text ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{rev_head, rev_tail}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload ++ text} <> acc) : List<&2, J.Lexeme>}: match text: case SNil{}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SCon{rev_head, rev_tail}, acc), J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload} <> acc), J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload ++ SNil{}} <> acc), Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SCon{rev_head, rev_tail}, acc), J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.flush_lexeme(SCon{rev_head, rev_tail}, acc)), J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload} <> acc), W.scan_punctuation_char(punctuation, suffix, SCon{rev_head, rev_tail}, acc, action), Equal.trans(List<&2, J.Lexeme>, J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.flush_lexeme(SCon{rev_head, rev_tail}, acc)), J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{String.reverse(SCon{rev_head, rev_tail})} <> acc), J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload} <> acc), {==}, Equal.cong(String, List<&2, J.Lexeme>, value => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{value} <> acc), String.reverse(SCon{rev_head, rev_tail}), payload, reverse_buffer))), Equal.cong(String, List<&2, J.Lexeme>, value => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{value} <> acc), payload, payload ++ SNil{}, Equal.sym(String, payload ++ SNil{}, payload, S.append_nil(payload)))) case SCon{+head, +tail}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{rev_head, rev_tail}, acc), J.lex_scan(tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, acc), J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload ++ SCon{head, tail}} <> acc), Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{rev_head, rev_tail}, acc), J.lex_scan(tail ++ (SCon{punctuation, SNil{}} ++ suffix), W.after_mode(J.lex_seed_action(SCon{head, tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), J.Outside{}), W.after_reversed(J.lex_seed_action(SCon{head, tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), head, SCon{rev_head, rev_tail}), W.after_acc(J.lex_seed_action(SCon{head, tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), head, SCon{rev_head, rev_tail}, acc)), J.lex_scan(tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, acc), W.lex_scan_step(head, tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{rev_head, rev_tail}, acc), Equal.cong(J.LexAction, List<&2, J.Lexeme>, lex_action => J.lex_scan(tail ++ (SCon{punctuation, SNil{}} ++ suffix), W.after_mode(lex_action, J.Outside{}), W.after_reversed(lex_action, head, SCon{rev_head, rev_tail}), W.after_acc(lex_action, head, SCon{rev_head, rev_tail}, acc)), J.lex_seed_action(SCon{head, tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), J.LexRaw{}, number_char_action(head, J.number_char(head), {==}, tail, state, evidence))), Equal.trans(List<&2, J.Lexeme>, J.lex_scan(tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, acc), J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{(payload ++ SCon{head, SNil{}}) ++ tail} <> acc), J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload ++ SCon{head, tail}} <> acc), lex_number_delimited_tail(tail, J.number_next(state, head), head, SCon{rev_head, rev_tail}, payload ++ SCon{head, SNil{}}, punctuation, suffix, acc, Equal.trans(String, String.reverse(SCon{head, SCon{rev_head, rev_tail}}), String.reverse(SCon{rev_head, rev_tail}) ++ SCon{head, SNil{}}, payload ++ SCon{head, SNil{}}, S.reverse_cons(head, SCon{rev_head, rev_tail}), Equal.cong(String, String, value => value ++ SCon{head, SNil{}}, String.reverse(SCon{rev_head, rev_tail}), payload, reverse_buffer)), action, number_valid_cons(head, tail, state, evidence)), Equal.cong(String, List<&2, J.Lexeme>, value => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{value} <> acc), (payload ++ SCon{head, SNil{}}) ++ tail, payload ++ SCon{head, tail}, S.append_assoc(payload, SCon{head, SNil{}}, tail)))) def lex_number_before_punctuation(+first: Char, +number_tail: String, +punctuation: Char, +suffix: String, +acc: List<&2, J.Lexeme>, action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}, +evidence: {J.number_valid(SCon{first, number_tail}) == True{} : Bool}) -> {J.lex_scan(SCon{first, number_tail} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{SCon{first, number_tail}} <> acc) : List<&2, J.Lexeme>}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{first, number_tail} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), J.lex_scan(number_tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{first, SNil{}}, acc), J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{SCon{first, number_tail}} <> acc), Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{first, number_tail} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), J.lex_scan(number_tail ++ (SCon{punctuation, SNil{}} ++ suffix), W.after_mode(J.lex_seed_action(SCon{first, number_tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), J.Outside{}), W.after_reversed(J.lex_seed_action(SCon{first, number_tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), first, SNil{}), W.after_acc(J.lex_seed_action(SCon{first, number_tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), first, SNil{}, acc)), J.lex_scan(number_tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{first, SNil{}}, acc), W.lex_scan_step(first, number_tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), Equal.cong(J.LexAction, List<&2, J.Lexeme>, lex_action => J.lex_scan(number_tail ++ (SCon{punctuation, SNil{}} ++ suffix), W.after_mode(lex_action, J.Outside{}), W.after_reversed(lex_action, first, SNil{}), W.after_acc(lex_action, first, SNil{}, acc)), J.lex_seed_action(SCon{first, number_tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), J.LexRaw{}, number_char_action(first, J.number_char(first), {==}, number_tail, J.NumberStart{}, evidence))), lex_number_delimited_tail(number_tail, J.number_next(J.NumberStart{}, first), first, SNil{}, SCon{first, SNil{}}, punctuation, suffix, acc, Equal.trans(String, String.reverse(SCon{first, SNil{}}), String.reverse(SNil{}) ++ SCon{first, SNil{}}, SCon{first, SNil{}}, S.reverse_cons(first, SNil{}), S.append_nil(SCon{first, SNil{}})), action, number_valid_cons(first, number_tail, J.NumberStart{}, evidence))) def lex_certified_number_before_punctuation(+text: String, +certificate: J.NumberCert<text>, +punctuation: Char, +suffix: String, +acc: List<&2, J.Lexeme>, action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(text ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{text} <> acc) : List<&2, J.Lexeme>}: match text: case SNil{}: Empty.absurd({J.lex_scan(SNil{} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{SNil{}} <> acc) : List<&2, J.Lexeme>}, false_true(Equal.trans(Bool, False{}, J.number_valid(SNil{}), True{}, {==}, P.cert_valid(SNil{}, certificate)))) case SCon{head, tail}: lex_number_before_punctuation(head, tail, punctuation, suffix, acc, action, P.cert_valid(text, certificate))