Split HasIO into HasIO and MonadIO

For things which don't require (>>=), HasIO is fine, otherwise MonadIO
gives access to the monad interface.
This commit is contained in:
Edwin Brady 2020-06-21 14:46:14 +01:00
parent d12487f529
commit 28855088c2
11 changed files with 59 additions and 49 deletions

View File

@ -20,6 +20,9 @@ Language changes:
Library changes: Library changes:
* `IO` operations in the `prelude` and `base` libraries now use the
`HasIO` interface, rather than using `IO` directly.
+ Also, added a `MonadIO` interface for operations which require `(>>=)`.
* Experimental `Data.Linear.Array` added to `contrib`, support mutable linear * Experimental `Data.Linear.Array` added to `contrib`, support mutable linear
arrays with constant time read/write, convertible to immutable arrays with arrays with constant time read/write, convertible to immutable arrays with
constant time read. constant time read.

View File

@ -14,19 +14,19 @@ max : IOArray elem -> Int
max = maxSize max = maxSize
export export
newArray : Int -> IO (IOArray elem) newArray : MonadIO io => Int -> io (IOArray elem)
newArray size newArray size
= pure (MkIOArray size !(primIO (prim__newArray size Nothing))) = pure (MkIOArray size !(primIO (prim__newArray size Nothing)))
export export
writeArray : IOArray elem -> Int -> elem -> IO () writeArray : MonadIO io => IOArray elem -> Int -> elem -> io ()
writeArray arr pos el writeArray arr pos el
= if pos < 0 || pos >= max arr = if pos < 0 || pos >= max arr
then pure () then pure ()
else primIO (prim__arraySet (content arr) pos (Just el)) else primIO (prim__arraySet (content arr) pos (Just el))
export export
readArray : IOArray elem -> Int -> IO (Maybe elem) readArray : MonadIO io => IOArray elem -> Int -> io (Maybe elem)
readArray arr pos readArray arr pos
= if pos < 0 || pos >= max arr = if pos < 0 || pos >= max arr
then pure Nothing then pure Nothing
@ -35,7 +35,8 @@ readArray arr pos
-- Make a new array of the given size with the elements copied from the -- Make a new array of the given size with the elements copied from the
-- other array -- other array
export export
newArrayCopy : (newsize : Int) -> IOArray elem -> IO (IOArray elem) newArrayCopy : MonadIO io =>
(newsize : Int) -> IOArray elem -> io (IOArray elem)
newArrayCopy newsize arr newArrayCopy newsize arr
= do let newsize' = if newsize < max arr then max arr else newsize = do let newsize' = if newsize < max arr then max arr else newsize
arr' <- newArray newsize' arr' <- newArray newsize'
@ -44,7 +45,7 @@ newArrayCopy newsize arr
where where
copyFrom : ArrayData (Maybe elem) -> copyFrom : ArrayData (Maybe elem) ->
ArrayData (Maybe elem) -> ArrayData (Maybe elem) ->
Int -> IO () Int -> io ()
copyFrom old new pos copyFrom old new pos
= if pos < 0 = if pos < 0
then pure () then pure ()
@ -53,10 +54,10 @@ newArrayCopy newsize arr
assert_total (copyFrom old new (pos - 1)) assert_total (copyFrom old new (pos - 1))
export export
toList : IOArray elem -> IO (List (Maybe elem)) toList : MonadIO io => IOArray elem -> io (List (Maybe elem))
toList arr = iter 0 (max arr) [] toList arr = iter 0 (max arr) []
where where
iter : Int -> Int -> List (Maybe elem) -> IO (List (Maybe elem)) iter : Int -> Int -> List (Maybe elem) -> io (List (Maybe elem))
iter pos end acc iter pos end acc
= if pos >= end = if pos >= end
then pure (reverse acc) then pure (reverse acc)

View File

@ -13,7 +13,7 @@ data IORef : Type -> Type where
MkRef : Mut a -> IORef a MkRef : Mut a -> IORef a
export export
newIORef : HasIO io => a -> io (IORef a) newIORef : MonadIO io => a -> io (IORef a)
newIORef val newIORef val
= do m <- primIO (prim__newIORef val) = do m <- primIO (prim__newIORef val)
pure (MkRef m) pure (MkRef m)
@ -29,7 +29,7 @@ writeIORef : HasIO io => IORef a -> (1 val : a) -> io ()
writeIORef (MkRef m) val = primIO (prim__writeIORef m val) writeIORef (MkRef m) val = primIO (prim__writeIORef m val)
export export
modifyIORef : HasIO io => IORef a -> (a -> a) -> io () modifyIORef : MonadIO io => IORef a -> (a -> a) -> io ()
modifyIORef ref f modifyIORef ref f
= do val <- readIORef ref = do val <- readIORef ref
writeIORef ref (f val) writeIORef ref (f val)

