proof/JSON_RenderLexProof.bend checks

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

Lexer/renderer bridge. All recursion follows the JSON value structure.

8 imports

import Base
import ../libs/JSON.bend as J
import ./JSON_SourceProof.bend as SP
import ./JSON_NumberLexProof.bend as Num
import ./JSON_PrimitiveProof.bend as P
import ./JSON_ListProof.bend as LP
import ./JSON_StringProof.bend as S
import ./JSON_LexWhitespaceProof.bend as W

Types

type Container source · line 41 · raw

Data

ArrayKind
```
Container
```
ObjectKind
```
Container
```

type Boundary source · line 177 · raw

Data

A rendered value is followed either by end of input or a JSON delimiter.

End
```
Boundary
```

Delimited

@mark:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.JsonPunctuation -> @suffix:String -> Boundary

Definitions

def reverse_concat source · line 11 · raw

@+xs:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> @+ys:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {List.reverse.go(&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme, List.append(&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme, xs, ys), acc) == List.reverse.go(&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme, ys, List.reverse.go(&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme, xs, acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def push source · line 18 · raw

@value:0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value -> @mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>

def push_append source · line 21 · raw

@+value:0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value -> @+mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {push(value, mode, acc) == List.append(&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.reverse_source_task(value, mode), acc) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def push_source source · line 26 · raw

@+value:0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value -> @+members:Bool -> @+suffix:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {List.reverse.go(&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.source(value, members, suffix), acc) == List.reverse.go(&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme, suffix, List.reverse.go(&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.source(value, members, []), acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def opening source · line 45 · raw

@kind:Container -> Char

def prefix_text source · line 50 · raw

@kind:Container -> @mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @text:String -> String

def prefix_acc source · line 56 · raw

@kind:Container -> @mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>

def scan_prefix source · line 62 · raw

@+kind:Container -> @+mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @+text:String -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(prefix_text(kind, mode, text), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", acc) == 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(text, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", prefix_acc(kind, mode, acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def push_array source · line 72 · raw

@+head:0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value -> @+tail:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value> -> @+mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{head <> tail}, mode, acc) == push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{tail}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMembers{}, push(head, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def push_object source · line 81 · raw

@+key:String -> @+head:0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value -> @+tail:List<&2, Sigma<&2, &2, String, k => 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value>> -> @+mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Obj{(key, head) <> tail}, mode, acc) == push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Obj{tail}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMembers{}, push(head, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderWhole{}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Punctuation{':'} <> 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Payload{String.append("\"", String.append(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.escape_string(key), "\""))} <> prefix_acc(ObjectKind{}, mode, acc))) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def number_tail_acc source · line 90 · raw

@+text:String -> @+state:0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.NumberState -> @+rev_head:Char -> @+rev_tail:String -> @+first:Char -> @+prefix_tail:String -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> @+reverse_prefix:{String.reverse(SCon{rev_head, rev_tail}) == SCon{first, prefix_tail} : String} -> @+evidence:{0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.number_valid_end(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.number_valid_step(text, state)) == True{} : Bool} -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(text, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, SCon{rev_head, rev_tail}, acc) == List.reverse(&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Payload{String.append(SCon{first, prefix_tail}, text)} <> acc) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def number_end source · line 147 · raw

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

def boundary_text source · line 181 · raw

@boundary:Boundary -> String

def finish source · line 186 · raw

@boundary:Boundary -> @acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>

def scan_boundary source · line 192 · raw

@+boundary:Boundary -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(boundary_text(boundary), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", acc) == finish(boundary, acc) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def atomic_end source · line 199 · raw

@+atom:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.AtomicValue -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.render(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.atomic_value(atom), False{}, ""), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", acc) == finish(End{}, push(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.atomic_value(atom), 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderWhole{}, acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def atomic_mode_end source · line 231 · raw

@+atom:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.AtomicValue -> @+mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.atomic_value(atom), mode, ""), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", acc) == finish(End{}, push(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.atomic_value(atom), mode, acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def atomic_lex source · line 251 · raw

@+atom:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.AtomicValue -> @+mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @+boundary:Boundary -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.atomic_value(atom), mode, boundary_text(boundary)), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", acc) == finish(boundary, push(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.atomic_value(atom), mode, acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def array_continuation source · line 272 · raw

@values:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value> -> @boundary:Boundary -> Boundary

def array_continuation_text source · line 278 · raw

@+values:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value> -> @+boundary:Boundary -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{values}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMembers{}, boundary_text(boundary)) == boundary_text(array_continuation(values, boundary)) : String}

def array_resume source · line 284 · raw

@+values:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value> -> @+boundary:Boundary -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> @tail_lex:{0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{values}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderAfterSeparator{}, boundary_text(boundary)), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Punctuation{','} <> acc) == finish(boundary, push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{values}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderAfterSeparator{}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Punctuation{','} <> acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>} -> {finish(array_continuation(values, boundary), acc) == finish(boundary, push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{values}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMembers{}, acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def object_continuation source · line 292 · raw

@values:List<&2, Sigma<&2, &2, String, k => 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value>> -> @boundary:Boundary -> Boundary

def object_continuation_text source · line 298 · raw

@+values:List<&2, Sigma<&2, &2, String, k => 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value>> -> @+boundary:Boundary -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Obj{values}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMembers{}, boundary_text(boundary)) == boundary_text(object_continuation(values, boundary)) : String}

def object_resume source · line 303 · raw

@+values:List<&2, Sigma<&2, &2, String, k => 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value>> -> @+boundary:Boundary -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> @tail_lex:{0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Obj{values}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderAfterSeparator{}, boundary_text(boundary)), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Punctuation{','} <> acc) == finish(boundary, push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Obj{values}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderAfterSeparator{}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Punctuation{','} <> acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>} -> {finish(object_continuation(values, boundary), acc) == finish(boundary, push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Obj{values}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMembers{}, acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def field_text source · line 309 · raw

@+key:String -> @+text:String -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.render_object_field("", key, text) == String.append(String.append("\"", String.append(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.escape_string(key), "\"")), String.append(":", text)) : String}

def scan_field source · line 329 · raw

@+key:String -> @+text:String -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.render_object_field("", key, text), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", acc) == 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(text, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Punctuation{':'} <> 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Payload{String.append("\"", String.append(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.escape_string(key), "\""))} <> acc) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def empty_array_end source · line 343 · raw

