json/json.bend checks

raw source on the hub · import 0x33fa1e8e9ce79cb0b4983b81c36ecdd3/json/json.bend as Json

2 imports

import Base
import ../utf8/utf8.bend as U

Types

type Json source · line 7 · raw

Data

JNull
```
Json
```
JBool
```
@value:Bool -> Json
```
JNum
```
@value:Number -> Json
```
JStr
```
@value:String -> Json
```
JArr
```
@items:List<&2, Json> -> Json
```
JObj
```
@fields:List<&2, Field> -> Json
```

type Field source · line 15 · raw

Data

Field
```
@key:String -> @value:Json -> Field
```

type Digit source · line 22 · raw

Data

D0
```
Digit
```
D1
```
Digit
```
D2
```
Digit
```
D3
```
Digit
```
D4
```
Digit
```
D5
```
Digit
```
D6
```
Digit
```
D7
```
Digit
```
D8
```
Digit
```
D9
```
Digit
```

type Lead source · line 35 · raw

Data

a leading digit: never 0

L1
```
Lead
```
L2
```
Lead
```
L3
```
Lead
```
L4
```
Lead
```
L5
```
Lead
```
L6
```
Lead
```
L7
```
Lead
```
L8
```
Lead
```
L9
```
Lead
```

type Int source · line 46 · raw

Data

IZero
```
Int
```

INon

@lead:Lead -> @rest:List<&2, Digit> -> Int

type Frac source · line 50 · raw

Data

FNone
```
Frac
```

FSome

@first:Digit -> @rest:List<&2, Digit> -> Frac

type Sign source · line 54 · raw

Data

NoSign
```
Sign
```
Plus
```
Sign
```
Minus
```
Sign
```

type Exp source · line 59 · raw

Data

ENone
```
Exp
```

ESome

@upper:Bool -> @sign:Sign -> @first:Digit -> @rest:List<&2, Digit> -> Exp

type Number source · line 63 · raw

Data

Number

@neg:Bool -> @int:Int -> @frac:Frac -> @exp:Exp -> Number

type Reason source · line 66 · raw

Data

UnexpectedEnd
```
Reason
```
UnexpectedChar
```
@char:Char -> Reason
```
TrailingInput
```
Reason
```
InvalidNumber
```
Reason
```
InvalidEscape
```
Reason
```
InvalidUnicode
```
Reason
```
LoneSurrogate
```
Reason
```
ControlChar
```
Reason
```
InvalidUtf8
```
Reason
```
Internal
```
Reason
```

type Error source · line 79 · raw

Data

offset counts chars from 0; line and column count from 1

Error

@reason:Reason -> @offset:U32 -> @line:U32 -> @column:U32 -> Error

type Lex source · line 89 · raw

Data

a lexed string and the input after it, or why lexing stopped and how many chars were left from where it went wrong. Errors count, not keep the input: keeping a String that is still being read shares it, and sharing any String counts references on every String in the program

LOk
```
@text:String -> @rest:String -> Lex
```
LBad
```
@reason:Reason -> @left:U32 -> Lex
```

type Class source · line 148 · raw

Data

how a char inside a string is treated; the printer and the lexer both decide through this one function, which is what lets PROOF.bend show that they agree

KCtrl
```
Class
```
KQuote
```
Class
```
KBack
```
Class
```
KPlain
```
Class
```

type Surr source · line 167 · raw

Data

NotSurr
```
Surr
```
High
```
Surr
```
Low
```
Surr
```

type SSt source · line 187 · raw

Data

inside a string: chars so far (reversed) and a pending high surrogate (0 if none). back counts the chars of an escape read before this one; SStop's back counts from where it went wrong through this char, and the lexer reads the input left once it has taken this char

SGo
```
@acc:String -> @hi:U32 -> SSt
```
SEsc
```
@acc:String -> @hi:U32 -> SSt
```

SHex

@acc:String -> @hi:U32 -> @left:Nat -> @code:U32 -> @back:U32 -> SSt

