git.iko.soy/Idris-dev
on d79a445 help sign in
Idris-dev/lib/IO.idr
67 lines 1.5 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 IntTy = ITNative | IT8 | IT16 | IT32 | IT64
25data FTy = FIntT IntTy | FFloat | FString | FPtr | FAny Type | FUnit
27FInt : FTy
28FInt = FIntT ITNative
30FChar : FTy
31FChar = FIntT IT8
33FShort : FTy
34FShort = FIntT IT16
36FLong : FTy
37FLong = FIntT IT64
39interpFTy : FTy -> Type
40interpFTy (FIntT ITNative) = Int
41interpFTy (FIntT IT8) = Bits8
42interpFTy (FIntT IT16) = Bits16
43interpFTy (FIntT IT32) = Bits32
44interpFTy (FIntT IT64) = Bits64
45interpFTy FFloat = Float
46interpFTy FString = String
47interpFTy FPtr = Ptr
48interpFTy (FAny t) = t
49interpFTy FUnit = ()
51ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
52ForeignTy Nil rt = IO (interpFTy rt)
53ForeignTy (t::ts) rt = interpFTy t -> ForeignTy ts rt
56data Foreign : Type -> Type where
57 FFun : String -> (xs:List FTy) -> (t:FTy) ->
58 Foreign (ForeignTy xs t)
60mkForeign : Foreign x -> x
61mkLazyForeign : Foreign x -> x
62-- mkForeign and mkLazyForeign compiled as primitives
64fork : |(thread:IO ()) -> IO Ptr
65fork x = io_return prim__vm -- compiled specially