Zygote of a JSON parser

JSON.idr

module JSON

import Data.HVect

import Control.Monad.Identity

import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Strings

%default total



data Query = INT
           | FLOAT
           | STRING
           | MANY Query
           | NTIMES Nat Query
           | MAYBE Query
           | ARR (Vect n Query)
           | OBJ (Vect n (String, Query))

vmap : (a -> b) -> Vect n a -> Vect n b
vmap f [] = []
vmap f (x::xs) = f x :: vmap f xs


mutual
  %assert_total
  interp : Query -> Type
  interp INT = Integer
  interp FLOAT = Float
  interp STRING = String
  interp (MANY q) = List (interp q)
  interp (NTIMES n q) = Vect n (interp q)
  interp (MAYBE q) = Maybe (interp q)
  interp (ARR qs) = HVect (vmap interp qs)
  interp (OBJ fs) = HVect (vmap interpField fs)

  interpField : (String, Query) -> Type
  interpField (name, q) = (String, interp q)

data JSONErr = Expected String String
             | EOF
             | Failure

partial
decimal : Parser (List (Fin 10))
decimal = some digit

partial --TODO : exponential notation
float : Parser Float
float = do i <- integer
           rest <- opt (char '.' $> decimal)
           let i' = fromInteger i
           pure $ if i' < 0 then i' - toFracPart rest else i' + toFracPart rest
  where floatDigit : Fin n -> Float
        floatDigit fZ = 0.0
        floatDigit (fS f) = 1.0 + floatDigit f
        toFracPart' : Nat -> List (Fin 10) -> Float
        toFracPart' _ [] = 0
        toFracPart' p (d::ds) = (1.0 / pow 10.0 p) * floatDigit d + toFracPart' (S p) ds
        toFracPart : Maybe (List (Fin 10)) -> Float
        toFracPart Nothing   = 0.0
        toFracPart (Just ds) = toFracPart' 1 ds

partial
str : Parser String
str = char '\"' $> stringContents
  where total
        isControl : Char -> Bool
        isControl '\"' = True
        isControl '\\' = True
        isControl '/' = True
        isControl 'b' = True
        isControl 'f' = True
        isControl 'n' = True
        isControl 'r' = True
        isControl 't' = True
        isControl _ = False

        partial
        stringContents : Parser String
        stringContents = (char '\"' $> pure "")
                         <|> (do char '\\'
                                 control <- satisfy isControl --todo unicode literals
                                 rest <- stringContents
                                 pure ('\\' `strCons` (control `strCons` rest)))
                         <|> (do here <- satisfy (const True)
                                 rest <- stringContents
                                 pure (strCons here rest))

partial
theStr : String -> Parser String
theStr s = (do s' <- str
               if s' == s
                 then pure s'
                 else empty) <?> "the string " ++ s

partial
comma : Parser ()
comma = space <$ char ',' <$ space

partial
colon : Parser ()
colon = space <$ char ':' <$ space

partial
inArr : Parser a -> Parser a
inArr p = do char '[' ; space ; res <- p ; space ; char ']' ; pure res

partial
inObj : Parser a -> Parser a
inObj p = do char '{' ; space ; res <- p ; space ; char '}' ; pure res

partial
parseArr : Parser a -> Parser (List a)
parseArr p = inArr (sepBy p comma)

partial
parseArrN : (n : Nat) -> Parser a -> Parser (Vect n a)
parseArrN n p = inArr (sepByN n p comma)

parseNull : Parser ()
parseNull = string "null"

partial
parseNullable : Parser a -> Parser (Maybe a)
parseNullable p = parseNull $> pure Nothing <|> [| Just p |]




partial
parseJSON : (q : Query) -> Parser (interp q)
parseJSON INT = integer -- TODO : exponential notation
parseJSON FLOAT = float
parseJSON STRING = str
parseJSON (MANY q) = parseArr (parseJSON q)
parseJSON (NTIMES n q) = parseArrN n (parseJSON q)
parseJSON (MAYBE q) = parseNullable (parseJSON q)
parseJSON (ARR qs) = inArr (parseArr qs)
  where partial
        parseArr' : (qs : Vect n Query) -> Parser (HVect (vmap interp qs))
        parseArr' [] = pure []
        parseArr' (q :: qs) = [| HVect.(::) (comma $> parseJSON q) (parseArr' qs) |]
        partial
        parseArr : (qs : Vect n Query) -> Parser (HVect (vmap interp qs))
        parseArr [] = pure []
        parseArr (q::qs) = [| HVect.(::) (parseJSON q) (parseArr' qs) |]
parseJSON (OBJ fs) = inObj (parsePairs fs) -- TODO: make it order-invariant, add non-strict version
  where partial
        parseField : (f : (String, Query)) -> Parser (interpField f)
        parseField (name, q) = map (\v => (name, v)) (theStr name $> colon $> parseJSON q)
        partial
        parsePairs' : (fs : Vect n (String, Query)) -> Parser (HVect (vmap interpField fs))
        parsePairs' [] = pure []
        parsePairs' (f::fs) = [| HVect.(::) (comma $> parseField f) (parsePairs' fs) |]
        partial
        parsePairs : (fs : Vect n (String, Query)) -> Parser (HVect (vmap interpField fs))
        parsePairs [] = pure []
        parsePairs (f::fs) = [| HVect.(::) (parseField f) (parsePairs' fs) |]