SStop
```
@reason:Reason -> @back:U32 -> SSt
```
SDone
```
@value:String -> SSt
```

type NC source · line 339 · raw

Data

what a char can be inside a number

CDig
```
@d:Digit -> NC
```
CMinus
```
NC
```
CPlus
```
NC
```
CDot
```
NC
```
CExpE
```
@upper:Bool -> NC
```
COther
```
NC
```

type NSt source · line 383 · raw

Data

states of [ minus ] int [ frac ] [ exp ]; digit lists are reversed

NStart
```
NSt
```
NMin
```
NSt
```
NZero
```
@neg:Bool -> NSt
```

NInt

@neg:Bool -> @lead:Lead -> @ds:List<&2, Digit> -> NSt

NDot
```
@neg:Bool -> @int:Int -> NSt
```

NFrac

@neg:Bool -> @int:Int -> @first:Digit -> @ds:List<&2, Digit> -> NSt

NE

@neg:Bool -> @int:Int -> @frac:Frac -> @upper:Bool -> NSt

NESign

@neg:Bool -> @int:Int -> @frac:Frac -> @upper:Bool -> @sign:Sign -> NSt

NExp

@neg:Bool -> @int:Int -> @frac:Frac -> @upper:Bool -> @sign:Sign -> @first:Digit -> @ds:List<&2, Digit> -> NSt

NHalt
```
@last:NSt -> @next:Char -> NSt
```

type NLex source · line 461 · raw

Data

a lexed number and the input after it

NOk
```
@value:Number -> @rest:String -> NLex
```
NBad
```
@reason:Reason -> @left:U32 -> NLex
```

type Frame source · line 501 · raw

Data

an open container; items and fields are reversed, key is the pending one

FArr
```
@items:List<&2, Json> -> Frame
```

FObj

@fields:List<&2, Field> -> @key:String -> Frame

type Mode source · line 506 · raw

Data

what the next token may be

MValue
```
Mode
```
MValueOrClose
```
Mode
```
MKeyOrClose
```
Mode
```
MKey
```
Mode
```
MColon
```
Mode
```
MCommaOrClose
```
Mode
```

type St source · line 514 · raw

Data

Run

@s:String -> @stack:List<&2, Frame> -> @mode:Mode -> St

Fin
```
@value:Json -> St
```
Bad
```
@reason:Reason -> @left:U32 -> St
```

type Loc source · line 667 · raw

Data

Loc
```
@line:U32 -> @column:U32 -> Loc
```

type Lines source · line 686 · raw

Data

what an error needs to know of the input, which is gone by then: its size, and where its line breaks are (last first)

Lines

@size:U32 -> @breaks:List<&2, U32> -> Lines

type Item source · line 1025 · raw

Data

show, one value at a time off an explicit stack, so nesting costs no machine stack. Each item is a value still to print, with show's more and depth. fuel only satisfies the termination check: it allows 2^32 - 1 values, and should it run out, show finishes the job, so the loop always writes what show writes (proof/print.bend)

Item

@value:Json -> @more:Bool -> @depth:Nat -> Item

type JKind source · line 1124 · raw

Data

KNull
```
JKind
```
KBool
```
JKind
```
KNumber
```
JKind
```
KString
```
JKind
```
KArray
```
JKind
```
KObject
```
JKind
```

type Step source · line 1133 · raw

Data

a step into a value: an object's key or an array's index

Name
```
@key:String -> Step
```
Index
```
@i:U32 -> Step
```

type Access source · line 1138 · raw

Data

why a read failed, and where: the path from the root, first step first

Missing
```
@path:List<&2, Step> -> Access
```

Expected

@path:List<&2, Step> -> @want:JKind -> @got:JKind -> Access

OutOfRange
```
@path:List<&2, Step> -> Access
```

type Digits source · line 1264 · raw

Data

all the digits, and how many come before the point

Digits

@ds:List<&2, Digit> -> @point:Nat -> Digits

type Lead0 source · line 1316 · raw

