diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md index 0aced22..18df77a 100644 --- a/src/Parser/Interface.md +++ b/src/Parser/Interface.md @@ -235,6 +235,7 @@ Attempt to parse a specified character export parseExactChar : Char -> Parser Char parseExactChar c = do + pnote "Parsing exact char: \{show c}" result <- parseChar (== c) id case result of GotChar char => pure char @@ -248,6 +249,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) id case result of GotChar char => pure char @@ -261,8 +263,11 @@ 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 + pnote "Parsing exact string \{show input}" GotChar next <- parseChar (== c) id | GotError err => throwParseError "Got \{show err} expected \{show c}" | EndOfInput => throwParseError "End of input" @@ -276,6 +281,7 @@ 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 @@ -292,12 +298,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/ParserState.md b/src/Parser/ParserState.md index be4a783..fb7c481 100644 --- a/src/Parser/ParserState.md +++ b/src/Parser/ParserState.md @@ -213,6 +213,7 @@ data ParserState : Type -> Type where ParseChar : (predicate : Char -> Bool) -> (err : Char -> e) -> ParserState (ParseCharResult e) ParseEoF : ParserState Bool + Note : Lazy String -> ParserState () ``` ### Actions @@ -262,6 +264,11 @@ parseCharE predicate err eof = do 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 @@ -299,6 +306,8 @@ handleParserStateIO pi (ParseChar predicate err) = do 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)) @@ -315,6 +324,11 @@ Wrapper with debugging output 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 @@ -341,6 +355,7 @@ unPS pi (ParseChar predicate err) = (GotChar char, {position := MkIndex next} pi) else (GotError $ err char, pi) unPS pi ParseEoF = (pi.end_of_input, pi) +unPS pi (Note _) = ((), pi) export runParserState : Has ParserState fs =>