json: Clean up json smoke test

src/Parser/Interface.md

@@ -20,8 +20,11 @@ Combine the parser state at time of error with an error message.
 ```idris
 public export
 data ParseError : Type where
+  -- TODO: Rename this constructor
   MkParseError : (state : ParserInternal Id) -> (message : String) -> ParseError
   BeforeParse : (message : String) -> ParseError
+  NestedErrors : (state : ParserInternal Id) -> (message : String)
+    -> (rest : List ParseError) -> ParseError
 ```
 
 <!-- idris
@@ -34,6 +37,13 @@ Show ParseError where
     in "Error at line \{line}, column \{col} (\{position}): \{message}"
   show (BeforeParse message) =
     "Error before parsing: \{message}"
+  show (NestedErrors state message rest) = 
+    let rest = assert_total $joinBy "\n" . map (("  " ++) . show) $ rest
+        (line, col) = positionPair state
+        (line, col) = (show line, show col)
+        position = show state.position.index
+        first = "Error at line \{line}, column \{col} (\{position}): \{message}"
+    in "\{first}\n\{rest}"
 -->
 
 ## Type Alias
@@ -41,7 +51,7 @@ Show ParseError where
 ```idris
 public export
 Parser : Type -> Type
-Parser a = Eff [ParserState, Except ParseError, Choose] a
+Parser a = Eff [ParserState, Except ParseError] a
 ```
 
 ## Error Generation
@@ -93,7 +103,7 @@ no paths in the `Choice` effect produce a returning parse.
 export
 rundownFirst : (f : Parser a) -> Eff [ParserState] (Either ParseError a)
 rundownFirst f = 
-  runExcept . guardMaybe "No returning parses" . runChoose {f = Maybe} $ f
+  runExcept f
 ```
 
 Provide wrappers for `rundownFirst` for evaluating it in various contexts.
@@ -148,27 +158,29 @@ tryMaybe f = try (map Just f) (\_ => pure Nothing)
 export
 tryEither : (f : Parser a) -> Parser (Either ParseError a)
 tryEither f = try (map Right f) (pure . Left)
-
-||| Converts any errors thrown by `f` into silent backtracking within `Choose`
-export
-tryEmpty : (f : Parser a) -> Parser a
-tryEmpty f = try f (\_ => empty)
 ```
 
 Attempt to parse one of the given input parsers, in the provided order, invoking
-the provided error action on failure. This will suppress any errors returned by
+the provided error action on failure.
-the input parsers by mapping them to `empty`.
 
 The state will not be modified when an input parser fails
 
 ```idris
 export
-oneOfE : Foldable f =>
+oneOfE : (err : String) -> List (Parser a) -> Parser a
-  (err : Parser a) -> f (Parser a) -> Parser a
+oneOfE err xs = do
-oneOfE err xs = foldr altE err xs
+  start <- save
+  oneOfE' err start [] xs
   where
-    altE : Parser a -> Parser a -> Parser a
+    oneOfE' : (err : String) -> (start : ParserInternal Id) 
-    altE f rest = (tryEmpty f) `alt` rest
+      -> (errs : List ParseError) -> List (Parser a) -> Parser a
+    oneOfE' err start errs [] = do
+      throw $ NestedErrors start err (reverse errs) 
+    oneOfE' err start errs (x :: xs) = do
+      x <- tryEither x
+      case x of
+        Right val => pure val
+        Left error => oneOfE' err start (error :: errs) xs
 ```
 
 Attempt to parse 0+ of an item
@@ -198,6 +210,7 @@ Lift a parser producing a `List` or `List1` of `Char` into a parser producing a
 `String`
 
 ```idris
+-- TODO: Rename these
 export
 parseString : Parser (List Char) -> Parser String
 parseString x = do
@@ -250,6 +263,40 @@ exactString str with (asList str)
     pure input
 ```
 
+Wrap a parser in delimiter characters, discarding the value of the delimiters
+
+```idris
+export
+delimited : (before, after : Char) -> Parser a -> Parser a
+delimited before after x = do
+  starting_state <- save
+  _ <- parseExactChar before
+  val <- x
+  Just _ <- tryMaybe $ parseExactChar after
+    | _ => throw $
+      MkParseError starting_state "Unmatched delimiter \{show before}"
+  pure val
+```
+
+Consume any number of characters of the provided character class and discard the
+result. Also a version for doing so on both sides of a provided parser
+
+```idris
+export
+nom : Parser Char -> Parser ()
+nom x = do
+  _ <- many x
+  pure ()
+
+export
+surround : (around : Parser Char) -> (item : Parser a) -> Parser a
+surround around item = do
+  nom around
+  val <- item
+  nom around
+  pure val
+```
+
 ### Composition of boolean functions
 
 ```idris

src/Parser/JSON.md

@@ -61,13 +61,24 @@ Show (JSONValue t) where
     in assert_total $ "{\{joinBy "," xs}}"
   show (VArray xs) = 
     let xs = dMap (\_,e => show e) xs
-    in assert_total $ "[\{joinBy "," . map show $ xs}]"
+    in assert_total $ "[\{joinBy "," xs}]"
   show (VString s) = "\"\{s}\""
   show (VNumber d) = show d
   show (VBool False) = "false"
   show (VBool True) = "true"
   show VNull = "null"
 
+-- TODO: Deal with keys potentially having different orders in different objects
+Eq (JSONValue t) where
+  (VObject xs) == (VObject ys) = 
+    assert_total $ xs $== ys
+  (VArray xs) == (VArray ys) = 
+    assert_total $ xs $== ys
+  (VString s) == (VString str) = s == str
+  (VNumber d) == (VNumber dbl) = d == dbl
+  (VBool b) == (VBool x) = b == x
+  VNull == VNull = True
+
 %hide Language.Reflection.TT.WithFC.value
 -->
 
@@ -121,10 +132,8 @@ Top level json value parser
 export 
 value : Parser (t : JSONType ** JSONValue t)
 value = do 
-  _ <- many whitespace
+  surround whitespace $ oneOfE 
-  val <- oneOfE 
+    "Expected JSON Value" 
-    (throwParseError "Expected JSON Value") 
-    (the (List _) 
     [
       dpairize object
     , dpairize array
@@ -132,9 +141,7 @@ value = do
     , dpairize number
     , dpairize bool
     , dpairize null
-      ])
+    ]
-  _ <- many whitespace
-  pure val
 ```
 
 Now go through our json value types
@@ -142,72 +149,76 @@ Now go through our json value types
 ```idris
 object = do
   oneOfE 
-    (throwParseError "Expected Object") 
+    "Expected Object" 
-    (the (List _) [emptyObject, occupiedObject])
+    [emptyObject, occupiedObject]
   where
     emptyObject : Parser (JSONValue TObject)
     emptyObject = do
-      _ <- parseExactChar '{'
+      delimited '{' '}' (nom whitespace)
-      _ <- many whitespace
-      _ <- parseExactChar '}'
       pure $ VObject Nil
-    firstKeyValue : Parser (t : JSONType ** (String, JSONValue t))
+    keyValue : Parser (t : JSONType ** (String, JSONValue t))
-    firstKeyValue = do
+    keyValue = do
-      _ <- many whitespace
+      VString key <- surround whitespace string
-      VString key <- string
-      _ <- many whitespace
       _ <- parseExactChar ':'
       (typ ** val) <- value
       pure (typ ** (key, val))
     restKeyValue : Parser (t : JSONType ** (String, JSONValue t))
     restKeyValue = do
       _ <- parseExactChar ','
-      firstKeyValue
+      keyValue
+    pairs : Parser (List1 (t : JSONType ** (String, JSONValue t)))
+    pairs = do
+      first <- keyValue
+      rest <- many restKeyValue
+      pure $ first ::: rest
     occupiedObject : Parser (JSONValue TObject)
     occupiedObject = do
-      _ <- parseExactChar '{'
+      val <- delimited '{' '}' pairs
-      first <- firstKeyValue
+      let (types ** xs) = DList.fromList (forget val)
-      rest <- many restKeyValue
-      _ <- parseExactChar '}'
-      let (types ** xs) = DList.fromList (first :: rest)
       pure $ VObject xs
 ```
 
 ```idris
 array = do
   oneOfE 
-    (throwParseError "Expected Array") 
+    "Expected Array" 
-    (the (List _) [emptyArray, occupiedArray])
+    [emptyArray, occupiedArray]
   where
     emptyArray : Parser (JSONValue TArray)
     emptyArray = do
-      _ <- parseExactChar '['
+      delimited '[' ']' (nom whitespace)
-      _ <- many whitespace
-      _ <- parseExactChar ']'
       pure $ VArray Nil
     restValue : Parser (t : JSONType ** JSONValue t)
     restValue = do
       _ <- parseExactChar ','
       value
+    values : Parser (List1 (t : JSONType ** JSONValue t))
+    values = do
+      first <- value
+      rest <- many restValue
+      pure $ first ::: rest 
     occupiedArray : Parser (JSONValue TArray)
     occupiedArray = do
       _ <- parseExactChar '['
-      first <- value
+      xs <- values
-      rest <- many restValue
       _ <- parseExactChar ']'
-      let (types ** xs) = DList.fromList (first :: rest)
+      -- TODO: Why is this busted?
+      -- xs <- delimited '[' ']' values
+      let (types ** xs) = DList.fromList (forget xs)
       pure $ VArray xs
 ```
 
 ```idris
 string = do
-  _ <- parseExactChar '"'
+  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"
       e2 <- parseError "End of input"
-  contents <- parseString . many $ parseCharE (not . (== '"')) (\_ => e1) e2
+      parseCharE (not . (== '"')) (\_ => e1) e2
-  _ <- parseExactChar '"'
-  pure $ VString contents
 ```
 
 ```idris
@@ -219,8 +230,8 @@ number = do
 ```idris
 bool = do
   oneOfE
-    (throwParseError "Expected Bool")
+    "Expected Bool"
-    (the (List _) [true, false])
+    [true, false]
   where
     true : Parser (JSONValue TBool)
     true = do
@@ -237,3 +248,36 @@ null = do
   _ <- exactString "null"
   pure VNull
 ```
+
+## Unit tests
+
+Quick smoke test
+
+```idris
+-- @@test JSON Quick Smoke
+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
+    | Left err => do
+      printLn err
+      pure False
+  putStrLn "Input: \{input}\nOutput: \{show type} -> \{show parsed}"
+  let reference_object = 
+    VObject [
+      ("string", VString "string")
+    , ("number", VNumber 5.0)
+    , ("true", VBool True)
+    , ("false", VBool False)
+    , ("null", VNull)
+    , ("array", VArray [
+        VNumber 1.0
+      , VNumber 2.0
+      , VNumber 3.0
+      ])
+    ]
+  case type of
+    TObject => pure $ parsed == reference_object
+    _ => pure False
+```