Data

leading zeros dropped, and how many

Lead0

@ds:List<&2, Digit> -> @zeros:Nat -> Lead0

type Hit source · line 1571 · raw

Data

a value at the end of a path, and the path walked, reversed

Hit

@value:Json -> @done:List<&2, Step> -> Hit

type Twice source · line 1575 · raw

Data

a string, rebuilt twice from one read

Twice
```
@a:String -> @b:String -> Twice
```

type Leaf source · line 1754 · raw

Data

a leaf copy, and the path to it, reversed

Leaf

@value:Json -> @done:List<&2, Step> -> Leaf

Definitions

def size source · line 94 · raw

@s:String -> @+n:U32 -> U32

the length of s, plus n

def in_range source · line 101 · raw

@+x:U32 -> @lo:U32 -> @hi:U32 -> Bool

def skip_ws source · line 105 · raw

@s:String -> String

RFC 8259 §2: only space, tab, LF and CR

def heads_eq source · line 119 · raw

@word:String -> @s:String -> Bool

whether the next chars of the word and the input agree

def expect.go source · line 128 · raw

@+word:String -> @+s:String -> @same:Bool -> Lex

a fixed word at the head of the input; same is heads_eq(word, s), tested before, since picking between both results would share the input

def expect source · line 139 · raw

@+word:String -> @+s:String -> Lex

def class.go source · line 154 · raw

@ctrl:Bool -> @+x:U32 -> Class

def class source · line 163 · raw

@+c:Char -> Class

U+0000 to U+001F are control chars

def surr source · line 172 · raw

@+x:U32 -> Surr

def hex_digit source · line 176 · raw

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

def pair source · line 194 · raw

@+hi:U32 -> @+lo:U32 -> U32

def push source · line 197 · raw

@acc:String -> @x:U32 -> SSt

def on_code source · line 200 · raw

@pending:Bool -> @k:Surr -> @acc:String -> @+hi:U32 -> @+x:U32 -> @back:U32 -> SSt

def code source · line 213 · raw

@acc:String -> @+hi:U32 -> @+x:U32 -> @back:U32 -> SSt

def keep.go source · line 217 · raw

@pending:Bool -> @acc:String -> @c:Char -> SSt

a char taken as is after a backslash

def keep source · line 224 · raw

@acc:String -> @+hi:U32 -> @c:Char -> SSt

def close.go source · line 227 · raw

@pending:Bool -> @acc:String -> SSt

def close source · line 234 · raw

@acc:String -> @+hi:U32 -> SSt

def unescape source · line 237 · raw

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

def letter.go source · line 254 · raw

@m:Maybe<&2, U32> -> @acc:String -> @+hi:U32 -> SSt

def letter source · line 262 · raw

@+c:Char -> @acc:String -> @+hi:U32 -> SSt

the letter after a backslash

def plain.go source · line 269 · raw

@pending:Bool -> @acc:String -> @+c:Char -> SSt

def s_go source · line 276 · raw

@k:Class -> @+c:Char -> @acc:String -> @+hi:U32 -> SSt

def s_esc source · line 287 · raw

@k:Class -> @+c:Char -> @acc:String -> @+hi:U32 -> SSt

def s_hex.go source · line 298 · raw

@left:Nat -> @d:Maybe<&2, U32> -> @acc:String -> @+hi:U32 -> @+x:U32 -> @back:U32 -> SSt

def s_step source · line 310 · raw

@st:SSt -> @+c:Char -> SSt

one char of a string body

def lex_str source · line 324 · raw

@s:String -> @st:SSt -> Lex

the body of a string, after its opening quote. A step never sees the input after its char: the closing quote and errors take effect one call later, where that input is the one being read

def nclass source · line 347 · raw

@c:Char -> NC

def rev source · line 395 · raw

@ds:List<&2, Digit> -> List<&2, Digit>

def first_digit source · line 398 · raw

@neg:Bool -> @d:Digit -> NSt

def num_step source · line 423 · raw