@+mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{[]}, mode, ""), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", acc) == finish(End{}, push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{[]}, mode, acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def empty_array_lex source · line 350 · raw

@+mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @+boundary:Boundary -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{[]}, mode, boundary_text(boundary)), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", acc) == finish(boundary, push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{[]}, mode, acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def empty_object_end source · line 370 · raw

@+mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Obj{[]}, mode, ""), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", acc) == finish(End{}, push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Obj{[]}, mode, acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def empty_object_lex source · line 377 · raw

@+mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @+boundary:Boundary -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Obj{[]}, mode, boundary_text(boundary)), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", acc) == finish(boundary, push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Obj{[]}, mode, acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def render_array source · line 397 · raw

@+head:0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value -> @+tail:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value> -> @+mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @+boundary:Boundary -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{head <> tail}, mode, boundary_text(boundary)) == prefix_text(ArrayKind{}, mode, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(head, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderWhole{}, boundary_text(array_continuation(tail, boundary)))) : String}

def lex_array source · line 422 · raw

@+head:0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value -> @+tail:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value> -> @+mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @+boundary:Boundary -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> @head_lex:{0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(head, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderWhole{}, boundary_text(array_continuation(tail, boundary))), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", prefix_acc(ArrayKind{}, mode, acc)) == finish(array_continuation(tail, boundary), push(head, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>} -> @tail_lex:{0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{tail}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderAfterSeparator{}, boundary_text(boundary)), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Punctuation{','} <> push(head, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))) == finish(boundary, push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{tail}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderAfterSeparator{}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Punctuation{','} <> push(head, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc)))) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>} -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{head <> tail}, mode, boundary_text(boundary)), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", acc) == finish(boundary, push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{head <> tail}, mode, acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def render_object source · line 462 · raw

@+key:String -> @+head:0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value -> @+tail:List<&2, Sigma<&2, &2, String, k => 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value>> -> @+mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @+boundary:Boundary -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Obj{(key, head) <> tail}, mode, boundary_text(boundary)) == prefix_text(ObjectKind{}, mode, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.render_object_field("", key, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(head, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderWhole{}, boundary_text(object_continuation(tail, boundary))))) : String}

def lex_object source · line 486 · raw

@+key:String -> @+head:0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value -> @+tail:List<&2, Sigma<&2, &2, String, k => 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value>> -> @+mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @+boundary:Boundary -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> @head_lex:{0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(head, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderWhole{}, boundary_text(object_continuation(tail, boundary))), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Punctuation{':'} <> 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Payload{String.append("\"", String.append(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.escape_string(key), "\""))} <> prefix_acc(ObjectKind{}, mode, acc)) == finish(object_continuation(tail, boundary), push(head, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderWhole{}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Punctuation{':'} <> 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Payload{String.append("\"", String.append(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.escape_string(key), "\""))} <> prefix_acc(ObjectKind{}, mode, acc))) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>} -> @tail_lex:{0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Obj{tail}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderAfterSeparator{}, boundary_text(boundary)), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Punctuation{','} <> push(head, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderWhole{}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Punctuation{':'} <> 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Payload{String.append("\"", String.append(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.escape_string(key), "\""))} <> prefix_acc(ObjectKind{}, mode, acc))) == finish(boundary, push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Obj{tail}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderAfterSeparator{}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Punctuation{','} <> push(head, 0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderWhole{}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Punctuation{':'} <> 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Payload{String.append("\"", String.append(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.escape_string(key), "\""))} <> prefix_acc(ObjectKind{}, mode, acc)))) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>} -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Obj{(key, head) <> tail}, mode, boundary_text(boundary)), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", acc) == finish(boundary, push(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Obj{(key, head) <> tail}, mode, acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def lex_value source · line 528 · raw

@+value:0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value -> @+mode:0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.RenderMode -> @+boundary:Boundary -> @+acc:List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme> -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/proof/JSON_SourceProof.render_task(value, mode, boundary_text(boundary)), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", acc) == finish(boundary, push(value, mode, acc)) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}

def lex_source source · line 551 · raw

@+value:0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.lex_scan(0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.stringify(value), 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Outside{}, "", []) == 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.source(value, False{}, []) : List<&2, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Lexeme>}