Zygote of a JSON parser
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) |] | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment