json

Json.parse

def Json.parse (s : String) : Either String Json

Parses a JSON text; the error names the character position (0-based) where parsing stopped.

Json.decode

def Json.decode {A : Type} (d : Json -> Either String A) (s : String) : Either String A

Parses a JSON text and decodes it; errors carry a path from the root ($).

Json.natOf

def Json.natOf (m : Option Nat) : Either String Nat

The natural number a parse produced, or the decoding error.

Json.intOf

def Json.intOf (t : String) (m : Option Nat) : Either String Int

An integer from its text: a natural number, or else a minus sign and a natural number.

Json.intNeg

def Json.intNeg (cs : List Char) : Either String Int

The text of a negative integer: a minus sign and the digits of its absolute value.

Json.intNegOf

def Json.intNegOf (m : Option Nat) : Either String Int

The integer whose absolute value a parse produced (minus zero is zero).

Json.itemSeg

def Json.itemSeg (i : Nat) : String

The path segment of the i-th item of an array: [i].

Json.itemsRest

def Json.itemsRest {A : Type} (r0 : Either String A) (r1 : Either String (List A)) : Either String (List A)

An item and the rest of the items, each already decoded, as a list (the first error wins).

Json.someOf

def Json.someOf {A : Type} (r : Either String A) : Either String (Option A)

A decoded value as just, or the decoding error.

Json.pairRest

def Json.pairRest {A B : Type} (r0 : Either String A) (r1 : Either String B) : Either String (A * B)

The two halves of a pair, each already decoded (the first error wins).

Json.ctorOf

def Json.ctorOf (j : Json) : Either String (String * List (String * Json))

The constructor name (field “k”) and all the fields of an object.

Json.fieldOpt

def Json.fieldOpt {A : Type} (c : String * List (String * Json)) (name : String) (d : Json -> Either String (Option A)) : Either String (Option A)

Like Json.field for a Maybe field: a missing field is nothing, as if it were null.

Json.decNatRT

def Json.decNatRT (n : Nat) : Json.decNat (Json.encNat n) = right n

Decoding an encoded natural number gives it back.

Json.decIntRT

def Json.decIntRT (v : Int) : Json.decInt (Json.encInt v) = right v

Decoding an encoded integer gives it back.

Json.isNull

def Json.isNull (j : Json) : Bool

Whether a JSON value is null.

Json.decOptionNotNull

def Json.decOptionNotNull {A : Type} (d : Json -> Either String A) (j : Json) (e : Json.isNull j = false) : Json.decOption d j = Json.someOf (d j)

On a value that is not null, decoding a Maybe is decoding the value as just.