json: delimited arrays

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 $
+    | _ => do
-      MkParseError starting_state "Unmatched delimiter \{show before}"
+      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

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

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

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
 ```
 
 <!-- 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
@@ -147,6 +156,17 @@ 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`
@@ -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
+data ParseCharResult : Type where
-  GotChar : (char : Char) -> ParseCharResult e
+  GotChar : (char : Char) -> ParseCharResult
-  GotError : (err : e) -> ParseCharResult e
+  GotError : (err : Char) -> ParseCharResult
-  EndOfInput : ParseCharResult e
+  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) 
+  ParseChar : (predicate : Char -> Bool) -> ParserState ParseCharResult
-    -> ParserState (ParseCharResult e)
+  ParseExactChar : (char : Char) -> ParserState ParseCharResult
   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
@@ -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) 
+parseChar : Has ParserState fs => (predicate : Char -> Bool)
-  -> Eff fs (ParseCharResult e)
+  -> Eff fs ParseCharResult
-parseChar predicate err = send $ ParseChar predicate err
+parseChar predicate = send $ ParseChar predicate 
 
-||| Wrapper for parseChar that folds the error message into effect stack with the
+||| Parse a char by exact value
-||| provided callback
+export 
-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
@@ -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 =>