JSON.Parser

Reexports

Definitions

jdouble : String -> Double

  We cannot use `cast` to convert all valid JSON numbers
  to `Double`. Fortunately, both the JavaScript and Scheme
  backends are more tolerant, so we can use a simple FFI call.

escape : SnocList Char -> Char -> SnocList Char

Totality: total
Visibility: public export

encode : String -> String

Totality: total
Visibility: public export

data JSON : Type

Totality: total
Visibility: public export
Constructors:

JNull : JSON

JInteger : Integer -> JSON

JDouble : Double -> JSON

JBool : Bool -> JSON

JString : String -> JSON

JArray : List JSON -> JSON

JObject : List (String, JSON) -> JSON

Hints:

Eq JSON

Show JSON

dropNull : JSON -> JSON

  Recursively drops `Null` entries from JSON objects.

Totality: total
Visibility: export

0 SK : Type -> Type

Totality: total
Visibility: public export

jsonDouble : RExp True

Totality: total
Visibility: export

json : P1 q (BoundedErr Void) JSON

Totality: total
Visibility: public export

parseJSON : Origin -> String -> Either (ParseError Void) JSON

Totality: total
Visibility: export

jsonArray : P1 q (BoundedErr Void) (List JSON)

  A parser that is capable of streaming a single large
  array of JSON values.

Totality: total
Visibility: public export

jsonValues : P1 q (BoundedErr Void) (List JSON)

  Parser that is capable of streaming large amounts of
  JSON values.
  
  Values need not be separated by whitespace but the longest
  possible value will always be consumed.

Totality: total
Visibility: public export