core: Notes

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

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 ()
 ```
 
 <!-- idris
@@ -221,6 +222,7 @@ Show (ParserState t) where
   show (Load pi) = "Loading state \{show pi}"
   show (ParseChar predicate err) = "Parsing char"
   show ParseEoF = "Parsing EoF"
+  show (Note _) = "Note"
 -->
 
 ### 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 =>