diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md index 49fe300..4656469 100644 --- a/src/Parser/Interface.md +++ b/src/Parser/Interface.md @@ -116,13 +116,6 @@ 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 @@ -235,7 +228,7 @@ Attempt to parse a specified character export parseExactChar : Char -> Parser Char parseExactChar c = do - result <- parseExactChar' c + result <- parseChar (== c) id case result of GotChar char => pure char GotError err => throwParseError "Got \{show err} Expected \{show c}" @@ -248,8 +241,7 @@ Attempt to parse one of a list of chars export parseTheseChars : List Char -> Parser Char parseTheseChars cs = do - pnote "Parsing one of: \{show cs}" - result <- parseChar (\x => any (== x) cs) + result <- parseChar (\x => any (== x) cs) id case result of GotChar char => pure char GotError err => throwParseError "Got \{show err} Expected one of \{show cs}" @@ -262,12 +254,9 @@ Attempt to parse an exact string export exactString : String -> Parser String exactString str with (asList str) - exactString "" | [] = do - pnote "Parsing the empty string" - pure "" + exactString "" | [] = pure "" exactString input@(strCons c str) | (c :: x) = do - pnote "Parsing exact string \{show input}" - GotChar next <- parseChar (== c) + GotChar next <- parseChar (== c) id | GotError err => throwParseError "Got \{show err} expected \{show c}" | EndOfInput => throwParseError "End of input" rest <- exactString str | x @@ -280,17 +269,12 @@ 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 - Right val <- tryEither x - | Left err => do - load starting_state - throw err + val <- x Just _ <- tryMaybe $ parseExactChar after - | _ => do - load starting_state - throw $ MkParseError starting_state "Unmatched delimiter \{show before}" + | _ => throw $ + MkParseError starting_state "Unmatched delimiter \{show before}" pure val ``` @@ -301,14 +285,12 @@ 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 311057d..f09c8dd 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -108,9 +108,8 @@ 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']) + 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}" @@ -133,7 +132,6 @@ Top level json value parser export value : Parser (t : JSONType ** JSONValue t) value = do - pnote "JSON Value" surround whitespace $ oneOfE "Expected JSON Value" [ @@ -150,7 +148,6 @@ Now go through our json value types ```idris object = do - pnote "JSON Object" oneOfE "Expected Object" [emptyObject, occupiedObject] @@ -183,7 +180,6 @@ object = do ```idris array = do - pnote "JSON Array" oneOfE "Expected Array" [emptyArray, occupiedArray] @@ -203,38 +199,36 @@ array = do pure $ first ::: rest occupiedArray : Parser (JSONValue TArray) occupiedArray = do - xs <- delimited '[' ']' values + _ <- parseExactChar '[' + xs <- values + _ <- parseExactChar ']' + -- TODO: Why is this busted? + -- 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 - 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" + e1 <- parseError "Expected non-quote, got quote" + e2 <- parseError "End of input" + parseCharE (not . (== '"')) (\_ => e1) e2 ``` ```idris number = do - pnote "JSON Number" d <- double pure $ VNumber d ``` ```idris bool = do - pnote "JSON Bool" oneOfE "Expected Bool" [true, false] @@ -251,7 +245,6 @@ bool = do ```idris null = do - pnote "JSON null" _ <- exactString "null" pure VNull ``` @@ -266,7 +259,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) <- runFirstIODebug value input + Right (type ** parsed) <- runFirstIO value input | Left err => do printLn err pure False diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md index 0c069ec..fb7b780 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) + GotChar char <- parseChar (hasDigit b) id | 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) + GotChar char <- parseChar (hasDigit base10) id | 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 8668a16..2a06858 100644 --- a/src/Parser/ParserState.md +++ b/src/Parser/ParserState.md @@ -12,9 +12,6 @@ import public Data.Refined.Int64 import public Data.SortedMap import public Data.IORef -import Data.Primitives.Interpolation -import System.File - import public Control.Eff ``` @@ -52,17 +49,11 @@ record Index (length : Int64) where ``` Stores the location we are currently at in the string, and metadata about it for @@ -156,17 +147,6 @@ positionPair pi = in (linum, col) ``` - - ### More Barbie Functionality Provide the barbie analogs of `map` and `traverse` for our `ParserInternal` @@ -195,10 +175,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 where - GotChar : (char : Char) -> ParseCharResult - GotError : (err : Char) -> ParseCharResult - EndOfInput : ParseCharResult +data ParseCharResult : Type -> Type where + GotChar : (char : Char) -> ParseCharResult e + GotError : (err : e) -> ParseCharResult e + EndOfInput : ParseCharResult e ``` ## The Effect Type @@ -210,22 +190,11 @@ 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) -> ParserState ParseCharResult - ParseExactChar : (char : Char) -> ParserState ParseCharResult + ParseChar : (predicate : Char -> Bool) -> (err : Char -> e) + -> ParserState (ParseCharResult e) ParseEoF : ParserState Bool - Note : Lazy String -> ParserState () ``` - - ### Actions ```idris @@ -243,25 +212,28 @@ 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) - -> Eff fs ParseCharResult -parseChar predicate = send $ ParseChar predicate +parseChar : Has ParserState fs => (predicate : Char -> Bool) -> (err : Char -> e) + -> Eff fs (ParseCharResult e) +parseChar predicate err = send $ ParseChar predicate err -||| Parse a char by exact value -export -parseExactChar' : Has ParserState fs => (chr : Char) -> Eff fs ParseCharResult -parseExactChar' chr = send $ ParseExactChar chr +||| 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" 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 @@ -278,14 +250,14 @@ handleParserStateIO pi Save = do handleParserStateIO pi (Load pj) = do pj <- btraverse newIORef pj writeIORef pi pj -handleParserStateIO pi (ParseChar predicate) = do +handleParserStateIO pi (ParseChar predicate err) = 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 char + | _ => pure . GotError $ err 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 @@ -296,14 +268,9 @@ handleParserStateIO pi (ParseChar predicate) = 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)) @@ -314,31 +281,13 @@ 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) = +unPS pi (ParseChar predicate err) = if pi.end_of_input then (EndOfInput, pi) else let @@ -349,10 +298,8 @@ unPS pi (ParseChar predicate) = (GotChar char, {end_of_input := True} pi) Just (Element next _) => (GotChar char, {position := MkIndex next} pi) - else (GotError char, pi) -unPS pi (ParseExactChar chr) = unPS pi (ParseChar (== chr)) + else (GotError $ err char, pi) unPS pi ParseEoF = (pi.end_of_input, pi) -unPS pi (Note _) = ((), pi) export runParserState : Has ParserState fs =>