proof/JSON_AssemblyProof.bend checks

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

5 imports

import Base
import ../libs/JSON.bend as J
import ./JSON_ListProof.bend as L
import ./JSON_PrimitiveProof.bend as P
import ./JSON_StringProof.bend as S

Types

type Mode source · line 10 · raw

Data

Whole
```
Mode
```
Members
```
Mode
```

Definitions

def R source · line 7 · raw

Type

def tokens source · line 14 · raw

@value:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value -> @mode:Mode -> @tail:List<&1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Token> -> List<&1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Token>

def start_members source · line 40 · raw

@value:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value -> @acc:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value> -> @fields:List<&2, Sigma<&2, &2, String, key => 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>> -> @kont:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.ParserKont -> 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Assembly

def start source · line 48 · raw

@value:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value -> @mode:Mode -> @acc:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value> -> @fields:List<&2, Sigma<&2, &2, String, key => 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>> -> @kont:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.ParserKont -> 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Assembly

def completed_members source · line 56 · raw

@value:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value -> @acc:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value> -> @fields:List<&2, Sigma<&2, &2, String, key => 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>> -> 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value

def completed source · line 64 · raw

@value:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value -> @mode:Mode -> @acc:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value> -> @fields:List<&2, Sigma<&2, &2, String, key => 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>> -> 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value

def atom_roundtrip source · line 72 · raw

@+value:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value -> @+mode:Mode -> @-tail:List<&1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Token> -> @+acc:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value> -> @+fields:List<&2, Sigma<&2, &2, String, key => 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>> -> @+kont:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.ParserKont -> @+text:String -> @started:{start(value, mode, acc, fields, kont) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NeedValue{kont} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Assembly} -> @completed_value:{completed(value, mode, acc, fields) == value : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value} -> @tokenized:{tokens(value, mode, tail) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Atom{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.decode_payload(text)} <> tail : List<&1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Token>} -> @decoded:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.decode_payload(text) == Done{value} : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assemble(tokens(value, mode, tail), start(value, mode, acc, fields, kont)) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assemble(tail, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assembly_resume(kont, completed(value, mode, acc, fields))) : R}

def array_first_atom source · line 96 · raw

@result:Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value> -> @-tail:List<&1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Token> -> @+kont:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.ParserKont -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assemble(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Atom{result} <> tail, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.ArrayFirst{kont}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assemble(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Atom{result} <> tail, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NeedValue{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.InArray{[], kont}}) : R}

def array_next_atom source · line 101 · raw

@result:Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value> -> @-tail:List<&1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Token> -> @+acc:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value> -> @+kont:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.ParserKont -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assemble(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Atom{result} <> tail, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.ArrayNext{acc, kont}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assemble(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Atom{result} <> tail, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NeedValue{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.InArray{acc, kont}}) : R}

def array_first source · line 107 · raw

@+value:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value -> @-tail:List<&1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Token> -> @+acc:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value> -> @+kont:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.ParserKont -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assemble(tokens(value, Whole{}, tail), 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.ArrayFirst{kont}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assemble(tokens(value, Whole{}, tail), 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NeedValue{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.InArray{[], kont}}) : R}

def array_next source · line 122 · raw

@+value:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value -> @-tail:List<&1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Token> -> @+acc:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value> -> @+kont:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.ParserKont -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assemble(tokens(value, Whole{}, tail), 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.ArrayNext{acc, kont}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assemble(tokens(value, Whole{}, tail), 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NeedValue{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.InArray{acc, kont}}) : R}

def roundtrip source · line 137 · raw

@+value:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value -> @+mode:Mode -> @-tail:List<&1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Token> -> @+acc:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value> -> @+fields:List<&2, Sigma<&2, &2, String, key => 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>> -> @+kont:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.ParserKont -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assemble(tokens(value, mode, tail), start(value, mode, acc, fields, kont)) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assemble(tail, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assembly_resume(kont, completed(value, mode, acc, fields))) : R}