mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 00:31:57 +03:00
Merge pull request #345 from edwinb/hasio
HasIO interface for IO actions
This commit is contained in:
Edwin Brady
GitHub
commit
1e6314c4cc
@ -20,6 +20,8 @@ Language changes:
|
||||
|
||||
Library changes:
|
||||
|
||||
* `IO` operations in the `prelude` and `base` libraries now use the
|
||||
`HasIO` interface, rather than using `IO` directly.
|
||||
* Experimental `Data.Linear.Array` added to `contrib`, support mutable linear
|
||||
arrays with constant time read/write, convertible to immutable arrays with
|
||||
constant time read.
|
||||
|
||||
@ -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. We can convert a primitive operation to one usable
|
||||
in ``HasIO`` using ``primIO``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
primIO : PrimIO a -> IO a
|
||||
primIO : HasIO io => 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:
|
||||
|
||||
|
||||
@ -428,6 +428,23 @@ 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 the ``HasIO`` interface:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interface Monad io => HasIO io where
|
||||
liftIO : (1 _ : IO a) -> io a
|
||||
|
||||
``HasIO`` explains, via ``liftIO``, how to convert a primitive ``IO`` operation
|
||||
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
|
||||
==============
|
||||
|
||||
|
||||
@ -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 ())
|
||||
$ \_ =>
|
||||
|
||||
@ -14,19 +14,19 @@ max : IOArray elem -> Int
|
||||
max = maxSize
|
||||
|
||||
export
|
||||
newArray : Int -> IO (IOArray elem)
|
||||
newArray : HasIO io => Int -> io (IOArray elem)
|
||||
newArray size
|
||||
= pure (MkIOArray size !(primIO (prim__newArray size Nothing)))
|
||||
|
||||
export
|
||||
writeArray : 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 : 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,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 : HasIO 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 : 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))
|
||||
iter : Int -> Int -> List (Maybe elem) -> io (List (Maybe elem))
|
||||
iter pos end acc
|
||||
= if pos >= end
|
||||
then pure (reverse acc)
|
||||
|
||||
@ -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)
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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)
|
||||
|
||||
@ -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, ()))
|
||||
|
||||
|
||||
@ -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 : HasIO 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 : HasIO io => Buffer -> io ()
|
||||
printBuffer buf = putStrLn $ !(dumpBuffer buf)
|
||||
@ -6,12 +6,12 @@ import Data.List
|
||||
|
||||
public export
|
||||
interface Random a where
|
||||
randomIO : 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 : (a, a) -> IO a
|
||||
randomRIO : HasIO 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
|
||||
|
||||
@ -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 : HasIO 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 : 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 : (sock : Socket)
|
||||
bind : HasIO 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 : HasIO 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 : HasIO 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 : HasIO 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 : HasIO 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 : HasIO 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 : HasIO 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 : HasIO 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 : HasIO 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
|
||||
|
||||
@ -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 : HasIO io => AnyPtr -> io Bool
|
||||
nullPtr p = do 0 <- primIO $ idrnet_isNull p
|
||||
| _ => pure True
|
||||
pure False
|
||||
|
||||
@ -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 : HasIO 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 : HasIO 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 : HasIO 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 : HasIO 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 : HasIO 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 : 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 : 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
|
||||
@ -178,10 +181,11 @@ foreignGetRecvfromPort (RFPtr p) = do
|
||||
||| @len Size of the expected message.
|
||||
|||
|
||||
export
|
||||
recvFromBuf : (sock : Socket)
|
||||
recvFromBuf : HasIO 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
|
||||
|
||||
|
||||
@ -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
|
||||
|
||||
-----------------------
|
||||
|
||||
@ -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
|
||||
|
||||
|
||||
@ -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))
|
||||
|
||||
|
||||
@ -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!
|
||||
|
||||
@ -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)
|
||||
|
||||
@ -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 ())
|
||||
$ \_ =>
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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,14 +50,14 @@ 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,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 []
|
||||
|
||||
Loading…
Reference in New Issue
Block a user