diff --git a/README.md b/README.md index 48644ce..dc78c7c 100644 --- a/README.md +++ b/README.md @@ -68,14 +68,10 @@ solution. Internal state of a parser - - [Numbers](src/Parser/Numbers.md) + - [ParserState](src/Parser/ParserState.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 607e26e..e8aff07 100644 --- a/advent.ipkg +++ b/advent.ipkg @@ -19,7 +19,6 @@ depends = base , tailrec , eff , elab-util - , sop , ansi , if-unsolved-implicit , c-ffi @@ -34,7 +33,6 @@ 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 2c65cfa..17c4ff9 100644 --- a/src/Parser/Interface.md +++ b/src/Parser/Interface.md @@ -235,20 +235,6 @@ 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 deleted file mode 100644 index 453177a..0000000 --- a/src/Parser/JSON.md +++ /dev/null @@ -1,211 +0,0 @@ -# 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 fb7b780..1f65bb5 100644 --- a/src/Parser/Numbers.md +++ b/src/Parser/Numbers.md @@ -96,10 +96,9 @@ integerBase10 = integer base10 ### Double ```idris --- TODO: Replicate `parseDouble` logic and make this base-generic export -double : Parser Double -double = do +double : Base -> Parser Double +double b = do starting_state <- save integer <- integer fraction <- tryMaybe fraction @@ -120,7 +119,7 @@ double = do where parseDigit : Parser Char parseDigit = do - GotChar char <- parseChar (hasDigit base10) id + GotChar char <- parseChar (hasDigit b) id | GotError e => throwParseError "\{show e} is not a digit" | EndOfInput => throwParseError "End Of Input" pure char @@ -145,6 +144,10 @@ double = do error <- replaceError "Expected digit" digits <- map forget $ atLeastOne error parseDigit pure . pack $ sign :: digits + +export +doubleBase10 : Parser Double +doubleBase10 = double base10 ``` ## Unit tests @@ -212,7 +215,7 @@ compareDouble string = do putStrLn "Failed to produce parser for \{string}" pure False Right result <- - runEff (rundownFirst double) [handleParserStateIO state] {m = IO} + runEff (rundownFirst doubleBase10) [handleParserStateIO state] {m = IO} | Left err => do printLn err pure False