libs/JSON.bend checks

raw source on the hub · import 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.bend as JSON

1 import

import Base

Types

type NumberCert source · line 10 · raw

@-s:String -> Data

Certified

@-s:String -> @witness:NumberProof(s) -> NumberCert<s>

type Value source · line 13 · raw

Data

Null
```
Value
```
Bool
```
@value:BoolType -> Value
```

Number

@lexeme:String -> @certificate:NumberCert<lexeme> -> Value

Str
```
@value:String -> Value
```
Arr
```
@values:List<&2, Value> -> Value
```

Obj

@fields:List<&2, Sigma<&2, &2, String, key => Value>> -> Value

type Error source · line 21 · raw

Data

Error
```
Error
```

type Parsed source · line 24 · raw

Type

Parsed
```
@value:Value -> @rest:String -> Parsed
```

type StringScan source · line 27 · raw

Data

StringScan

@value:String -> @rest:String -> StringScan

type StringScanState source · line 30 · raw

Type

ScanText

@input:String -> @reversed:String -> StringScanState

ScanControl

@character:Char -> @rest:String -> @reversed:String -> @control:BoolType -> StringScanState

ScanUnicode

@parsed:Result<&1, &1, Error, HexScan> -> @reversed:String -> StringScanState

ScanUnicodeHigh

@code:U32 -> @rest:String -> @reversed:String -> @is_high:BoolType -> StringScanState

ScanUnicodeLow

@high:U32 -> @original:String -> @parsed:Result<&1, &1, Error, HexScan> -> @reversed:String -> StringScanState

ScanUnicodeLowClass

@high:U32 -> @low:U32 -> @rest:String -> @original:String -> @reversed:String -> @valid:BoolType -> StringScanState

type NumberState source · line 38 · raw

Data

NumberStart
```
NumberState
```
NumberMinus
```
NumberState
```
NumberZero
```
NumberState
```
NumberInteger
```
NumberState
```
NumberDot
```
NumberState
```
NumberFraction
```
NumberState
```
NumberExponent
```
NumberState
```
NumberExponentSign
```
NumberState
```
NumberExponentDigits
```
NumberState
```
NumberInvalid
```
NumberState
```

type EscapeClass source · line 141 · raw

Data

Raw
```
EscapeClass
```
Backslash
```
EscapeClass
```
Quote
```
EscapeClass
```
Control0
```
EscapeClass
```
Control1
```
EscapeClass
```
Control2
```
EscapeClass
```
Control3
```
EscapeClass
```
Control4
```
EscapeClass
```
Control5
```
EscapeClass
```
Control6
```
EscapeClass
```
Control7
```
EscapeClass
```
Control8
```
EscapeClass
```
Control9
```
EscapeClass
```
Control10
```
EscapeClass
```
Control11
```
EscapeClass
```
Control12
```
EscapeClass
```
Control13
```
EscapeClass
```
Control14
```
EscapeClass
```
Control15
```
EscapeClass
```
Control16
```
EscapeClass
```
Control17
```
EscapeClass
```
Control18
```
EscapeClass
```
Control19
```
EscapeClass
```
Control20
```
EscapeClass
```
Control21
```
EscapeClass
```
Control22
```
EscapeClass
```
Control23
```
EscapeClass
```
Control24
```
EscapeClass
```
Control25
```
EscapeClass
```
Control26
```
EscapeClass
```
Control27
```
EscapeClass
```
Control28
```
EscapeClass
```
Control29
```
EscapeClass
```
Control30
```
EscapeClass
```
Control31
```
EscapeClass
```

type QuoteAction source · line 216 · raw

Data

QuoteBackslash
```
QuoteAction
```
QuoteEnd
```
QuoteAction
```
QuotePlain
```
QuoteAction
```

type HexScan source · line 321 · raw

Data

A hexadecimal escape is exactly four digits. The code preserves standalone UTF-16 surrogate escapes and combines adjacent high/low pairs into a scalar. This accepts the JSON string grammar without silently replacing code units.

HexScan
```
@code:U32 -> @rest:String -> HexScan
```

