Json

Imports
open Array;
Table of Contents

Types

Json

(type)
type Json

Constructors

For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.

Json (opaque · mk*)

mkNull

def mkNull : Json

mkBool

def mkBool (b : Bool) : Json

mkInt

def mkInt (i : Int) : Json

mkFloat

def mkFloat (f : Float) : Json

mkString

def mkString (s : String) : Json

mkArray

def mkArray (1 xs : Array Json) : Json

mkObject

An empty JSON object. Use setKey to populate.
def mkObject : Json

Functions

json

def json : Unit

parse

Parses a JSON string. Raises at runtime on malformed input.
def parse (s : String | s ≠ "") : Json

parseFile

Parses a JSON file at path.
def parseFile (path : String | path ≠ "") : Json

stringify

Serializes a Json value to its string form. The result is always non-empty (json.dumps(None) yields "null").
def stringify (j : Json) : {s : String | s ≠ ""}

stringifyPretty

Pretty-prints a Json value with 2-space indentation. Always non-empty.
def stringifyPretty (j : Json) : {s : String | s ≠ ""}

writeFile

Writes a Json value to a file.
def writeFile (path : String | path ≠ "") (j : Json) : Unit

isNull

def isNull (j : Json) : Bool

isBool

def isBool (j : Json) : Bool

isNumber

def isNumber (j : Json) : Bool

isString

def isString (j : Json) : Bool

isArray

def isArray (j : Json) : Bool

isObject

def isObject (j : Json) : Bool

asBool

def asBool (j : Json) : Bool

asInt

def asInt (j : Json) : Int

asFloat

def asFloat (j : Json) : Float

asString

def asString (j : Json) : String

has

Returns true if j is an object containing key.
def has (j : Json) (key : String) : Bool

get

Looks up a key in a JSON object. Raises at runtime if j is not an object or key is absent.
def get (j : Json) (key : String) : Json

length

Returns the length of an array (or string/object). Raises if j has no len.
def length (j : Json) : {x : Int | x ≥ 0}

at

Indexes into a JSON array. Raises at runtime if i is out of range.
def at (j : Json) (i : Int | i ≥ 0) : Json

mkNull

def mkNull : Json

mkBool

def mkBool (b : Bool) : Json

mkInt

def mkInt (i : Int) : Json

mkFloat

def mkFloat (f : Float) : Json

mkString

def mkString (s : String) : Json

mkArray

def mkArray (1 xs : Array Json) : Json

mkObject

An empty JSON object. Use setKey to populate.
def mkObject : Json

setKey

Returns a new object with key set to value. Raises at runtime if j is not an object.
def setKey (j : Json) (key : String) (value : Json) : Json