# JSON Parser

```idris
module Parser.JSON

import public Parser
import public Parser.Numbers

import Control.Monad.Eval

import Structures.Dependent.DList
```

```idris hide
import System
import Derive.Prelude
import Generics.Derive

%hide Generics.Derive.Eq
%hide Generics.Derive.Ord
%hide Generics.Derive.Show

%language ElabReflection
```

## JSON components

Types a JSON value is allowed to have

```idris
public export
data JSONType : Type where
  TObject : JSONType
  TArray : JSONType
  TString : JSONType
  TNumber : JSONType
  TBool : JSONType
  TNull : JSONType
%runElab derive "JSONType" [Generic, Meta, Eq, Ord, Show, DecEq]
%name JSONType type, type2, type3
```

A JSON value indexed by its type

```idris
public export
data JSONValue : JSONType -> Type where
  VObject : {types : List JSONType} 
    -> DList JSONType (\t => (String, JSONValue t)) types -> JSONValue TObject
  VArray : {types : List JSONType}
    -> DList JSONType JSONValue types -> JSONValue TArray
  VString : (s : String) -> JSONValue TString
  VNumber : (d : Double) -> JSONValue TNumber
  VBool : (b : Bool) -> JSONValue TBool
  VNull : JSONValue TNull
%name JSONValue value, value2, value3
```

```idris hide
export
Show (JSONValue t) where
  show (VObject xs) = 
    let xs = dMap (\_,(key, value) => "\"\{key}\":\{show value}") xs
    in assert_total $ "{\{joinBy "," xs}}"
  show (VArray xs) = 
    let xs = dMap (\_,e => show e) xs
    in assert_total $ "[\{joinBy "," xs}]"
  show (VString s) = "\"\{s}\""
  show (VNumber d) = show d
  show (VBool False) = "false"
  show (VBool True) = "true"
  show VNull = "null"

-- TODO: Deal with keys potentially having different orders in different objects
export
Eq (JSONValue t) where
  (VObject xs) == (VObject ys) = 
    assert_total $ xs $== ys
  (VArray xs) == (VArray ys) = 
    assert_total $ xs $== ys
  (VString s) == (VString str) = s == str
  (VNumber d) == (VNumber dbl) = d == dbl
  (VBool b) == (VBool x) = b == x
  VNull == VNull = True

%hide Language.Reflection.TT.WithFC.value
```

### JSON Functions

`foldl` Analog for consuming a JSON structure by values. Ignores the keys in
objects.

```idris
export
dFoldL : {t : JSONType} 
  -> (acc -> (type : JSONType) -> (val : JSONValue type) -> acc) 
  -> acc -> JSONValue t -> acc
dFoldL f acc' (VObject xs) = 
  let recur : acc -> (v : JSONType) -> (String, JSONValue v) -> acc
      recur acc' v (key, value) = dFoldL f acc' value
  in DList.dFoldL recur acc' xs
dFoldL f acc' (VArray xs) = 
  let recur : acc -> (v : JSONType) -> JSONValue v -> acc
      recur acc' v value = dFoldL f acc' value
  in DList.dFoldL recur acc' xs
dFoldL f acc (VString s) = f acc _ (VString s)
dFoldL f acc (VNumber d) = f acc _ (VNumber d)
dFoldL f acc (VBool b) = f acc _ (VBool b)
dFoldL f acc VNull = f acc _ VNull
```

Look up a property in an object

```idris
export
getProperty : (prop : String) -> (object : JSONValue TObject)
  -> Maybe (type : JSONType ** JSONValue type)
getProperty prop (VObject xs) = 
  case dFind (\_, (key, _) => key == prop) xs of
    Nothing => Nothing
    Just (type ** (_, val)) => Just (type ** val)
```

Return the values from an object.

```idris
export
getValues : (object : JSONValue TObject) 
  -> (types : List JSONType ** DList JSONType JSONValue types)
getValues (VObject xs) = 
  dMap' (\t, (k, v) => (t ** v)) xs
```

Recursively apply a filter to a JSON structure.

```idris
export
dFilter : (f : (type : JSONType) -> (val : JSONValue type) -> Bool) 
  -> {t : JSONType} -> JSONValue t -> Maybe (JSONValue t)
dFilter f value = eval $ dFilter' f value
  where
    dFilter' : (f : (type : JSONType) -> (val : JSONValue type) -> Bool) 
      -> {t : JSONType} -> JSONValue t -> Eval $ Maybe (JSONValue t)
    dFilter' f (VObject xs) = do
      True <- pure $ f _ (VObject xs)
        | _ => pure Nothing
      let xs = toList xs
      xs : List (Maybe (x : JSONType ** (String, JSONValue x))) <- 
        traverse
          (\(t ** (k, v)) => do
            Just v <- dFilter' f v
              | _ => pure Nothing
            pure $ Just (t ** (k, v)))
          xs
      let (_ ** xs) : (t : List JSONType ** DList _ _ t) = 
        fromList $ catMaybes xs
      pure . Just $ VObject xs
    dFilter' f (VArray xs) = do 
      True <- pure $ f _ (VArray xs)
        | _ => pure Nothing
      let xs = toList xs
      xs : List (Maybe (x : JSONType ** JSONValue x)) <- 
        traverse
          (\(t ** v) => do
            Just v <- dFilter' f v
              | _ => pure Nothing
            pure $ Just (t ** v))
          xs
      let (_ ** xs) : (t : List JSONType ** DList _ _ t) = 
        fromList $ catMaybes xs
      pure . Just $ VArray xs
    dFilter' f x =
      pure $ case f _ x of
        False => Nothing
        True => Just x
```

