Extra.idr

module Data.String.Extra

%access public export
%default total

||| Remove the first `n` characters from a string. Returns the empty string if
||| the input string is too short.
drop : (n : Nat) -> (input : String) -> String
drop n str = substr n (length str) str

||| Remove the last `n` characters from a string. Returns the empty string if
||| the input string is too short.
dropLast : (n : Nat) -> (input : String) -> String
dropLast n str = reverse (drop n (reverse str))

||| Remove the first and last `n` characters from a string. Returns the empty
||| string if the input string is too short.
shrink : (n : Nat) -> (input : String) -> String
shrink n str = dropLast n (drop n str)

||| Join the strings from a `Foldable` by the given string.
join : (by : String) -> Foldable t => (xs : t String) -> String
join by xs = drop (length by)
                  (foldl (\acc, x => acc ++ by ++ x) "" xs)

||| Get a character from a string, if it's long enough.
index : (n : Nat) -> (str : String) -> Maybe Char
index n str with (unpack str)
  index n str | [] = Nothing
  index Z str | (x :: xs) = Just x
  index (S k) str | (x :: xs) = index k str | xs

JSON.idr

||| The JSON language, as described at http://json.org/
module Language.JSON

import Data.String.Extra as SE
import Language.JSON.String
-- import Text.Lexer
import Text.Parser

%default total
%access export

Literal : Type -> Type
Literal t = (Lexer, String -> t)

||| Make a TokenMap entry for a lexer which always maps to the same value.
verbatim : Lexer -> tok -> (Lexer, String -> tok)
verbatim l t = (l, const t)

||| Make a TokenMap entry for a Literal.
literal : Literal t -> (t -> tok) -> (Lexer, String -> tok)
literal (l, f) g = (l, g . f)


-- %hide Text.Lexer.stringLit

public export
data JSONValue
   = JSONNull
   | JSONBoolean Bool
   | JSONNumber Double
   | JSONString String
   | JSONArray (List JSONValue)
   | JSONObject (List (String, JSONValue))

%name JSONValue json

mutual
  private
  stringifyArray : List JSONValue -> String
  stringifyArray [] = ""
  stringifyArray (x :: []) = stringify x
  stringifyArray (x :: xs) = stringify x ++ "," ++ stringifyArray xs

  private
  stringifyProp : (String, JSONValue) -> String
  stringifyProp (key, value) = show key ++ ":" ++ stringify value

  private
  stringifyObject : List (String, JSONValue) -> String
  stringifyObject [] = ""
  stringifyObject (x :: []) = stringifyProp x
  stringifyObject (x :: xs) = stringifyProp x ++ "," ++ stringifyObject xs

  ||| Convert a `JSONValue` into its string representation. No whitespace
  ||| is added.
  stringify : JSONValue -> String
  stringify JSONNull = "null"
  stringify (JSONBoolean x) = if x then "true" else "false"
  stringify (JSONNumber x) = show x
  stringify (JSONString x) = show x
  stringify (JSONArray xs) = "[" ++ stringifyArray xs ++ "]"
  stringify (JSONObject xs) = "{" ++ stringifyObject xs ++ "}"

Show JSONValue where
  show = stringify

data Bracket = Open | Close

data JSONToken
   = JTIgnore
   | JTNullLit
   | JTBooleanLit Bool
   | JTNumberLit Double
   | JTStringLit String
   | JTSquare Bracket
   | JTCurly Bracket
   | JTColon
   | JTComma

||| A null literal ("null")
null : Lexer
null = exact "null"

||| A boolean literal ("true" or "false")
boolean : Literal Bool
boolean = (exact "true" <|> exact "false", (== "true"))

||| Recognises a JSON number literal and converts to a Double.
number : Literal Double
number = (numberLit, cast)
  where
    numberLit : Lexer
    numberLit
      = let sign  = opt $ is '-'
            whole = is '0' <|> (range '1' '9' <+> digits)
            frac  = opt $ is '.' <+> digits
            exp   = opt $ like 'e' <+> opt (oneOf "+-") <+> digits in
            sign <+> whole <+> frac <+> exp


jsonTokenMap : TokenMap JSONToken
jsonTokenMap
  = [ verbatim spaces         JTIgnore
    , verbatim (is '{')       (JTCurly Open)
    , verbatim (is '}')       (JTCurly Close)
    , verbatim (is '[')       (JTSquare Open)
    , verbatim (is ']')       (JTSquare Close)
    , verbatim (is ':')       JTColon
    , verbatim (is ',')       JTComma
    , verbatim null           JTNullLit
    , literal boolean         JTBooleanLit
    , literal number          JTNumberLit
    , (stringLit, JTStringLit)
    -- , literal string          JTStringLit
    ]

lexJSON : String -> Maybe (List JSONToken)
lexJSON str
  = case lex jsonTokenMap str of
         (tokens, _, _, "") => Just (map tok tokens)
         _ => Nothing

JSONRule : Type
JSONRule = Grammar JSONToken True JSONValue

syntax match [tok_pat]
  = the (Grammar _ True ()) $
    terminal (\tok => case tok of
                           tok_pat => Just ()
                           _ => Nothing)

mutual
  parseNull : JSONRule
  parseNull
    = do match JTNullLit
         pure JSONNull

  parseBoolean : JSONRule
  parseBoolean = terminal $
    \tok => case tok of
                 JTBooleanLit x => Just (JSONBoolean x)
                 _ => Nothing

  parseNumber : JSONRule
  parseNumber = terminal $
    \tok => case tok of
                 JTNumberLit x => Just (JSONNumber x)
                 _ => Nothing

  rawParseString : Grammar JSONToken True String
  rawParseString = terminal $
    \tok => case tok of
                 JTStringLit x => Just x
                 _ => Nothing

  parseString : JSONRule
  parseString = pure (JSONString !rawParseString)

  parseArray : JSONRule
  parseArray
    = do match (JTSquare Open)
         commit
         xs <- parseArrayValues
         match (JTSquare Close)
         pure (JSONArray xs)
    where
      parseArrayValues : Grammar JSONToken False (List JSONValue)
      parseArrayValues = sepBy (match JTComma) parseJSONValue

  parseObject : JSONRule
  parseObject
    = do match (JTCurly Open)
         commit
         xs <- parseObjectProperties
         match (JTCurly Close)
         pure (JSONObject xs)
    where
      parseObjectProperties : Grammar JSONToken False (List (String, JSONValue))
      parseObjectProperties = sepBy (match JTComma) $
        do key <- rawParseString
           match JTColon
           value <- parseJSONValue
           pure (key, value)

  parseJSONValue : Grammar JSONToken True JSONValue
  parseJSONValue = parseArray
               <|> parseObject
               <|> parseNumber
               <|> parseString
               <|> parseBoolean
               <|> parseNull

parseJSON : String -> Maybe JSONValue
parseJSON x = case (lexJSON x) of
                   Nothing => Nothing
                   Just ts => case (parse ts parseJSONValue) of
                                   Right (v, []) => Just v
                                   _ => Nothing