diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md index 3dc4251..4656469 100644 --- a/src/Parser/Interface.md +++ b/src/Parser/Interface.md @@ -20,8 +20,11 @@ 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 @@ -41,7 +51,7 @@ Show ParseError where ```idris public export Parser : Type -> Type -Parser a = Eff [ParserState, Except ParseError, Choose] a +Parser a = Eff [ParserState, Except ParseError] a ``` ## Error Generation @@ -93,7 +103,7 @@ no paths in the `Choice` effect produce a returning parse. export rundownFirst : (f : Parser a) -> Eff [ParserState] (Either ParseError a) rundownFirst f = - runExcept . guardMaybe "No returning parses" . runChoose {f = Maybe} $ f + runExcept f ``` Provide wrappers for `rundownFirst` for evaluating it in various contexts. @@ -148,27 +158,29 @@ 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. This will suppress any errors returned by -the input parsers by mapping them to `empty`. +the provided error action on failure. The state will not be modified when an input parser fails ```idris export -oneOfE : Foldable f => - (err : Parser a) -> f (Parser a) -> Parser a -oneOfE err xs = foldr altE err xs +oneOfE : (err : String) -> List (Parser a) -> Parser a +oneOfE err xs = do + start <- save + oneOfE' err start [] xs where - altE : Parser a -> Parser a -> Parser a - altE f rest = (tryEmpty f) `alt` rest + 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 ``` Attempt to parse 0+ of an item @@ -198,6 +210,7 @@ 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 @@ -250,6 +263,40 @@ 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 7e83fd7..f09c8dd 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -61,13 +61,24 @@ Show (JSONValue t) where in assert_total $ "{\{joinBy "," xs}}" show (VArray xs) = let xs = dMap (\_,e => show e) xs - in assert_total $ "[\{joinBy "," . map show $ 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 --> @@ -121,20 +132,16 @@ Top level json value parser 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 + 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 @@ -142,72 +149,76 @@ Now go through our json value types ```idris object = do oneOfE - (throwParseError "Expected Object") - (the (List _) [emptyObject, occupiedObject]) + "Expected Object" + [emptyObject, occupiedObject] where emptyObject : Parser (JSONValue TObject) emptyObject = do - _ <- parseExactChar '{' - _ <- many whitespace - _ <- parseExactChar '}' + delimited '{' '}' (nom whitespace) pure $ VObject Nil - firstKeyValue : Parser (t : JSONType ** (String, JSONValue t)) - firstKeyValue = do - _ <- many whitespace - VString key <- string - _ <- many whitespace + keyValue : Parser (t : JSONType ** (String, JSONValue t)) + keyValue = do + VString key <- surround whitespace string _ <- parseExactChar ':' (typ ** val) <- value pure (typ ** (key, val)) restKeyValue : Parser (t : JSONType ** (String, JSONValue t)) restKeyValue = do _ <- parseExactChar ',' - firstKeyValue + 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 - _ <- parseExactChar '{' - first <- firstKeyValue - rest <- many restKeyValue - _ <- parseExactChar '}' - let (types ** xs) = DList.fromList (first :: rest) + val <- delimited '{' '}' pairs + let (types ** xs) = DList.fromList (forget val) pure $ VObject xs ``` ```idris array = do oneOfE - (throwParseError "Expected Array") - (the (List _) [emptyArray, occupiedArray]) + "Expected Array" + [emptyArray, occupiedArray] where emptyArray : Parser (JSONValue TArray) emptyArray = do - _ <- parseExactChar '[' - _ <- many whitespace - _ <- parseExactChar ']' + delimited '[' ']' (nom whitespace) 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 '[' - first <- value - rest <- many restValue + xs <- values _ <- parseExactChar ']' - let (types ** xs) = DList.fromList (first :: rest) + -- TODO: Why is this busted? + -- xs <- delimited '[' ']' values + let (types ** xs) = DList.fromList (forget xs) 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 + 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 ``` ```idris @@ -219,8 +230,8 @@ number = do ```idris bool = do oneOfE - (throwParseError "Expected Bool") - (the (List _) [true, false]) + "Expected Bool" + [true, false] where true : Parser (JSONValue TBool) true = do @@ -237,3 +248,36 @@ 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 +```