git.iko.soy/Idris-dev
on ff0fbfa help sign in
Idris-dev/lib/IO.idr
51 lines 1.2 kB history raw
1import Prelude.List
3%access public
5abstract data IO a = prim__IO a
7abstract
8io_bind : IO a -> (a -> IO b) -> IO b
9io_bind (prim__IO v) k = k v
11unsafePerformIO : IO a -> a
12-- compiled as primitive
14abstract
15io_return : a -> IO a
16io_return x = prim__IO x
18-- This may seem pointless, but we can use it to force an
19-- evaluation of main that Epic wouldn't otherwise do...
21run__IO : IO () -> IO ()
22run__IO v = io_bind v (\v' => io_return v')
24data FTy = FInt | FFloat | FChar | FString | FPtr | FAny Type | FUnit
26interpFTy : FTy -> Type
27interpFTy FInt = Int
28interpFTy FFloat = Float
29interpFTy FChar = Char
30interpFTy FString = String
31interpFTy FPtr = Ptr
32interpFTy (FAny t) = t
33interpFTy FUnit = ()
35ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
36ForeignTy Nil rt = IO (interpFTy rt)
37ForeignTy (t::ts) rt = interpFTy t -> ForeignTy ts rt
40data Foreign : Type -> Type where
41 FFun : String -> (xs:List FTy) -> (t:FTy) ->
42 Foreign (ForeignTy xs t)
44mkForeign : Foreign x -> x
45mkLazyForeign : Foreign x -> x
46-- mkForeign and mkLazyForeign compiled as primitives
48fork : |(thread:IO ()) -> IO Ptr
49fork x = io_return prim__vm -- compiled specially