mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-27 13:40:15 +03:00
Return Bool from IOArray.writeArray
As suggested in #1677. Crashing on out-of-bounds might be more practical, but we can reconsider it later.
This commit is contained in:
parent
50c0116780
commit
c80a502627
@ -21,11 +21,12 @@ newArray size
|
||||
= pure (MkIOArray size !(primIO (prim__newArray size Nothing)))
|
||||
|
||||
export
|
||||
writeArray : HasIO io => IOArray elem -> Int -> elem -> io ()
|
||||
writeArray : HasIO io => IOArray elem -> Int -> elem -> io Bool
|
||||
writeArray arr pos el
|
||||
= if pos < 0 || pos >= max arr
|
||||
then pure ()
|
||||
else primIO (prim__arraySet (content arr) pos (Just el))
|
||||
then pure False
|
||||
else do primIO (prim__arraySet (content arr) pos (Just el))
|
||||
pure True
|
||||
|
||||
export
|
||||
readArray : HasIO io => IOArray elem -> Int -> io (Maybe elem)
|
||||
|
@ -17,7 +17,7 @@ public export
|
||||
interface Array arr => MArray arr where
|
||||
newArray : (size : Int) -> (1 _ : (1 _ : arr t) -> a) -> a
|
||||
-- Array is unchanged if the index is out of bounds
|
||||
write : (1 _ : arr t) -> Int -> t -> arr t
|
||||
write : (1 _ : arr t) -> Int -> t -> Res Bool (const (arr t))
|
||||
|
||||
mread : (1 _ : arr t) -> Int -> Res (Maybe t) (const (arr t))
|
||||
msize : (1 _ : arr t) -> Res Int (const (arr t))
|
||||
@ -45,8 +45,8 @@ MArray LinArray where
|
||||
newArray size k = k (MkLinArray (unsafePerformIO (newArray size)))
|
||||
|
||||
write (MkLinArray a) i el
|
||||
= unsafePerformIO (do writeArray a i el
|
||||
pure (MkLinArray a))
|
||||
= unsafePerformIO (do ok <- writeArray a i el
|
||||
pure (ok # MkLinArray a))
|
||||
msize (MkLinArray a) = max a # MkLinArray a
|
||||
mread (MkLinArray a) i
|
||||
= unsafePerformIO (readArray a i) # MkLinArray a
|
||||
@ -71,5 +71,6 @@ copyArray newsize a
|
||||
else let val # a = mread a pos
|
||||
1 a' = case val of
|
||||
Nothing => a'
|
||||
Just v => write a' pos v in
|
||||
Just v => let (ok # a') = write a' pos v in
|
||||
a' in
|
||||
copyContent (pos - 1) a a'
|
||||
|
@ -1,10 +1,21 @@
|
||||
import Data.IOArray
|
||||
|
||||
import System
|
||||
|
||||
main : IO ()
|
||||
main
|
||||
= do x <- newArray 20
|
||||
writeArray x 10 "Hello"
|
||||
writeArray x 11 "World"
|
||||
True <- writeArray x 10 "Hello"
|
||||
| False => do putStrLn "should success 1"
|
||||
exitFailure
|
||||
True <- writeArray x 11 "World"
|
||||
| False => do putStrLn "should success 2"
|
||||
exitFailure
|
||||
|
||||
False <- writeArray x 20 "World"
|
||||
| True => do putStrLn "should fail"
|
||||
exitFailure
|
||||
|
||||
printLn !(toList x)
|
||||
|
||||
y <- fromList (map Just [1,2,3,4,5])
|
||||
|
@ -1,10 +1,21 @@
|
||||
import Data.IOArray
|
||||
|
||||
import System
|
||||
|
||||
main : IO ()
|
||||
main
|
||||
= do x <- newArray 20
|
||||
writeArray x 10 "Hello"
|
||||
writeArray x 11 "World"
|
||||
True <- writeArray x 10 "Hello"
|
||||
| False => do putStrLn "should success 1"
|
||||
exitFailure
|
||||
True <- writeArray x 11 "World"
|
||||
| False => do putStrLn "should success 2"
|
||||
exitFailure
|
||||
|
||||
False <- writeArray x 20 "World"
|
||||
| True => do putStrLn "should fail"
|
||||
exitFailure
|
||||
|
||||
printLn !(toList x)
|
||||
|
||||
y <- fromList (map Just [1,2,3,4,5])
|
||||
|
Loading…
Reference in New Issue
Block a user