mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 20:23:11 +03:00
161 lines
4.3 KiB
Idris
161 lines
4.3 KiB
Idris
module PrimIO
|
|
|
|
import Builtin
|
|
|
|
public export
|
|
data IORes : Type -> Type where
|
|
MkIORes : (result : a) -> (1 x : %World) -> IORes a
|
|
|
|
||| Idris's primitive IO, for building abstractions on top of.
|
|
public export
|
|
PrimIO : Type -> Type
|
|
PrimIO a = (1 x : %World) -> IORes a
|
|
|
|
export
|
|
data IO : Type -> Type where
|
|
MkIO : (1 fn : PrimIO a) -> IO a
|
|
|
|
export
|
|
prim_io_pure : a -> PrimIO a
|
|
prim_io_pure x = \w => MkIORes x w
|
|
|
|
%inline
|
|
export
|
|
io_pure : a -> IO a
|
|
io_pure x = MkIO (\w => MkIORes x w)
|
|
|
|
export
|
|
prim_io_bind : (1 act : PrimIO a) -> (1 k : a -> PrimIO b) -> PrimIO b
|
|
prim_io_bind fn k w
|
|
= let MkIORes x' w' = fn w in k x' w'
|
|
|
|
-- There's a special case for inlining this is Compiler.Inline, because
|
|
-- the inliner is cautious about case blocks at the moment. Once it's less
|
|
-- cautious, add an explicit %inline directive and take out the special case.
|
|
-- See also dealing with the newtype optimisation via %World in
|
|
-- Compiler.CompileExpr
|
|
export
|
|
io_bind : (1 act : IO a) -> (1 k : a -> IO b) -> IO b
|
|
io_bind (MkIO fn) k
|
|
= MkIO (\w => let MkIORes x' w' = fn w
|
|
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
|
|
public export
|
|
data Ptr : Type -> Type where [external]
|
|
|
|
-- A pointer to any type (representing a void* in foreign calls)
|
|
public export
|
|
data AnyPtr : Type where [external]
|
|
|
|
public export
|
|
data ThreadID : Type where [external]
|
|
|
|
public export
|
|
data FArgList : Type where
|
|
Nil : FArgList
|
|
(::) : {a : Type} -> (1 arg : a) -> (1 args : FArgList) -> FArgList
|
|
|
|
%extern prim__cCall : (ret : Type) -> String -> (1 args : FArgList) ->
|
|
(1 x : %World) -> IORes ret
|
|
%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
|
|
|
|
export %inline
|
|
toPrim : (1 act : IO a) -> PrimIO a
|
|
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)
|
|
|
|
export %inline
|
|
cCall : (ret : Type) -> String -> FArgList -> IO ret
|
|
cCall ret fn args = primIO (prim__cCall ret fn args)
|
|
|
|
%foreign "C:idris2_isNull, libidris2_support"
|
|
export
|
|
prim__nullAnyPtr : AnyPtr -> Int
|
|
|
|
prim__forgetPtr : Ptr t -> AnyPtr
|
|
prim__forgetPtr = believe_me
|
|
|
|
export %inline
|
|
prim__nullPtr : Ptr t -> Int -- can't pass 'type' to a foreign function
|
|
prim__nullPtr p = prim__nullAnyPtr (prim__forgetPtr p)
|
|
|
|
%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
|
|
|
|
unsafeDestroyWorld : (1 x : %World) -> a -> a
|
|
unsafeDestroyWorld %MkWorld x = x
|
|
|
|
export
|
|
unsafePerformIO : IO a -> a
|
|
unsafePerformIO (MkIO f)
|
|
= unsafeCreateWorld (\w => case f w of
|
|
MkIORes res w' => unsafeDestroyWorld w' res)
|