View File

@ -10,7 +10,7 @@ interface Ref m (r : Type -> Type) | m where
writeRef : r a -> a -> m () writeRef : r a -> a -> m ()
export export
HasIO io => Ref io IORef where MonadIO io => Ref io IORef where
newRef = newIORef newRef = newIORef
readRef = readIORef readRef = readIORef
writeRef = writeIORef writeRef = writeIORef

View File

@ -42,7 +42,7 @@ prim_setEnv : String -> String -> Int -> PrimIO Int
prim_unsetEnv : String -> PrimIO Int prim_unsetEnv : String -> PrimIO Int
export export
getEnv : HasIO io => String -> io (Maybe String) getEnv : MonadIO io => String -> io (Maybe String)
getEnv var getEnv var
= do env <- primIO $ prim_getEnv var = do env <- primIO $ prim_getEnv var
if prim__nullPtr env /= 0 if prim__nullPtr env /= 0
@ -50,7 +50,7 @@ getEnv var
else pure (Just (prim__getString env)) else pure (Just (prim__getString env))
export export
getEnvironment : HasIO io => io (List (String, String)) getEnvironment : MonadIO io => io (List (String, String))
getEnvironment = getAllPairs 0 [] getEnvironment = getAllPairs 0 []
where where
splitEq : String -> (String, String) splitEq : String -> (String, String)
@ -67,7 +67,7 @@ getEnvironment = getAllPairs 0 []
else getAllPairs (n + 1) (prim__getString envPair :: acc) else getAllPairs (n + 1) (prim__getString envPair :: acc)
export export
setEnv : HasIO io => String -> String -> Bool -> io Bool setEnv : MonadIO io => String -> String -> Bool -> io Bool
setEnv var val overwrite setEnv var val overwrite
= do ok <- primIO $ prim_setEnv var val (if overwrite then 1 else 0) = do ok <- primIO $ prim_setEnv var val (if overwrite then 1 else 0)
if ok == 0 if ok == 0
@ -75,7 +75,7 @@ setEnv var val overwrite
else pure False else pure False
export export
unsetEnv : HasIO io => String -> io Bool unsetEnv : MonadIO io => String -> io Bool
unsetEnv var unsetEnv var
= do ok <- primIO $ prim_unsetEnv var = do ok <- primIO $ prim_unsetEnv var
if ok == 0 if ok == 0
@ -95,7 +95,7 @@ system cmd = primIO (prim_system cmd)
prim_time : PrimIO Int prim_time : PrimIO Int
export export
time : HasIO io => io Integer time : MonadIO io => io Integer
time = pure $ cast !(primIO prim_time) time = pure $ cast !(primIO prim_time)
%foreign libc "exit" %foreign libc "exit"

View File

