From d12487f52916842e80b8e04d305fd48bb1465282 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 21 Jun 2020 01:18:43 +0100 Subject: [PATCH 1/6] HasIO interface for IO actions Also updates the Prelude and some base libraries to use HasIO rather than using IO directly. --- libs/base/Control/App.idr | 2 +- libs/base/Data/IORef.idr | 8 +-- libs/base/Data/Ref.idr | 2 +- libs/base/System.idr | 30 +++++----- libs/base/System/Directory.idr | 18 +++--- libs/base/System/File.idr | 53 ++++++++--------- libs/base/System/REPL.idr | 9 +-- libs/prelude/Prelude.idr | 86 +++++++++++++++++++++++++++- libs/prelude/PrimIO.idr | 79 ++----------------------- tests/idris2/coverage008/expected | 2 +- tests/idris2/coverage010/expected | 2 +- tests/idris2/real002/Control/App.idr | 2 +- tests/idris2/with003/Main.idr | 4 ++ tests/idris2/with003/expected | 28 ++++----- tests/idris2/with003/input | 4 +- 15 files changed, 175 insertions(+), 154 deletions(-) diff --git a/libs/base/Control/App.idr b/libs/base/Control/App.idr index ba6b30a9b..8c9512e46 100644 --- a/libs/base/Control/App.idr +++ b/libs/base/Control/App.idr @@ -333,7 +333,7 @@ HasErr Void e => PrimIO e where fork thread = MkApp $ prim_app_bind - (toPrimApp $ PrimIO.fork $ + (toPrimApp $ Prelude.fork $ do run thread pure ()) $ \_ => diff --git a/libs/base/Data/IORef.idr b/libs/base/Data/IORef.idr index 347929066..1bef1d916 100644 --- a/libs/base/Data/IORef.idr +++ b/libs/base/Data/IORef.idr @@ -13,23 +13,23 @@ data IORef : Type -> Type where MkRef : Mut a -> IORef a export -newIORef : a -> IO (IORef a) +newIORef : HasIO io => a -> io (IORef a) newIORef val = do m <- primIO (prim__newIORef val) pure (MkRef m) %inline export -readIORef : IORef a -> IO a +readIORef : HasIO io => IORef a -> io a readIORef (MkRef m) = primIO (prim__readIORef m) %inline export -writeIORef : IORef a -> (1 val : a) -> IO () +writeIORef : HasIO io => IORef a -> (1 val : a) -> io () writeIORef (MkRef m) val = primIO (prim__writeIORef m val) export -modifyIORef : IORef a -> (a -> a) -> IO () +modifyIORef : HasIO io => IORef a -> (a -> a) -> io () modifyIORef ref f = do val <- readIORef ref writeIORef ref (f val) diff --git a/libs/base/Data/Ref.idr b/libs/base/Data/Ref.idr index 7d3439248..153240afa 100644 --- a/libs/base/Data/Ref.idr +++ b/libs/base/Data/Ref.idr @@ -10,7 +10,7 @@ interface Ref m (r : Type -> Type) | m where writeRef : r a -> a -> m () export -Ref IO IORef where +HasIO io => Ref io IORef where newRef = newIORef readRef = readIORef writeRef = writeIORef diff --git a/libs/base/System.idr b/libs/base/System.idr index 66c259b10..9424c0671 100644 --- a/libs/base/System.idr +++ b/libs/base/System.idr @@ -16,11 +16,11 @@ prim_sleep : Int -> PrimIO () prim_usleep : Int -> PrimIO () export -sleep : Int -> IO () +sleep : HasIO io => Int -> io () sleep sec = primIO (prim_sleep sec) export -usleep : (x : Int) -> So (x >= 0) => IO () +usleep : HasIO io => (x : Int) -> So (x >= 0) => io () usleep sec = primIO (prim_usleep sec) -- This one is going to vary for different back ends. Probably needs a @@ -29,7 +29,7 @@ usleep sec = primIO (prim_usleep sec) prim__getArgs : PrimIO (List String) export -getArgs : IO (List String) +getArgs : HasIO io => io (List String) getArgs = primIO prim__getArgs %foreign libc "getenv" @@ -42,7 +42,7 @@ prim_setEnv : String -> String -> Int -> PrimIO Int prim_unsetEnv : String -> PrimIO Int export -getEnv : String -> IO (Maybe String) +getEnv : HasIO io => String -> io (Maybe String) getEnv var = do env <- primIO $ prim_getEnv var if prim__nullPtr env /= 0 @@ -50,7 +50,7 @@ getEnv var else pure (Just (prim__getString env)) export -getEnvironment : IO (List (String, String)) +getEnvironment : HasIO io => io (List (String, String)) getEnvironment = getAllPairs 0 [] where splitEq : String -> (String, String) @@ -59,7 +59,7 @@ getEnvironment = getAllPairs 0 [] (_, v') = break (/= '=') v in (k, v') - getAllPairs : Int -> List String -> IO (List (String, String)) + getAllPairs : Int -> List String -> io (List (String, String)) getAllPairs n acc = do envPair <- primIO $ prim_getEnvPair n if prim__nullPtr envPair /= 0 @@ -67,7 +67,7 @@ getEnvironment = getAllPairs 0 [] else getAllPairs (n + 1) (prim__getString envPair :: acc) export -setEnv : String -> String -> Bool -> IO Bool +setEnv : HasIO io => String -> String -> Bool -> io Bool setEnv var val overwrite = do ok <- primIO $ prim_setEnv var val (if overwrite then 1 else 0) if ok == 0 @@ -75,7 +75,7 @@ setEnv var val overwrite else pure False export -unsetEnv : String -> IO Bool +unsetEnv : HasIO io => String -> io Bool unsetEnv var = do ok <- primIO $ prim_unsetEnv var if ok == 0 @@ -87,7 +87,7 @@ unsetEnv var prim_system : String -> PrimIO Int export -system : String -> IO Int +system : HasIO io => String -> io Int system cmd = primIO (prim_system cmd) %foreign support "idris2_time" @@ -95,7 +95,7 @@ system cmd = primIO (prim_system cmd) prim_time : PrimIO Int export -time : IO Integer +time : HasIO io => io Integer time = pure $ cast !(primIO prim_time) %foreign libc "exit" @@ -114,16 +114,16 @@ data ExitCode : Type where ExitFailure : (errNo : Int) -> (So (not $ errNo == 0)) => ExitCode export -exitWith : ExitCode -> IO a -exitWith ExitSuccess = believe_me $ primIO $ prim_exit 0 -exitWith (ExitFailure code) = believe_me $ primIO $ prim_exit code +exitWith : HasIO io => ExitCode -> io a +exitWith ExitSuccess = primIO $ believe_me $ prim_exit 0 +exitWith (ExitFailure code) = primIO $ believe_me $ prim_exit code ||| Exit the program indicating failure. export -exitFailure : IO a +exitFailure : HasIO io => io a exitFailure = exitWith (ExitFailure 1) ||| Exit the program after a successful run. export -exitSuccess : IO a +exitSuccess : HasIO io => io a exitSuccess = exitWith ExitSuccess diff --git a/libs/base/System/Directory.idr b/libs/base/System/Directory.idr index c58f2ba4d..76008738e 100644 --- a/libs/base/System/Directory.idr +++ b/libs/base/System/Directory.idr @@ -12,7 +12,7 @@ support fn = "C:" ++ fn ++ ", libidris2_support" %foreign support "idris2_fileErrno" prim_fileErrno : PrimIO Int -returnError : IO (Either FileError a) +returnError : HasIO io => io (Either FileError a) returnError = do err <- primIO prim_fileErrno case err of @@ -23,7 +23,7 @@ returnError 4 => pure $ Left FileExists _ => pure $ Left (GenericFileError (err-5)) -ok : a -> IO (Either FileError a) +ok : HasIO io => a -> io (Either FileError a) ok x = pure (Right x) %foreign support "idris2_currentDirectory" @@ -52,7 +52,7 @@ data Directory : Type where MkDir : DirPtr -> Directory export -createDir : String -> IO (Either FileError ()) +createDir : HasIO io => String -> io (Either FileError ()) createDir dir = do res <- primIO (prim_createDir dir) if res == 0 @@ -60,13 +60,13 @@ createDir dir else returnError export -changeDir : String -> IO Bool +changeDir : HasIO io => String -> io Bool changeDir dir = do ok <- primIO (prim_changeDir dir) pure (ok == 0) export -currentDir : IO (Maybe String) +currentDir : HasIO io => io (Maybe String) currentDir = do res <- primIO prim_currentDir if prim__nullPtr res /= 0 @@ -74,7 +74,7 @@ currentDir else pure (Just (prim__getString res)) export -openDir : String -> IO (Either FileError Directory) +openDir : HasIO io => String -> io (Either FileError Directory) openDir d = do res <- primIO (prim_openDir d) if prim__nullAnyPtr res /= 0 @@ -82,15 +82,15 @@ openDir d else ok (MkDir res) export -closeDir : Directory -> IO () +closeDir : HasIO io => Directory -> io () closeDir (MkDir d) = primIO (prim_closeDir d) export -removeDir : String -> IO () +removeDir : HasIO io => String -> io () removeDir dirName = primIO (prim_removeDir dirName) export -dirEntry : Directory -> IO (Either FileError String) +dirEntry : HasIO io => Directory -> io (Either FileError String) dirEntry (MkDir d) = do res <- primIO (prim_dirEntry d) if prim__nullPtr res /= 0 diff --git a/libs/base/System/File.idr b/libs/base/System/File.idr index 83a6c4c2a..3b9b6db19 100644 --- a/libs/base/System/File.idr +++ b/libs/base/System/File.idr @@ -84,7 +84,7 @@ data FileError = GenericFileError Int -- errno | PermissionDenied | FileExists -returnError : IO (Either FileError a) +returnError : HasIO io => io (Either FileError a) returnError = do err <- primIO prim_fileErrno case err of @@ -104,7 +104,7 @@ Show FileError where show PermissionDenied = "Permission Denied" show FileExists = "File Exists" -ok : a -> IO (Either FileError a) +ok : HasIO io => a -> io (Either FileError a) ok x = pure (Right x) public export @@ -124,7 +124,7 @@ stderr : File stderr = FHandle prim__stderr export -openFile : String -> Mode -> IO (Either FileError File) +openFile : HasIO io => String -> Mode -> io (Either FileError File) openFile f m = do res <- primIO (prim__open f (modeStr m) 0) if prim__nullAnyPtr res /= 0 @@ -132,17 +132,17 @@ openFile f m else ok (FHandle res) export -closeFile : File -> IO () +closeFile : HasIO io => File -> io () closeFile (FHandle f) = primIO (prim__close f) export -fileError : File -> IO Bool +fileError : HasIO io => File -> io Bool fileError (FHandle f) = do x <- primIO $ prim_error f pure (x /= 0) export -fGetLine : (h : File) -> IO (Either FileError String) +fGetLine : HasIO io => (h : File) -> io (Either FileError String) fGetLine (FHandle f) = do res <- primIO (prim__readLine f) if prim__nullPtr res /= 0 @@ -150,7 +150,7 @@ fGetLine (FHandle f) else ok (prim__getString res) export -fGetChars : (h : File) -> Int -> IO (Either FileError String) +fGetChars : HasIO io => (h : File) -> Int -> io (Either FileError String) fGetChars (FHandle f) max = do res <- primIO (prim__readChars max f) if prim__nullPtr res /= 0 @@ -158,7 +158,7 @@ fGetChars (FHandle f) max else ok (prim__getString res) export -fGetChar : (h : File) -> IO (Either FileError Char) +fGetChar : HasIO io => (h : File) -> io (Either FileError Char) fGetChar (FHandle h) = do c <- primIO (prim__readChar h) ferr <- primIO (prim_error h) @@ -167,7 +167,7 @@ fGetChar (FHandle h) else ok (cast c) export -fPutStr : (h : File) -> String -> IO (Either FileError ()) +fPutStr : HasIO io => (h : File) -> String -> io (Either FileError ()) fPutStr (FHandle f) str = do res <- primIO (prim__writeLine f str) if res == 0 @@ -175,23 +175,23 @@ fPutStr (FHandle f) str else ok () export -fPutStrLn : (h : File) -> String -> IO (Either FileError ()) +fPutStrLn : HasIO io => (h : File) -> String -> io (Either FileError ()) fPutStrLn f str = fPutStr f (str ++ "\n") export -fEOF : (h : File) -> IO Bool +fEOF : HasIO io => (h : File) -> io Bool fEOF (FHandle f) = do res <- primIO (prim__eof f) pure (res /= 0) export -fflush : (h : File) -> IO () +fflush : HasIO io => (h : File) -> io () fflush (FHandle f) = do primIO (prim__flush f) pure () export -popen : String -> Mode -> IO (Either FileError File) +popen : HasIO io => String -> Mode -> io (Either FileError File) popen f m = do ptr <- primIO (prim__popen f (modeStr m)) if prim__nullAnyPtr ptr /= 0 @@ -199,11 +199,11 @@ popen f m = do else pure (Right (FHandle ptr)) export -pclose : File -> IO () +pclose : HasIO io => File -> io () pclose (FHandle h) = primIO (prim__pclose h) export -fileAccessTime : (h : File) -> IO (Either FileError Int) +fileAccessTime : HasIO io => (h : File) -> io (Either FileError Int) fileAccessTime (FHandle f) = do res <- primIO (prim__fileAccessTime f) if res > 0 @@ -211,7 +211,7 @@ fileAccessTime (FHandle f) else returnError export -fileModifiedTime : (h : File) -> IO (Either FileError Int) +fileModifiedTime : HasIO io => (h : File) -> io (Either FileError Int) fileModifiedTime (FHandle f) = do res <- primIO (prim__fileModifiedTime f) if res > 0 @@ -219,7 +219,7 @@ fileModifiedTime (FHandle f) else returnError export -fileStatusTime : (h : File) -> IO (Either FileError Int) +fileStatusTime : HasIO io => (h : File) -> io (Either FileError Int) fileStatusTime (FHandle f) = do res <- primIO (prim__fileStatusTime f) if res > 0 @@ -227,7 +227,7 @@ fileStatusTime (FHandle f) else returnError export -removeFile : String -> IO (Either FileError ()) +removeFile : HasIO io => String -> io (Either FileError ()) removeFile fname = do res <- primIO (prim__removeFile fname) if res == 0 @@ -235,7 +235,7 @@ removeFile fname else returnError export -fileSize : (h : File) -> IO (Either FileError Int) +fileSize : HasIO io => (h : File) -> io (Either FileError Int) fileSize (FHandle f) = do res <- primIO (prim__fileSize f) if res >= 0 @@ -243,13 +243,13 @@ fileSize (FHandle f) else returnError export -fPoll : File -> IO Bool +fPoll : HasIO io => File -> io Bool fPoll (FHandle f) = do p <- primIO (prim__fPoll f) pure (p > 0) export -readFile : String -> IO (Either FileError String) +readFile : HasIO io => String -> io (Either FileError String) readFile file = do Right h <- openFile file Read | Left err => returnError @@ -259,7 +259,7 @@ readFile file closeFile h pure (Right (fastAppend content)) where - read : List String -> File -> IO (Either FileError (List String)) + read : List String -> File -> io (Either FileError (List String)) read acc h = do eof <- fEOF h if eof @@ -271,8 +271,9 @@ readFile file ||| Write a string to a file export -writeFile : (filepath : String) -> (contents : String) -> - IO (Either FileError ()) +writeFile : HasIO io => + (filepath : String) -> (contents : String) -> + io (Either FileError ()) writeFile fn contents = do Right h <- openFile fn WriteTruncate | Left err => pure (Left err) @@ -306,7 +307,7 @@ mkMode p getMs = sum . map getM export -chmodRaw : String -> Int -> IO (Either FileError ()) +chmodRaw : HasIO io => String -> Int -> io (Either FileError ()) chmodRaw fname p = do ok <- primIO $ prim__chmod fname p if ok == 0 @@ -314,5 +315,5 @@ chmodRaw fname p else returnError export -chmod : String -> Permissions -> IO (Either FileError ()) +chmod : HasIO io => String -> Permissions -> io (Either FileError ()) chmod fname p = chmodRaw fname (mkMode p) diff --git a/libs/base/System/REPL.idr b/libs/base/System/REPL.idr index 26e8a9b6a..9ef353ea6 100644 --- a/libs/base/System/REPL.idr +++ b/libs/base/System/REPL.idr @@ -8,8 +8,9 @@ import System.File ||| @ onInput the function to run on reading input, returning a String to ||| output and a new state. Returns Nothing if the repl should exit export -replWith : (state : a) -> (prompt : String) -> - (onInput : a -> String -> Maybe (String, a)) -> IO () +replWith : HasIO io => + (state : a) -> (prompt : String) -> + (onInput : a -> String -> Maybe (String, a)) -> io () replWith acc prompt fn = do eof <- fEOF stdin if eof @@ -28,8 +29,8 @@ replWith acc prompt fn ||| @ onInput the function to run on reading input, returning a String to ||| output export -repl : (prompt : String) -> - (onInput : String -> String) -> IO () +repl : HasIO io => + (prompt : String) -> (onInput : String -> String) -> io () repl prompt fn = replWith () prompt (\x, s => Just (fn s, ())) diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr index 40e22468b..8b473b902 100644 --- a/libs/prelude/Prelude.idr +++ b/libs/prelude/Prelude.idr @@ -1563,14 +1563,96 @@ public export Monad IO where b >>= k = io_bind b k +public export +interface Monad io => HasIO io where + liftIO : (1 _ : IO a) -> io a + +public export %inline +HasIO IO where + liftIO x = x + +export %inline +primIO : HasIO io => (1 fn : (1 x : %World) -> IORes a) -> io a +primIO op = liftIO (fromPrim op) + +%extern +prim__onCollectAny : AnyPtr -> (AnyPtr -> PrimIO ()) -> PrimIO GCAnyPtr +%extern +prim__onCollect : Ptr t -> (Ptr t -> PrimIO ()) -> PrimIO (GCPtr t) + +export +onCollectAny : AnyPtr -> (AnyPtr -> IO ()) -> IO GCAnyPtr +onCollectAny ptr c = fromPrim (prim__onCollectAny ptr (\x => toPrim (c x))) + +export +onCollect : Ptr t -> (Ptr t -> IO ()) -> IO (GCPtr t) +onCollect ptr c = fromPrim (prim__onCollect ptr (\x => toPrim (c x))) + +%foreign "C:idris2_getString, libidris2_support" +export +prim__getString : Ptr String -> String + +%foreign "C:putchar,libc 6" +prim__putChar : Char -> (1 x : %World) -> IORes () +%foreign "C:getchar,libc 6" +%extern prim__getChar : (1 x : %World) -> IORes Char + +%foreign "C:idris2_getStr,libidris2_support" +prim__getStr : PrimIO String +%foreign "C:idris2_putStr,libidris2_support" +prim__putStr : String -> PrimIO () + +||| Output a string to stdout without a trailing newline. +export +putStr : HasIO io => String -> io () +putStr str = primIO (prim__putStr str) + +||| Output a string to stdout with a trailing newline. +export +putStrLn : HasIO io => String -> io () +putStrLn str = putStr (prim__strAppend str "\n") + +||| Read one line of input from stdin, without the trailing newline. +export +getLine : HasIO io => io String +getLine = primIO prim__getStr + +||| Write a single character to stdout. +export +putChar : HasIO io => Char -> io () +putChar c = primIO (prim__putChar c) + +||| Write a single character to stdout, with a trailing newline. +export +putCharLn : HasIO io => Char -> io () +putCharLn c = putStrLn (prim__cast_CharString c) + +||| Read a single character from stdin. +export +getChar : HasIO io => io Char +getChar = primIO prim__getChar + +export +prim_fork : (1 prog : PrimIO ()) -> PrimIO ThreadID +prim_fork act w = prim__schemeCall ThreadID "blodwen-thread" [act] w + +export +fork : (1 prog : IO ()) -> IO ThreadID +fork act = schemeCall ThreadID "blodwen-thread" [toPrim act] + +%foreign "C:idris2_readString, libidris2_support" +export +prim__getErrno : Int + + ||| Output something showable to stdout, without a trailing newline. export -print : Show a => a -> IO () +print : (HasIO io, Show a) => a -> io () print x = putStr $ show x ||| Output something showable to stdout, with a trailing newline. export -printLn : Show a => a -> IO () +printLn : (HasIO io, Show a) => a -> io () printLn x = putStrLn $ show x ----------------------- diff --git a/libs/prelude/PrimIO.idr b/libs/prelude/PrimIO.idr index 45e6300bf..6f1e7924d 100644 --- a/libs/prelude/PrimIO.idr +++ b/libs/prelude/PrimIO.idr @@ -41,11 +41,6 @@ io_bind (MkIO fn) k MkIO res = k x' in res w') -%foreign "C:putchar,libc 6" -prim__putChar : Char -> (1 x : %World) -> IORes () -%foreign "C:getchar,libc 6" -%extern prim__getChar : (1 x : %World) -> IORes Char - -- A pointer representing a given parameter type -- The parameter is a phantom type, to help differentiate between -- different pointer types @@ -72,14 +67,16 @@ data FArgList : Type where Nil : FArgList (::) : {a : Type} -> (1 arg : a) -> (1 args : FArgList) -> FArgList +export %extern prim__cCall : (ret : Type) -> String -> (1 args : FArgList) -> (1 x : %World) -> IORes ret +export %extern prim__schemeCall : (ret : Type) -> String -> (1 args : FArgList) -> (1 x : %World) -> IORes ret export %inline -primIO : (1 fn : (1 x : %World) -> IORes a) -> IO a -primIO op = MkIO op +fromPrim : (1 fn : (1 x : %World) -> IORes a) -> IO a +fromPrim op = MkIO op export %inline toPrim : (1 act : IO a) -> PrimIO a @@ -87,11 +84,11 @@ toPrim (MkIO fn) = fn export %inline schemeCall : (ret : Type) -> String -> (1 args : FArgList) -> IO ret -schemeCall ret fn args = primIO (prim__schemeCall ret fn args) +schemeCall ret fn args = fromPrim (prim__schemeCall ret fn args) export %inline cCall : (ret : Type) -> String -> FArgList -> IO ret -cCall ret fn args = primIO (prim__cCall ret fn args) +cCall ret fn args = fromPrim (prim__cCall ret fn args) %foreign "C:idris2_isNull, libidris2_support" export @@ -104,70 +101,6 @@ export %inline prim__nullPtr : Ptr t -> Int -- can't pass 'type' to a foreign function prim__nullPtr p = prim__nullAnyPtr (prim__forgetPtr p) -%extern -prim__onCollectAny : AnyPtr -> (AnyPtr -> PrimIO ()) -> PrimIO GCAnyPtr -%extern -prim__onCollect : Ptr t -> (Ptr t -> PrimIO ()) -> PrimIO (GCPtr t) - -export -onCollectAny : AnyPtr -> (AnyPtr -> IO ()) -> IO GCAnyPtr -onCollectAny ptr c = primIO (prim__onCollectAny ptr (\x => toPrim (c x))) - -export -onCollect : Ptr t -> (Ptr t -> IO ()) -> IO (GCPtr t) -onCollect ptr c = primIO (prim__onCollect ptr (\x => toPrim (c x))) - -%foreign "C:idris2_getString, libidris2_support" -export -prim__getString : Ptr String -> String - -%foreign "C:idris2_getStr,libidris2_support" -prim__getStr : PrimIO String -%foreign "C:idris2_putStr,libidris2_support" -prim__putStr : String -> PrimIO () - -||| Output a string to stdout without a trailing newline. -export -putStr : String -> IO () -putStr str = primIO (prim__putStr str) - -||| Output a string to stdout with a trailing newline. -export -putStrLn : String -> IO () -putStrLn str = putStr (prim__strAppend str "\n") - -||| Read one line of input from stdin, without the trailing newline. -export -getLine : IO String -getLine = primIO prim__getStr - -||| Write a single character to stdout. -export -putChar : Char -> IO () -putChar c = primIO (prim__putChar c) - -||| Write a single character to stdout, with a trailing newline. -export -putCharLn : Char -> IO () -putCharLn c = putStrLn (prim__cast_CharString c) - -||| Read a single character from stdin. -export -getChar : IO Char -getChar = primIO prim__getChar - -export -fork : (1 prog : IO ()) -> IO ThreadID -fork (MkIO act) = schemeCall ThreadID "blodwen-thread" [act] - -export -prim_fork : (1 prog : PrimIO ()) -> PrimIO ThreadID -prim_fork act w = prim__schemeCall ThreadID "blodwen-thread" [act] w - -%foreign "C:idris2_readString, libidris2_support" -export -prim__getErrno : Int - unsafeCreateWorld : (1 f : (1 x : %World) -> a) -> a unsafeCreateWorld f = f %MkWorld diff --git a/tests/idris2/coverage008/expected b/tests/idris2/coverage008/expected index 77b301b2d..cfbd64774 100644 --- a/tests/idris2/coverage008/expected +++ b/tests/idris2/coverage008/expected @@ -1,6 +1,6 @@ 1/1: Building wcov (wcov.idr) Main> Main.tfoo is total Main> Main.wfoo is total -Main> Main.wbar is not covering due to call to function Main.with block in 1376 +Main> Main.wbar is not covering due to call to function Main.with block in 1387 Main> Main.wbar1 is total Main> Bye for now! diff --git a/tests/idris2/coverage010/expected b/tests/idris2/coverage010/expected index 20cebab1e..3204bc8a5 100644 --- a/tests/idris2/coverage010/expected +++ b/tests/idris2/coverage010/expected @@ -3,4 +3,4 @@ casetot.idr:12:1--13:1:main is not covering at: 12 main : IO () 13 main = do - Calls non covering function Main.case block in 2101(617) + Calls non covering function Main.case block in 2114(619) diff --git a/tests/idris2/real002/Control/App.idr b/tests/idris2/real002/Control/App.idr index 87a35547f..00ea36a2a 100644 --- a/tests/idris2/real002/Control/App.idr +++ b/tests/idris2/real002/Control/App.idr @@ -333,7 +333,7 @@ HasErr Void e => PrimIO e where fork thread = MkApp $ prim_app_bind - (toPrimApp $ PrimIO.fork $ + (toPrimApp $ Prelude.fork $ do run thread pure ()) $ \_ => diff --git a/tests/idris2/with003/Main.idr b/tests/idris2/with003/Main.idr index ccd8b981e..677990504 100644 --- a/tests/idris2/with003/Main.idr +++ b/tests/idris2/with003/Main.idr @@ -3,6 +3,10 @@ module Main import Data.List import Data.Vect +-- needs to be concretely in IO to test error messages +myPrintLn : String -> IO () +myPrintLn = printLn + -- add some definition of (>>=) in another namespace namespace Other public export diff --git a/tests/idris2/with003/expected b/tests/idris2/with003/expected index e40156698..a3c2d2afd 100644 --- a/tests/idris2/with003/expected +++ b/tests/idris2/with003/expected @@ -1,5 +1,5 @@ 1/1: Building Main (Main.idr) -Main> (interactive):1:60--1:73:Sorry, I can't find any elaboration which works. All errors: +Main> (interactive):1:66--1:81:Sorry, I can't find any elaboration which works. All errors: If Prelude.>>=: Sorry, I can't find any elaboration which works. All errors: If Prelude.>>=: When unifying ?_ -> IO () and IO ?b Mismatch between: @@ -7,8 +7,8 @@ Mismatch between: and IO ?b at: -1 do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo" - ^^^^^^^^^^^^^ +1 do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" + ^^^^^^^^^^^^^^^ If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b @@ -17,8 +17,8 @@ Mismatch between: and IO ?b at: -1 do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo" - ^^^^^^^^^^^^^^^^^^^^^^^^ +1 do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" + ^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -29,8 +29,8 @@ Mismatch between: and IO ?b at: -1 do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo" - ^^^^^^^^^^^^^^^^^^^^^^^^ +1 do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" + ^^^^^^^^^^^^^^^^^^^^^^^^^^ If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors: @@ -40,8 +40,8 @@ Mismatch between: and IO ?b at: -1 do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo" - ^^^^^^^^^^^^^ +1 do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" + ^^^^^^^^^^^^^^^ If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b @@ -50,15 +50,15 @@ Mismatch between: and IO ?b at: -1 do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo" - ^^^^^^^^^^^^^^^^^^^^^^^^ +1 do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" + ^^^^^^^^^^^^^^^^^^^^^^^^^^ -Main> (interactive):1:57--1:62:Can't find an implementation for Num () at: -1 with Prelude.(>>=) do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo" - ^^^^^ +Main> (interactive):1:61--1:66:Can't find an implementation for Num () at: +1 with Prelude.(>>=) do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" + ^^^^^ Main> (interactive):1:4--1:6:Ambiguous elaboration at: 1 :t [] diff --git a/tests/idris2/with003/input b/tests/idris2/with003/input index f04257864..c77625533 100644 --- a/tests/idris2/with003/input +++ b/tests/idris2/with003/input @@ -1,5 +1,5 @@ -do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo" -with Prelude.(>>=) do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo" +do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" +with Prelude.(>>=) do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" :t [] :t with Vect.Nil [] :t with Prelude.Nil [] From 28855088c2d2c7ac48010c372cf2cb7b3528581f Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 21 Jun 2020 14:46:14 +0100 Subject: [PATCH 2/6] Split HasIO into HasIO and MonadIO For things which don't require (>>=), HasIO is fine, otherwise MonadIO gives access to the monad interface. --- CHANGELOG.md | 3 +++ libs/base/Data/IOArray.idr | 15 ++++++----- libs/base/Data/IORef.idr | 4 +-- libs/base/Data/Ref.idr | 2 +- libs/base/System.idr | 10 +++---- libs/base/System/Directory.idr | 14 +++++----- libs/base/System/File.idr | 44 +++++++++++++++---------------- libs/base/System/REPL.idr | 4 +-- libs/prelude/Prelude.idr | 8 +++++- tests/idris2/coverage008/expected | 2 +- tests/idris2/coverage010/expected | 2 +- 11 files changed, 59 insertions(+), 49 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 75196a1b1..4856fe9be 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -20,6 +20,9 @@ Language 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 arrays with constant time read/write, convertible to immutable arrays with constant time read. diff --git a/libs/base/Data/IOArray.idr b/libs/base/Data/IOArray.idr index 3d87dda01..fadc026b3 100644 --- a/libs/base/Data/IOArray.idr +++ b/libs/base/Data/IOArray.idr @@ -14,19 +14,19 @@ max : IOArray elem -> Int max = maxSize export -newArray : Int -> IO (IOArray elem) +newArray : MonadIO io => Int -> io (IOArray elem) newArray size = pure (MkIOArray size !(primIO (prim__newArray size Nothing))) export -writeArray : IOArray elem -> Int -> elem -> IO () +writeArray : MonadIO io => IOArray elem -> Int -> elem -> io () writeArray arr pos el = if pos < 0 || pos >= max arr then pure () else primIO (prim__arraySet (content arr) pos (Just el)) export -readArray : IOArray elem -> Int -> IO (Maybe elem) +readArray : MonadIO io => IOArray elem -> Int -> io (Maybe elem) readArray arr pos = if pos < 0 || pos >= max arr then pure Nothing @@ -35,7 +35,8 @@ readArray arr pos -- Make a new array of the given size with the elements copied from the -- other array export -newArrayCopy : (newsize : Int) -> IOArray elem -> IO (IOArray elem) +newArrayCopy : MonadIO io => + (newsize : Int) -> IOArray elem -> io (IOArray elem) newArrayCopy newsize arr = do let newsize' = if newsize < max arr then max arr else newsize arr' <- newArray newsize' @@ -44,7 +45,7 @@ newArrayCopy newsize arr where copyFrom : ArrayData (Maybe elem) -> ArrayData (Maybe elem) -> - Int -> IO () + Int -> io () copyFrom old new pos = if pos < 0 then pure () @@ -53,10 +54,10 @@ newArrayCopy newsize arr assert_total (copyFrom old new (pos - 1)) export -toList : IOArray elem -> IO (List (Maybe elem)) +toList : MonadIO io => IOArray elem -> io (List (Maybe elem)) toList arr = iter 0 (max arr) [] 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 = if pos >= end then pure (reverse acc) diff --git a/libs/base/Data/IORef.idr b/libs/base/Data/IORef.idr index 1bef1d916..c511f5167 100644 --- a/libs/base/Data/IORef.idr +++ b/libs/base/Data/IORef.idr @@ -13,7 +13,7 @@ data IORef : Type -> Type where MkRef : Mut a -> IORef a export -newIORef : HasIO io => a -> io (IORef a) +newIORef : MonadIO io => a -> io (IORef a) newIORef val = do m <- primIO (prim__newIORef val) 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) export -modifyIORef : HasIO io => IORef a -> (a -> a) -> io () +modifyIORef : MonadIO io => IORef a -> (a -> a) -> io () modifyIORef ref f = do val <- readIORef ref writeIORef ref (f val) diff --git a/libs/base/Data/Ref.idr b/libs/base/Data/Ref.idr index 153240afa..b012a45f8 100644 --- a/libs/base/Data/Ref.idr +++ b/libs/base/Data/Ref.idr @@ -10,7 +10,7 @@ interface Ref m (r : Type -> Type) | m where writeRef : r a -> a -> m () export -HasIO io => Ref io IORef where +MonadIO io => Ref io IORef where newRef = newIORef readRef = readIORef writeRef = writeIORef diff --git a/libs/base/System.idr b/libs/base/System.idr index 9424c0671..2a56c2286 100644 --- a/libs/base/System.idr +++ b/libs/base/System.idr @@ -42,7 +42,7 @@ prim_setEnv : String -> String -> Int -> PrimIO Int prim_unsetEnv : String -> PrimIO Int export -getEnv : HasIO io => String -> io (Maybe String) +getEnv : MonadIO io => String -> io (Maybe String) getEnv var = do env <- primIO $ prim_getEnv var if prim__nullPtr env /= 0 @@ -50,7 +50,7 @@ getEnv var else pure (Just (prim__getString env)) export -getEnvironment : HasIO io => io (List (String, String)) +getEnvironment : MonadIO io => io (List (String, String)) getEnvironment = getAllPairs 0 [] where splitEq : String -> (String, String) @@ -67,7 +67,7 @@ getEnvironment = getAllPairs 0 [] else getAllPairs (n + 1) (prim__getString envPair :: acc) export -setEnv : HasIO io => String -> String -> Bool -> io Bool +setEnv : MonadIO io => String -> String -> Bool -> io Bool setEnv var val overwrite = do ok <- primIO $ prim_setEnv var val (if overwrite then 1 else 0) if ok == 0 @@ -75,7 +75,7 @@ setEnv var val overwrite else pure False export -unsetEnv : HasIO io => String -> io Bool +unsetEnv : MonadIO io => String -> io Bool unsetEnv var = do ok <- primIO $ prim_unsetEnv var if ok == 0 @@ -95,7 +95,7 @@ system cmd = primIO (prim_system cmd) prim_time : PrimIO Int export -time : HasIO io => io Integer +time : MonadIO io => io Integer time = pure $ cast !(primIO prim_time) %foreign libc "exit" diff --git a/libs/base/System/Directory.idr b/libs/base/System/Directory.idr index 76008738e..2949c59ae 100644 --- a/libs/base/System/Directory.idr +++ b/libs/base/System/Directory.idr @@ -12,7 +12,7 @@ support fn = "C:" ++ fn ++ ", libidris2_support" %foreign support "idris2_fileErrno" prim_fileErrno : PrimIO Int -returnError : HasIO io => io (Either FileError a) +returnError : MonadIO io => io (Either FileError a) returnError = do err <- primIO prim_fileErrno case err of @@ -23,7 +23,7 @@ returnError 4 => pure $ Left FileExists _ => 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) %foreign support "idris2_currentDirectory" @@ -52,7 +52,7 @@ data Directory : Type where MkDir : DirPtr -> Directory export -createDir : HasIO io => String -> io (Either FileError ()) +createDir : MonadIO io => String -> io (Either FileError ()) createDir dir = do res <- primIO (prim_createDir dir) if res == 0 @@ -60,13 +60,13 @@ createDir dir else returnError export -changeDir : HasIO io => String -> io Bool +changeDir : MonadIO io => String -> io Bool changeDir dir = do ok <- primIO (prim_changeDir dir) pure (ok == 0) export -currentDir : HasIO io => io (Maybe String) +currentDir : MonadIO io => io (Maybe String) currentDir = do res <- primIO prim_currentDir if prim__nullPtr res /= 0 @@ -74,7 +74,7 @@ currentDir else pure (Just (prim__getString res)) export -openDir : HasIO io => String -> io (Either FileError Directory) +openDir : MonadIO io => String -> io (Either FileError Directory) openDir d = do res <- primIO (prim_openDir d) if prim__nullAnyPtr res /= 0 @@ -90,7 +90,7 @@ removeDir : HasIO io => String -> io () removeDir dirName = primIO (prim_removeDir dirName) export -dirEntry : HasIO io => Directory -> io (Either FileError String) +dirEntry : MonadIO io => Directory -> io (Either FileError String) dirEntry (MkDir d) = do res <- primIO (prim_dirEntry d) if prim__nullPtr res /= 0 diff --git a/libs/base/System/File.idr b/libs/base/System/File.idr index 3b9b6db19..5e376e622 100644 --- a/libs/base/System/File.idr +++ b/libs/base/System/File.idr @@ -84,7 +84,7 @@ data FileError = GenericFileError Int -- errno | PermissionDenied | FileExists -returnError : HasIO io => io (Either FileError a) +returnError : MonadIO io => io (Either FileError a) returnError = do err <- primIO prim_fileErrno case err of @@ -104,7 +104,7 @@ Show FileError where show PermissionDenied = "Permission Denied" 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) public export @@ -124,7 +124,7 @@ stderr : File stderr = FHandle prim__stderr export -openFile : HasIO io => String -> Mode -> io (Either FileError File) +openFile : MonadIO io => String -> Mode -> io (Either FileError File) openFile f m = do res <- primIO (prim__open f (modeStr m) 0) if prim__nullAnyPtr res /= 0 @@ -136,13 +136,13 @@ closeFile : HasIO io => File -> io () closeFile (FHandle f) = primIO (prim__close f) export -fileError : HasIO io => File -> io Bool +fileError : MonadIO io => File -> io Bool fileError (FHandle f) = do x <- primIO $ prim_error f pure (x /= 0) export -fGetLine : HasIO io => (h : File) -> io (Either FileError String) +fGetLine : MonadIO io => (h : File) -> io (Either FileError String) fGetLine (FHandle f) = do res <- primIO (prim__readLine f) if prim__nullPtr res /= 0 @@ -150,7 +150,7 @@ fGetLine (FHandle f) else ok (prim__getString res) 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 = do res <- primIO (prim__readChars max f) if prim__nullPtr res /= 0 @@ -158,7 +158,7 @@ fGetChars (FHandle f) max else ok (prim__getString res) export -fGetChar : HasIO io => (h : File) -> io (Either FileError Char) +fGetChar : MonadIO io => (h : File) -> io (Either FileError Char) fGetChar (FHandle h) = do c <- primIO (prim__readChar h) ferr <- primIO (prim_error h) @@ -167,7 +167,7 @@ fGetChar (FHandle h) else ok (cast c) export -fPutStr : HasIO io => (h : File) -> String -> io (Either FileError ()) +fPutStr : MonadIO io => (h : File) -> String -> io (Either FileError ()) fPutStr (FHandle f) str = do res <- primIO (prim__writeLine f str) if res == 0 @@ -175,23 +175,23 @@ fPutStr (FHandle f) str else ok () 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") export -fEOF : HasIO io => (h : File) -> io Bool +fEOF : MonadIO io => (h : File) -> io Bool fEOF (FHandle f) = do res <- primIO (prim__eof f) pure (res /= 0) export -fflush : HasIO io => (h : File) -> io () +fflush : MonadIO io => (h : File) -> io () fflush (FHandle f) = do primIO (prim__flush f) pure () export -popen : HasIO io => String -> Mode -> io (Either FileError File) +popen : MonadIO io => String -> Mode -> io (Either FileError File) popen f m = do ptr <- primIO (prim__popen f (modeStr m)) if prim__nullAnyPtr ptr /= 0 @@ -203,7 +203,7 @@ pclose : HasIO io => File -> io () pclose (FHandle h) = primIO (prim__pclose h) export -fileAccessTime : HasIO io => (h : File) -> io (Either FileError Int) +fileAccessTime : MonadIO io => (h : File) -> io (Either FileError Int) fileAccessTime (FHandle f) = do res <- primIO (prim__fileAccessTime f) if res > 0 @@ -211,7 +211,7 @@ fileAccessTime (FHandle f) else returnError export -fileModifiedTime : HasIO io => (h : File) -> io (Either FileError Int) +fileModifiedTime : MonadIO io => (h : File) -> io (Either FileError Int) fileModifiedTime (FHandle f) = do res <- primIO (prim__fileModifiedTime f) if res > 0 @@ -219,7 +219,7 @@ fileModifiedTime (FHandle f) else returnError export -fileStatusTime : HasIO io => (h : File) -> io (Either FileError Int) +fileStatusTime : MonadIO io => (h : File) -> io (Either FileError Int) fileStatusTime (FHandle f) = do res <- primIO (prim__fileStatusTime f) if res > 0 @@ -227,7 +227,7 @@ fileStatusTime (FHandle f) else returnError export -removeFile : HasIO io => String -> io (Either FileError ()) +removeFile : MonadIO io => String -> io (Either FileError ()) removeFile fname = do res <- primIO (prim__removeFile fname) if res == 0 @@ -235,7 +235,7 @@ removeFile fname else returnError export -fileSize : HasIO io => (h : File) -> io (Either FileError Int) +fileSize : MonadIO io => (h : File) -> io (Either FileError Int) fileSize (FHandle f) = do res <- primIO (prim__fileSize f) if res >= 0 @@ -243,13 +243,13 @@ fileSize (FHandle f) else returnError export -fPoll : HasIO io => File -> io Bool +fPoll : MonadIO io => File -> io Bool fPoll (FHandle f) = do p <- primIO (prim__fPoll f) pure (p > 0) export -readFile : HasIO io => String -> io (Either FileError String) +readFile : MonadIO io => String -> io (Either FileError String) readFile file = do Right h <- openFile file Read | Left err => returnError @@ -271,7 +271,7 @@ readFile file ||| Write a string to a file export -writeFile : HasIO io => +writeFile : MonadIO io => (filepath : String) -> (contents : String) -> io (Either FileError ()) writeFile fn contents = do @@ -307,7 +307,7 @@ mkMode p getMs = sum . map getM export -chmodRaw : HasIO io => String -> Int -> io (Either FileError ()) +chmodRaw : MonadIO io => String -> Int -> io (Either FileError ()) chmodRaw fname p = do ok <- primIO $ prim__chmod fname p if ok == 0 @@ -315,5 +315,5 @@ chmodRaw fname p else returnError export -chmod : HasIO io => String -> Permissions -> io (Either FileError ()) +chmod : MonadIO io => String -> Permissions -> io (Either FileError ()) chmod fname p = chmodRaw fname (mkMode p) diff --git a/libs/base/System/REPL.idr b/libs/base/System/REPL.idr index 9ef353ea6..f51aeb3ab 100644 --- a/libs/base/System/REPL.idr +++ b/libs/base/System/REPL.idr @@ -8,7 +8,7 @@ import System.File ||| @ onInput the function to run on reading input, returning a String to ||| output and a new state. Returns Nothing if the repl should exit export -replWith : HasIO io => +replWith : MonadIO io => (state : a) -> (prompt : String) -> (onInput : a -> String -> Maybe (String, a)) -> io () replWith acc prompt fn @@ -29,7 +29,7 @@ replWith acc prompt fn ||| @ onInput the function to run on reading input, returning a String to ||| output export -repl : HasIO io => +repl : MonadIO io => (prompt : String) -> (onInput : String -> String) -> io () repl prompt fn = replWith () prompt (\x, s => Just (fn s, ())) diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr index 8b473b902..d38d96c56 100644 --- a/libs/prelude/Prelude.idr +++ b/libs/prelude/Prelude.idr @@ -1564,9 +1564,15 @@ Monad IO where b >>= k = io_bind b k public export -interface Monad io => HasIO io where +interface HasIO io where 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 HasIO IO where liftIO x = x diff --git a/tests/idris2/coverage008/expected b/tests/idris2/coverage008/expected index cfbd64774..54edf0f50 100644 --- a/tests/idris2/coverage008/expected +++ b/tests/idris2/coverage008/expected @@ -1,6 +1,6 @@ 1/1: Building wcov (wcov.idr) Main> Main.tfoo 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> Bye for now! diff --git a/tests/idris2/coverage010/expected b/tests/idris2/coverage010/expected index 3204bc8a5..c2e2da8d2 100644 --- a/tests/idris2/coverage010/expected +++ b/tests/idris2/coverage010/expected @@ -3,4 +3,4 @@ casetot.idr:12:1--13:1:main is not covering at: 12 main : IO () 13 main = do - Calls non covering function Main.case block in 2114(619) + Calls non covering function Main.case block in 2119(619) From 1b15463746a688de38a7af44576b3b540a5bf555 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 21 Jun 2020 15:25:40 +0100 Subject: [PATCH 3/6] Update libraries and docs with HasIO/MonadIO --- docs/source/ffi/ffi.rst | 27 ++++++++++------ docs/source/tutorial/interfaces.rst | 19 +++++++++++ libs/contrib/Debug/Buffer.idr | 10 +++--- libs/contrib/System/Random.idr | 12 +++---- libs/network/Network/Socket.idr | 48 ++++++++++++++++------------ libs/network/Network/Socket/Data.idr | 4 +-- libs/network/Network/Socket/Raw.idr | 44 +++++++++++++------------ tests/chez/chez010/CB.idr | 4 +-- 8 files changed, 103 insertions(+), 65 deletions(-) diff --git a/docs/source/ffi/ffi.rst b/docs/source/ffi/ffi.rst index 0179a7cf0..8296c60b8 100644 --- a/docs/source/ffi/ffi.rst +++ b/docs/source/ffi/ffi.rst @@ -88,17 +88,19 @@ returns a primitive IO action: Internally, ``PrimIO Int`` is a function which takes the current (linear) state of the world, and returns an ``Int`` with an updated state of the world. -We can convert this into an ``IO`` action using ``primIO``: +In general, ``IO`` operations in an Idris program are defined as instances +of the ``HasIO`` interface (or ``MonadIO``). We can convert a primitive +operation to one usable in ``HasIO`` using ``primIO``: .. code-block:: idris - primIO : PrimIO a -> IO a + primIO : HasIO a => PrimIO a -> io a So, we can extend our program as follows: .. code-block:: idris - addWithMessage : String -> Int -> Int -> IO Int + addWithMessage : HasIO io => String -> Int -> Int -> io Int addWithMessage s x y = primIO $ prim_addWithMessage s x y main : IO () @@ -218,16 +220,17 @@ which takes a callback that takes a ``char*`` and an ``int`` and returns a return f(x, y); } -Then, we can access this from Idris by declaring it as a ``%foreign`` -function and wrapping it in ``IO``, with the C function calling the Idris -function as the callback: +Then, we can access this from Idris by declaring it as a ``%foreign`` function +and wrapping it in the ``HasIO`` interface, with the C function calling the +Idris function as the callback: .. code-block:: idris %foreign (libsmall "applyFn") prim_applyFn : String -> Int -> (String -> Int -> String) -> PrimIO String - applyFn : String -> Int -> (String -> Int -> String) -> IO String + applyFn : HasIO io => + String -> Int -> (String -> Int -> String) -> io String applyFn c i f = primIO $ prim_applyFn c i f For example, we can try this as follows: @@ -256,14 +259,18 @@ As a variant, the callback could have a side effect: prim_applyFnIO : String -> Int -> (String -> Int -> PrimIO String) -> PrimIO String -This is a little more fiddly to lift to an ``IO`` function, due to the callback, -but we can do so using ``toPrim : IO a -> PrimIO a``: +This is a little more fiddly to lift to a ``HasIO`` function, +due to the callback, but we can do so using ``toPrim : IO a -> PrimIO a``: .. code-block:: idris - applyFnIO : String -> Int -> (String -> Int -> IO String) -> IO String + applyFnIO : HasIO io => + String -> Int -> (String -> Int -> IO String) -> io String applyFnIO c i f = primIO $ prim_applyFnIO c i (\s, i => toPrim $ f s i) +Note that the callback is explicitly in ``IO`` here, since ``HasIO`` doesn't +have a general method for extracting the primitive ``IO`` operation. + For example, we can extend the above ``pluralise`` example to print a message in the callback: diff --git a/docs/source/tutorial/interfaces.rst b/docs/source/tutorial/interfaces.rst index 13601a9ae..95cd37206 100644 --- a/docs/source/tutorial/interfaces.rst +++ b/docs/source/tutorial/interfaces.rst @@ -428,6 +428,25 @@ would be: m_add : Maybe Int -> Maybe Int -> Maybe Int m_add x y = [ x' + y' | x' <- x, y' <- y ] +Interfaces and IO +================= + +In general, ``IO`` operations in the libraries aren't written using ``IO`` +directly, but rather via one of the following interfaces: + +.. code-block:: idris + + interface HasIO io where + liftIO : (1 _ : IO a) -> io a + + interface (Monad io, HasIO io) => MonadIO io where + +``HasIO`` explains, via ``liftIO``, how to convert a primitive ``IO`` operation +to an operation in some underlying type. ``MonadIO`` has no methods, but +adds an additional ``Monad`` constraint. These interfaces allow a programmer +to define some more expressive notion of interactive program, while still +giving direct access to ``IO`` primitives. + Idiom brackets ============== diff --git a/libs/contrib/Debug/Buffer.idr b/libs/contrib/Debug/Buffer.idr index 5671c7f6c..2f7161402 100644 --- a/libs/contrib/Debug/Buffer.idr +++ b/libs/contrib/Debug/Buffer.idr @@ -31,14 +31,14 @@ group n xs = worker [] xs worker acc ys = worker ((take n ys)::acc) (drop n ys) export -dumpBuffer : Buffer -> IO String +dumpBuffer : MonadIO io => Buffer -> io String dumpBuffer buf = do - size <- rawSize buf - dat <- bufferData buf + size <- liftIO $ rawSize buf + dat <- liftIO $ bufferData buf let rows = group 16 dat let hex = showSep "\n" 0 (map renderRow rows) pure $ hex ++ "\n\ntotal size = " ++ show size export -printBuffer : Buffer -> IO () -printBuffer buf = putStrLn $ !(dumpBuffer buf) \ No newline at end of file +printBuffer : MonadIO io => Buffer -> io () +printBuffer buf = putStrLn $ !(dumpBuffer buf) diff --git a/libs/contrib/System/Random.idr b/libs/contrib/System/Random.idr index d5ddf438a..c0de3261b 100644 --- a/libs/contrib/System/Random.idr +++ b/libs/contrib/System/Random.idr @@ -6,12 +6,12 @@ import Data.List public export interface Random a where - randomIO : IO a + randomIO : MonadIO io => io a -- Takes a range (lo, hi), and returns a random value uniformly -- distributed in the closed interval [lo, hi]. It is unspecified what -- happens if lo > hi. - randomRIO : (a, a) -> IO a + randomRIO : MonadIO io => (a, a) -> io a prim_randomInt : Int -> IO Int prim_randomInt upperBound = schemeCall Int "blodwen-random" [upperBound] @@ -23,12 +23,12 @@ Random Int where let maxInt = shiftL 1 31 - 1 minInt = negate $ shiftL 1 31 range = maxInt - minInt - in map (+ minInt) $ prim_randomInt range + in map (+ minInt) $ liftIO $ prim_randomInt range -- Generate a random value within [lo, hi]. randomRIO (lo, hi) = let range = hi - lo + 1 - in map (+ lo) $ prim_randomInt range + in map (+ lo) $ liftIO $ prim_randomInt range prim_randomDouble : IO Double prim_randomDouble = schemeCall Double "blodwen-random" [] @@ -36,10 +36,10 @@ prim_randomDouble = schemeCall Double "blodwen-random" [] public export Random Double where -- Generate a random value within [0, 1]. - randomIO = prim_randomDouble + randomIO = liftIO prim_randomDouble -- Generate a random value within [lo, hi]. - randomRIO (lo, hi) = map ((+ lo) . (* (hi - lo))) prim_randomDouble + randomRIO (lo, hi) = map ((+ lo) . (* (hi - lo))) (liftIO prim_randomDouble) ||| Sets the random seed export diff --git a/libs/network/Network/Socket.idr b/libs/network/Network/Socket.idr index e7ebf26e0..38a1d4bd5 100644 --- a/libs/network/Network/Socket.idr +++ b/libs/network/Network/Socket.idr @@ -14,10 +14,11 @@ import Network.FFI ||| Creates a UNIX socket with the given family, socket type and protocol ||| number. Returns either a socket or an error. export -socket : (fam : SocketFamily) +socket : MonadIO io + => (fam : SocketFamily) -> (ty : SocketType) -> (pnum : ProtocolNumber) - -> IO (Either SocketError Socket) + -> io (Either SocketError Socket) socket sf st pn = do socket_res <- primIO $ idrnet_socket (toCode sf) (toCode st) pn @@ -27,17 +28,18 @@ socket sf st pn = do ||| Close a socket export -close : Socket -> IO () +close : MonadIO io => Socket -> io () close sock = do _ <- primIO $ socket_close $ descriptor sock pure () ||| Binds a socket to the given socket address and port. ||| Returns 0 on success, an error code otherwise. export -bind : (sock : Socket) +bind : MonadIO io + => (sock : Socket) -> (addr : Maybe SocketAddress) -> (port : Port) - -> IO Int + -> io Int bind sock addr port = do bind_res <- primIO $ idrnet_bind (descriptor sock) @@ -57,10 +59,11 @@ bind sock addr port = do ||| Connects to a given address and port. ||| Returns 0 on success, and an error number on error. export -connect : (sock : Socket) +connect : MonadIO io + => (sock : Socket) -> (addr : SocketAddress) -> (port : Port) - -> IO ResultCode + -> io ResultCode connect sock addr port = do conn_res <- primIO $ idrnet_connect (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port @@ -73,7 +76,7 @@ connect sock addr port = do ||| ||| @sock The socket to listen on. export -listen : (sock : Socket) -> IO Int +listen : MonadIO io => (sock : Socket) -> io Int listen sock = do listen_res <- primIO $ socket_listen (descriptor sock) BACKLOG if listen_res == (-1) @@ -89,8 +92,9 @@ listen sock = do ||| ||| @sock The socket used to establish connection. export -accept : (sock : Socket) - -> IO (Either SocketError (Socket, SocketAddress)) +accept : MonadIO io + => (sock : Socket) + -> io (Either SocketError (Socket, SocketAddress)) accept sock = do -- We need a pointer to a sockaddr structure. This is then passed into @@ -115,9 +119,10 @@ accept sock = do ||| @sock The socket on which to send the message. ||| @msg The data to send. export -send : (sock : Socket) +send : MonadIO io + => (sock : Socket) -> (msg : String) - -> IO (Either SocketError ResultCode) + -> io (Either SocketError ResultCode) send sock dat = do send_res <- primIO $ idrnet_send (descriptor sock) dat @@ -135,9 +140,10 @@ send sock dat = do ||| @sock The socket on which to receive the message. ||| @len How much of the data to receive. export -recv : (sock : Socket) +recv : MonadIO io + => (sock : Socket) -> (len : ByteLength) - -> IO (Either SocketError (String, ResultCode)) + -> io (Either SocketError (String, ResultCode)) recv sock len = do -- Firstly make the request, get some kind of recv structure which -- contains the result of the recv and possibly the retrieved payload @@ -166,11 +172,11 @@ recv sock len = do ||| ||| @sock The socket on which to receive the message. export -recvAll : (sock : Socket) -> IO (Either SocketError String) +recvAll : MonadIO io => (sock : Socket) -> io (Either SocketError String) recvAll sock = recvRec sock [] 64 where partial - recvRec : Socket -> List String -> ByteLength -> IO (Either SocketError String) + recvRec : Socket -> List String -> ByteLength -> io (Either SocketError String) recvRec sock acc n = do res <- recv sock n case res of Left c => pure (Left c) @@ -188,11 +194,12 @@ recvAll sock = recvRec sock [] 64 ||| @port The port on which to send the message. ||| @msg The message to send. export -sendTo : (sock : Socket) +sendTo : MonadIO io + => (sock : Socket) -> (addr : SocketAddress) -> (port : Port) -> (msg : String) - -> IO (Either SocketError ByteLength) + -> io (Either SocketError ByteLength) sendTo sock addr p dat = do sendto_res <- primIO $ idrnet_sendto (descriptor sock) dat (show addr) p (toCode $ family sock) @@ -213,9 +220,10 @@ sendTo sock addr p dat = do ||| @len Size of the expected message. ||| export -recvFrom : (sock : Socket) +recvFrom : MonadIO io + => (sock : Socket) -> (len : ByteLength) - -> IO (Either SocketError (UDPAddrInfo, String, ResultCode)) + -> io (Either SocketError (UDPAddrInfo, String, ResultCode)) recvFrom sock bl = do recv_ptr <- primIO $ idrnet_recvfrom (descriptor sock) bl diff --git a/libs/network/Network/Socket/Data.idr b/libs/network/Network/Socket/Data.idr index 0310ce7af..a5df9f585 100644 --- a/libs/network/Network/Socket/Data.idr +++ b/libs/network/Network/Socket/Data.idr @@ -68,11 +68,11 @@ idrnet_isNull : (ptr : AnyPtr) -> PrimIO Int export -getErrno : IO SocketError +getErrno : HasIO io => io SocketError getErrno = primIO $ idrnet_errno export -nullPtr : AnyPtr -> IO Bool +nullPtr : MonadIO io => AnyPtr -> io Bool nullPtr p = do 0 <- primIO $ idrnet_isNull p | _ => pure True pure False diff --git a/libs/network/Network/Socket/Raw.idr b/libs/network/Network/Socket/Raw.idr index 8bbebb8e7..ad4d3f16d 100644 --- a/libs/network/Network/Socket/Raw.idr +++ b/libs/network/Network/Socket/Raw.idr @@ -27,39 +27,39 @@ data SockaddrPtr = SAPtr AnyPtr ||| Put a value in a buffer export -sock_poke : BufPtr -> Int -> Int -> IO () +sock_poke : HasIO io => BufPtr -> Int -> Int -> io () sock_poke (BPtr ptr) offset val = primIO $ idrnet_poke ptr offset val ||| Take a value from a buffer export -sock_peek : BufPtr -> Int -> IO Int +sock_peek : HasIO io => BufPtr -> Int -> io Int sock_peek (BPtr ptr) offset = primIO $ idrnet_peek ptr offset ||| Frees a given pointer export -sock_free : BufPtr -> IO () +sock_free : HasIO io => BufPtr -> io () sock_free (BPtr ptr) = primIO $ idrnet_free ptr export -sockaddr_free : SockaddrPtr -> IO () +sockaddr_free : HasIO io => SockaddrPtr -> io () sockaddr_free (SAPtr ptr) = primIO $ idrnet_free ptr ||| Allocates an amount of memory given by the ByteLength parameter. ||| ||| Used to allocate a mutable pointer to be given to the Recv functions. export -sock_alloc : ByteLength -> IO BufPtr +sock_alloc : MonadIO io => ByteLength -> io BufPtr sock_alloc bl = map BPtr $ primIO $ idrnet_malloc bl ||| Retrieves the port the given socket is bound to export -getSockPort : Socket -> IO Port +getSockPort : HasIO io => Socket -> io Port getSockPort sock = primIO $ idrnet_sockaddr_port $ descriptor sock ||| Retrieves a socket address from a sockaddr pointer export -getSockAddr : SockaddrPtr -> IO SocketAddress +getSockAddr : MonadIO io => SockaddrPtr -> io SocketAddress getSockAddr (SAPtr ptr) = do addr_family_int <- primIO $ idrnet_sockaddr_family ptr @@ -73,12 +73,12 @@ getSockAddr (SAPtr ptr) = do Just AF_UNSPEC => pure InvalidAddress) export -freeRecvStruct : RecvStructPtr -> IO () +freeRecvStruct : HasIO io => RecvStructPtr -> io () freeRecvStruct (RSPtr p) = primIO $ idrnet_free_recv_struct p ||| Utility to extract data. export -freeRecvfromStruct : RecvfromStructPtr -> IO () +freeRecvfromStruct : HasIO io => RecvfromStructPtr -> io () freeRecvfromStruct (RFPtr p) = primIO $ idrnet_free_recvfrom_struct p ||| Sends the data in a given memory location @@ -90,10 +90,11 @@ freeRecvfromStruct (RFPtr p) = primIO $ idrnet_free_recvfrom_struct p ||| @ptr The location containing the data to send. ||| @len How much of the data to send. export -sendBuf : (sock : Socket) +sendBuf : MonadIO io + => (sock : Socket) -> (ptr : BufPtr) -> (len : ByteLength) - -> IO (Either SocketError ResultCode) + -> io (Either SocketError ResultCode) sendBuf sock (BPtr ptr) len = do send_res <- primIO $ idrnet_send_buf (descriptor sock) ptr len @@ -110,10 +111,11 @@ sendBuf sock (BPtr ptr) len = do ||| @ptr The location containing the data to receive. ||| @len How much of the data to receive. export -recvBuf : (sock : Socket) +recvBuf : MonadIO io + => (sock : Socket) -> (ptr : BufPtr) -> (len : ByteLength) - -> IO (Either SocketError ResultCode) + -> io (Either SocketError ResultCode) recvBuf sock (BPtr ptr) len = do recv_res <- primIO $ idrnet_recv_buf (descriptor sock) ptr len @@ -132,12 +134,13 @@ recvBuf sock (BPtr ptr) len = do ||| @ptr A Pointer to the buffer containing the message. ||| @len The size of the message. export -sendToBuf : (sock : Socket) +sendToBuf : MonadIO io + => (sock : Socket) -> (addr : SocketAddress) -> (port : Port) -> (ptr : BufPtr) -> (len : ByteLength) - -> IO (Either SocketError ResultCode) + -> io (Either SocketError ResultCode) sendToBuf sock addr p (BPtr dat) len = do sendto_res <- primIO $ idrnet_sendto_buf (descriptor sock) dat len (show addr) p (toCode $ family sock) @@ -148,19 +151,19 @@ sendToBuf sock addr p (BPtr dat) len = do ||| Utility function to get the payload of the sent message as a `String`. export -foreignGetRecvfromPayload : RecvfromStructPtr -> IO String +foreignGetRecvfromPayload : HasIO io => RecvfromStructPtr -> io String foreignGetRecvfromPayload (RFPtr p) = primIO $ idrnet_get_recvfrom_payload p ||| Utility function to return senders socket address. export -foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress +foreignGetRecvfromAddr : MonadIO io => RecvfromStructPtr -> io SocketAddress foreignGetRecvfromAddr (RFPtr p) = do sockaddr_ptr <- map SAPtr $ primIO $ idrnet_get_recvfrom_sockaddr p getSockAddr sockaddr_ptr ||| Utility function to return sender's IPV4 port. export -foreignGetRecvfromPort : RecvfromStructPtr -> IO Port +foreignGetRecvfromPort : MonadIO io => RecvfromStructPtr -> io Port foreignGetRecvfromPort (RFPtr p) = do sockaddr_ptr <- primIO $ idrnet_get_recvfrom_sockaddr p port <- primIO $ idrnet_sockaddr_ipv4_port sockaddr_ptr @@ -178,10 +181,11 @@ foreignGetRecvfromPort (RFPtr p) = do ||| @len Size of the expected message. ||| export -recvFromBuf : (sock : Socket) +recvFromBuf : MonadIO io + => (sock : Socket) -> (ptr : BufPtr) -> (len : ByteLength) - -> IO (Either SocketError (UDPAddrInfo, ResultCode)) + -> io (Either SocketError (UDPAddrInfo, ResultCode)) recvFromBuf sock (BPtr ptr) bl = do recv_ptr <- primIO $ idrnet_recvfrom_buf (descriptor sock) ptr bl diff --git a/tests/chez/chez010/CB.idr b/tests/chez/chez010/CB.idr index 3407df547..80b46cdf0 100644 --- a/tests/chez/chez010/CB.idr +++ b/tests/chez/chez010/CB.idr @@ -13,11 +13,11 @@ prim_applyCharFn : Char -> Int -> (Char -> Int -> PrimIO Char) -> PrimIO Char %foreign libcb "applyIntFnPure" applyIntFnPure : Int -> Int -> (Int -> Int -> Int) -> Int -applyIntFn : Int -> Int -> (Int -> Int -> IO Int) -> IO Int +applyIntFn : HasIO io => Int -> Int -> (Int -> Int -> IO Int) -> io Int applyIntFn x y fn = primIO $ prim_applyIntFn x y (\a, b => toPrim (fn a b)) -applyCharFn : Char -> Int -> (Char -> Int -> IO Char) -> IO Char +applyCharFn : HasIO io => Char -> Int -> (Char -> Int -> IO Char) -> io Char applyCharFn x y fn = primIO $ prim_applyCharFn x y (\a, b => toPrim (fn a b)) From dbdf7dab3dd56703428d2c540ea720f6c26f1616 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 21 Jun 2020 19:21:22 +0100 Subject: [PATCH 4/6] Back to HasIO, remove MonadIO Following a fairly detailed discussion on slack, the feeling is generally that it's better to have a single interface. While precision is nice, it doesn't appear to buy us anything here. If that turns out to be wrong, or limiting somehow, we can revisit it later. Also: - it's easier for backend authors if the type of IO operations is slightly less restrictive. For example, if it's in HasIO, that limits alternative implementations, which might be awkward for some alternative back ends. - it's one less extra detail to learn. This is minor, but there needs to be a clear advantage if there's more detail to learn. - It is difficult to think of an underlying type that can't have a Monad instance (I have personally never encountered one - if they turns out to exist, again, we can revisit!) --- docs/source/ffi/ffi.rst | 4 +-- docs/source/tutorial/interfaces.rst | 14 ++++----- libs/base/Data/IOArray.idr | 10 +++---- libs/base/Data/IORef.idr | 4 +-- libs/base/Data/Ref.idr | 2 +- libs/base/System.idr | 10 +++---- libs/base/System/Directory.idr | 14 ++++----- libs/base/System/File.idr | 44 ++++++++++++++-------------- libs/base/System/REPL.idr | 4 +-- libs/contrib/Debug/Buffer.idr | 4 +-- libs/contrib/System/Random.idr | 4 +-- libs/network/Network/Socket.idr | 22 +++++++------- libs/network/Network/Socket/Data.idr | 2 +- libs/network/Network/Socket/Raw.idr | 16 +++++----- libs/prelude/Prelude.idr | 8 +---- tests/idris2/coverage008/expected | 2 +- tests/idris2/coverage010/expected | 2 +- 17 files changed, 79 insertions(+), 87 deletions(-) diff --git a/docs/source/ffi/ffi.rst b/docs/source/ffi/ffi.rst index 8296c60b8..50f64b0b4 100644 --- a/docs/source/ffi/ffi.rst +++ b/docs/source/ffi/ffi.rst @@ -89,8 +89,8 @@ returns a primitive IO action: Internally, ``PrimIO Int`` is a function which takes the current (linear) state of the world, and returns an ``Int`` with an updated state of the world. In general, ``IO`` operations in an Idris program are defined as instances -of the ``HasIO`` interface (or ``MonadIO``). We can convert a primitive -operation to one usable in ``HasIO`` using ``primIO``: +of the ``HasIO`` interface. We can convert a primitive operation to one usable +in ``HasIO`` using ``primIO``: .. code-block:: idris diff --git a/docs/source/tutorial/interfaces.rst b/docs/source/tutorial/interfaces.rst index 95cd37206..a10208c10 100644 --- a/docs/source/tutorial/interfaces.rst +++ b/docs/source/tutorial/interfaces.rst @@ -432,20 +432,18 @@ Interfaces and IO ================= In general, ``IO`` operations in the libraries aren't written using ``IO`` -directly, but rather via one of the following interfaces: +directly, but rather via the ``HasIO`` interface: .. code-block:: idris - interface HasIO io where + interface Monad io => HasIO io where liftIO : (1 _ : IO a) -> io a - interface (Monad io, HasIO io) => MonadIO io where - ``HasIO`` explains, via ``liftIO``, how to convert a primitive ``IO`` operation -to an operation in some underlying type. ``MonadIO`` has no methods, but -adds an additional ``Monad`` constraint. These interfaces allow a programmer -to define some more expressive notion of interactive program, while still -giving direct access to ``IO`` primitives. +to an operation in some underlying type, as long as that type has a ``Monad`` +implementation. These interface allows a programmer to define some more +expressive notion of interactive program, while still giving direct access to +``IO`` primitives. Idiom brackets ============== diff --git a/libs/base/Data/IOArray.idr b/libs/base/Data/IOArray.idr index fadc026b3..37df6964a 100644 --- a/libs/base/Data/IOArray.idr +++ b/libs/base/Data/IOArray.idr @@ -14,19 +14,19 @@ max : IOArray elem -> Int max = maxSize export -newArray : MonadIO io => Int -> io (IOArray elem) +newArray : HasIO io => Int -> io (IOArray elem) newArray size = pure (MkIOArray size !(primIO (prim__newArray size Nothing))) export -writeArray : MonadIO io => IOArray elem -> Int -> elem -> io () +writeArray : HasIO io => IOArray elem -> Int -> elem -> io () writeArray arr pos el = if pos < 0 || pos >= max arr then pure () else primIO (prim__arraySet (content arr) pos (Just el)) export -readArray : MonadIO io => IOArray elem -> Int -> io (Maybe elem) +readArray : HasIO io => IOArray elem -> Int -> io (Maybe elem) readArray arr pos = if pos < 0 || pos >= max arr then pure Nothing @@ -35,7 +35,7 @@ readArray arr pos -- Make a new array of the given size with the elements copied from the -- other array export -newArrayCopy : MonadIO io => +newArrayCopy : HasIO io => (newsize : Int) -> IOArray elem -> io (IOArray elem) newArrayCopy newsize arr = do let newsize' = if newsize < max arr then max arr else newsize @@ -54,7 +54,7 @@ newArrayCopy newsize arr assert_total (copyFrom old new (pos - 1)) export -toList : MonadIO io => IOArray elem -> io (List (Maybe elem)) +toList : HasIO io => IOArray elem -> io (List (Maybe elem)) toList arr = iter 0 (max arr) [] where iter : Int -> Int -> List (Maybe elem) -> io (List (Maybe elem)) diff --git a/libs/base/Data/IORef.idr b/libs/base/Data/IORef.idr index c511f5167..1bef1d916 100644 --- a/libs/base/Data/IORef.idr +++ b/libs/base/Data/IORef.idr @@ -13,7 +13,7 @@ data IORef : Type -> Type where MkRef : Mut a -> IORef a export -newIORef : MonadIO io => a -> io (IORef a) +newIORef : HasIO io => a -> io (IORef a) newIORef val = do m <- primIO (prim__newIORef val) 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) export -modifyIORef : MonadIO io => IORef a -> (a -> a) -> io () +modifyIORef : HasIO io => IORef a -> (a -> a) -> io () modifyIORef ref f = do val <- readIORef ref writeIORef ref (f val) diff --git a/libs/base/Data/Ref.idr b/libs/base/Data/Ref.idr index b012a45f8..153240afa 100644 --- a/libs/base/Data/Ref.idr +++ b/libs/base/Data/Ref.idr @@ -10,7 +10,7 @@ interface Ref m (r : Type -> Type) | m where writeRef : r a -> a -> m () export -MonadIO io => Ref io IORef where +HasIO io => Ref io IORef where newRef = newIORef readRef = readIORef writeRef = writeIORef diff --git a/libs/base/System.idr b/libs/base/System.idr index 2a56c2286..9424c0671 100644 --- a/libs/base/System.idr +++ b/libs/base/System.idr @@ -42,7 +42,7 @@ prim_setEnv : String -> String -> Int -> PrimIO Int prim_unsetEnv : String -> PrimIO Int export -getEnv : MonadIO io => String -> io (Maybe String) +getEnv : HasIO io => String -> io (Maybe String) getEnv var = do env <- primIO $ prim_getEnv var if prim__nullPtr env /= 0 @@ -50,7 +50,7 @@ getEnv var else pure (Just (prim__getString env)) export -getEnvironment : MonadIO io => io (List (String, String)) +getEnvironment : HasIO io => io (List (String, String)) getEnvironment = getAllPairs 0 [] where splitEq : String -> (String, String) @@ -67,7 +67,7 @@ getEnvironment = getAllPairs 0 [] else getAllPairs (n + 1) (prim__getString envPair :: acc) export -setEnv : MonadIO io => String -> String -> Bool -> io Bool +setEnv : HasIO io => String -> String -> Bool -> io Bool setEnv var val overwrite = do ok <- primIO $ prim_setEnv var val (if overwrite then 1 else 0) if ok == 0 @@ -75,7 +75,7 @@ setEnv var val overwrite else pure False export -unsetEnv : MonadIO io => String -> io Bool +unsetEnv : HasIO io => String -> io Bool unsetEnv var = do ok <- primIO $ prim_unsetEnv var if ok == 0 @@ -95,7 +95,7 @@ system cmd = primIO (prim_system cmd) prim_time : PrimIO Int export -time : MonadIO io => io Integer +time : HasIO io => io Integer time = pure $ cast !(primIO prim_time) %foreign libc "exit" diff --git a/libs/base/System/Directory.idr b/libs/base/System/Directory.idr index 2949c59ae..76008738e 100644 --- a/libs/base/System/Directory.idr +++ b/libs/base/System/Directory.idr @@ -12,7 +12,7 @@ support fn = "C:" ++ fn ++ ", libidris2_support" %foreign support "idris2_fileErrno" prim_fileErrno : PrimIO Int -returnError : MonadIO io => io (Either FileError a) +returnError : HasIO io => io (Either FileError a) returnError = do err <- primIO prim_fileErrno case err of @@ -23,7 +23,7 @@ returnError 4 => pure $ Left FileExists _ => pure $ Left (GenericFileError (err-5)) -ok : MonadIO io => a -> io (Either FileError a) +ok : HasIO io => a -> io (Either FileError a) ok x = pure (Right x) %foreign support "idris2_currentDirectory" @@ -52,7 +52,7 @@ data Directory : Type where MkDir : DirPtr -> Directory export -createDir : MonadIO io => String -> io (Either FileError ()) +createDir : HasIO io => String -> io (Either FileError ()) createDir dir = do res <- primIO (prim_createDir dir) if res == 0 @@ -60,13 +60,13 @@ createDir dir else returnError export -changeDir : MonadIO io => String -> io Bool +changeDir : HasIO io => String -> io Bool changeDir dir = do ok <- primIO (prim_changeDir dir) pure (ok == 0) export -currentDir : MonadIO io => io (Maybe String) +currentDir : HasIO io => io (Maybe String) currentDir = do res <- primIO prim_currentDir if prim__nullPtr res /= 0 @@ -74,7 +74,7 @@ currentDir else pure (Just (prim__getString res)) export -openDir : MonadIO io => String -> io (Either FileError Directory) +openDir : HasIO io => String -> io (Either FileError Directory) openDir d = do res <- primIO (prim_openDir d) if prim__nullAnyPtr res /= 0 @@ -90,7 +90,7 @@ removeDir : HasIO io => String -> io () removeDir dirName = primIO (prim_removeDir dirName) export -dirEntry : MonadIO io => Directory -> io (Either FileError String) +dirEntry : HasIO io => Directory -> io (Either FileError String) dirEntry (MkDir d) = do res <- primIO (prim_dirEntry d) if prim__nullPtr res /= 0 diff --git a/libs/base/System/File.idr b/libs/base/System/File.idr index 5e376e622..3b9b6db19 100644 --- a/libs/base/System/File.idr +++ b/libs/base/System/File.idr @@ -84,7 +84,7 @@ data FileError = GenericFileError Int -- errno | PermissionDenied | FileExists -returnError : MonadIO io => io (Either FileError a) +returnError : HasIO io => io (Either FileError a) returnError = do err <- primIO prim_fileErrno case err of @@ -104,7 +104,7 @@ Show FileError where show PermissionDenied = "Permission Denied" show FileExists = "File Exists" -ok : MonadIO io => a -> io (Either FileError a) +ok : HasIO io => a -> io (Either FileError a) ok x = pure (Right x) public export @@ -124,7 +124,7 @@ stderr : File stderr = FHandle prim__stderr export -openFile : MonadIO io => String -> Mode -> io (Either FileError File) +openFile : HasIO io => String -> Mode -> io (Either FileError File) openFile f m = do res <- primIO (prim__open f (modeStr m) 0) if prim__nullAnyPtr res /= 0 @@ -136,13 +136,13 @@ closeFile : HasIO io => File -> io () closeFile (FHandle f) = primIO (prim__close f) export -fileError : MonadIO io => File -> io Bool +fileError : HasIO io => File -> io Bool fileError (FHandle f) = do x <- primIO $ prim_error f pure (x /= 0) export -fGetLine : MonadIO io => (h : File) -> io (Either FileError String) +fGetLine : HasIO io => (h : File) -> io (Either FileError String) fGetLine (FHandle f) = do res <- primIO (prim__readLine f) if prim__nullPtr res /= 0 @@ -150,7 +150,7 @@ fGetLine (FHandle f) else ok (prim__getString res) export -fGetChars : MonadIO io => (h : File) -> Int -> io (Either FileError String) +fGetChars : HasIO io => (h : File) -> Int -> io (Either FileError String) fGetChars (FHandle f) max = do res <- primIO (prim__readChars max f) if prim__nullPtr res /= 0 @@ -158,7 +158,7 @@ fGetChars (FHandle f) max else ok (prim__getString res) export -fGetChar : MonadIO io => (h : File) -> io (Either FileError Char) +fGetChar : HasIO io => (h : File) -> io (Either FileError Char) fGetChar (FHandle h) = do c <- primIO (prim__readChar h) ferr <- primIO (prim_error h) @@ -167,7 +167,7 @@ fGetChar (FHandle h) else ok (cast c) export -fPutStr : MonadIO io => (h : File) -> String -> io (Either FileError ()) +fPutStr : HasIO io => (h : File) -> String -> io (Either FileError ()) fPutStr (FHandle f) str = do res <- primIO (prim__writeLine f str) if res == 0 @@ -175,23 +175,23 @@ fPutStr (FHandle f) str else ok () export -fPutStrLn : MonadIO io => (h : File) -> String -> io (Either FileError ()) +fPutStrLn : HasIO io => (h : File) -> String -> io (Either FileError ()) fPutStrLn f str = fPutStr f (str ++ "\n") export -fEOF : MonadIO io => (h : File) -> io Bool +fEOF : HasIO io => (h : File) -> io Bool fEOF (FHandle f) = do res <- primIO (prim__eof f) pure (res /= 0) export -fflush : MonadIO io => (h : File) -> io () +fflush : HasIO io => (h : File) -> io () fflush (FHandle f) = do primIO (prim__flush f) pure () export -popen : MonadIO io => String -> Mode -> io (Either FileError File) +popen : HasIO io => String -> Mode -> io (Either FileError File) popen f m = do ptr <- primIO (prim__popen f (modeStr m)) if prim__nullAnyPtr ptr /= 0 @@ -203,7 +203,7 @@ pclose : HasIO io => File -> io () pclose (FHandle h) = primIO (prim__pclose h) export -fileAccessTime : MonadIO io => (h : File) -> io (Either FileError Int) +fileAccessTime : HasIO io => (h : File) -> io (Either FileError Int) fileAccessTime (FHandle f) = do res <- primIO (prim__fileAccessTime f) if res > 0 @@ -211,7 +211,7 @@ fileAccessTime (FHandle f) else returnError export -fileModifiedTime : MonadIO io => (h : File) -> io (Either FileError Int) +fileModifiedTime : HasIO io => (h : File) -> io (Either FileError Int) fileModifiedTime (FHandle f) = do res <- primIO (prim__fileModifiedTime f) if res > 0 @@ -219,7 +219,7 @@ fileModifiedTime (FHandle f) else returnError export -fileStatusTime : MonadIO io => (h : File) -> io (Either FileError Int) +fileStatusTime : HasIO io => (h : File) -> io (Either FileError Int) fileStatusTime (FHandle f) = do res <- primIO (prim__fileStatusTime f) if res > 0 @@ -227,7 +227,7 @@ fileStatusTime (FHandle f) else returnError export -removeFile : MonadIO io => String -> io (Either FileError ()) +removeFile : HasIO io => String -> io (Either FileError ()) removeFile fname = do res <- primIO (prim__removeFile fname) if res == 0 @@ -235,7 +235,7 @@ removeFile fname else returnError export -fileSize : MonadIO io => (h : File) -> io (Either FileError Int) +fileSize : HasIO io => (h : File) -> io (Either FileError Int) fileSize (FHandle f) = do res <- primIO (prim__fileSize f) if res >= 0 @@ -243,13 +243,13 @@ fileSize (FHandle f) else returnError export -fPoll : MonadIO io => File -> io Bool +fPoll : HasIO io => File -> io Bool fPoll (FHandle f) = do p <- primIO (prim__fPoll f) pure (p > 0) export -readFile : MonadIO io => String -> io (Either FileError String) +readFile : HasIO io => String -> io (Either FileError String) readFile file = do Right h <- openFile file Read | Left err => returnError @@ -271,7 +271,7 @@ readFile file ||| Write a string to a file export -writeFile : MonadIO io => +writeFile : HasIO io => (filepath : String) -> (contents : String) -> io (Either FileError ()) writeFile fn contents = do @@ -307,7 +307,7 @@ mkMode p getMs = sum . map getM export -chmodRaw : MonadIO io => String -> Int -> io (Either FileError ()) +chmodRaw : HasIO io => String -> Int -> io (Either FileError ()) chmodRaw fname p = do ok <- primIO $ prim__chmod fname p if ok == 0 @@ -315,5 +315,5 @@ chmodRaw fname p else returnError export -chmod : MonadIO io => String -> Permissions -> io (Either FileError ()) +chmod : HasIO io => String -> Permissions -> io (Either FileError ()) chmod fname p = chmodRaw fname (mkMode p) diff --git a/libs/base/System/REPL.idr b/libs/base/System/REPL.idr index f51aeb3ab..9ef353ea6 100644 --- a/libs/base/System/REPL.idr +++ b/libs/base/System/REPL.idr @@ -8,7 +8,7 @@ import System.File ||| @ onInput the function to run on reading input, returning a String to ||| output and a new state. Returns Nothing if the repl should exit export -replWith : MonadIO io => +replWith : HasIO io => (state : a) -> (prompt : String) -> (onInput : a -> String -> Maybe (String, a)) -> io () replWith acc prompt fn @@ -29,7 +29,7 @@ replWith acc prompt fn ||| @ onInput the function to run on reading input, returning a String to ||| output export -repl : MonadIO io => +repl : HasIO io => (prompt : String) -> (onInput : String -> String) -> io () repl prompt fn = replWith () prompt (\x, s => Just (fn s, ())) diff --git a/libs/contrib/Debug/Buffer.idr b/libs/contrib/Debug/Buffer.idr index 2f7161402..f0841f91c 100644 --- a/libs/contrib/Debug/Buffer.idr +++ b/libs/contrib/Debug/Buffer.idr @@ -31,7 +31,7 @@ group n xs = worker [] xs worker acc ys = worker ((take n ys)::acc) (drop n ys) export -dumpBuffer : MonadIO io => Buffer -> io String +dumpBuffer : HasIO io => Buffer -> io String dumpBuffer buf = do size <- liftIO $ rawSize buf dat <- liftIO $ bufferData buf @@ -40,5 +40,5 @@ dumpBuffer buf = do pure $ hex ++ "\n\ntotal size = " ++ show size export -printBuffer : MonadIO io => Buffer -> io () +printBuffer : HasIO io => Buffer -> io () printBuffer buf = putStrLn $ !(dumpBuffer buf) diff --git a/libs/contrib/System/Random.idr b/libs/contrib/System/Random.idr index c0de3261b..ec0653be3 100644 --- a/libs/contrib/System/Random.idr +++ b/libs/contrib/System/Random.idr @@ -6,12 +6,12 @@ import Data.List public export interface Random a where - randomIO : MonadIO io => io a + randomIO : HasIO io => io a -- Takes a range (lo, hi), and returns a random value uniformly -- distributed in the closed interval [lo, hi]. It is unspecified what -- happens if lo > hi. - randomRIO : MonadIO io => (a, a) -> io a + randomRIO : HasIO io => (a, a) -> io a prim_randomInt : Int -> IO Int prim_randomInt upperBound = schemeCall Int "blodwen-random" [upperBound] diff --git a/libs/network/Network/Socket.idr b/libs/network/Network/Socket.idr index 38a1d4bd5..4ff0d8586 100644 --- a/libs/network/Network/Socket.idr +++ b/libs/network/Network/Socket.idr @@ -14,7 +14,7 @@ import Network.FFI ||| Creates a UNIX socket with the given family, socket type and protocol ||| number. Returns either a socket or an error. export -socket : MonadIO io +socket : HasIO io => (fam : SocketFamily) -> (ty : SocketType) -> (pnum : ProtocolNumber) @@ -28,14 +28,14 @@ socket sf st pn = do ||| Close a socket export -close : MonadIO io => Socket -> io () +close : HasIO io => Socket -> io () close sock = do _ <- primIO $ socket_close $ descriptor sock pure () ||| Binds a socket to the given socket address and port. ||| Returns 0 on success, an error code otherwise. export -bind : MonadIO io +bind : HasIO io => (sock : Socket) -> (addr : Maybe SocketAddress) -> (port : Port) @@ -59,7 +59,7 @@ bind sock addr port = do ||| Connects to a given address and port. ||| Returns 0 on success, and an error number on error. export -connect : MonadIO io +connect : HasIO io => (sock : Socket) -> (addr : SocketAddress) -> (port : Port) @@ -76,7 +76,7 @@ connect sock addr port = do ||| ||| @sock The socket to listen on. export -listen : MonadIO io => (sock : Socket) -> io Int +listen : HasIO io => (sock : Socket) -> io Int listen sock = do listen_res <- primIO $ socket_listen (descriptor sock) BACKLOG if listen_res == (-1) @@ -92,7 +92,7 @@ listen sock = do ||| ||| @sock The socket used to establish connection. export -accept : MonadIO io +accept : HasIO io => (sock : Socket) -> io (Either SocketError (Socket, SocketAddress)) accept sock = do @@ -119,7 +119,7 @@ accept sock = do ||| @sock The socket on which to send the message. ||| @msg The data to send. export -send : MonadIO io +send : HasIO io => (sock : Socket) -> (msg : String) -> io (Either SocketError ResultCode) @@ -140,7 +140,7 @@ send sock dat = do ||| @sock The socket on which to receive the message. ||| @len How much of the data to receive. export -recv : MonadIO io +recv : HasIO io => (sock : Socket) -> (len : ByteLength) -> io (Either SocketError (String, ResultCode)) @@ -172,7 +172,7 @@ recv sock len = do ||| ||| @sock The socket on which to receive the message. export -recvAll : MonadIO io => (sock : Socket) -> io (Either SocketError String) +recvAll : HasIO io => (sock : Socket) -> io (Either SocketError String) recvAll sock = recvRec sock [] 64 where partial @@ -194,7 +194,7 @@ recvAll sock = recvRec sock [] 64 ||| @port The port on which to send the message. ||| @msg The message to send. export -sendTo : MonadIO io +sendTo : HasIO io => (sock : Socket) -> (addr : SocketAddress) -> (port : Port) @@ -220,7 +220,7 @@ sendTo sock addr p dat = do ||| @len Size of the expected message. ||| export -recvFrom : MonadIO io +recvFrom : HasIO io => (sock : Socket) -> (len : ByteLength) -> io (Either SocketError (UDPAddrInfo, String, ResultCode)) diff --git a/libs/network/Network/Socket/Data.idr b/libs/network/Network/Socket/Data.idr index a5df9f585..2a403fe1a 100644 --- a/libs/network/Network/Socket/Data.idr +++ b/libs/network/Network/Socket/Data.idr @@ -72,7 +72,7 @@ getErrno : HasIO io => io SocketError getErrno = primIO $ idrnet_errno export -nullPtr : MonadIO io => AnyPtr -> io Bool +nullPtr : HasIO io => AnyPtr -> io Bool nullPtr p = do 0 <- primIO $ idrnet_isNull p | _ => pure True pure False diff --git a/libs/network/Network/Socket/Raw.idr b/libs/network/Network/Socket/Raw.idr index ad4d3f16d..bf2743874 100644 --- a/libs/network/Network/Socket/Raw.idr +++ b/libs/network/Network/Socket/Raw.idr @@ -48,7 +48,7 @@ sockaddr_free (SAPtr ptr) = primIO $ idrnet_free ptr ||| ||| Used to allocate a mutable pointer to be given to the Recv functions. export -sock_alloc : MonadIO io => ByteLength -> io BufPtr +sock_alloc : HasIO io => ByteLength -> io BufPtr sock_alloc bl = map BPtr $ primIO $ idrnet_malloc bl ||| Retrieves the port the given socket is bound to @@ -59,7 +59,7 @@ getSockPort sock = primIO $ idrnet_sockaddr_port $ descriptor sock ||| Retrieves a socket address from a sockaddr pointer export -getSockAddr : MonadIO io => SockaddrPtr -> io SocketAddress +getSockAddr : HasIO io => SockaddrPtr -> io SocketAddress getSockAddr (SAPtr ptr) = do addr_family_int <- primIO $ idrnet_sockaddr_family ptr @@ -90,7 +90,7 @@ freeRecvfromStruct (RFPtr p) = primIO $ idrnet_free_recvfrom_struct p ||| @ptr The location containing the data to send. ||| @len How much of the data to send. export -sendBuf : MonadIO io +sendBuf : HasIO io => (sock : Socket) -> (ptr : BufPtr) -> (len : ByteLength) @@ -111,7 +111,7 @@ sendBuf sock (BPtr ptr) len = do ||| @ptr The location containing the data to receive. ||| @len How much of the data to receive. export -recvBuf : MonadIO io +recvBuf : HasIO io => (sock : Socket) -> (ptr : BufPtr) -> (len : ByteLength) @@ -134,7 +134,7 @@ recvBuf sock (BPtr ptr) len = do ||| @ptr A Pointer to the buffer containing the message. ||| @len The size of the message. export -sendToBuf : MonadIO io +sendToBuf : HasIO io => (sock : Socket) -> (addr : SocketAddress) -> (port : Port) @@ -156,14 +156,14 @@ foreignGetRecvfromPayload (RFPtr p) = primIO $ idrnet_get_recvfrom_payload p ||| Utility function to return senders socket address. export -foreignGetRecvfromAddr : MonadIO io => RecvfromStructPtr -> io SocketAddress +foreignGetRecvfromAddr : HasIO io => RecvfromStructPtr -> io SocketAddress foreignGetRecvfromAddr (RFPtr p) = do sockaddr_ptr <- map SAPtr $ primIO $ idrnet_get_recvfrom_sockaddr p getSockAddr sockaddr_ptr ||| Utility function to return sender's IPV4 port. export -foreignGetRecvfromPort : MonadIO io => RecvfromStructPtr -> io Port +foreignGetRecvfromPort : HasIO io => RecvfromStructPtr -> io Port foreignGetRecvfromPort (RFPtr p) = do sockaddr_ptr <- primIO $ idrnet_get_recvfrom_sockaddr p port <- primIO $ idrnet_sockaddr_ipv4_port sockaddr_ptr @@ -181,7 +181,7 @@ foreignGetRecvfromPort (RFPtr p) = do ||| @len Size of the expected message. ||| export -recvFromBuf : MonadIO io +recvFromBuf : HasIO io => (sock : Socket) -> (ptr : BufPtr) -> (len : ByteLength) diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr index d38d96c56..8b473b902 100644 --- a/libs/prelude/Prelude.idr +++ b/libs/prelude/Prelude.idr @@ -1564,15 +1564,9 @@ Monad IO where b >>= k = io_bind b k public export -interface HasIO io where +interface Monad io => HasIO io where 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 HasIO IO where liftIO x = x diff --git a/tests/idris2/coverage008/expected b/tests/idris2/coverage008/expected index 54edf0f50..cfbd64774 100644 --- a/tests/idris2/coverage008/expected +++ b/tests/idris2/coverage008/expected @@ -1,6 +1,6 @@ 1/1: Building wcov (wcov.idr) Main> Main.tfoo is total Main> Main.wfoo is total -Main> Main.wbar is not covering due to call to function Main.with block in 1392 +Main> Main.wbar is not covering due to call to function Main.with block in 1387 Main> Main.wbar1 is total Main> Bye for now! diff --git a/tests/idris2/coverage010/expected b/tests/idris2/coverage010/expected index c2e2da8d2..3204bc8a5 100644 --- a/tests/idris2/coverage010/expected +++ b/tests/idris2/coverage010/expected @@ -3,4 +3,4 @@ casetot.idr:12:1--13:1:main is not covering at: 12 main : IO () 13 main = do - Calls non covering function Main.case block in 2119(619) + Calls non covering function Main.case block in 2114(619) From 0316dfa41733f352f4e70764929c03bcdd0786cc Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 21 Jun 2020 19:41:18 +0100 Subject: [PATCH 5/6] Remove reference to MonadIO from CHANGELOG --- CHANGELOG.md | 1 - 1 file changed, 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4856fe9be..1cf227521 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -22,7 +22,6 @@ 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 arrays with constant time read/write, convertible to immutable arrays with constant time read. From 413e75b6a30ffb7cc67eea2b7f5ec513bb03d116 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 21 Jun 2020 19:56:23 +0100 Subject: [PATCH 6/6] Fix documentaton error --- docs/source/ffi/ffi.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/ffi/ffi.rst b/docs/source/ffi/ffi.rst index 50f64b0b4..f5aaf38a4 100644 --- a/docs/source/ffi/ffi.rst +++ b/docs/source/ffi/ffi.rst @@ -94,7 +94,7 @@ in ``HasIO`` using ``primIO``: .. code-block:: idris - primIO : HasIO a => PrimIO a -> io a + primIO : HasIO io => PrimIO a -> io a So, we can extend our program as follows: