json: Bool and null

src/Parser/Interface.md

@@ -20,11 +20,8 @@ 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
@@ -37,13 +34,6 @@ 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
@@ -51,7 +41,7 @@ Show ParseError where
 ```idris
 public export
 Parser : Type -> Type
-Parser a = Eff [ParserState, Except ParseError] a
+Parser a = Eff [ParserState, Except ParseError, Choose] a
 ```
 
 ## Error Generation
@@ -103,7 +93,7 @@ no paths in the `Choice` effect produce a returning parse.
 export
 rundownFirst : (f : Parser a) -> Eff [ParserState] (Either ParseError a)
 rundownFirst f = 
-  runExcept f
+  runExcept . guardMaybe "No returning parses" . runChoose {f = Maybe} $ f
 ```
 
 Provide wrappers for `rundownFirst` for evaluating it in various contexts.
@@ -158,29 +148,27 @@ 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.
+the provided error action on failure. This will suppress any errors returned by
+the input parsers by mapping them to `empty`.
 
 The state will not be modified when an input parser fails
 
 ```idris
 export
-oneOfE : (err : String) -> List (Parser a) -> Parser a
-oneOfE err xs = do
-  start <- save
-  oneOfE' err start [] xs
+oneOfE : Foldable f =>
+  (err : Parser a) -> f (Parser a) -> Parser a
+oneOfE err xs = foldr altE err xs
   where
-    oneOfE' : (err : String) -> (start : ParserInternal Id) 
-      -> (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
+    altE : Parser a -> Parser a -> Parser a
+    altE f rest = (tryEmpty f) `alt` rest
 ```
 
 Attempt to parse 0+ of an item
@@ -210,7 +198,6 @@ 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
@@ -263,40 +250,6 @@ 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,24 +61,13 @@ Show (JSONValue t) where
     in assert_total $ "{\{joinBy "," xs}}"
   show (VArray xs) = 
     let xs = dMap (\_,e => show e) xs
-    in assert_total $ "[\{joinBy "," xs}]"
+    in assert_total $ "[\{joinBy "," . map show $ 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
 -->
 
@@ -132,16 +121,20 @@ Top level json value parser
 export 
 value : Parser (t : JSONType ** JSONValue t)
 value = do 
-  surround whitespace $ oneOfE 
-    "Expected JSON Value" 
-    [
-      dpairize object
-    , dpairize array
-    , dpairize string
-    , dpairize number
-    , dpairize bool
-    , dpairize null
-    ]
+  _ <- many whitespace
+  val <- oneOfE 
+    (throwParseError "Expected JSON Value") 
+    (the (List _) 
+      [
+        dpairize object
+      , dpairize array
+      , dpairize string
+      , dpairize number
+      , dpairize bool
+      , dpairize null
+      ])
+  _ <- many whitespace
+  pure val
 ```
 
 Now go through our json value types
@@ -149,76 +142,72 @@ Now go through our json value types
 ```idris
 object = do
   oneOfE 
-    "Expected Object" 
-    [emptyObject, occupiedObject]
+    (throwParseError "Expected Object") 
+    (the (List _) [emptyObject, occupiedObject])
   where
     emptyObject : Parser (JSONValue TObject)
     emptyObject = do
-      delimited '{' '}' (nom whitespace)
+      _ <- parseExactChar '{'
+      _ <- many whitespace
+      _ <- parseExactChar '}'
       pure $ VObject Nil
-    keyValue : Parser (t : JSONType ** (String, JSONValue t))
-    keyValue = do
-      VString key <- surround whitespace string
+    firstKeyValue : Parser (t : JSONType ** (String, JSONValue t))
+    firstKeyValue = do
+      _ <- many whitespace
+      VString key <- string
+      _ <- many whitespace
       _ <- parseExactChar ':'
       (typ ** val) <- value
       pure (typ ** (key, val))
     restKeyValue : Parser (t : JSONType ** (String, JSONValue t))
     restKeyValue = do
       _ <- parseExactChar ','
-      keyValue
-    pairs : Parser (List1 (t : JSONType ** (String, JSONValue t)))
-    pairs = do
-      first <- keyValue
-      rest <- many restKeyValue
-      pure $ first ::: rest
+      firstKeyValue
     occupiedObject : Parser (JSONValue TObject)
     occupiedObject = do
-      val <- delimited '{' '}' pairs
-      let (types ** xs) = DList.fromList (forget val)
+      _ <- parseExactChar '{'
+      first <- firstKeyValue
+      rest <- many restKeyValue
+      _ <- parseExactChar '}'
+      let (types ** xs) = DList.fromList (first :: rest)
       pure $ VObject xs
 ```
 
 ```idris
 array = do
   oneOfE 
-    "Expected Array" 
-    [emptyArray, occupiedArray]
+    (throwParseError "Expected Array") 
+    (the (List _) [emptyArray, occupiedArray])
   where
     emptyArray : Parser (JSONValue TArray)
     emptyArray = do
-      delimited '[' ']' (nom whitespace)
+      _ <- parseExactChar '['
+      _ <- 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 '['
-      xs <- values
+      first <- value
+      rest <- many restValue
       _ <- parseExactChar ']'
-      -- TODO: Why is this busted?
-      -- xs <- delimited '[' ']' values
-      let (types ** xs) = DList.fromList (forget xs)
+      let (types ** xs) = DList.fromList (first :: rest)
       pure $ VArray xs
 ```
 
 ```idris
 string = do
-  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"
-      parseCharE (not . (== '"')) (\_ => e1) e2
+  _ <- parseExactChar '"'
+  -- TODO: Handle control characters properly
+  e1 <- parseError "Expected non-quote, got quote"
+  e2 <- parseError "End of input"
+  contents <- parseString . many $ parseCharE (not . (== '"')) (\_ => e1) e2
+  _ <- parseExactChar '"'
+  pure $ VString contents
 ```
 
 ```idris
@@ -230,8 +219,8 @@ number = do
 ```idris
 bool = do
   oneOfE
-    "Expected Bool"
-    [true, false]
+    (throwParseError "Expected Bool")
+    (the (List _) [true, false])
   where
     true : Parser (JSONValue TBool)
     true = do
@@ -248,36 +237,3 @@ 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
-```