From d12487f52916842e80b8e04d305fd48bb1465282 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 21 Jun 2020 01:18:43 +0100 Subject: [PATCH] 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 []