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) id
-  result <- parseChar (\x => any (== x) cs)
   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
+  exactString "" | [] = pure ""
-    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
-    GotChar next <- parseChar (== c)
       | 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
+  val <- x
-    | Left err => do
-      load starting_state
-      throw err
   Just _ <- tryMaybe $ parseExactChar after
-    | _ => do
+    | _ => throw $
-      load starting_state
+      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

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 . (== '"'))
+      e1 <- parseError "Expected non-quote, got quote"
-      case result of
+      e2 <- parseError "End of input"
-        GotChar char => pure char
+      parseCharE (not . (== '"')) (\_ => e1) e2
-        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]
@@ -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

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

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
 ```
 
 <!-- idris
-export
 Eq (Index i) where
   x == y = x.index == y.index
 
-export
 Ord (Index i) where
   compare x y = compare x.index y.index
-
-export
-Show (Index i) where
-  show (MkIndex index) = show index
 -->
 
 Stores the location we are currently at in the string, and metadata about it for
@@ -156,17 +147,6 @@ positionPair pi =
           in (linum, col)
 ```
 
-<!-- idris
-export
-Show (ParserInternal Id) where
-  show pi = 
-    let (line, col) = positionPair pi
-        current = assert_total $ strIndex pi.input (cast pi.position.index) 
-        pos = pi.position.index
-        eof = show pi.end_of_input
-    in "Position: \{pos}(\{line}, \{col}}) Value: \{show current} EoF: \{eof}"
--->
-
 ### 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
+data ParseCharResult : Type -> Type where
-  GotChar : (char : Char) -> ParseCharResult
+  GotChar : (char : Char) -> ParseCharResult e
-  GotError : (err : Char) -> ParseCharResult
+  GotError : (err : e) -> ParseCharResult e
-  EndOfInput : ParseCharResult
+  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
+  ParseChar : (predicate : Char -> Bool) -> (err : Char -> e) 
-  ParseExactChar : (char : Char) -> ParserState ParseCharResult
+    -> ParserState (ParseCharResult e)
   ParseEoF : ParserState Bool
-  Note : Lazy String -> ParserState ()
 ```
 
-<!-- idris
-Show (ParserState t) where
-  show Save = "Saving state"
-  show (Load pi) = "Loading state \{show pi}"
-  show (ParseChar predicate) = "Parsing char"
-  show (ParseExactChar char) = "Parsing char \{show char}"
-  show ParseEoF = "Parsing EoF"
-  show (Note _) = "Note"
--->
-
 ### 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)
+parseChar : Has ParserState fs => (predicate : Char -> Bool) -> (err : Char -> e) 
-  -> Eff fs ParseCharResult
+  -> Eff fs (ParseCharResult e)
-parseChar predicate = send $ ParseChar predicate 
+parseChar predicate err = send $ ParseChar predicate err
 
-||| Parse a char by exact value
+||| Wrapper for parseChar that folds the error message into effect stack with the
+||| provided callback
 export
-parseExactChar' : Has ParserState fs => (chr : Char) -> Eff fs ParseCharResult
+parseCharE : Has ParserState fs => Has (Except e) fs => 
-parseExactChar' chr = send $ ParseExactChar chr
+  (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)
+      else (GotError $ err 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 =>