## Parsers

We are going to get mutually recursive here. Instead of using a `mutual` block,
we will use the more modern style of declaring all our types ahead of our
definitions.

```idris
export
object : Parser (JSONValue TObject)
export
array : Parser (JSONValue TArray)
export
string : Parser (JSONValue TString)
export
number : Parser (JSONValue TNumber)
export
bool : Parser (JSONValue TBool)
export
null : Parser (JSONValue TNull)
```

Define a `whitespace` character class based on the json specifications

```idris
whitespace : Parser Char
whitespace = do
  pnote "Whitespace character"
  theseChars [' ', '\n', '\r', '\t']
```

Convenience function

```idris
dpairize : {t : JSONType} -> 
  Parser (JSONValue t) -> Parser (t' : JSONType ** JSONValue t')
dpairize x = do
  x <- x
  pure (_ ** x)
```

Top level json value parser

```idris
export 
value : Parser (t : JSONType ** JSONValue t)
value = do 
  pnote "JSON Value"
  surround whitespace $ oneOfE 
    "Expected JSON Value" 
    [
      dpairize object
    , dpairize array
    , dpairize string
    , dpairize number
    , dpairize bool
    , dpairize null
    ]
```

Now go through our json value types

```idris
object = do
  pnote "JSON Object"
  oneOfE 
    "Expected Object" 
    [emptyObject, occupiedObject]
  where
    emptyObject : Parser (JSONValue TObject)
    emptyObject = do
      delimited '{' '}' (nom whitespace)
      pure $ VObject Nil
    keyValue : Parser (t : JSONType ** (String, JSONValue t))
    keyValue = do
      VString key <- surround whitespace string
      _ <- charExact ':'
      (typ ** val) <- value
      pure (typ ** (key, val))
    restKeyValue : Parser (t : JSONType ** (String, JSONValue t))
    restKeyValue = do
      _ <- charExact ','
      keyValue
    pairs : Parser (List1 (t : JSONType ** (String, JSONValue t)))
    pairs = do
      first <- keyValue
      rest <- many restKeyValue
      -- TODO: headTail combinator for this
      pure $ first ::: rest
    occupiedObject : Parser (JSONValue TObject)
    occupiedObject = do
      val <- delimited '{' '}' pairs
      let (types ** xs) = DList.fromList (forget val)
      pure $ VObject xs
```

```idris
array = do
  pnote "JSON Array"
  oneOfE 
    "Expected Array" 
    [emptyArray, occupiedArray]
  where
    emptyArray : Parser (JSONValue TArray)
    emptyArray = do
      delimited '[' ']' (nom whitespace)
      pure $ VArray Nil
    restValue : Parser (t : JSONType ** JSONValue t)
    restValue = do
      _ <- charExact ','
      value
    values : Parser (List1 (t : JSONType ** JSONValue t))
    values = do
      first <- value
      rest <- many restValue
      pure $ first ::: rest 
    occupiedArray : Parser (JSONValue TArray)
    occupiedArray = do
      xs <- delimited '[' ']' values
      let (types ** xs) = DList.fromList (forget xs)
      pure $ VArray xs
```

```idris
string = do
  pnote "JSON String"
  str <- liftString $ delimited '"' '"' (many stringCharacter)
  pure $ VString str
  where
    -- TODO: Handle control characters properly
    stringCharacter : Parser Char
    stringCharacter = do
      result <- charPredicate (not . (== '"'))
      case result of
        GotChar char => pure char
        GotError err =>
          throwParseError "Expected string character, got \{show err}"
        EndOfInput => throwParseError "Unexpected end of input"
```

```idris
number = do
  pnote "JSON Number"
  d <- double
  pure $ VNumber d
```

```idris
bool = do
  pnote "JSON Bool"
  oneOfE
    "Expected Bool"
    [true, false]
  where
    true : Parser (JSONValue TBool)
    true = do
      _ <- exactString "true" 
      pure $ VBool True
    false : Parser (JSONValue TBool)
    false = do
      _ <- exactString "false" 
      pure $ VBool False
```

```idris
null = do
  pnote "JSON null"
  _ <- exactString "null"
  pure VNull
```

## Unit tests

Quick smoke test

```idris
-- @@test JSON Quick Smoke
quickSmoke : IO Bool
quickSmoke = do
  let input = "{\"string\":\"string\",\"number\":5,\"true\":true,\"false\":false,\"null\":null,\"array\":[1,2,3]}"
  putStrLn input
  Right (type ** parsed) <- runFirstIODebug value input
    | Left err => do
      printLn err
      pure False
  putStrLn "Input: \{input}\nOutput: \{show type} -> \{show parsed}"
  let reference_object = 
    VObject [
      ("string", VString "string")
    , ("number", VNumber 5.0)
    , ("true", VBool True)
    , ("false", VBool False)
    , ("null", VNull)
    , ("array", VArray [
        VNumber 1.0
      , VNumber 2.0
      , VNumber 3.0
      ])
    ]
  case type of
    TObject => pure $ parsed == reference_object
    _ => pure False
```