json/value.bend checks

raw source on the hub · import 0x729eecea86ea5a2cdba3a2856a313bca/json/value.bend as Value

json/value: a JSON value. Arrays and objects hold their cells inside the type (JCons, JPair, JNil) rather than in a List, so every traversal is a structural recursion on one argument -- which Bend's termination checker accepts, and which keeps laws provable. Build and read them through the defs below, never by hand.

2 imports

import Base
import ../lazy/lazy.bend as Lazy

Types

type Json source · line 10 · raw

Data

a JSON value; JNil, JCons and JPair are the cells of arrays and objects

JNull
```
Json
```
JBool
```
@b:Bool -> Json
```
JNum
```
@raw:String -> Json
```
JStr
```
@s:String -> Json
```
JArr
```
@items:Json -> Json
```
JObj
```
@pairs:Json -> Json
```
JNil
```
Json
```
JCons
```
@head:Json -> @tail:Json -> Json
```

JPair

@key:String -> @val:Json -> @rest:Json -> Json

Definitions

def reverse source · line 22 · raw

@cells:Json -> @acc:Json -> Json

reverses a chain of JCons or JPair cells onto acc

def arr.go source · line 32 · raw

@items:List<&2, Json> -> Json

builders

def arr source · line 40 · raw

@items:List<&2, Json> -> Json

an array from a list

def obj.go source · line 43 · raw

@pairs:List<&1, Pair(String, Json)> -> Json

def obj source · line 51 · raw

@pairs:List<&1, Pair(String, Json)> -> Json

an object from pairs

def num source · line 55 · raw

@n:U32 -> Json

a number

def find source · line 60 · raw

@cells:Json -> @+key:String -> Json

accessors: a missing key or a wrong kind reads as JNull / None / the default, so paths chain: get(get(msg, "params"), "textDocument")

def get source · line 69 · raw

@j:Json -> @key:String -> Json

an object's value at a key; JNull when it is not an object or has no such key

def str_or source · line 77 · raw

@j:Json -> @default:String -> String

a string's text, else the default

def u32_or source · line 85 · raw

@j:Json -> @default:U32 -> U32

a number as a U32, else the default

def first source · line 93 · raw

@j:Json -> Json

an array's first item