~/bend-docscommunity

proof/JSON_ParallelProof.bend checks

raw source on the hub · import qasim-bend-kit@0.1.0.0/proof/JSON_ParallelProof.bend as JSON_ParallelProof

2 imports
import Base
import ../libs/JSON.bend as J

Definitions

def forest source · line 5 · raw

@trees:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.LexTree> -> @tail:List<&1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Token> -> List<&1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Token>

Semantic token sequence for a forest, independent of its scheduling shape.

def flat source · line 10 · raw

@items:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> @tail:List<&1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Token> -> List<&1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Token>

def join source · line 15 · raw

@+trees:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.LexTree> -> @-tail:List<&1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Token> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.token_list(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.decode_tree(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_join(trees)), tail) == forest(trees, tail) : List<&1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Token>}

def pairs source · line 23 · raw

@+trees:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.LexTree> -> @-tail:List<&1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Token> -> {forest(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_pairs(trees), tail) == forest(trees, tail) : List<&1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Token>}

def balance source · line 32 · raw

@+fuel:Nat -> @+trees:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.LexTree> -> @-tail:List<&1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Token> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.token_list(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.decode_tree(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_balance(fuel, trees)), tail) == forest(trees, tail) : List<&1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Token>}

def leaves source · line 46 · raw

@+items:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> @-tail:List<&1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Token> -> {forest(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_leaves(items), tail) == flat(items, tail) : List<&1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Token>}

def decode source · line 54 · raw

@+items:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> @-tail:List<&1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Token> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.token_list(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.decode_tree(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_tree(items)), tail) == flat(items, tail) : List<&1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Token>}