git.iko.soy/Idris-dev
on 08e9182 help sign in
Idris-dev/lib/IO.idr
53 lines 1.3 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 xs t = mkForeign' (reverse xs) (IO (interpFTy t)) where
37 mkForeign' : List FTy -> Type -> Type
38 mkForeign' Nil ty = ty
39 mkForeign' (s :: ss) ty = mkForeign' ss (interpFTy s -> ty)
42data Foreign : Type -> Type where
43 FFun : String -> (xs:List FTy) -> (t:FTy) ->
44 Foreign (ForeignTy xs t)
46mkForeign : Foreign x -> x
47mkLazyForeign : Foreign x -> x
48-- mkForeign and mkLazyForeign compiled as primitives
50fork : |(thread:IO ()) -> IO Ptr
51fork x = io_return prim__vm -- compiled specially