@ -12,7 +12,7 @@ support fn = "C:" ++ fn ++ ", libidris2_support"
%foreign support "idris2_fileErrno" %foreign support "idris2_fileErrno"
prim_fileErrno : PrimIO Int prim_fileErrno : PrimIO Int
returnError : HasIO io => io (Either FileError a) returnError : MonadIO io => io (Either FileError a)
returnError returnError
= do err <- primIO prim_fileErrno = do err <- primIO prim_fileErrno
case err of case err of
@ -23,7 +23,7 @@ returnError
4 => pure $ Left FileExists 4 => pure $ Left FileExists
_ => pure $ Left (GenericFileError (err-5)) _ => pure $ Left (GenericFileError (err-5))
ok : HasIO io => a -> io (Either FileError a) ok : MonadIO io => a -> io (Either FileError a)
ok x = pure (Right x) ok x = pure (Right x)
%foreign support "idris2_currentDirectory" %foreign support "idris2_currentDirectory"
@ -52,7 +52,7 @@ data Directory : Type where
MkDir : DirPtr -> Directory MkDir : DirPtr -> Directory
export export
createDir : HasIO io => String -> io (Either FileError ()) createDir : MonadIO io => String -> io (Either FileError ())
createDir dir createDir dir
= do res <- primIO (prim_createDir dir) = do res <- primIO (prim_createDir dir)
if res == 0 if res == 0
@ -60,13 +60,13 @@ createDir dir
else returnError else returnError
export export
changeDir : HasIO io => String -> io Bool changeDir : MonadIO io => String -> io Bool
changeDir dir changeDir dir
= do ok <- primIO (prim_changeDir dir) = do ok <- primIO (prim_changeDir dir)
pure (ok == 0) pure (ok == 0)
export export
currentDir : HasIO io => io (Maybe String) currentDir : MonadIO io => io (Maybe String)
currentDir currentDir
= do res <- primIO prim_currentDir = do res <- primIO prim_currentDir
if prim__nullPtr res /= 0 if prim__nullPtr res /= 0
@ -74,7 +74,7 @@ currentDir
else pure (Just (prim__getString res)) else pure (Just (prim__getString res))
export export
openDir : HasIO io => String -> io (Either FileError Directory) openDir : MonadIO io => String -> io (Either FileError Directory)
openDir d openDir d
= do res <- primIO (prim_openDir d) = do res <- primIO (prim_openDir d)
if prim__nullAnyPtr res /= 0 if prim__nullAnyPtr res /= 0
@ -90,7 +90,7 @@ removeDir : HasIO io => String -> io ()
removeDir dirName = primIO (prim_removeDir dirName) removeDir dirName = primIO (prim_removeDir dirName)
export export
dirEntry : HasIO io => Directory -> io (Either FileError String) dirEntry : MonadIO io => Directory -> io (Either FileError String)
dirEntry (MkDir d) dirEntry (MkDir d)
= do res <- primIO (prim_dirEntry d) = do res <- primIO (prim_dirEntry d)
if prim__nullPtr res /= 0 if prim__nullPtr res /= 0

View File

@ -84,7 +84,7 @@ data FileError = GenericFileError Int -- errno
| PermissionDenied | PermissionDenied
| FileExists | FileExists
returnError : HasIO io => io (Either FileError a) returnError : MonadIO io => io (Either FileError a)
returnError returnError
= do err <- primIO prim_fileErrno = do err <- primIO prim_fileErrno
case err of case err of
@ -104,7 +104,7 @@ Show FileError where
show PermissionDenied = "Permission Denied" show PermissionDenied = "Permission Denied"
show FileExists = "File Exists" show FileExists = "File Exists"
ok : HasIO io => a -> io (Either FileError a) ok : MonadIO io => a -> io (Either FileError a)
ok x = pure (Right x) ok x = pure (Right x)
public export public export
@ -124,7 +124,7 @@ stderr : File
stderr = FHandle prim__stderr stderr = FHandle prim__stderr
export export
openFile : HasIO io => String -> Mode -> io (Either FileError File) openFile : MonadIO io => String -> Mode -> io (Either FileError File)
openFile f m openFile f m
= do res <- primIO (prim__open f (modeStr m) 0) = do res <- primIO (prim__open f (modeStr m) 0)
if prim__nullAnyPtr res /= 0 if prim__nullAnyPtr res /= 0
@ -136,13 +136,13 @@ closeFile : HasIO io => File -> io ()
closeFile (FHandle f) = primIO (prim__close f) closeFile (FHandle f) = primIO (prim__close f)
export export
fileError : HasIO io => File -> io Bool fileError : MonadIO io => File -> io Bool
fileError (FHandle f) fileError (FHandle f)
= do x <- primIO $ prim_error f = do x <- primIO $ prim_error f
pure (x /= 0) pure (x /= 0)
export export
fGetLine : HasIO io => (h : File) -> io (Either FileError String) fGetLine : MonadIO io => (h : File) -> io (Either FileError String)
fGetLine (FHandle f) fGetLine (FHandle f)
= do res <- primIO (prim__readLine f) = do res <- primIO (prim__readLine f)
if prim__nullPtr res /= 0 if prim__nullPtr res /= 0
@ -150,7 +150,7 @@ fGetLine (FHandle f)
else ok (prim__getString res) else ok (prim__getString res)
export export
fGetChars : HasIO io => (h : File) -> Int -> io (Either FileError String) fGetChars : MonadIO io => (h : File) -> Int -> io (Either FileError String)
fGetChars (FHandle f) max fGetChars (FHandle f) max
= do res <- primIO (prim__readChars max f) = do res <- primIO (prim__readChars max f)
if prim__nullPtr res /= 0 if prim__nullPtr res /= 0
@ -158,7 +158,7 @@ fGetChars (FHandle f) max
else ok (prim__getString res) else ok (prim__getString res)
export export
fGetChar : HasIO io => (h : File) -> io (Either FileError Char) fGetChar : MonadIO io => (h : File) -> io (Either FileError Char)
fGetChar (FHandle h) fGetChar (FHandle h)
= do c <- primIO (prim__readChar h) = do c <- primIO (prim__readChar h)
ferr <- primIO (prim_error h) ferr <- primIO (prim_error h)
@ -167,7 +167,7 @@ fGetChar (FHandle h)
else ok (cast c) else ok (cast c)
export export
fPutStr : HasIO io => (h : File) -> String -> io (Either FileError ()) fPutStr : MonadIO io => (h : File) -> String -> io (Either FileError ())
fPutStr (FHandle f) str fPutStr (FHandle f) str
= do res <- primIO (prim__writeLine f str) = do res <- primIO (prim__writeLine f str)
if res == 0 if res == 0
@ -175,23 +175,23 @@ fPutStr (FHandle f) str
else ok () else ok ()
export export
fPutStrLn : HasIO io => (h : File) -> String -> io (Either FileError ()) fPutStrLn : MonadIO io => (h : File) -> String -> io (Either FileError ())
fPutStrLn f str = fPutStr f (str ++ "\n") fPutStrLn f str = fPutStr f (str ++ "\n")
export export
fEOF : HasIO io => (h : File) -> io Bool fEOF : MonadIO io => (h : File) -> io Bool
fEOF (FHandle f) fEOF (FHandle f)
= do res <- primIO (prim__eof f) = do res <- primIO (prim__eof f)
pure (res /= 0) pure (res /= 0)
export export
fflush : HasIO io => (h : File) -> io () fflush : MonadIO io => (h : File) -> io ()
fflush (FHandle f) fflush (FHandle f)
= do primIO (prim__flush f) = do primIO (prim__flush f)
pure () pure ()
export export
popen : HasIO io => String -> Mode -> io (Either FileError File) popen : MonadIO io => String -> Mode -> io (Either FileError File)
popen f m = do popen f m = do
ptr <- primIO (prim__popen f (modeStr m)) ptr <- primIO (prim__popen f (modeStr m))
if prim__nullAnyPtr ptr /= 0 if prim__nullAnyPtr ptr /= 0
@ -203,7 +203,7 @@ pclose : HasIO io => File -> io ()
pclose (FHandle h) = primIO (prim__pclose h) pclose (FHandle h) = primIO (prim__pclose h)
export export
fileAccessTime : HasIO io => (h : File) -> io (Either FileError Int) fileAccessTime : MonadIO io => (h : File) -> io (Either FileError Int)
fileAccessTime (FHandle f) fileAccessTime (FHandle f)
= do res <- primIO (prim__fileAccessTime f) = do res <- primIO (prim__fileAccessTime f)
if res > 0 if res > 0
@ -211,7 +211,7 @@ fileAccessTime (FHandle f)
else returnError else returnError
export export
fileModifiedTime : HasIO io => (h : File) -> io (Either FileError Int) fileModifiedTime : MonadIO io => (h : File) -> io (Either FileError Int)
fileModifiedTime (FHandle f) fileModifiedTime (FHandle f)
= do res <- primIO (prim__fileModifiedTime f) = do res <- primIO (prim__fileModifiedTime f)
if res > 0 if res > 0
@ -219,7 +219,7 @@ fileModifiedTime (FHandle f)
else returnError else returnError
export export
fileStatusTime : HasIO io => (h : File) -> io (Either FileError Int) fileStatusTime : MonadIO io => (h : File) -> io (Either FileError Int)
fileStatusTime (FHandle f) fileStatusTime (FHandle f)
= do res <- primIO (prim__fileStatusTime f) = do res <- primIO (prim__fileStatusTime f)
if res > 0 if res > 0
@ -227,7 +227,7 @@ fileStatusTime (FHandle f)
else returnError else returnError
export export
removeFile : HasIO io => String -> io (Either FileError ()) removeFile : MonadIO io => String -> io (Either FileError ())
removeFile fname removeFile fname
= do res <- primIO (prim__removeFile fname) = do res <- primIO (prim__removeFile fname)
if res == 0 if res == 0
@ -235,7 +235,7 @@ removeFile fname
else returnError else returnError
export export
fileSize : HasIO io => (h : File) -> io (Either FileError Int) fileSize : MonadIO io => (h : File) -> io (Either FileError Int)
fileSize (FHandle f) fileSize (FHandle f)
= do res <- primIO (prim__fileSize f) = do res <- primIO (prim__fileSize f)
if res >= 0 if res >= 0
@ -243,13 +243,13 @@ fileSize (FHandle f)
else returnError else returnError
export export
fPoll : HasIO io => File -> io Bool fPoll : MonadIO io => File -> io Bool
fPoll (FHandle f) fPoll (FHandle f)
= do p <- primIO (prim__fPoll f) = do p <- primIO (prim__fPoll f)
pure (p > 0) pure (p > 0)
export export
readFile : HasIO io => String -> io (Either FileError String) readFile : MonadIO io => String -> io (Either FileError String)
readFile file readFile file
= do Right h <- openFile file Read = do Right h <- openFile file Read
| Left err => returnError | Left err => returnError
@ -271,7 +271,7 @@ readFile file
||| Write a string to a file ||| Write a string to a file
export export
writeFile : HasIO io => writeFile : MonadIO io =>
(filepath : String) -> (contents : String) -> (filepath : String) -> (contents : String) ->
io (Either FileError ()) io (Either FileError ())
writeFile fn contents = do writeFile fn contents = do
@ -307,7 +307,7 @@ mkMode p
getMs = sum . map getM getMs = sum . map getM
export export
chmodRaw : HasIO io => String -> Int -> io (Either FileError ()) chmodRaw : MonadIO io => String -> Int -> io (Either FileError ())
chmodRaw fname p chmodRaw fname p
= do ok <- primIO $ prim__chmod fname p = do ok <- primIO $ prim__chmod fname p
if ok == 0 if ok == 0
@ -315,5 +315,5 @@ chmodRaw fname p
else returnError else returnError
export export
chmod : HasIO io => String -> Permissions -> io (Either FileError ()) chmod : MonadIO io => String -> Permissions -> io (Either FileError ())
chmod fname p = chmodRaw fname (mkMode p) chmod fname p = chmodRaw fname (mkMode p)

