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 (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: {x : String | x != ""}) : Json

parseFile

Parses a JSON file at path.
def parseFile (path: {p : String | p != ""}) : 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: {p : String | p != ""}) (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: {x : Int | x >= 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 (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