Idris2/libs/prelude/PrimIO.idr

107 lines
2.8 KiB
Idris
Raw Normal View History

2020-05-18 15:59:07 +03:00
module PrimIO
import Builtin
%default total
2020-05-18 15:59:07 +03:00
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
2021-06-16 17:22:30 +03:00
prim__io_pure = MkIORes
2020-05-18 15:59:07 +03:00
%inline
export
io_pure : a -> IO a
2021-06-16 17:22:30 +03:00
io_pure x = MkIO (MkIORes x)
2020-05-18 15:59:07 +03:00
export
prim__io_bind : (1 act : PrimIO a) -> (1 k : a -> PrimIO b) -> PrimIO b
prim__io_bind fn k w
2020-05-18 15:59:07 +03:00
= 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')
-- 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]
-- As Ptr, but associated with a finaliser that is run on garbage collection
public export
data GCPtr : Type -> Type where [external]
-- As AnyPtr, but associated with a finaliser that is run on garbage collection
public export
data GCAnyPtr : Type where [external]
2020-05-18 15:59:07 +03:00
public export
data ThreadID : Type where [external]
export %inline
fromPrim : (1 fn : (1 x : %World) -> IORes a) -> IO a
fromPrim op = MkIO op
2020-05-18 15:59:07 +03:00
export %inline
toPrim : (1 act : IO a) -> PrimIO a
toPrim (MkIO fn) = fn
2021-04-23 13:09:31 +03:00
%foreign "C:idris2_isNull, libidris2_support, idris_support.h"
2020-06-18 01:29:54 +03:00
"javascript:lambda:x=>x===undefined||x===null?1n:0n"
2020-05-18 15:59:07 +03:00
export
prim__nullAnyPtr : AnyPtr -> Int
2021-04-23 13:09:31 +03:00
%foreign "C:idris2_getNull, libidris2_support, idris_support.h"
export
prim__getNullAnyPtr : AnyPtr
export
prim__castPtr : AnyPtr -> Ptr t
prim__castPtr = believe_me
export
2020-05-18 15:59:07 +03:00
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)
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
2020-05-18 15:59:07 +03:00
unsafePerformIO (MkIO f)
= unsafeCreateWorld (\w => case f w of
MkIORes res w' => unsafeDestroyWorld w' res)