0 | module PrimIO
  1 |
  2 | import Builtin
  3 |
  4 | %default total
  5 |
  6 | public export
  7 | data IORes : Type -> Type where
  8 |      MkIORes : (result : a) -> (1 x : %World) -> IORes a
  9 |
 10 | ||| Idris's primitive IO, for building abstractions on top of.
 11 | public export
 12 | PrimIO : Type -> Type
 13 | PrimIO a = (1 x : %World) -> IORes a
 14 |
 15 | ||| The internal representation of I/O computations.
 16 | export
 17 | data IO : Type -> Type where
 18 |      MkIO : (1 fn : PrimIO a) -> IO a
 19 |
 20 | export
 21 | prim__io_pure : a -> PrimIO a
 22 | prim__io_pure = MkIORes
 23 |
 24 | %inline
 25 | export
 26 | io_pure : a -> IO a
 27 | io_pure x = MkIO (MkIORes x)
 28 |
 29 | export
 30 | prim__io_bind : (1 act : PrimIO a) -> (1 k : a -> PrimIO b) -> PrimIO b
 31 | prim__io_bind fn k w
 32 |     = let MkIORes x' w' = fn w in k x' w'
 33 |
 34 | -- There's a special case for inlining this is Compiler.Inline, because
 35 | -- the inliner is cautious about case blocks at the moment. Once it's less
 36 | -- cautious, add an explicit %inline directive and take out the special case.
 37 | -- See also dealing with the newtype optimisation via %World in
 38 | -- Compiler.CompileExpr
 39 | export
 40 | io_bind : (1 act : IO a) -> (1 k : a -> IO b) -> IO b
 41 | io_bind (MkIO fn) k
 42 |     = MkIO (\w => let MkIORes x' w' = fn w
 43 |                       MkIO res = k x' in
 44 |                       res w')
 45 |
 46 | -- A pointer representing a given parameter type
 47 | -- The parameter is a phantom type, to help differentiate between
 48 | -- different pointer types
 49 | public export
 50 | data Ptr : Type -> Type where [external]
 51 |
 52 | -- A pointer to any type (representing a void* in foreign calls)
 53 | public export
 54 | data AnyPtr : Type where [external]
 55 |
 56 | -- As Ptr, but associated with a finaliser that is run on garbage collection
 57 | public export
 58 | data GCPtr : Type -> Type where [external]
 59 |
 60 | -- As AnyPtr, but associated with a finaliser that is run on garbage collection
 61 | public export
 62 | data GCAnyPtr : Type where [external]
 63 |
 64 | public export
 65 | data ThreadID : Type where [external]
 66 |
 67 | export %inline
 68 | fromPrim : (1 fn : (1 x : %World) -> IORes a) -> IO a
 69 | fromPrim op = MkIO op
 70 |
 71 | export %inline
 72 | toPrim : (1 act : IO a) -> PrimIO a
 73 | toPrim (MkIO fn) = fn
 74 |
 75 | %foreign "C:idris2_isNull, libidris2_support, idris_support.h"
 76 |          "javascript:lambda:x=>x===undefined||x===null?1:0"
 77 | export
 78 | prim__nullAnyPtr : AnyPtr -> Int
 79 |
 80 | %foreign "C:idris2_getNull, libidris2_support, idris_support.h"
 81 | export
 82 | prim__getNullAnyPtr : AnyPtr
 83 |
 84 | export
 85 | prim__castPtr : AnyPtr -> Ptr t
 86 | prim__castPtr = believe_me
 87 |
 88 | export
 89 | prim__forgetPtr : Ptr t -> AnyPtr
 90 | prim__forgetPtr = believe_me
 91 |
 92 | export %inline
 93 | prim__nullPtr : Ptr t -> Int -- can't pass 'type' to a foreign function
 94 | prim__nullPtr p = prim__nullAnyPtr (prim__forgetPtr p)
 95 |
 96 | unsafeCreateWorld : (1 f : (1 x : %World) -> a) -> a
 97 | unsafeCreateWorld f = f %MkWorld
 98 |
 99 | unsafeDestroyWorld : (1 x : %World) -> a -> a
100 | unsafeDestroyWorld %MkWorld x = x
101 |
102 | export
103 | unsafePerformIO : IO a -> a
104 | unsafePerformIO (MkIO f)
105 |     = unsafeCreateWorld (\w => case f w of
106 |                                MkIORes res w' => unsafeDestroyWorld w' res)
107 |