git.iko.soy/Idris-dev
on aa42f71 help sign in
Idris-dev/lib/IO.idr
95 lines 2.1 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 = ITChar | ITNative | IT8 | IT16 | IT32 | IT64 | IT8x16 | IT16x8 | IT32x4 | IT64x2
25data FTy = FIntT IntTy
26 | FFunction FTy FTy
27 | FFloat
28 | FString
29 | FPtr
30 | FAny Type
31 | FUnit
33FInt : FTy
34FInt = FIntT ITNative
36FChar : FTy
37FChar = FIntT ITChar
39FByte : FTy
40FByte = FIntT IT8
42FShort : FTy
43FShort = FIntT IT16
45FLong : FTy
46FLong = FIntT IT64
48FBits8x16 : FTy
49FBits8x16 = FIntT IT8x16
51FBits16x8 : FTy
52FBits16x8 = FIntT IT16x8
54FBits32x4 : FTy
55FBits32x4 = FIntT IT32x4
57FBits64x2 : FTy
58FBits64x2 = FIntT IT64x2
60interpFTy : FTy -> Type
61interpFTy (FIntT ITNative) = Int
62interpFTy (FIntT ITChar) = Char
63interpFTy (FIntT IT8) = Bits8
64interpFTy (FIntT IT16) = Bits16
65interpFTy (FIntT IT32) = Bits32
66interpFTy (FIntT IT64) = Bits64
67interpFTy (FAny t) = t
68interpFTy FFloat = Float
69interpFTy FString = String
70interpFTy FPtr = Ptr
71interpFTy (FIntT IT8x16) = Bits8x16
72interpFTy (FIntT IT16x8) = Bits16x8
73interpFTy (FIntT IT32x4) = Bits32x4
74interpFTy (FIntT IT64x2) = Bits64x2
75interpFTy FUnit = ()
77interpFTy (FFunction a b) = interpFTy a -> interpFTy b
79ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
80ForeignTy Nil rt = IO (interpFTy rt)
81ForeignTy (t::ts) rt = interpFTy t -> ForeignTy ts rt
84data Foreign : Type -> Type where
85 FFun : String -> (xs:List FTy) -> (t:FTy) ->
86 Foreign (ForeignTy xs t)
88mkForeign : Foreign x -> x
89mkLazyForeign : Foreign x -> x
90-- mkForeign and mkLazyForeign compiled as primitives
92fork : |(thread:IO ()) -> IO Ptr
93fork x = io_return prim__vm -- compiled specially