@st:NSt -> @k:NC -> @c:Char -> NSt

one char of a number; a char the number cannot take ends it, and the lexer resumes from it

def num_end source · line 466 · raw

@st:NSt -> @rest:String -> NLex

a char that starts no value at all is reported as itself

def lex_num source · line 485 · raw

@s:String -> @st:NSt -> NLex

a step never sees the input after its char, so where the number ends takes effect one call later

def unexpected source · line 519 · raw

@s:String -> St

def end source · line 526 · raw

@value:Json -> @rest:String -> St

def emit source · line 534 · raw

@v:Json -> @s:String -> @stack:List<&2, Frame> -> St

a finished value goes into the container above it

def num_token source · line 550 · raw

@l:NLex -> @stack:List<&2, Frame> -> St

def mk_str source · line 557 · raw

@s:String -> Json

def mk_true source · line 560 · raw

@s:String -> Json

def mk_false source · line 563 · raw

@s:String -> Json

def mk_null source · line 566 · raw

@s:String -> Json

def value source · line 569 · raw

@s:String -> @stack:List<&2, Frame> -> St

def key source · line 586 · raw

@l:Lex -> @stack:List<&2, Frame> -> St

def close_arr source · line 595 · raw

@t:String -> @stack:List<&2, Frame> -> St

def close_obj source · line 602 · raw

@t:String -> @stack:List<&2, Frame> -> St

def comma source · line 609 · raw

@t:String -> @stack:List<&2, Frame> -> St

def dispatch source · line 618 · raw

@mode:Mode -> @s:String -> @stack:List<&2, Frame> -> St

def loop source · line 660 · raw

@fuel:Nat -> @st:St -> St

every step eats a token, so the input's length bounds the steps

def locate source · line 670 · raw

@n:Nat -> @s:String -> @+line:U32 -> @+col:U32 -> Loc

def position.go source · line 679 · raw

@r:Reason -> @+offset:U32 -> @l:Loc -> Error

def lines source · line 689 · raw

@s:String -> @+at:U32 -> @bs:List<&2, U32> -> Lines

def line_col source · line 700 · raw

@bs:List<&2, U32> -> @+at:U32 -> @+line:U32 -> @+m:U32 -> Loc

the line and column of offset at: one line per break before it, and the column counts from the last of them (m is one past it, 0 if none)

def error source · line 708 · raw

@ls:Lines -> @r:Reason -> @left:U32 -> Error

def finish source · line 714 · raw

@ls:Lines -> @st:St -> Result<&2, &2, Error, Json>

def skip_bom source · line 724 · raw

@s:String -> String

RFC 8259 §8.1: a parser MAY skip a leading byte order mark

def parse source · line 732 · raw

@+s:String -> Result<&2, &2, Error, Json>

RFC 8259 §2: JSON-text = ws value ws

def bad_utf8 source · line 738 · raw

@+at:U32 -> @+before:String -> Error

def parse_text source · line 741 · raw

@t:0x33fa1e8e9ce79cb0b4983b81c36ecdd3/utf8/utf8.Text -> Result<&2, &2, Error, Json>

def parse_bytes source · line 749 · raw

@bs:List<&2, U32> -> Result<&2, &2, Error, Json>

provisional: parse raw bytes (0..255), which must be UTF-8

def digit_char source · line 757 · raw

@d:Digit -> Char

def lead_char source · line 780 · raw

@l:Lead -> Char

def digits_k source · line 801 · raw

@ds:List<&2, Digit> -> @k:String -> String

def int_k source · line 808 · raw

@i:Int -> @k:String -> String

def frac_k source · line 815 · raw

@f:Frac -> @k:String -> String

def sign_k source · line 822 · raw

@s:Sign -> @k:String -> String

def exp_k source · line 831 · raw

@e:Exp -> @k:String -> String

def neg_k source · line 838 · raw

@neg:Bool -> @k:String -> String

def num_k source · line 845 · raw

@n:Number -> @k:String -> String

