diff --git a/README.md b/README.md index dc78c7c..48644ce 100644 --- a/README.md +++ b/README.md @@ -68,10 +68,14 @@ solution. Internal state of a parser - - [ParserState](src/Parser/ParserState.md) + - [Numbers](src/Parser/Numbers.md) 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/Interface.md b/src/Parser/Interface.md index 17c4ff9..2c65cfa 100644 --- a/src/Parser/Interface.md +++ b/src/Parser/Interface.md @@ -235,6 +235,20 @@ parseTheseChars cs = do EndOfInput => throwParseError "End of input" ``` +Attempt to parse an exact string + +```idris +exactString : String -> Parser String +exactString str with (asList str) + exactString "" | [] = pure "" + exactString input@(strCons c str) | (c :: x) = do + GotChar next <- parseChar (== c) id + | GotError err => throwParseError "Got \{show err} expected \{show c}" + | EndOfInput => throwParseError "End of input" + rest <- exactString str | x + pure input +``` + ### Composition of boolean functions ```idris diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md new file mode 100644 index 0000000..453177a --- /dev/null +++ b/src/Parser/JSON.md @@ -0,0 +1,211 @@ +# JSON Parser + +```idris +module Parser.JSON + +import public Parser +import public Parser.Numbers + +import Structures.Dependent.DList +``` + + + +## 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 +``` + + + +## 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 + result <- + parseChar (\x => any (== x) $ the (List _) [' ', '\n', '\r', '\t']) id + case result of + GotChar char => pure char + GotError err => throwParseError "Expected whitespace, got: \{show err}" + EndOfInput => throwParseError "End of Input" +``` + +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 + _ <- many whitespace + val <- oneOfE + (throwParseError "Expected JSON Value") + (the (List _) + [ + dpairize object + , dpairize array + , dpairize string + , dpairize number + , dpairize bool + , dpairize null + ]) + _ <- many whitespace + pure val +``` + +Now go through our json value types + +```idris +object = do + oneOfE + (throwParseError "Expected Object") + (the (List _) [emptyObject, occupiedObject]) + where + emptyObject : Parser (JSONValue TObject) + emptyObject = do + _ <- parseExactChar '{' + _ <- many whitespace + _ <- parseExactChar '}' + pure $ VObject Nil + firstKeyValue : Parser (t : JSONType ** (String, JSONValue t)) + firstKeyValue = do + _ <- many whitespace + VString key <- string + _ <- many whitespace + _ <- parseExactChar ':' + (typ ** val) <- value + pure (typ ** (key, val)) + restKeyValue : Parser (t : JSONType ** (String, JSONValue t)) + restKeyValue = do + _ <- parseExactChar ',' + firstKeyValue + occupiedObject : Parser (JSONValue TObject) + occupiedObject = do + _ <- parseExactChar '{' + first <- firstKeyValue + rest <- many restKeyValue + _ <- parseExactChar '}' + let (types ** xs) = DList.fromList (first :: rest) + pure $ VObject xs +``` + +```idris +array = do + oneOfE + (throwParseError "Expected Array") + (the (List _) [emptyArray, occupiedArray]) + where + emptyArray : Parser (JSONValue TArray) + emptyArray = do + _ <- parseExactChar '[' + _ <- many whitespace + _ <- parseExactChar ']' + pure $ VArray Nil + restValue : Parser (t : JSONType ** JSONValue t) + restValue = do + _ <- parseExactChar ',' + value + occupiedArray : Parser (JSONValue TArray) + occupiedArray = do + _ <- parseExactChar '[' + first <- value + rest <- many restValue + _ <- parseExactChar ']' + let (types ** xs) = DList.fromList (first :: rest) + pure $ VArray xs +``` + +```idris +string = do + _ <- parseExactChar '"' + -- TODO: Handle control characters properly + e1 <- parseError "Expected non-quote, got quote" + e2 <- parseError "End of input" + contents <- parseString . many $ parseCharE (not . (== '"')) (\_ => e1) e2 + _ <- parseExactChar '"' + pure $ VString contents +``` diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md index 1f65bb5..fb7b780 100644 --- a/src/Parser/Numbers.md +++ b/src/Parser/Numbers.md @@ -96,9 +96,10 @@ integerBase10 = integer base10 ### Double ```idris +-- TODO: Replicate `parseDouble` logic and make this base-generic export -double : Base -> Parser Double -double b = do +double : Parser Double +double = do starting_state <- save integer <- integer fraction <- tryMaybe fraction @@ -119,7 +120,7 @@ double b = do where parseDigit : Parser Char parseDigit = do - GotChar char <- parseChar (hasDigit b) id + GotChar char <- parseChar (hasDigit base10) id | GotError e => throwParseError "\{show e} is not a digit" | EndOfInput => throwParseError "End Of Input" pure char @@ -144,10 +145,6 @@ double b = do error <- replaceError "Expected digit" digits <- map forget $ atLeastOne error parseDigit pure . pack $ sign :: digits - -export -doubleBase10 : Parser Double -doubleBase10 = double base10 ``` ## Unit tests @@ -215,7 +212,7 @@ compareDouble string = do putStrLn "Failed to produce parser for \{string}" pure False Right result <- - runEff (rundownFirst doubleBase10) [handleParserStateIO state] {m = IO} + runEff (rundownFirst double) [handleParserStateIO state] {m = IO} | Left err => do printLn err pure False