diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md index 4656469..3dc4251 100644 --- a/src/Parser/Interface.md +++ b/src/Parser/Interface.md @@ -20,11 +20,8 @@ Combine the parser state at time of error with an error message. ```idris public export data ParseError : Type where - -- TODO: Rename this constructor MkParseError : (state : ParserInternal Id) -> (message : String) -> ParseError BeforeParse : (message : String) -> ParseError - NestedErrors : (state : ParserInternal Id) -> (message : String) - -> (rest : List ParseError) -> ParseError ``` ## Type Alias @@ -51,7 +41,7 @@ Show ParseError where ```idris public export Parser : Type -> Type -Parser a = Eff [ParserState, Except ParseError] a +Parser a = Eff [ParserState, Except ParseError, Choose] a ``` ## Error Generation @@ -103,7 +93,7 @@ no paths in the `Choice` effect produce a returning parse. export rundownFirst : (f : Parser a) -> Eff [ParserState] (Either ParseError a) rundownFirst f = - runExcept f + runExcept . guardMaybe "No returning parses" . runChoose {f = Maybe} $ f ``` Provide wrappers for `rundownFirst` for evaluating it in various contexts. @@ -158,29 +148,27 @@ tryMaybe f = try (map Just f) (\_ => pure Nothing) export tryEither : (f : Parser a) -> Parser (Either ParseError a) tryEither f = try (map Right f) (pure . Left) + +||| Converts any errors thrown by `f` into silent backtracking within `Choose` +export +tryEmpty : (f : Parser a) -> Parser a +tryEmpty f = try f (\_ => empty) ``` Attempt to parse one of the given input parsers, in the provided order, invoking -the provided error action on failure. +the provided error action on failure. This will suppress any errors returned by +the input parsers by mapping them to `empty`. The state will not be modified when an input parser fails ```idris export -oneOfE : (err : String) -> List (Parser a) -> Parser a -oneOfE err xs = do - start <- save - oneOfE' err start [] xs +oneOfE : Foldable f => + (err : Parser a) -> f (Parser a) -> Parser a +oneOfE err xs = foldr altE err xs where - oneOfE' : (err : String) -> (start : ParserInternal Id) - -> (errs : List ParseError) -> List (Parser a) -> Parser a - oneOfE' err start errs [] = do - throw $ NestedErrors start err (reverse errs) - oneOfE' err start errs (x :: xs) = do - x <- tryEither x - case x of - Right val => pure val - Left error => oneOfE' err start (error :: errs) xs + altE : Parser a -> Parser a -> Parser a + altE f rest = (tryEmpty f) `alt` rest ``` Attempt to parse 0+ of an item @@ -210,7 +198,6 @@ Lift a parser producing a `List` or `List1` of `Char` into a parser producing a `String` ```idris --- TODO: Rename these export parseString : Parser (List Char) -> Parser String parseString x = do @@ -263,40 +250,6 @@ exactString str with (asList str) pure input ``` -Wrap a parser in delimiter characters, discarding the value of the delimiters - -```idris -export -delimited : (before, after : Char) -> Parser a -> Parser a -delimited before after x = do - starting_state <- save - _ <- parseExactChar before - val <- x - Just _ <- tryMaybe $ parseExactChar after - | _ => throw $ - MkParseError starting_state "Unmatched delimiter \{show before}" - pure val -``` - -Consume any number of characters of the provided character class and discard the -result. Also a version for doing so on both sides of a provided parser - -```idris -export -nom : Parser Char -> Parser () -nom x = do - _ <- many x - pure () - -export -surround : (around : Parser Char) -> (item : Parser a) -> Parser a -surround around item = do - nom around - val <- item - nom around - pure val -``` - ### Composition of boolean functions ```idris diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md index f09c8dd..7e83fd7 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -61,24 +61,13 @@ Show (JSONValue t) where in assert_total $ "{\{joinBy "," xs}}" show (VArray xs) = let xs = dMap (\_,e => show e) xs - in assert_total $ "[\{joinBy "," xs}]" + in assert_total $ "[\{joinBy "," . map show $ 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 --> @@ -132,16 +121,20 @@ Top level json value parser export value : Parser (t : JSONType ** JSONValue t) value = do - surround whitespace $ oneOfE - "Expected JSON Value" - [ - dpairize object - , dpairize array - , dpairize string - , dpairize number - , dpairize bool - , dpairize null - ] + _ <- 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 @@ -149,76 +142,72 @@ Now go through our json value types ```idris object = do oneOfE - "Expected Object" - [emptyObject, occupiedObject] + (throwParseError "Expected Object") + (the (List _) [emptyObject, occupiedObject]) where emptyObject : Parser (JSONValue TObject) emptyObject = do - delimited '{' '}' (nom whitespace) + _ <- parseExactChar '{' + _ <- many whitespace + _ <- parseExactChar '}' pure $ VObject Nil - keyValue : Parser (t : JSONType ** (String, JSONValue t)) - keyValue = do - VString key <- surround whitespace string + 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 ',' - keyValue - pairs : Parser (List1 (t : JSONType ** (String, JSONValue t))) - pairs = do - first <- keyValue - rest <- many restKeyValue - pure $ first ::: rest + firstKeyValue occupiedObject : Parser (JSONValue TObject) occupiedObject = do - val <- delimited '{' '}' pairs - let (types ** xs) = DList.fromList (forget val) + _ <- parseExactChar '{' + first <- firstKeyValue + rest <- many restKeyValue + _ <- parseExactChar '}' + let (types ** xs) = DList.fromList (first :: rest) pure $ VObject xs ``` ```idris array = do oneOfE - "Expected Array" - [emptyArray, occupiedArray] + (throwParseError "Expected Array") + (the (List _) [emptyArray, occupiedArray]) where emptyArray : Parser (JSONValue TArray) emptyArray = do - delimited '[' ']' (nom whitespace) + _ <- parseExactChar '[' + _ <- many whitespace + _ <- parseExactChar ']' pure $ VArray Nil restValue : Parser (t : JSONType ** JSONValue t) restValue = do _ <- parseExactChar ',' value - values : Parser (List1 (t : JSONType ** JSONValue t)) - values = do - first <- value - rest <- many restValue - pure $ first ::: rest occupiedArray : Parser (JSONValue TArray) occupiedArray = do _ <- parseExactChar '[' - xs <- values + first <- value + rest <- many restValue _ <- parseExactChar ']' - -- TODO: Why is this busted? - -- xs <- delimited '[' ']' values - let (types ** xs) = DList.fromList (forget xs) + let (types ** xs) = DList.fromList (first :: rest) pure $ VArray xs ``` ```idris string = do - str <- parseString $ delimited '"' '"' (many stringCharacter) - pure $ VString str - where - -- TODO: Handle control characters properly - stringCharacter : Parser Char - stringCharacter = do - e1 <- parseError "Expected non-quote, got quote" - e2 <- parseError "End of input" - parseCharE (not . (== '"')) (\_ => e1) e2 + _ <- 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 ``` ```idris @@ -230,8 +219,8 @@ number = do ```idris bool = do oneOfE - "Expected Bool" - [true, false] + (throwParseError "Expected Bool") + (the (List _) [true, false]) where true : Parser (JSONValue TBool) true = do @@ -248,36 +237,3 @@ null = do _ <- 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) <- runFirstIO 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 -```