idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 20:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Add bounds checking

Browse Source
This commit is contained in:
Niklas Larsson 2020-07-05 00:59:57 +02:00
parent f290c6c3ce
commit d97789190d
2 changed files with 34 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
libs/contrib/Data/String/Parser.idr
View File

@ -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 []

4
samples/StringParser.idr
View File

@ -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