Add option

libs/contrib/Data/String/Parser.idr

@@ -14,6 +14,13 @@ record State where
     pos : Int
     maxPos : Int
 
+Show State where
+    show s = "(" ++ show s.input ++", " ++ show s.pos ++ ", " ++ show s.maxPos ++")"
+
+dumpState : State -> State
+dumpState s = unsafePerformIO $ do printLn s
+                                   pure s
+
 data Result a = Fail Int String | OK a State
 
 
@@ -86,7 +93,7 @@ satisfy f = P $ \s => do if s.pos < s.maxPos
 public export
 string : Monad m => String -> ParseT m ()
 string str = P $ \s => do let len = strLength str
-                          if s.pos+len < s.maxPos
+                          if s.pos+len <= s.maxPos
                               then do let head = strSubstr s.pos len s.input
                                       if head == str
                                         then pure $ OK () (S s.input (s.pos + len) s.maxPos)
@@ -110,4 +117,8 @@ mutual
 public export
 takeWhile : Monad m => (Char -> Bool) -> ParseT m String
 takeWhile f = do ls <- many (satisfy f)
-                 pure $ pack ls
+                 pure $ pack ls
+
+export
+option : Monad m => a -> ParseT m a -> ParseT m a
+option def p = p <|> pure def

samples/StringParser.idr

@@ -1,12 +1,19 @@
 module Main
 
-import Data.String.Parser
 import Control.Monad.Identity
 import Control.Monad.Trans
 
+import Data.Maybe
+import Data.String.Parser
+
 %default partial
 -- Buld this program with '-p contrib'
 
+showRes : Show a => Either String a -> IO ()
+showRes res = case res of
+                Left err => putStrLn err
+                Right xs => printLn xs
+
 -- test lifting
 parseStuff : ParseT IO ()
 parseStuff = do a <- string "abc"
@@ -18,10 +25,12 @@ parseStuff = do a <- string "abc"
 pureParsing : String -> Either String (List Char)
 pureParsing str = parse (many (satisfy isDigit)) str
 
-showRes : Show a => Either String a -> IO ()
-showRes res = case res of
-                Left err => putStrLn err
-                Right xs => printLn xs
+
+
+optParser : ParseT IO String
+optParser = do res <- option "" (takeWhile isDigit)
+               string "def"
+               pure $ res
 
 main : IO ()
 main = do
@@ -37,4 +46,8 @@ main = do
     showRes $ pureParsing "63553"
     s <- parseT (takeWhile isDigit) "887abc8993"
     showRes s
+    res <- parseT optParser "123def"
+    showRes res
+    res <- parseT optParser "def"
+    showRes res
     pure ()