import Data.String
import Data.List
import Data.Maybe
import System.File
import Language.JSON

-- We'll use these two records to demonstrate encoding and
-- decoding of custom types below.
record Response1 where
  constructor MkResponse1
  page : Int
  fruits : List String

record Response2 where
  constructor MkResponse2
  page : Int
  fruits : List String

main : IO ()
main = do
  -- First we'll look at encoding basic data types to
  -- JSON strings. Here are some examples for atomic
  -- values.
  putStrLn $ show $ encode True
  putStrLn $ show $ encode 1
  putStrLn $ show $ encode 2.34
  putStrLn $ show $ encode "gopher"

  -- And here are some for lists and dictionaries, which encode
  -- to JSON arrays and objects as you'd expect.
  let slcD = ["apple", "peach", "pear"]
  putStrLn $ show $ encode slcD

  let mapD = [("apple", 5), ("lettuce", 7)]
  putStrLn $ show $ encode mapD

  -- The JSON package can automatically encode your
  -- custom data types. It will only include exported
  -- fields in the encoded output and will by default
  -- use those names as the JSON keys.
  let res1D = MkResponse1 1 ["apple", "peach", "pear"]
  putStrLn $ show $ encode res1D

  -- Now let's look at decoding JSON data into Idris
  -- values. Here's an example for a generic data
  -- structure.
  let byt = "{\"num\":6.13,\"strs\":[\"a\",\"b\"]}"

  -- We need to provide a type where the JSON
  -- package can put the decoded data. This
  -- `Maybe (List (String, JSON))` will hold a dictionary of strings
  -- to arbitrary data types.
  case decode byt of
    Just (JObject dat) => do
      putStrLn $ show dat
      -- In order to use the values in the decoded map,
      -- we'll need to convert them to their appropriate type.
      -- For example here we convert the value in `num` to
      -- the expected `Double` type.
      case lookup "num" dat of
        Just (JNumber num) => putStrLn $ show num
        _ => putStrLn "Failed to find 'num'"

      -- Accessing nested data requires a series of
      -- pattern matches.
      case lookup "strs" dat of
        Just (JArray strs) => 
          case head' strs of
            Just (JString str1) => putStrLn str1
            _ -> putStrLn "Failed to get first string"
        _ -> putStrLn "Failed to find 'strs'"
    _ -> putStrLn "Failed to parse JSON"

  -- We can also decode JSON into custom data types.
  -- This has the advantages of adding additional
  -- type-safety to our programs and eliminating the
  -- need for type assertions when accessing the decoded
  -- data.
  let str = "{\"page\": 1, \"fruits\": [\"apple\", \"peach\"]}"
  case decode str of
    Just (JObject obj) => 
      case fromJSON obj of
        Just res => do
          putStrLn $ show res
          putStrLn $ show $ head' (fruits res)
        Nothing -> putStrLn "Failed to parse into Response2"
    _ -> putStrLn "Failed to parse JSON"

  -- In the examples above we always used strings as
  -- intermediates between the data and JSON representation.
  -- We can also stream JSON encodings directly to files or
  -- even network connections.
  let d = [("apple", 5), ("lettuce", 7)]
  Right () <- writeFile "output.json" (show $ encode d)
    | Left err => putStrLn $ "Error writing file: " ++ show err
  pure ()