diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md index 4656469..49fe300 100644 --- a/src/Parser/Interface.md +++ b/src/Parser/Interface.md @@ -116,6 +116,13 @@ runFirstIO f str = do | _ => pure . Left $ BeforeParse "Empty input" runEff (rundownFirst f) [handleParserStateIO state] +export +runFirstIODebug : (f : Parser a) -> String -> IO (Either ParseError a) +runFirstIODebug f str = do + Just state <- newInternalIO str + | _ => pure . Left $ BeforeParse "Empty input" + runEff (rundownFirst f) [handleParserStateIODebug state] + export runFirst : (f : Parser a) -> String -> Eff fs (Either ParseError a) runFirst f str = do @@ -228,7 +235,7 @@ Attempt to parse a specified character export parseExactChar : Char -> Parser Char parseExactChar c = do - result <- parseChar (== c) id + result <- parseExactChar' c case result of GotChar char => pure char GotError err => throwParseError "Got \{show err} Expected \{show c}" @@ -241,7 +248,8 @@ Attempt to parse one of a list of chars export parseTheseChars : List Char -> Parser Char parseTheseChars cs = do - result <- parseChar (\x => any (== x) cs) id + pnote "Parsing one of: \{show cs}" + result <- parseChar (\x => any (== x) cs) case result of GotChar char => pure char GotError err => throwParseError "Got \{show err} Expected one of \{show cs}" @@ -254,9 +262,12 @@ Attempt to parse an exact string export exactString : String -> Parser String exactString str with (asList str) - exactString "" | [] = pure "" + exactString "" | [] = do + pnote "Parsing the empty string" + pure "" exactString input@(strCons c str) | (c :: x) = do - GotChar next <- parseChar (== c) id + pnote "Parsing exact string \{show input}" + GotChar next <- parseChar (== c) | GotError err => throwParseError "Got \{show err} expected \{show c}" | EndOfInput => throwParseError "End of input" rest <- exactString str | x @@ -269,12 +280,17 @@ Wrap a parser in delimiter characters, discarding the value of the delimiters export delimited : (before, after : Char) -> Parser a -> Parser a delimited before after x = do + pnote "Parsing delimited by \{show before} \{show after}" starting_state <- save _ <- parseExactChar before - val <- x + Right val <- tryEither x + | Left err => do + load starting_state + throw err Just _ <- tryMaybe $ parseExactChar after - | _ => throw $ - MkParseError starting_state "Unmatched delimiter \{show before}" + | _ => do + load starting_state + throw $ MkParseError starting_state "Unmatched delimiter \{show before}" pure val ``` @@ -285,12 +301,14 @@ result. Also a version for doing so on both sides of a provided parser export nom : Parser Char -> Parser () nom x = do + pnote "Nomming" _ <- many x pure () export surround : (around : Parser Char) -> (item : Parser a) -> Parser a surround around item = do + pnote "Surrounding" nom around val <- item nom around diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md index f09c8dd..311057d 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -108,8 +108,9 @@ Define a `whitespace` character class based on the json specifications ```idris whitespace : Parser Char whitespace = do + pnote "Whitespace character" result <- - parseChar (\x => any (== x) $ the (List _) [' ', '\n', '\r', '\t']) id + parseChar (\x => any (== x) $ the (List _) [' ', '\n', '\r', '\t']) case result of GotChar char => pure char GotError err => throwParseError "Expected whitespace, got: \{show err}" @@ -132,6 +133,7 @@ Top level json value parser export value : Parser (t : JSONType ** JSONValue t) value = do + pnote "JSON Value" surround whitespace $ oneOfE "Expected JSON Value" [ @@ -148,6 +150,7 @@ Now go through our json value types ```idris object = do + pnote "JSON Object" oneOfE "Expected Object" [emptyObject, occupiedObject] @@ -180,6 +183,7 @@ object = do ```idris array = do + pnote "JSON Array" oneOfE "Expected Array" [emptyArray, occupiedArray] @@ -199,36 +203,38 @@ array = do pure $ first ::: rest occupiedArray : Parser (JSONValue TArray) occupiedArray = do - _ <- parseExactChar '[' - xs <- values - _ <- parseExactChar ']' - -- TODO: Why is this busted? - -- xs <- delimited '[' ']' values + xs <- delimited '[' ']' values let (types ** xs) = DList.fromList (forget xs) pure $ VArray xs ``` ```idris string = do + pnote "JSON String" 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 + result <- parseChar (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] @@ -245,6 +251,7 @@ bool = do ```idris null = do + pnote "JSON null" _ <- exactString "null" pure VNull ``` @@ -259,7 +266,7 @@ 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 + Right (type ** parsed) <- runFirstIODebug value input | Left err => do printLn err pure False diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md index fb7b780..0c069ec 100644 --- a/src/Parser/Numbers.md +++ b/src/Parser/Numbers.md @@ -63,7 +63,7 @@ nat b = do where parseDigit : Parser Nat parseDigit = do - GotChar char <- parseChar (hasDigit b) id + GotChar char <- parseChar (hasDigit b) | GotError e => throwParseError "\{show e} is not a digit" | EndOfInput => throwParseError "End Of Input" case digitValue b char of @@ -120,7 +120,7 @@ double = do where parseDigit : Parser Char parseDigit = do - GotChar char <- parseChar (hasDigit base10) id + GotChar char <- parseChar (hasDigit base10) | GotError e => throwParseError "\{show e} is not a digit" | EndOfInput => throwParseError "End Of Input" pure char diff --git a/src/Parser/ParserState.md b/src/Parser/ParserState.md index 2a06858..8668a16 100644 --- a/src/Parser/ParserState.md +++ b/src/Parser/ParserState.md @@ -12,6 +12,9 @@ import public Data.Refined.Int64 import public Data.SortedMap import public Data.IORef +import Data.Primitives.Interpolation +import System.File + import public Control.Eff ``` @@ -49,11 +52,17 @@ record Index (length : Int64) where ``` Stores the location we are currently at in the string, and metadata about it for @@ -147,6 +156,17 @@ positionPair pi = in (linum, col) ``` + + ### More Barbie Functionality Provide the barbie analogs of `map` and `traverse` for our `ParserInternal` @@ -175,10 +195,10 @@ btraverse fun (MkInternal input length line_starts position end_of_input) = ```idris ||| Three way result returned from attempting to parse a single char public export -data ParseCharResult : Type -> Type where - GotChar : (char : Char) -> ParseCharResult e - GotError : (err : e) -> ParseCharResult e - EndOfInput : ParseCharResult e +data ParseCharResult : Type where + GotChar : (char : Char) -> ParseCharResult + GotError : (err : Char) -> ParseCharResult + EndOfInput : ParseCharResult ``` ## The Effect Type @@ -190,11 +210,22 @@ data ParserState : Type -> Type where Load : (ParserInternal Id) -> ParserState () -- TODO: Maybe add a ParseString that parses a string of characters as a -- string using efficent slicing? - ParseChar : (predicate : Char -> Bool) -> (err : Char -> e) - -> ParserState (ParseCharResult e) + ParseChar : (predicate : Char -> Bool) -> ParserState ParseCharResult + ParseExactChar : (char : Char) -> ParserState ParseCharResult ParseEoF : ParserState Bool + Note : Lazy String -> ParserState () ``` + + ### Actions ```idris @@ -212,28 +243,25 @@ load pi = send $ Load pi ||| predicate, updates the state if parsing succeeds, does not alter it in an ||| error condition. export -parseChar : Has ParserState fs => (predicate : Char -> Bool) -> (err : Char -> e) - -> Eff fs (ParseCharResult e) -parseChar predicate err = send $ ParseChar predicate err +parseChar : Has ParserState fs => (predicate : Char -> Bool) + -> Eff fs ParseCharResult +parseChar predicate = send $ ParseChar predicate -||| Wrapper for parseChar that folds the error message into effect stack with the -||| provided callback -export -parseCharE : Has ParserState fs => Has (Except e) fs => - (predicate : Char -> Bool) -> (err : Char -> e) -> (eof : Lazy e) - -> Eff fs Char -parseCharE predicate err eof = do - result <- parseChar predicate id - case result of - GotChar char => pure char - GotError x => throw $ err x - EndOfInput => throw eof +||| Parse a char by exact value +export +parseExactChar' : Has ParserState fs => (chr : Char) -> Eff fs ParseCharResult +parseExactChar' chr = send $ ParseExactChar chr ||| "Parse" the end of input, returning `True` if the parser state is currently ||| at the end of the input export parseEoF : Has ParserState fs => Eff fs Bool parseEoF = send ParseEoF + +||| Make a note to be output when running with a debug handler +export +pnote : Has ParserState fs => Lazy String -> Eff fs () +pnote x = send $ Note x ``` ## Handling a ParserState @@ -250,14 +278,14 @@ handleParserStateIO pi Save = do handleParserStateIO pi (Load pj) = do pj <- btraverse newIORef pj writeIORef pi pj -handleParserStateIO pi (ParseChar predicate err) = do +handleParserStateIO pi (ParseChar predicate) = do pi <- readIORef pi False <- readIORef pi.end_of_input - | _ => pure $ EndOfInput + | _ => pure EndOfInput position <- readIORef pi.position let char = assert_total $ strIndex pi.input (cast position.index) True <- pure $ predicate char - | _ => pure . GotError $ err char + | _ => pure $ GotError char -- Our refinement type on the position forces us to check that the length is -- in bounds after incrementing it, if its out of bounds, set the end_of_input -- flag @@ -268,9 +296,14 @@ handleParserStateIO pi (ParseChar predicate err) = do Just (Element next _) => do writeIORef pi.position $ MkIndex next pure $ GotChar char +handleParserStateIO pi (ParseExactChar chr) = do + -- TODO: do this directly? + handleParserStateIO pi (ParseChar (== chr)) handleParserStateIO pi ParseEoF = do pi <- readIORef pi readIORef pi.end_of_input +-- We ignore notes in non-debug mode +handleParserStateIO pi (Note _) = pure () export newInternalIO : HasIO io => String -> io $ Maybe (IORef (ParserInternal IORef)) @@ -281,13 +314,31 @@ newInternalIO str = do map Just $ newIORef internal ``` +Wrapper with debugging output + +```idris +export +handleParserStateIODebug : HasIO io => + IORef (ParserInternal IORef) -> ParserState t -> io t +handleParserStateIODebug x (Note note) = do + state <- readIORef x + state <- btraverse readIORef state + _ <- fPutStrLn stderr "Note \{note} -> \{show state}" + pure () +handleParserStateIODebug x y = do + state <- readIORef x + state <- btraverse readIORef state + _ <- fPutStrLn stderr "\{show y} -> \{show state}" + handleParserStateIO x y +``` + ### State context ```idris unPS : ParserInternal Id -> ParserState a -> (a, ParserInternal Id) unPS pi Save = (pi, pi) unPS pi (Load pj) = ((), pi) -unPS pi (ParseChar predicate err) = +unPS pi (ParseChar predicate) = if pi.end_of_input then (EndOfInput, pi) else let @@ -298,8 +349,10 @@ unPS pi (ParseChar predicate err) = (GotChar char, {end_of_input := True} pi) Just (Element next _) => (GotChar char, {position := MkIndex next} pi) - else (GotError $ err char, pi) + else (GotError char, pi) +unPS pi (ParseExactChar chr) = unPS pi (ParseChar (== chr)) unPS pi ParseEoF = (pi.end_of_input, pi) +unPS pi (Note _) = ((), pi) export runParserState : Has ParserState fs =>