Add test and documentation

libs/contrib/Data/String/Parser.idr

@@ -8,6 +8,7 @@ import Data.Strings
 
 %default partial
 
+||| The input state, pos is position in the string and maxPos is the length of the input string.
 record State where
     constructor S
     input : String
@@ -17,10 +18,13 @@ record State where
 Show State where
     show s = "(" ++ show s.input ++", " ++ show s.pos ++ ", " ++ show s.maxPos ++")"
 
+||| A debug helper to print out the input state during parsing.
 dumpState : State -> State
 dumpState s = unsafePerformIO $ do printLn s
                                    pure s
 
+
+||| Result of applying a parser
 data Result a = Fail Int String | OK a State
 
 
@@ -70,17 +74,24 @@ MonadTrans ParseT where
     lift x = P $ \s => do res <-x
                           pure $ OK res s
 
+||| Run a parser in a monad
+||| Returns a tuple of the result and final position on success.
+||| Returns an error message on failure.
 public export
-parseT : Monad m => ParseT m a -> String -> m (Either String a)
+parseT : Monad m => ParseT m a -> String -> m (Either String (a, Int))
 parseT p str = do res <- p.runParser (S str 0 (strLength str))
                   case res of
-                      OK r s => pure $ Right r
+                      OK r s => pure $ Right (r, s.pos)
                       Fail i err => pure $ Left $ fastAppend ["Parse failed at position ", show i, ": ", err]
 
+||| Run a parser in a pure function
+||| Returns a tuple of the result and final position on success.
+||| Returns an error message on failure.
 public export
-parse : Parser a ->  String -> Either String a
+parse : Parser a -> String -> Either String (a, Int)
 parse p str = runIdentity $ parseT p str
 
+||| Succeeds if the next char satisfies the predicate `f`
 public export
 satisfy : Monad m => (Char -> Bool) -> ParseT m Char
 satisfy f = P $ \s => do if s.pos < s.maxPos
@@ -90,6 +101,8 @@ satisfy f = P $ \s => do if s.pos < s.maxPos
                                     then pure $ OK ch (S s.input (s.pos + 1) s.maxPos)
                                     else pure $ Fail (s.pos) "satisfy"
                             else pure $ Fail (s.pos) "satisfy"
+
+||| Succeeds if the string `str` follows.
 public export
 string : Monad m => String -> ParseT m ()
 string str = P $ \s => do let len = strLength str
@@ -100,29 +113,37 @@ string str = P $ \s => do let len = strLength str
                                         else pure $ Fail (s.pos) ("string " ++ show str)
                               else pure $ Fail (s.pos) ("string " ++ show str)
 
+||| Succeeds if the next char is `c`
 public export
 char : Monad m => Char -> ParseT m ()
 char c = do _ <- satisfy (== c)
             pure ()
 
 mutual
+    ||| Succeeds if `p` succeeds, will continue to match `p` until it fails
+    ||| and accumulate the results in a list
     public export
     some : Monad m => ParseT m a -> ParseT m (List a)
     some p = pure (!p :: !(many p))
 
+    ||| Always succeeds, will accumulate the results of `p` in a list until it fails.
     public export
     many : Monad m => ParseT m a -> ParseT m (List a)
     many p = some p <|> pure []
 
+||| Always succeeds, applies the predicate `f` on chars until it fails and creates a string
+||| from the results.
 public export
 takeWhile : Monad m => (Char -> Bool) -> ParseT m String
 takeWhile f = do ls <- many (satisfy f)
                  pure $ pack ls
 
+||| Returns the result of the parser `p` or `def` if it fails.
 export
 option : Monad m => a -> ParseT m a -> ParseT m a
 option def p = p <|> pure def
 
+||| Returns a Maybe that contains the result of `p` if it succeeds or `Nothing` if it fails.
 export
 optional : Monad m => ParseT m a -> ParseT m (Maybe a)
-optional p = (p >>= \res => pure $ Just res) <|> pure Nothing
+optional p = (p >>= \res => pure $ Just res) <|> pure Nothing

tests/Main.idr

@@ -120,7 +120,7 @@ chezTests
       "chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
       "chez013", "chez014", "chez015", "chez016", "chez017", "chez018",
       "chez019", "chez020", "chez021", "chez022", "chez023", "chez024",
-      "chez025", "chez026",
+      "chez025", "chez026", "chez027",
       "reg001"]
 
 ideModeTests : List String

tests/chez/chez027/StringParser.idr

@@ -7,12 +7,12 @@ import Data.Maybe
 import Data.String.Parser
 
 %default partial
--- Buld this program with '-p contrib'
+-- Build this program with '-p contrib'
 
-showRes : Show a => Either String a -> IO ()
+showRes : Show a => Either String (a, Int) -> IO ()
 showRes res = case res of
                 Left err => putStrLn err
-                Right xs => printLn xs
+                Right (xs, rem) => printLn xs
 
 -- test lifting
 parseStuff : ParseT IO ()
@@ -22,16 +22,17 @@ parseStuff = do a <- string "abc"
                 pure ()
 
 -- test a parsing from a pure function
-pureParsing : String -> Either String (List Char)
+pureParsing : String -> Either String ((List Char), Int)
 pureParsing str = parse (many (satisfy isDigit)) str
 
 
-
+-- test option
 optParser : ParseT IO String
 optParser = do res <- option "" (takeWhile isDigit)
                string "def"
                pure $ res
 
+-- test optional
 maybeParser : ParseT IO Bool
 maybeParser = do res <- optional (string "abc")
                  string "def"
@@ -40,14 +41,14 @@ maybeParser = do res <- optional (string "abc")
 main : IO ()
 main = do
     res <- parseT parseStuff "abcdef"
-    res <- parseT (string "hi") "hideous"
+    res <- parseT (string "hi") "hiyaaaaaa"
     case res of
         Left err => putStrLn "NOOOOOOO!"
-        Right () => putStrLn "YEEEES!"
-    digs <- parseT (satisfy isDigit) "a"
+        Right ((), i) => printLn i
+    bad <- parseT (satisfy isDigit) "a"
+    showRes bad
+    digs <- parseT (many (satisfy isDigit)) "766775"
     showRes digs
-    migs <- parseT (many (satisfy isDigit)) "766775"
-    showRes migs
     showRes $ pureParsing "63553"
     s <- parseT (takeWhile isDigit) "887abc8993"
     showRes s

tests/chez/chez027/expected

@@ -0,0 +1,12 @@
+hiya
+2
+Parse failed at position 0: satisfy
+['7', '6', '6', '7', '7', '5']
+['6', '3', '5', '5', '3']
+"887"
+"123"
+""
+True
+False
+1/1: Building StringParser (StringParser.idr)
+Main> Main> Bye for now!

tests/chez/chez027/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez027/run

@@ -0,0 +1,3 @@
+$1 --no-banner -p contrib StringParser.idr < input
+
+rm -rf build