def digits_out source · line 851 · raw

@ds:List<&2, Digit> -> @out:String -> String

the same text, pushed onto a reversed output: a tail call per digit

def int_out source · line 858 · raw

@i:Int -> @out:String -> String

def frac_out source · line 865 · raw

@f:Frac -> @out:String -> String

def sign_out source · line 872 · raw

@s:Sign -> @out:String -> String

def exp_out source · line 881 · raw

@e:Exp -> @out:String -> String

def neg_out source · line 888 · raw

@neg:Bool -> @out:String -> String

def num_out source · line 895 · raw

@n:Number -> @out:String -> String

def num_text source · line 900 · raw

@n:Number -> String

def hex_char source · line 903 · raw

@+x:U32 -> Char

def ctrl_text source · line 907 · raw

@+c:Char -> String

the escape of a control char

def put source · line 924 · raw

@chunk:String -> @out:String -> String

output is built reversed: put pushes a chunk onto it

def esc_char source · line 927 · raw

@k:Class -> @+c:Char -> @out:String -> String

def escape source · line 938 · raw

@s:String -> @out:String -> String

def quote source · line 945 · raw

@s:String -> @out:String -> String

def put_copy source · line 950 · raw

@chunk:String -> @out:String -> String

put, for a chunk used again: it pushes new chars, so the chunk is only read and never shared (sharing any String counts references on all)

def indent source · line 957 · raw

@n:Nat -> @+unit:String -> @out:String -> String

def br source · line 965 · raw

@pretty:Bool -> @+unit:String -> @n:Nat -> @out:String -> String

a line break then the indent of depth n; nothing when compact

def colon source · line 972 · raw

@pretty:Bool -> @out:String -> String

def opener source · line 979 · raw

@more:Bool -> @c:Char -> @out:String -> String

def show source · line 988 · raw

@j:Json -> @+more:Bool -> @+pretty:Bool -> @+unit:String -> @+d:Nat -> @out:String -> String

more: j is the tail of a container that already printed its first item; items are tail calls, so only nesting grows the stack

def show_all source · line 1028 · raw

@items:List<&2, Item> -> @+pretty:Bool -> @+unit:String -> @out:String -> String

def print_loop source · line 1035 · raw

@fuel:Nat -> @items:List<&2, Item> -> @+pretty:Bool -> @+unit:String -> @out:String -> String

def print_fuel source · line 1066 · raw

Nat

def encode source · line 1069 · raw

@j:Json -> String

def pretty source · line 1073 · raw

@j:Json -> @unit:String -> String

unit is the indent of one level, e.g. " "

def num.go source · line 1079 · raw

@l:NLex -> Maybe<&2, Json>

def num source · line 1087 · raw

@s:String -> Maybe<&2, Json>

a number from its text, if the text is a JSON number

def num_u32.go source · line 1090 · raw

@m:Maybe<&2, Json> -> Json

def num_u32 source · line 1097 · raw

@x:U32 -> Json

def num_f32 source · line 1101 · raw

@x:F32 -> Maybe<&2, Json>

None for inf and nan

def is_ok source · line 1107 · raw

@r:Result<&2, &2, Error, Json> -> Bool

def is_null source · line 1114 · raw

@j:Json -> Bool

def kind source · line 1143 · raw

@j:Json -> JKind

def expected source · line 1158 · raw

@want:JKind -> @j:Json -> Access

def string source · line 1161 · raw

@j:Json -> Result<&2, &2, Access, String>

def bool source · line 1168 · raw

@j:Json -> Result<&2, &2, Access, Bool>

def number source · line 1176 · raw

@j:Json -> Result<&2, &2, Access, Number>

the number exactly as written, for what u32 and f32 cannot hold

def array source · line 1184 · raw

@j:Json -> Result<&2, &2, Access, List<&2, Json>>

the items, in order

def object source · line 1192 · raw

@j:Json -> Result<&2, &2, Access, List<&2, Field>>

the fields, in order, duplicates kept

