Add takeWhile

add substring and length primitives to Data.Strings

libs/base/Data/Strings.idr

@@ -171,6 +171,14 @@ export partial
 strIndex : String -> Int -> Char
 strIndex = prim__strIndex
 
+export partial
+strLength : String -> Int
+strLength = prim__strLength
+
+export partial
+strSubstr : Int -> Int -> String -> String
+strSubstr = prim__strSubstr
+
 export partial
 strTail : String -> String
 strTail = prim__strTail

libs/contrib/Data/String/Parser.idr

@@ -8,16 +8,15 @@ import Data.Strings
 
 %default partial
 
-public export
 record State where
     constructor S
     input : String
     pos : Int
     maxPos : Int
 
-public export
 data Result a = Fail Int String | OK a State
 
+
 public export
 record ParseT (m : Type -> Type) (a : Type) where
     constructor P
@@ -66,7 +65,7 @@ MonadTrans ParseT where
 
 public export
 parseT : Monad m => ParseT m a -> String -> m (Either String a)
-parseT p str = do res <- p.runParser (S str 0 (cast $ length str))
+parseT p str = do res <- p.runParser (S str 0 (strLength str))
                   case res of
                       OK r s => pure $ Right r
                       Fail i err => pure $ Left $ fastAppend ["Parse failed at position ", show i, ": ", err]
@@ -86,9 +85,9 @@ satisfy f = P $ \s => do if s.pos < s.maxPos
                             else pure $ Fail (s.pos) "satisfy"
 public export
 string : Monad m => String -> ParseT m ()
-string str = P $ \s => do let len : Int = cast $ length str
+string str = P $ \s => do let len = strLength str
                           if s.pos+len < s.maxPos
-                              then do let head = substr (fromInteger $ cast s.pos) (length str) s.input
+                              then do let head = strSubstr s.pos len s.input
                                       if head == str
                                         then pure $ OK () (S s.input (s.pos + len) s.maxPos)
                                         else pure $ Fail (s.pos) ("string " ++ show str)
@@ -108,3 +107,7 @@ mutual
     many : Monad m => ParseT m a -> ParseT m (List a)
     many p = some p <|> pure []
 
+public export
+takeWhile : Monad m => (Char -> Bool) -> ParseT m String
+takeWhile f = do ls <- many (satisfy f)
+                 pure $ pack ls

samples/StringParser.idr

@@ -7,15 +7,22 @@ import Control.Monad.Trans
 %default partial
 -- Buld this program with '-p contrib'
 
+-- test lifting
 parseStuff : ParseT IO ()
 parseStuff = do a <- string "abc"
                 lift $ putStrLn "hiya"
                 b <- string "def"
                 pure ()
 
+-- test a parsing from a pure function
 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
+
 main : IO ()
 main = do
     res <- parseT parseStuff "abcdef"
@@ -23,16 +30,11 @@ main = do
     case res of
         Left err => putStrLn "NOOOOOOO!"
         Right () => putStrLn "YEEEES!"
-    digs <- parseT (satisfy isDigit) "8878993"
-    case digs of
-        Left err => putStrLn "NOOOOOOO!"
-        Right ds => printLn ds
+    digs <- parseT (satisfy isDigit) "a"
+    showRes digs
     migs <- parseT (many (satisfy isDigit)) "766775"
-    case migs of
-        Left err => putStrLn "NOOOOOOO!"
-        Right ds => printLn ds
-    let pp = pureParsing "63553"
-    case pp of
-        Left err => putStrLn err
-        Right xs => printLn xs
+    showRes migs
+    showRes $ pureParsing "63553"
+    s <- parseT (takeWhile isDigit) "887abc8993"
+    showRes s
     pure ()