type NumberChar source · line 512 · raw

Data

NMinus
```
NumberChar
```
NPlus
```
NumberChar
```
NDot
```
NumberChar
```
NExp
```
NumberChar
```
NZero
```
NumberChar
```
NDigit
```
NumberChar
```
NOther
```
NumberChar
```

type ParserKont source · line 671 · raw

Data

The parser is an explicit machine. Its fuel decreases on every state transition, including transitions between container contexts.

Top
```
ParserKont
```

InArray

@acc:List<&2, Value> -> @parent:ParserKont -> ParserKont

InObject

@key:String -> @acc:List<&2, Sigma<&2, &2, String, key => Value>> -> @parent:ParserKont -> ParserKont

type ParserState source · line 676 · raw

Type

ParseValue

@clean:String -> @kont:ParserKont -> ParserState

ParsedResult

@result:Result<&1, &1, Error, Parsed> -> @kont:ParserKont -> ParserState

StringResult

@result:Result<&1, &1, Error, StringScan> -> @kont:ParserKont -> ParserState

ArrayStart

@clean:String -> @acc:List<&2, Value> -> @empty_allowed:BoolType -> @kont:ParserKont -> ParserState

ArrayAfter

@value:Value -> @clean:String -> @acc:List<&2, Value> -> @kont:ParserKont -> ParserState

ObjectStart

@clean:String -> @acc:List<&2, Sigma<&2, &2, String, key => Value>> -> @empty_allowed:BoolType -> @kont:ParserKont -> ParserState

ObjectKey

@result:Result<&1, &1, Error, StringScan> -> @acc:List<&2, Sigma<&2, &2, String, key => Value>> -> @kont:ParserKont -> ParserState

ObjectColon

@key:String -> @clean:String -> @acc:List<&2, Sigma<&2, &2, String, key => Value>> -> @kont:ParserKont -> ParserState

ObjectAfter

@key:String -> @value:Value -> @clean:String -> @acc:List<&2, Sigma<&2, &2, String, key => Value>> -> @kont:ParserKont -> ParserState

Complete
```
@parsed:Parsed -> ParserState
```

type FastString source · line 842 · raw

Data

Common JSON escapes have a structural decoder. Less common Unicode escape spellings use the complete UTF-16 decoder below through the fallback.

Decoded
```
@text:String -> FastString
```
InvalidString
```
FastString
```
UnicodeFallback
```
FastString
```

type Lexeme source · line 934 · raw

Data

Lexical boundaries are found once. Token payloads are then parsed on a balanced fork tree, so strings and numbers in one document can use different GPU lanes. Delimiter assembly follows token order.

Punctuation
```
@character:Char -> Lexeme
```
Payload
```
@text:String -> Lexeme
```

type LexMode source · line 943 · raw

Data

Outside
```
LexMode
```
Quoted
```
LexMode
```
Escaped
```
LexMode
```

type LexAction source · line 948 · raw

Data

LexStop
```
LexAction
```
LexEscapedChar
```
LexAction
```
LexBackslash
```
LexAction
```
LexStringEnd
```
LexAction
```
LexStringChar
```
LexAction
```
LexQuote
```
LexAction
```
LexWhitespace
```
LexAction
```
LexPunctuation
```
@character:Char -> LexAction
```
LexRaw
```
LexAction
```

type LexTree source · line 1062 · raw

Data

LexEmpty
```
LexTree
```
LexLeaf
```
@lexeme:Lexeme -> LexTree
```

LexBranch

@left:LexTree -> @right:LexTree -> LexTree

type Token source · line 1067 · raw

Type

Delimiter
```
@character:Char -> Token
```

Atom

@result:Result<&1, &1, Error, Value> -> Token

type TokenTree source · line 1071 · raw

Type

TokensEmpty
```
TokenTree
```
TokenLeaf
```
@token:Token -> TokenTree
```

TokenBranch

@left:TokenTree -> @right:TokenTree -> TokenTree

type Assembly source · line 1123 · raw

Type

