Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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
You can’t perform that action at this time.