def lead_digit source · line 1205 · raw

@l:Lead -> Digit

def digit_nat source · line 1226 · raw

@d:Digit -> Nat

def dlen source · line 1249 · raw

@ds:List<&2, Digit> -> @+n:Nat -> Nat

def frac_digits source · line 1256 · raw

@f:Frac -> List<&2, Digit>

def with_point.go source · line 1268 · raw

@n:Nat -> @l:Lead -> @ds:List<&2, Digit> -> @f:Frac -> Digits

n is counted first: passing ds on before a read of it would share it

def with_point source · line 1271 · raw

@i:Int -> @f:Frac -> Digits

def nat_min.go source · line 1280 · raw

@le:Bool -> @+a:Nat -> @+b:Nat -> Nat

the smaller of two Nats; Base's Nat.min counts down one by one, which overflows the stack on large values, where Nat.is_le runs natively

def nat_min source · line 1287 · raw

@+a:Nat -> @+b:Nat -> Nat

def exp_val source · line 1292 · raw

@ds:List<&2, Digit> -> @+acc:Nat -> Nat

an exponent's value, held at 2^32 - 1 once past it: past any input's length, so a larger one decides nothing differently

def exp_up source · line 1299 · raw

@e:Exp -> Nat

def exp_down source · line 1308 · raw

@e:Exp -> Nat

def drop_lead source · line 1319 · raw

@ds:List<&2, Digit> -> @+z:Nat -> Lead0

def drop_zeros source · line 1326 · raw

@ds:List<&2, Digit> -> List<&2, Digit>

def rev_digits source · line 1333 · raw

@ds:List<&2, Digit> -> @acc:List<&2, Digit> -> List<&2, Digit>

def strip_trailing source · line 1341 · raw

@ds:List<&2, Digit> -> List<&2, Digit>

trailing zeros do not change the value

def dvalue source · line 1344 · raw

@ds:List<&2, Digit> -> @+acc:Nat -> Nat

def times10 source · line 1351 · raw

@n:Nat -> @+acc:Nat -> Nat

def u32.fits.go source · line 1358 · raw

@ok:Bool -> @+v:Nat -> Result<&2, &2, Access, U32>

def u32.fits source · line 1365 · raw

@+v:Nat -> Result<&2, &2, Access, U32>

def u32.whole source · line 1368 · raw

@ok:Bool -> @sig:List<&2, Digit> -> @+shift:Nat -> Result<&2, &2, Access, U32>

def u32.sig source · line 1377 · raw

@+k:Nat -> @neg:Bool -> @sig:List<&2, Digit> -> @+hi:Nat -> @+low:Nat -> Result<&2, &2, Access, U32>

hi is where the point falls plus the leading zeros and the negative exponent moved across; lo is the digits' count plus the same

def u32.trail source · line 1386 · raw

@neg:Bool -> @+sig:List<&2, Digit> -> @+hi:Nat -> @+low:Nat -> Result<&2, &2, Access, U32>

def u32.lead source · line 1389 · raw

@neg:Bool -> @l:Lead0 -> @+point:Nat -> @+up:Nat -> @+down:Nat -> Result<&2, &2, Access, U32>

def u32.digits source · line 1394 · raw

@neg:Bool -> @d:Digits -> @+e:Exp -> Result<&2, &2, Access, U32>

def u32.num source · line 1399 · raw

@n:Number -> Result<&2, &2, Access, U32>

def u32 source · line 1405 · raw

@j:Json -> Result<&2, &2, Access, U32>

a whole number from 0 to 2^32 - 1, however it is written: 1e2, 100.0

def finite source · line 1413 · raw

@+x:F32 -> Bool

not infinite or NaN: an F32's exponent bits are all ones only for those

def f32.fin source · line 1416 · raw

@ok:Bool -> @+x:F32 -> Result<&2, &2, Access, F32>

def f32.go source · line 1423 · raw

@m:Maybe<&2, F32> -> Result<&2, &2, Access, F32>

def f32 source · line 1432 · raw

@j:Json -> Result<&2, &2, Access, F32>

the nearest F32: past 2^24 not every whole number has one, and a number past the largest F32 (about 3.4e38) is OutOfRange, not infinity

def index.go source · line 1439 · raw

@xs:List<&2, Json> -> @n:Nat -> @+i:U32 -> Result<&2, &2, Access, Json>

def index source · line 1449 · raw

@j:Json -> @+i:U32 -> Result<&2, &2, Access, Json>

the item at index i of an array

def same source · line 1458 · raw

@a:String -> @b:String -> @ok:Bool -> Bool

whether two strings are equal, by reading them only: String.eq hands its strings back, which would share them

def get.keep source · line 1467 · raw

@hit:Bool -> @v:Json -> @found:Maybe<&2, Json> -> Maybe<&2, Json>

def get.go source · line 1475 · raw

@fs:List<&2, Field> -> @+k:String -> @found:Maybe<&2, Json> -> Maybe<&2, Json>

the last field named k: a later duplicate overrides, so every field is read

def get.fin source · line 1482 · raw

@m:Maybe<&2, Json> -> @k:String -> Result<&2, &2, Access, Json>

def get source · line 1490 · raw

@j:Json -> @+k:String -> Result<&2, &2, Access, Json>

the value of key k in an object; the last one wins on duplicates

def kind_name source · line 1497 · raw

@k:JKind -> String

def ident_char source · line 1514 · raw

@+x:U32 -> @first:Bool -> Bool

a key that reads unambiguously after a dot: a letter or _, then letters, digits or _

def ident.go source · line 1518 · raw

@s:String -> @first:Bool -> @ok:Bool -> Bool

def ident source · line 1525 · raw

@k:String -> Bool

def key_text source · line 1531 · raw

@plain:Bool -> @k:String -> @out:String -> String

a key as a path writes it, pushed onto a reversed output: .key when plain, else ["key"] as JSON writes the string, so a dot or bracket in a key reads as part of it

def path_text source · line 1538 · raw

@p:List<&2, Step> -> @out:String -> String

def message_access source · line 1548 · raw

@a:Access -> String

e.g. "$.user.tags[0]: expected string, found number"

def with_path source · line 1561 · raw

@done:List<&2, Step> -> @a:Access -> Access

an error found after walking done (reversed): its path gets done in front

def twice source · line 1578 · raw

@s:String -> @a:String -> @b:String -> Twice

def at.next source · line 1585 · raw

@r:Result<&2, &2, Access, Json> -> @done:List<&2, Step> -> @go:(@_:Json -> @_:List<&2, Step> -> Result<&2, &2, Access, Hit>) -> Result<&2, &2, Access, Hit>

def at.key source · line 1592 · raw

@k:Twice -> @j:Json -> @done:List<&2, Step> -> @go:(@_:Json -> @_:String -> @_:List<&2, Step> -> Result<&2, &2, Access, Hit>) -> Result<&2, &2, Access, Hit>

def at.go source · line 1598 · raw

@steps:List<&2, Step> -> @j:Json -> @done:List<&2, Step> -> Result<&2, &2, Access, Hit>

a key is both looked up and kept in the path, so the lookup gets a copy

def at.fin source · line 1607 · raw

@r:Result<&2, &2, Access, Hit> -> Result<&2, &2, Access, Json>

def at source · line 1615 · raw

@j:Json -> @path:List<&2, Step> -> Result<&2, &2, Access, Json>

the value at a path of keys and indexes

def copy_bool source · line 1623 · raw

@b:Bool -> Bool

def copy_text source · line 1630 · raw

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

def copy_digit source · line 1637 · raw

@d:Digit -> Digit

def copy_digits source · line 1660 · raw

@ds:List<&2, Digit> -> @acc:List<&2, Digit> -> List<&2, Digit>

def copy_lead source · line 1667 · raw

@l:Lead -> Lead

def copy_int source · line 1688 · raw