NeedValue
```
@kont:ParserKont -> Assembly
```
ArrayFirst
```
@kont:ParserKont -> Assembly
```

ArrayNext

@acc:List<&2, Value> -> @kont:ParserKont -> Assembly

ArrayComma

@acc:List<&2, Value> -> @kont:ParserKont -> Assembly

ObjectFirst
```
@kont:ParserKont -> Assembly
```

ObjectNext

@acc:List<&2, Sigma<&2, &2, String, key => Value>> -> @kont:ParserKont -> Assembly

NeedColon

@key:String -> @acc:List<&2, Sigma<&2, &2, String, key => Value>> -> @kont:ParserKont -> Assembly

ObjectComma

@acc:List<&2, Sigma<&2, &2, String, key => Value>> -> @kont:ParserKont -> Assembly

Assembled
```
@value:Value -> Assembly
```
AssemblyError
```
Assembly
```

type Batch source · line 1219 · raw

Data

Independent documents form a fork/join tree. Keep sibling subtrees similar in total input size to distribute work across GPU lanes (or CPU workers).

Document
```
@text:String -> Batch
```
Documents
```
@left:Batch -> @right:Batch -> Batch
```

type BatchResult source · line 1223 · raw

Type

DocumentResult

@result:Result<&1, &1, Error, Value> -> BatchResult

DocumentResults

@left:BatchResult -> @right:BatchResult -> BatchResult

Definitions

def BoolType source · line 7 · raw

Data

JSON values preserve number lexemes as strings. This keeps integers and fractional/exponent forms lossless without imposing a fixed numeric width. Number carries grammar evidence so every constructible number is valid JSON. Use number(text) or parse(text) to create numbers from runtime strings.

def whitespace source · line 50 · raw

@s:String -> String

def is_control source · line 67 · raw

@c:Char -> BoolType

def escape_char_special source · line 103 · raw

@c:Char -> String

def escape_class source · line 178 · raw

@character:Char -> EscapeClass

def quote_action_from_class source · line 221 · raw

@class:EscapeClass -> QuoteAction

def quote_action source · line 227 · raw

@character:Char -> QuoteAction

def quote_lex_action source · line 230 · raw

@action:QuoteAction -> LexAction

def escape_char_from_class source · line 236 · raw

@character:Char -> @class:EscapeClass -> String

def escape_char source · line 274 · raw

@+character:Char -> String

def escape_string source · line 277 · raw

@s:String -> String

def render_object_field source · line 286 · raw

@prefix:String -> @key:String -> @value_text:String -> String

Structural rendering has no fuel limit. Tail mode emits the comma before each subsequent member and the closing delimiter at the empty tail.

def render source · line 289 · raw

@value:Value -> @members:BoolType -> @suffix:String -> String

def stringify source · line 315 · raw

@value:Value -> String

def hex_digit source · line 324 · raw

@c:Char -> Maybe<&2, U32>

def scan_hex source · line 350 · raw

@n:Nat -> @s:String -> @acc:U32 -> Result<&1, &1, Error, HexScan>

def string_push source · line 405 · raw

@c:Char -> @result:Result<&1, &1, Error, StringScan> -> Result<&1, &1, Error, StringScan>

def scan_string_machine source · line 415 · raw

@fuel:Nat -> @state:StringScanState -> Result<&1, &1, Error, StringScan>

def scan_string source · line 486 · raw

@+s:String -> Result<&1, &1, Error, StringScan>

def scan_number source · line 489 · raw

@s:String -> @acc:String -> StringScan

def number_char source · line 521 · raw

@c:Char -> NumberChar

def number_step source · line 540 · raw

@character:NumberChar -> @state:NumberState -> NumberState

def number_next source · line 569 · raw

@state:NumberState -> @c:Char -> NumberState

def number_valid_end source · line 574 · raw

@state:NumberState -> BoolType

def number_valid_step source · line 587 · raw

@s:String -> @state:NumberState -> NumberState

def number_valid source · line 596 · raw

@+s:String -> BoolType

def NumberProofFrom source · line 599 · raw

@valid:BoolType -> Data

