git.iko.soy/Idris-dev
on de0bcbd help sign in
Idris-dev/lib/IO.idr
149 lines 3.5 kB history raw
1import Prelude.List
3%access public
5abstract data PrimIO a = prim__IO a
7abstract data World = TheWorld
9abstract WorldRes : Type -> Type
10WorldRes x = x
12-- abstract data WorldRes a = MkWR a World
14abstract data IO a = MkIO (World -> PrimIO (WorldRes a))
16abstract
17prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b
18prim_io_bind (prim__IO v) k = k v
20unsafePerformPrimIO : PrimIO a -> a
21-- compiled as primitive
23abstract
24prim_io_return : a -> PrimIO a
25prim_io_return x = prim__IO x
27data IntTy = ITChar | ITNative | IT8 | IT16 | IT32 | IT64 | IT8x16 | IT16x8 | IT32x4 | IT64x2
28data FTy = FIntT IntTy
29 | FFunction FTy FTy
30 | FFloat
31 | FString
32 | FPtr
33 | FAny Type
34 | FUnit
36FInt : FTy
37FInt = FIntT ITNative
39FChar : FTy
40FChar = FIntT ITChar
42FByte : FTy
43FByte = FIntT IT8
45FShort : FTy
46FShort = FIntT IT16
48FLong : FTy
49FLong = FIntT IT64
51FBits8 : FTy
52FBits8 = FIntT IT8
54FBits16 : FTy
55FBits16 = FIntT IT16
57FBits32 : FTy
58FBits32 = FIntT IT32
60FBits64 : FTy
61FBits64 = FIntT IT64
63FBits8x16 : FTy
64FBits8x16 = FIntT IT8x16
66FBits16x8 : FTy
67FBits16x8 = FIntT IT16x8
69FBits32x4 : FTy
70FBits32x4 = FIntT IT32x4
72FBits64x2 : FTy
73FBits64x2 = FIntT IT64x2
75interpFTy : FTy -> Type
76interpFTy (FIntT ITNative) = Int
77interpFTy (FIntT ITChar) = Char
78interpFTy (FIntT IT8) = Bits8
79interpFTy (FIntT IT16) = Bits16
80interpFTy (FIntT IT32) = Bits32
81interpFTy (FIntT IT64) = Bits64
82interpFTy (FAny t) = t
83interpFTy FFloat = Float
84interpFTy FString = String
85interpFTy FPtr = Ptr
86interpFTy (FIntT IT8x16) = Bits8x16
87interpFTy (FIntT IT16x8) = Bits16x8
88interpFTy (FIntT IT32x4) = Bits32x4
89interpFTy (FIntT IT64x2) = Bits64x2
90interpFTy FUnit = ()
92interpFTy (FFunction a b) = interpFTy a -> interpFTy b
94ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
95ForeignTy Nil rt = World -> PrimIO (interpFTy rt)
96ForeignTy (t::ts) rt = interpFTy t -> ForeignTy ts rt
99data Foreign : Type -> Type where
100 FFun : String -> (xs:List FTy) -> (t:FTy) ->
101 Foreign (ForeignTy xs t)
103mkForeignPrim : Foreign x -> x
104mkLazyForeignPrim : Foreign x -> x
105-- mkForeign and mkLazyForeign compiled as primitives
107abstract
108io_bind : IO a -> (a -> IO b) -> IO b
109io_bind (MkIO fn) k
110 = MkIO (\w => prim_io_bind (fn w)
111 (\ b => case k b of
112 MkIO fkb => fkb w))
114abstract
115io_return : a -> IO a
116io_return x = MkIO (\w => prim_io_return x)
118liftPrimIO : (World -> PrimIO a) -> IO a
119liftPrimIO f = MkIO (\w => prim_io_bind (f w)
120 (\x => prim_io_return x))
122run__IO : IO () -> PrimIO ()
123run__IO (MkIO f) = prim_io_bind (f TheWorld)
124 (\ b => prim_io_return b)
126run__provider : IO a -> PrimIO a
127run__provider (MkIO f) = prim_io_bind (f TheWorld)
128 (\ b => prim_io_return b)
130-- io_bind v (\v' => io_return v')
132prim_fork : |(thread:PrimIO ()) -> PrimIO Ptr
133prim_fork x = prim_io_return prim__vm -- compiled specially
135fork : |(thread:IO ()) -> IO Ptr
136fork (MkIO f) = MkIO (\w => prim_io_bind
137 (prim_fork (prim_io_bind (f w)
138 (\ x => prim_io_return x)))
139 (\x => prim_io_return x))
141partial
142prim_fread : Ptr -> IO String
143prim_fread h = MkIO (\w => prim_io_return (prim__readString h))
145unsafePerformIO : IO a -> a
146unsafePerformIO (MkIO f) = unsafePerformPrimIO
147 (prim_io_bind (f TheWorld) (\ b => prim_io_return b))