@i:Int -> Int

def copy_frac source · line 1695 · raw

@f:Frac -> Frac

def copy_sign source · line 1702 · raw

@s:Sign -> Sign

def copy_exp source · line 1711 · raw

@e:Exp -> Exp

def copy_leaf source · line 1720 · raw

@j:Json -> Json

a scalar copied; an array or object becomes an empty one, which keeps its kind for the error a scalar read gives

def last_key.pick source · line 1735 · raw

@hit:Bool -> @here:Nat -> @found:Nat -> Nat

def last_key source · line 1743 · raw

@fs:List<&2, Field> -> @+k:String -> @+i:Nat -> @found:Nat -> Nat

the position of the last field named k, plus one; 0n when there is none

def missing source · line 1750 · raw

@done:List<&2, Step> -> Result<&2, &2, Access, Leaf>

def walk source · line 1761 · raw

@fuel:Nat -> @steps:List<&2, Step> -> @mode:Nat -> @n:Nat -> @j:Json -> @fs:List<&2, Field> -> @xs:List<&2, Json> -> @done:List<&2, Step> -> Result<&2, &2, Access, Leaf>

a read-only walk: it passes parts of j on as they are and never keeps them, so the caller can read j again. It stays in one def, with a mode for where it is: 0n at j; 1n at field n (plus one, 0n for none) of fs; 2n skipping n fields of fs; 3n skipping n items of xs

def read_at.fin source · line 1790 · raw

@-A:Data -> @r:Result<&2, &2, Access, A> -> @done:List<&2, Step> -> Result<&2, &2, Access, A>

def read_at.leaf source · line 1797 · raw

@-A:Data -> @r:Result<&2, &2, Access, Leaf> -> @f:(@_:Json -> Result<&2, &2, Access, A>) -> Result<&2, &2, Access, A>

def read_at source · line 1806 · raw

@-A:Data -> @j:Json -> @path:List<&2, Step> -> @f:(@_:Json -> Result<&2, &2, Access, A>) -> Result<&2, &2, Access, A>

a level A read of a copy of the value at a path; its error gets the full path

def string_at source · line 1809 · raw

@j:Json -> @path:List<&2, Step> -> Result<&2, &2, Access, String>

def bool_at source · line 1812 · raw

@j:Json -> @path:List<&2, Step> -> Result<&2, &2, Access, Bool>

def u32_at source · line 1815 · raw

@j:Json -> @path:List<&2, Step> -> Result<&2, &2, Access, U32>

def f32_at source · line 1818 · raw

@j:Json -> @path:List<&2, Step> -> Result<&2, &2, Access, F32>

def number_at source · line 1821 · raw

@j:Json -> @path:List<&2, Step> -> Result<&2, &2, Access, Number>

def array_at source · line 1824 · raw

@j:Json -> @path:List<&2, Step> -> Result<&2, &2, Access, List<&2, Json>>

def object_at source · line 1827 · raw

@j:Json -> @path:List<&2, Step> -> Result<&2, &2, Access, List<&2, Field>>

def map source · line 1833 · raw

@-A:Data -> @-B:Data -> @r:Result<&2, &2, Access, A> -> @f:(@_:A -> B) -> Result<&2, &2, Access, B>

def both source · line 1841 · raw

@-A:Data -> @-B:Data -> @-C:Data -> @r1:Result<&2, &2, Access, A> -> @r2:Result<&2, &2, Access, B> -> @f:(@_:A -> @_:B -> C) -> Result<&2, &2, Access, C>

two reads, joined by f; the first error wins

def reason source · line 1853 · raw

@r:Reason -> String

def position source · line 1877 · raw

@r:Reason -> @+offset:U32 -> @s:String -> Error

the error at an offset of s, with its line and column

def message source · line 1881 · raw

@e:Error -> String

e.g. "3:5: unexpected ','"

Templates

template token source · line 543 · raw

@-mk:(@_:String -> Json) -> @l:Lex -> @stack:List<&2, Frame> -> St