def NumberProof source · line 606 · raw

@s:String -> Data

def null_token source · line 609 · raw

@s:String -> @matches:BoolType -> Result<&1, &1, Error, Parsed>

def true_token source · line 616 · raw

@s:String -> @matches:BoolType -> Result<&1, &1, Error, Parsed>

def false_token source · line 623 · raw

@s:String -> @matches:BoolType -> Result<&1, &1, Error, Parsed>

def from_string_scan source · line 630 · raw

@scanned:Result<&1, &1, Error, StringScan> -> Result<&1, &1, Error, Parsed>

def number_proof source · line 639 · raw

@+lexeme:String -> @evidence:{number_valid(lexeme) == True{} : BoolType} -> NumberProof(lexeme)

def number_lexeme source · line 644 · raw

@+lexeme:String -> @rest:String -> @valid:BoolType -> @evidence:{number_valid(lexeme) == valid : BoolType} -> Result<&1, &1, Error, Parsed>

def from_number_scan source · line 654 · raw

@scan:StringScan -> Result<&1, &1, Error, Parsed>

def parse_number source · line 659 · raw

@s:String -> Result<&1, &1, Error, Parsed>

def number_from_digit source · line 662 · raw

@s:String -> @digit:BoolType -> Result<&1, &1, Error, Parsed>

def resume_value source · line 688 · raw

@value:Value -> @rest:String -> @kont:ParserKont -> ParserState

def parse_machine source · line 697 · raw

@fuel:Nat -> @state:ParserState -> Result<&1, &1, Error, Parsed>

def parse_value source · line 818 · raw

@+s:String -> Result<&1, &1, Error, Parsed>

def finish_rest_clean source · line 821 · raw

@value:Value -> @clean:String -> Result<&1, &1, Error, Value>

def finish_rest source · line 828 · raw

@value:Value -> @rest:String -> Result<&1, &1, Error, Value>

def finish source · line 831 · raw

@r:Result<&1, &1, Error, Parsed> -> Result<&1, &1, Error, Value>

def fast_push source · line 847 · raw

@result:FastString -> @character:Char -> FastString

def fast_raw source · line 853 · raw

@control:BoolType -> @result:FastString -> @character:Char -> FastString

def fast_string source · line 858 · raw

@text:String -> FastString

def fast_result source · line 907 · raw

@result:FastString -> @original:String -> Result<&1, &1, Error, Value>

def payload_other source · line 913 · raw

@text:String -> Result<&1, &1, Error, Value>

def payload_number source · line 921 · raw

@+text:String -> @valid:BoolType -> @evidence:{number_valid(text) == valid : BoolType} -> Result<&1, &1, Error, Value>

def decode_payload source · line 928 · raw

@+text:String -> Result<&1, &1, Error, Value>

def flush_lexeme source · line 938 · raw

@reversed:String -> @acc:List<&2, Lexeme> -> List<&2, Lexeme>

def lex_outside_other source · line 959 · raw

@character:Char -> LexAction

def lex_outside_action source · line 974 · raw

@character:Char -> @number_kind:NumberChar -> LexAction

def lex_action source · line 979 · raw

@mode:LexMode -> @character:Char -> @number_kind:NumberChar -> LexAction

def lex_seed_action source · line 985 · raw

@text:String -> @mode:LexMode -> LexAction

def lex_end source · line 990 · raw

@+mode:LexMode -> @reversed:String -> @acc:List<&2, Lexeme> -> List<&2, Lexeme>

def lexemes source · line 996 · raw

@text:String -> @+mode:LexMode -> @reversed:String -> @acc:List<&2, Lexeme> -> @action:LexAction -> List<&2, Lexeme>

def lex_scan source · line 1025 · raw

@+text:String -> @+mode:LexMode -> @reversed:String -> @acc:List<&2, Lexeme> -> List<&2, Lexeme>

def source_text source · line 1033 · raw

@text:String -> @acc:List<&2, Lexeme> -> List<&2, Lexeme>

The reverse token stream that corresponds to render(value, mode, suffix). It is used for the structural parser/renderer proof.