View File

@ -8,7 +8,7 @@ import System.File
||| @ onInput the function to run on reading input, returning a String to ||| @ onInput the function to run on reading input, returning a String to
||| output and a new state. Returns Nothing if the repl should exit ||| output and a new state. Returns Nothing if the repl should exit
export export
replWith : HasIO io => replWith : MonadIO io =>
(state : a) -> (prompt : String) -> (state : a) -> (prompt : String) ->
(onInput : a -> String -> Maybe (String, a)) -> io () (onInput : a -> String -> Maybe (String, a)) -> io ()
replWith acc prompt fn replWith acc prompt fn
@ -29,7 +29,7 @@ replWith acc prompt fn
||| @ onInput the function to run on reading input, returning a String to ||| @ onInput the function to run on reading input, returning a String to
||| output ||| output
export export
repl : HasIO io => repl : MonadIO io =>
(prompt : String) -> (onInput : String -> String) -> io () (prompt : String) -> (onInput : String -> String) -> io ()
repl prompt fn repl prompt fn
= replWith () prompt (\x, s => Just (fn s, ())) = replWith () prompt (\x, s => Just (fn s, ()))

View File

@ -1564,9 +1564,15 @@ Monad IO where
b >>= k = io_bind b k b >>= k = io_bind b k
public export public export
interface Monad io => HasIO io where interface HasIO io where
liftIO : (1 _ : IO a) -> io a liftIO : (1 _ : IO a) -> io a
public export
interface (Monad io, HasIO io) => MonadIO io where
public export %inline
(Monad io, HasIO io) => MonadIO io where
public export %inline public export %inline
HasIO IO where HasIO IO where
liftIO x = x liftIO x = x

View File

@ -1,6 +1,6 @@
1/1: Building wcov (wcov.idr) 1/1: Building wcov (wcov.idr)
Main> Main.tfoo is total Main> Main.tfoo is total
Main> Main.wfoo is total Main> Main.wfoo is total
Main> Main.wbar is not covering due to call to function Main.with block in 1387 Main> Main.wbar is not covering due to call to function Main.with block in 1392
Main> Main.wbar1 is total Main> Main.wbar1 is total
Main> Bye for now! Main> Bye for now!

View File

@ -3,4 +3,4 @@ casetot.idr:12:1--13:1:main is not covering at:
12 main : IO () 12 main : IO ()
13 main = do 13 main = do
Calls non covering function Main.case block in 2114(619) Calls non covering function Main.case block in 2119(619)