~/bend-docscommunity

proof/JSON_NumberLexProof.bend checks

raw source on the hub · import 0x3d2147650fe101ae3c3e4a95333b4238/proof/JSON_NumberLexProof.bend as JSON_NumberLexProof

5 imports
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

Definitions

def false_true source · line 7 · raw

@e:{False{} == True{} : Bool} -> Empty

def number_valid_cons source · line 11 · raw

@+character:Char -> @+tail:String -> @+state:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberState -> @evidence:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_end(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_step(SCon{character, tail}, state)) == True{} : Bool} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_end(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_step(tail, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_next(state, character))) == True{} : Bool}

def number_other_invalid source · line 37 · raw

@state:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberState -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_step(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NOther{}, state) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberInvalid{} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberState}

def number_next_other source · line 50 · raw

@+character:Char -> @+state:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberState -> @evidence:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_char(character) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NOther{} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberChar} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_next(state, character) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberInvalid{} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberState}

def invalid_valid_tail source · line 83 · raw

@+tail:String -> @+state:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberState -> @+character:Char -> @other:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_char(character) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NOther{} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberChar} -> @evidence:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_end(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_step(SCon{character, tail}, state)) == True{} : Bool} -> Empty

def plain_lexemes source · line 101 · raw

@+text:String -> @reversed:String -> @acc:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Lexeme> -> List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Lexeme>

def number_char_action source · line 106 · raw

@+character:Char -> @+class:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberChar -> @class_eq:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_char(character) == class : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberChar} -> @+tail:String -> @+state:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberState -> @evidence:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_end(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_step(SCon{character, tail}, state)) == True{} : Bool} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.lex_outside_action(character, class) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.LexRaw{} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.LexAction}

def number_prefix_mode source · line 123 · raw

@+text:String -> @+state:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberState -> @+evidence:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_end(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_step(text, state)) == True{} : Bool} -> {0x3d2147650fe101ae3c3e4a95333b4238/proof/JSON_LexWhitespaceProof.prefix_mode(text, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.LexMode}

def number_prefix_acc source · line 140 · raw

@+text:String -> @+state:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberState -> @+reversed:String -> @+acc:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Lexeme> -> @+evidence:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_end(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_step(text, state)) == True{} : Bool} -> {0x3d2147650fe101ae3c3e4a95333b4238/proof/JSON_LexWhitespaceProof.prefix_acc(text, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{}, reversed, acc) == acc : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Lexeme>}

def number_prefix_reversed source · line 164 · raw

@+text:String -> @+state:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberState -> @+reversed:String -> @+evidence:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_end(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_step(text, state)) == True{} : Bool} -> {0x3d2147650fe101ae3c3e4a95333b4238/proof/JSON_LexWhitespaceProof.prefix_reversed(text, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{}, reversed) == String.append(String.reverse(text), reversed) : String}

def lex_number_valid source · line 203 · raw

@+text:String -> @+state:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberState -> @+reversed:String -> @+acc:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Lexeme> -> @+evidence:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_end(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_step(text, state)) == True{} : Bool} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.lex_scan(text, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{}, reversed, acc) == plain_lexemes(text, reversed, acc) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Lexeme>}

def lex_number_tail source · line 226 · raw

@+text:String -> @+state:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.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:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_end(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_step(text, state)) == True{} : Bool} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.lex_scan(text, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{}, SCon{rev_head, rev_tail}, []) == [0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Payload{String.append(SCon{first, prefix_tail}, text)}] : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Lexeme>}

def lex_number_payload source · line 282 · raw

@+text:String -> @+evidence:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid(text) == True{} : Bool} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.lex_scan(text, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{}, "", []) == [0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Payload{text}] : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Lexeme>}

def lex_number_delimited_tail source · line 310 · raw

@+text:String -> @+state:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberState -> @+rev_head:Char -> @+rev_tail:String -> @+payload:String -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Lexeme> -> @reverse_buffer:{String.reverse(SCon{rev_head, rev_tail}) == payload : String} -> @action:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.LexPunctuation{punctuation} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.LexAction} -> @+evidence:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_end(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_step(text, state)) == True{} : Bool} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.lex_scan(String.append(text, String.append(SCon{punctuation, ""}, suffix)), 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{}, SCon{rev_head, rev_tail}, acc) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.lex_scan(suffix, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{}, "", 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Punctuation{punctuation} <> 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Payload{String.append(payload, text)} <> acc) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Lexeme>}

def lex_number_before_punctuation source · line 368 · raw

@+first:Char -> @+number_tail:String -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Lexeme> -> @action:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.LexPunctuation{punctuation} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.LexAction} -> @+evidence:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid(SCon{first, number_tail}) == True{} : Bool} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.lex_scan(String.append(SCon{first, number_tail}, String.append(SCon{punctuation, ""}, suffix)), 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{}, "", acc) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.lex_scan(suffix, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{}, "", 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Punctuation{punctuation} <> 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Payload{SCon{first, number_tail}} <> acc) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Lexeme>}

def lex_certified_number_before_punctuation source · line 397 · raw

@+text:String -> @+certificate:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberCert<text> -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Lexeme> -> @action:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.LexPunctuation{punctuation} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.LexAction} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.lex_scan(String.append(text, String.append(SCon{punctuation, ""}, suffix)), 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{}, "", acc) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.lex_scan(suffix, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Outside{}, "", 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Punctuation{punctuation} <> 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Payload{text} <> acc) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Lexeme>}