From d97789190d85e78770d2a488ae0cb04e69e40d39 Mon Sep 17 00:00:00 2001
From: Niklas Larsson <niklas@mm.st>
Date: Sun, 5 Jul 2020 00:59:57 +0200
Subject: [PATCH] Add bounds checking

---
 libs/contrib/Data/String/Parser.idr | 41 +++++++++++++++++++++--------
 samples/StringParser.idr            |  4 +++
 2 files changed, 34 insertions(+), 11 deletions(-)

diff --git a/libs/contrib/Data/String/Parser.idr b/libs/contrib/Data/String/Parser.idr
index 9043c6b59..a81c32962 100644
--- a/libs/contrib/Data/String/Parser.idr
+++ b/libs/contrib/Data/String/Parser.idr
@@ -11,6 +11,7 @@ record State where
     constructor S
     input : String
     pos : Int
+    maxPos : Int
 
 public export
 data Result a = Fail Int String | OK a State
@@ -59,7 +60,7 @@ Monad m => Alternative (ParseT m) where
 
 public export
 parseT : Monad m => ParseT m a -> String -> m (Either String a)
-parseT p str = do res <- p.runParser (S str 0)
+parseT p str = do res <- p.runParser (S str 0 (cast $ length str))
                   case res of
                       OK r s => pure$ Right r
                       Fail i err => pure$ Left $ fastAppend ["Parse failed at position ", show i, ": ", err]
@@ -70,16 +71,34 @@ parse p str = runIdentity $ parseT p str
 
 public export
 satisfy : Monad m => (Char -> Bool) -> ParseT m Char
-satisfy f = P $ \s => do let ch = strIndex s.input s.pos
-                         if f ch
-                             then pure $ OK ch (S s.input (s.pos + 1))
-                             else pure $ Fail (s.pos) "satisfy"
-
+satisfy f = P $ \s => do if s.pos < s.maxPos
+                            then do
+                                let ch = strIndex s.input s.pos
+                                if f ch
+                                    then pure $ OK ch (S s.input (s.pos + 1) s.maxPos)
+                                    else pure $ Fail (s.pos) "satisfy"
+                            else pure $ Fail (s.pos) "satisfy"
 public export
 string : Monad m => String -> ParseT m ()
-string str = P $ \s => do let len = length str
-                          let head = substr (fromInteger $ cast s.pos) len s.input
-                          if head == str
-                            then pure $ OK () (S s.input (s.pos + cast len))
-                            else pure $ Fail (s.pos) ("string " ++ show str)
+string str = P $ \s => do let len : Int = cast $ length str
+                          if s.pos+len < s.maxPos
+                              then do let head = substr (fromInteger $ cast s.pos) (length str) s.input
+                                      if head == str
+                                        then pure $ OK () (S s.input (s.pos + len) s.maxPos)
+                                        else pure $ Fail (s.pos) ("string " ++ show str)
+                              else pure $ Fail (s.pos) ("string " ++ show str)
+
+public export
+char : Monad m => Char -> ParseT m ()
+char c = do _ <- satisfy (== c)
+            pure ()
+
+mutual
+    public export
+    some : Monad m => ParseT m a -> ParseT m (List a)
+    some p = pure (!p :: !(many p))
+
+    public export
+    many : Monad m => ParseT m a -> ParseT m (List a)
+    many p = some p <|> pure []
 
diff --git a/samples/StringParser.idr b/samples/StringParser.idr
index 2f31fb779..16f145ea6 100644
--- a/samples/StringParser.idr
+++ b/samples/StringParser.idr
@@ -14,5 +14,9 @@ main = do
         Right () => putStrLn "YEEEES!"
     digs <- parseT (satisfy isDigit) "8878993"
     case digs of
+        Left err => putStrLn "NOOOOOOO!"
+        Right ds => printLn ds
+    migs <- parseT (many (satisfy isDigit)) "766775"
+    case migs of
         Left err => putStrLn "NOOOOOOO!"
         Right ds => printLn ds
\ No newline at end of file