From d030bd79c5e360b93873f993dc95fa15aaadbae5 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sat, 25 Jan 2025 02:27:25 -0500 Subject: [PATCH] Add JSON Parser --- README.md | 4 + advent.ipkg | 2 + src/Parser/JSON.md | 285 +++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 291 insertions(+) create mode 100644 src/Parser/JSON.md diff --git a/README.md b/README.md index 5e93985..6629953 100644 --- a/README.md +++ b/README.md @@ -75,6 +75,10 @@ solution. Parsers for numerical values in multiple bases + - [JSON](src/Parser/JSON.md) + + JSON Parser + ## Index of years and days - 2015 diff --git a/advent.ipkg b/advent.ipkg index e8aff07..607e26e 100644 --- a/advent.ipkg +++ b/advent.ipkg @@ -19,6 +19,7 @@ depends = base , tailrec , eff , elab-util + , sop , ansi , if-unsolved-implicit , c-ffi @@ -33,6 +34,7 @@ modules = Runner , Parser , Parser.Interface , Parser.Numbers + , Parser.JSON -- main file (i.e. file to load at REPL) main = Main diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md new file mode 100644 index 0000000..6602210 --- /dev/null +++ b/src/Parser/JSON.md @@ -0,0 +1,285 @@ +# JSON Parser + +```idris +module Parser.JSON + +import public Parser +import public Parser.Numbers + +import Structures.Dependent.DList +``` + +```idris hide +import System +import Derive.Prelude +import Generics.Derive + +%hide Generics.Derive.Eq +%hide Generics.Derive.Ord +%hide Generics.Derive.Show + +%language ElabReflection +``` + +## JSON components + +Types a JSON value is allowed to have + +```idris +public export +data JSONType : Type where + TObject : JSONType + TArray : JSONType + TString : JSONType + TNumber : JSONType + TBool : JSONType + TNull : JSONType +%runElab derive "JSONType" [Generic, Meta, Eq, Ord, Show, DecEq] +%name JSONType type, type2, type3 +``` + +A JSON value indexed by its type + +```idris +public export +data JSONValue : JSONType -> Type where + VObject : {types : List JSONType} + -> DList JSONType (\t => (String, JSONValue t)) types -> JSONValue TObject + VArray : {types : List JSONType} + -> DList JSONType JSONValue types -> JSONValue TArray + VString : (s : String) -> JSONValue TString + VNumber : (d : Double) -> JSONValue TNumber + VBool : (b : Bool) -> JSONValue TBool + VNull : JSONValue TNull +%name JSONValue value, value2, value3 +``` + +```idris hide +Show (JSONValue t) where + show (VObject xs) = + let xs = dMap (\_,(key, value) => "\"\{key}\":\{show value}") xs + in assert_total $ "{\{joinBy "," xs}}" + show (VArray xs) = + let xs = dMap (\_,e => show e) xs + in assert_total $ "[\{joinBy "," xs}]" + show (VString s) = "\"\{s}\"" + show (VNumber d) = show d + show (VBool False) = "false" + show (VBool True) = "true" + show VNull = "null" + +-- TODO: Deal with keys potentially having different orders in different objects +Eq (JSONValue t) where + (VObject xs) == (VObject ys) = + assert_total $ xs $== ys + (VArray xs) == (VArray ys) = + assert_total $ xs $== ys + (VString s) == (VString str) = s == str + (VNumber d) == (VNumber dbl) = d == dbl + (VBool b) == (VBool x) = b == x + VNull == VNull = True + +%hide Language.Reflection.TT.WithFC.value +``` + +## Parsers + +We are going to get mutually recursive here. Instead of using a `mutual` block, +we will use the more modern style of declaring all our types ahead of our +definitions. + +```idris +export +object : Parser (JSONValue TObject) +export +array : Parser (JSONValue TArray) +export +string : Parser (JSONValue TString) +export +number : Parser (JSONValue TNumber) +export +bool : Parser (JSONValue TBool) +export +null : Parser (JSONValue TNull) +``` + +Define a `whitespace` character class based on the json specifications + +```idris +whitespace : Parser Char +whitespace = do + pnote "Whitespace character" + theseChars [' ', '\n', '\r', '\t'] +``` + +Convenience function + +```idris +dpairize : {t : JSONType} -> + Parser (JSONValue t) -> Parser (t' : JSONType ** JSONValue t') +dpairize x = do + x <- x + pure (_ ** x) +``` + +Top level json value parser + +```idris +export +value : Parser (t : JSONType ** JSONValue t) +value = do + pnote "JSON Value" + surround whitespace $ oneOfE + "Expected JSON Value" + [ + dpairize object + , dpairize array + , dpairize string + , dpairize number + , dpairize bool + , dpairize null + ] +``` + +Now go through our json value types + +```idris +object = do + pnote "JSON Object" + oneOfE + "Expected Object" + [emptyObject, occupiedObject] + where + emptyObject : Parser (JSONValue TObject) + emptyObject = do + delimited '{' '}' (nom whitespace) + pure $ VObject Nil + keyValue : Parser (t : JSONType ** (String, JSONValue t)) + keyValue = do + VString key <- surround whitespace string + _ <- charExact ':' + (typ ** val) <- value + pure (typ ** (key, val)) + restKeyValue : Parser (t : JSONType ** (String, JSONValue t)) + restKeyValue = do + _ <- charExact ',' + keyValue + pairs : Parser (List1 (t : JSONType ** (String, JSONValue t))) + pairs = do + first <- keyValue + rest <- many restKeyValue + pure $ first ::: rest + occupiedObject : Parser (JSONValue TObject) + occupiedObject = do + val <- delimited '{' '}' pairs + let (types ** xs) = DList.fromList (forget val) + pure $ VObject xs +``` + +```idris +array = do + pnote "JSON Array" + oneOfE + "Expected Array" + [emptyArray, occupiedArray] + where + emptyArray : Parser (JSONValue TArray) + emptyArray = do + delimited '[' ']' (nom whitespace) + pure $ VArray Nil + restValue : Parser (t : JSONType ** JSONValue t) + restValue = do + _ <- charExact ',' + value + values : Parser (List1 (t : JSONType ** JSONValue t)) + values = do + first <- value + rest <- many restValue + pure $ first ::: rest + occupiedArray : Parser (JSONValue TArray) + occupiedArray = do + xs <- delimited '[' ']' values + let (types ** xs) = DList.fromList (forget xs) + pure $ VArray xs +``` + +```idris +string = do + pnote "JSON String" + str <- liftString $ delimited '"' '"' (many stringCharacter) + pure $ VString str + where + -- TODO: Handle control characters properly + stringCharacter : Parser Char + stringCharacter = do + result <- charPredicate (not . (== '"')) + case result of + GotChar char => pure char + GotError err => + throwParseError "Expected string character, got \{show err}" + EndOfInput => throwParseError "Unexpected end of input" +``` + +```idris +number = do + pnote "JSON Number" + d <- double + pure $ VNumber d +``` + +```idris +bool = do + pnote "JSON Bool" + oneOfE + "Expected Bool" + [true, false] + where + true : Parser (JSONValue TBool) + true = do + _ <- exactString "true" + pure $ VBool True + false : Parser (JSONValue TBool) + false = do + _ <- exactString "false" + pure $ VBool False +``` + +```idris +null = do + pnote "JSON null" + _ <- exactString "null" + pure VNull +``` + +## Unit tests + +Quick smoke test + +```idris +-- @@test JSON Quick Smoke +quickSmoke : IO Bool +quickSmoke = do + let input = "{\"string\":\"string\",\"number\":5,\"true\":true,\"false\":false,\"null\":null,\"array\":[1,2,3]}" + putStrLn input + Right (type ** parsed) <- runFirstIODebug value input + | Left err => do + printLn err + pure False + putStrLn "Input: \{input}\nOutput: \{show type} -> \{show parsed}" + let reference_object = + VObject [ + ("string", VString "string") + , ("number", VNumber 5.0) + , ("true", VBool True) + , ("false", VBool False) + , ("null", VNull) + , ("array", VArray [ + VNumber 1.0 + , VNumber 2.0 + , VNumber 3.0 + ]) + ] + case type of + TObject => pure $ parsed == reference_object + _ => pure False +```