def source source · line 1036 · raw

@value:Value -> @members:BoolType -> @acc:List<&2, Lexeme> -> List<&2, Lexeme>

def lex_leaves source · line 1076 · raw

@items:List<&2, Lexeme> -> List<&2, LexTree>

def lex_pairs source · line 1081 · raw

@trees:List<&2, LexTree> -> List<&2, LexTree>

def lex_join source · line 1087 · raw

@trees:List<&2, LexTree> -> LexTree

def lex_balance source · line 1092 · raw

@fuel:Nat -> @trees:List<&2, LexTree> -> LexTree

def lex_tree source · line 1101 · raw

@+items:List<&2, Lexeme> -> LexTree

def decode_lexeme source · line 1104 · raw

@lexeme:Lexeme -> Token

def decode_tree source · line 1109 · raw

@tree:LexTree -> TokenTree

def token_list source · line 1117 · raw

@tree:TokenTree -> @tail:List<&1, Token> -> List<&1, Token>

def assembly_resume source · line 1135 · raw

@kont:ParserKont -> @value:Value -> Assembly

def assembly_atom source · line 1141 · raw

@result:Result<&1, &1, Error, Value> -> @kont:ParserKont -> Assembly

def assembly_value source · line 1146 · raw

@token:Token -> @kont:ParserKont -> Assembly

def assembly_key_value source · line 1153 · raw

@result:Result<&1, &1, Error, Value> -> @acc:List<&2, Sigma<&2, &2, String, key => Value>> -> @kont:ParserKont -> Assembly

def assembly_key source · line 1159 · raw

@token:Token -> @acc:List<&2, Sigma<&2, &2, String, key => Value>> -> @kont:ParserKont -> Assembly

def assembly_step source · line 1165 · raw

@state:Assembly -> @token:Token -> Assembly

def assembly_finish source · line 1194 · raw

@state:Assembly -> Result<&1, &1, Error, Value>

def assemble source · line 1199 · raw

@tokens:List<&1, Token> -> @state:Assembly -> Result<&1, &1, Error, Value>

def parse_normalized source · line 1204 · raw

@text:String -> Result<&1, &1, Error, Value>

def parse source · line 1209 · raw

@+text:String -> Result<&1, &1, Error, Value>

Call as parse!(text) to place the complete parse on Bend's GPU scheduler when one is available. The ordinary call remains useful on small inputs.

def number source · line 1214 · raw

@+text:String -> Result<&1, &1, Error, Value>

Smart constructor. Validation evidence is checked by Bend and is not an unchecked assertion supplied by callers.

def parse_batch source · line 1227 · raw

@batch:Batch -> BatchResult

def parse_gpu source · line 1238 · raw

@text:String -> Result<&1, &1, Error, Value>

The ! entry points request GPU execution; Bend provides the CPU fallback. A single document has sequential grammar dependencies. For parallel work, use parse_batch_gpu with independent documents.

def parse_batch_gpu source · line 1241 · raw

@batch:Batch -> BatchResult

def batch_leaves source · line 1247 · raw

@texts:List<&2, String> -> List<&2, Batch>

Build a balanced fork tree from documents in source order. Pairing adjacent trees on each pass keeps the depth logarithmic without copying input text. For best lane balance, supply documents of similar lengths/complexity.

def batch_pairs source · line 1254 · raw

@trees:List<&2, Batch> -> List<&2, Batch>

def batch_build source · line 1263 · raw

@fuel:Nat -> @trees:List<&2, Batch> -> Maybe<&2, Batch>

def batch_from_list source · line 1276 · raw

@+texts:List<&2, String> -> Maybe<&2, Batch>

def parse_optional_batch_gpu source · line 1279 · raw

@batch:Maybe<&2, Batch> -> Maybe<&1, BatchResult>

def parse_many_gpu source · line 1288 · raw

@texts:List<&2, String> -> Maybe<&1, BatchResult>

Build the fork tree before entering the device. None represents an empty input list; each document's parse failure remains at its own result leaf.