git.iko.soy/Idris-dev
on 1280aea help sign in
Idris-dev/lib/IO.idr
75 lines 1.7 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
26 | FFunction FTy FTy
27 | FFloat
28 | FString
29 | FPtr
30 | FAny Type
31 | FUnit
33FInt : FTy
34FInt = FIntT ITNative
36FChar : FTy
37FChar = FIntT IT8
39FShort : FTy
40FShort = FIntT IT16
42FLong : FTy
43FLong = FIntT IT64
45interpFTy : FTy -> Type
46interpFTy (FIntT ITNative) = Int
47interpFTy (FIntT IT8) = Bits8
48interpFTy (FIntT IT16) = Bits16
49interpFTy (FIntT IT32) = Bits32
50interpFTy (FIntT IT64) = Bits64
51interpFTy (FAny t) = t
52interpFTy FFloat = Float
53interpFTy FString = String
54interpFTy FPtr = Ptr
55interpFTy FUnit = ()
57interpFTy (FFunction a b) = interpFTy a -> interpFTy b
59ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
60ForeignTy Nil rt = IO (interpFTy rt)
61ForeignTy (t::ts) rt = interpFTy t -> ForeignTy ts rt
64data Foreign : Type -> Type where
65 FFun : String -> (xs:List FTy) -> (t:FTy) ->
66 Foreign (ForeignTy xs t)
68mkForeign : Foreign x -> x
69mkLazyForeign : Foreign x -> x
70-- mkForeign and mkLazyForeign compiled as primitives
72fork : |(thread:IO ()) -> IO Ptr
73fork x = io_return prim__vm -- compiled specially