-
Notifications
You must be signed in to change notification settings - Fork 644
/
IO.idr
376 lines (297 loc) · 11.9 KB
/
IO.idr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
%unqualified
import Builtins
import Prelude.List
%access export
||| Idris's primitive IO, for building abstractions on top of
data PrimIO : Type -> Type where
Prim__IO : a -> PrimIO a
||| A token representing the world, for use in `IO`
data World = TheWorld prim__WorldType
world : World -> prim__WorldType
world (TheWorld w) = w
WorldRes : Type -> Type
WorldRes x = x
||| An FFI specifier, which describes how a particular compiler
||| backend handles foreign function calls.
public export
record FFI where
constructor MkFFI
||| A family describing which types are available in the FFI
ffi_types : Type -> Type
||| The type used to specify the names of foreign functions in this FFI
ffi_fn : Type
||| How this FFI describes exported datatypes
ffi_data : Type
||| The IO type, parameterised over the FFI that is available within
||| it.
data IO' : (lang : FFI) -> Type -> Type where
MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a
public export
data FTy : FFI -> List Type -> Type -> Type where
FRet : ffi_types f t -> FTy f xs (IO' f t)
FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)
namespace ForeignEnv
data FEnv : FFI -> List Type -> Type where
Nil : FEnv f []
(::) : (ffi_types f t, t) -> FEnv f xs -> FEnv f (t :: xs)
ForeignPrimType : (xs : List Type) -> FEnv ffi xs -> Type -> Type
ForeignPrimType {ffi} [] [] t = World -> ffi_fn ffi -> ffi_types ffi t -> PrimIO t
ForeignPrimType {ffi} (x :: xs) ((a, _) :: env) t
= (ffi_types ffi x, x) -> ForeignPrimType xs env t
%inline
private
applyEnv : (env : FEnv ffi xs) ->
ForeignPrimType xs env t ->
World -> ffi_fn ffi -> ffi_types ffi t -> PrimIO t
applyEnv [] f = f
applyEnv (x@(_, _) :: xs) f = applyEnv xs (f x)
mkForeignPrim : {xs : _} -> {ffi : _} -> {env : FEnv ffi xs} -> {t : Type} ->
ForeignPrimType xs env t
-- compiled as primitive. Compiler assumes argument order, so make it
-- explicit here.
%inline
private
foreign_prim : (f : FFI) ->
(fname : ffi_fn f) -> FTy f xs ty -> FEnv f xs -> ty
foreign_prim f fname (FRet y) env
= MkIO (\w => applyEnv env mkForeignPrim w fname y)
foreign_prim f fname (FFun arg sc) env
= \x => foreign_prim f fname sc ((arg, x) :: env)
||| Call a foreign function.
|||
||| The particular semantics of foreign function calls depend on the
||| Idris compiler backend in use. For the default C backend, see the
||| documentation for `FFI_C`.
|||
||| For more details, please consult [the Idris documentation](http://docs.idris-lang.org/en/latest/reference/ffi.html).
|||
||| @ f an FFI descriptor, which is specific to the compiler backend.
||| @ fname the name of the foreign function
||| @ ty the Idris type for the foreign function
||| @ fty an automatically-found proof that the Idris type works with
||| the FFI in question
%inline
foreign : (f : FFI) -> (fname : ffi_fn f) -> (ty : Type) ->
{auto fty : FTy f [] ty} -> ty
foreign ffi fname ty {fty} = foreign_prim ffi fname fty []
prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b
prim_io_bind (Prim__IO v) k = k v
unsafePerformPrimIO : PrimIO a -> a
-- compiled as primitive
prim_io_pure : a -> PrimIO a
prim_io_pure x = Prim__IO x
-- Don't %inline; the compiler treats it specially
io_bind : IO' l a -> (a -> IO' l b) -> IO' l b
io_bind (MkIO fn)
= \k => MkIO (\w => prim_io_bind (fn w)
(\ b => case k b of
MkIO fkb => fkb w))
io_pure : a -> IO' l a
io_pure x = MkIO (\w => prim_io_pure x)
liftPrimIO : (World -> PrimIO a) -> IO' l a
liftPrimIO = MkIO
call__IO : IO' ffi a -> PrimIO a
call__IO (MkIO f) = f (TheWorld prim__TheWorld)
-- Concrete type makes it easier to elaborate at top level
run__IO : IO' ffi () -> PrimIO ()
run__IO f = call__IO f
unsafePerformIO : IO' ffi a -> a
unsafePerformIO (MkIO f) = unsafePerformPrimIO
(prim_io_bind (f (TheWorld prim__TheWorld)) (\ b => prim_io_pure b))
prim_read : IO' l String
prim_read = MkIO (\w => prim_io_pure (prim__readString (world w)))
prim_write : String -> IO' l Int
prim_write s
= MkIO (\w => prim_io_pure (prim__writeString (world w) s))
prim_fread : Ptr -> IO' l String
prim_fread h = MkIO (\w => prim_io_pure (prim__readFile (world w) h))
prim_freadChars : Int -> Ptr -> IO' l String
prim_freadChars len h
= MkIO (\w => prim_io_pure (prim__readChars (world w) len h))
prim_fwrite : Ptr -> String -> IO' l Int
prim_fwrite h s
= MkIO (\w => prim_io_pure (prim__writeFile (world w) h s))
--------- The C FFI
namespace FFI_C
public export
data Raw : Type -> Type where
-- code generated can assume it's compiled just as 't'
MkRaw : (x : t) -> Raw t
public export
data CFnPtr : Type -> Type where
MkCFnPtr : (x : t) -> CFnPtr t
mutual
||| Supported C integer types
public export
data C_IntTypes : Type -> Type where
C_IntChar : C_IntTypes Char
C_IntNative : C_IntTypes Int
C_IntBits8 : C_IntTypes Bits8
C_IntBits16 : C_IntTypes Bits16
C_IntBits32 : C_IntTypes Bits32
C_IntBits64 : C_IntTypes Bits64
public export
data C_FnTypes : Type -> Type where
C_Fn : C_Types s -> C_FnTypes t -> C_FnTypes (s -> t)
C_FnIO : C_Types t -> C_FnTypes (IO' FFI_C t)
C_FnBase : C_Types t -> C_FnTypes t
||| Supported C foreign types
public export
data C_Types : Type -> Type where
C_Str : C_Types String
C_Float : C_Types Double
C_Ptr : C_Types Ptr
C_MPtr : C_Types ManagedPtr
C_Unit : C_Types ()
C_Any : C_Types (Raw a)
C_FnT : C_FnTypes t -> C_Types (CFnPtr t)
C_IntT : C_IntTypes i -> C_Types i
C_CData : C_Types CData
||| A descriptor for the C FFI. See the constructors of `C_Types`
||| and `C_IntTypes` for the concrete types that are available.
%error_reverse
public export
FFI_C : FFI
FFI_C = MkFFI C_Types String String
||| Interactive programs, describing I/O actions and returning a value.
||| @res The result type of the program
%error_reverse
public export
IO : (res : Type) -> Type
IO = IO' FFI_C
-- Tell erasure analysis not to erase the argument
%used MkRaw x
%used MkCFnPtr x
-- Cannot be relaxed as is used by type providers and they expect IO a
-- in the first argument.
run__provider : IO a -> PrimIO a
run__provider (MkIO f) = f (TheWorld prim__TheWorld)
prim_fork : PrimIO () -> PrimIO Ptr
prim_fork x = prim_io_pure (prim__vm prim__TheWorld) -- compiled specially
namespace IO
fork : IO' l () -> IO' l Ptr
fork (MkIO f) = MkIO (\w => prim_io_bind
(prim_fork (prim_io_bind (f w)
(\ x => prim_io_pure x)))
(\x => prim_io_pure x))
getMyVM : IO' l Ptr
getMyVM = MkIO (\w => prim_io_pure (prim__vm (world w)))
forceGC : IO ()
forceGC = io_bind getMyVM
(\vm => foreign FFI_C "idris_forceGC" (Ptr -> IO ()) vm)
getErrno : IO Int
getErrno = foreign FFI_C "idris_errno" (IO Int)
--------- The Javascript/Node FFI
-- Supported JS foreign types
mutual
public export
data JsFn : Type -> Type where
MkJsFn : (x : t) -> JsFn t
public export
data JS_IntTypes : Type -> Type where
JS_IntChar : JS_IntTypes Char
JS_IntNative : JS_IntTypes Int
public export
data JS_FnTypes : Type -> Type where
JS_Fn : JS_Types s -> JS_FnTypes t -> JS_FnTypes (s -> t)
JS_FnIO : JS_Types t -> JS_FnTypes (IO' l t)
JS_FnBase : JS_Types t -> JS_FnTypes t
public export
data JS_Types : Type -> Type where
JS_Str : JS_Types String
JS_Float : JS_Types Double
JS_Ptr : JS_Types Ptr
JS_Unit : JS_Types ()
JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
JS_IntT : JS_IntTypes i -> JS_Types i
-- Tell erasure analysis not to erase the argument. Needs to be outside the
-- mutual block, since directives are done on the first pass and in the first
-- pass we only have 'JsFn' and not the constructor.
%used MkJsFn x
||| The JavaScript FFI. The strings naming functions in this API are
||| JavaScript code snippets, into which the arguments are substituted
||| for the placeholders `%0`, `%1`, etc.
%error_reverse
public export
FFI_JS : FFI
FFI_JS = MkFFI JS_Types String String
%error_reverse
public export
JS_IO : Type -> Type
JS_IO = IO' FFI_JS
--------- Foreign Exports
namespace FFI_Export
-- It's just like Data.List.Elem, but we don't need all the other stuff
-- that comes with it, just a proof that a data type is defined.
public export
data DataDefined : Type -> List (Type, s) -> s -> Type where
DHere : DataDefined x ((x, t) :: xs) t
DThere : DataDefined x xs t -> DataDefined x (y :: xs) t
public export
data FFI_Base : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where
FFI_ExpType : {n : ffi_data f} -> (def : DataDefined t xs n) -> FFI_Base f xs t
FFI_Prim : (prim : ffi_types f t) -> FFI_Base f xs t
%used FFI_ExpType n
%used FFI_ExpType def
%used FFI_Prim prim
public export
data FFI_Exportable : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where
FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO' f t)
FFI_Fun : (b : FFI_Base f xs s) -> (a : FFI_Exportable f xs t) -> FFI_Exportable f xs (s -> t)
FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t
%used FFI_IO b
%used FFI_Fun b
%used FFI_Fun a
%used FFI_Ret b
public export
data FFI_Export : (f : FFI) -> String -> List (Type, ffi_data f) -> Type where
Data : (x : Type) -> (n : ffi_data f) ->
(es : FFI_Export f h ((x, n) :: xs)) -> FFI_Export f h xs
Fun : (fn : t) -> (n : ffi_fn f) -> {auto prf : FFI_Exportable f xs t} ->
(es : FFI_Export f h xs) -> FFI_Export f h xs
End : FFI_Export f h xs
%used Data x
%used Data n
%used Data es
%used Fun fn
%used Fun n
%used Fun es
%used Fun prf
-- Accessing memory
prim_peek8 : Ptr -> Int -> IO Bits8
prim_peek8 ptr offset = MkIO (\w => prim_io_pure (prim__peek8 (world w) ptr offset))
prim_poke8 : Ptr -> Int -> Bits8 -> IO Int
prim_poke8 ptr offset val = MkIO (\w => prim_io_pure (
prim__poke8 (world w) ptr offset val))
prim_peek16 : Ptr -> Int -> IO Bits16
prim_peek16 ptr offset = MkIO (\w => prim_io_pure (prim__peek16 (world w) ptr offset))
prim_poke16 : Ptr -> Int -> Bits16 -> IO Int
prim_poke16 ptr offset val = MkIO (\w => prim_io_pure (
prim__poke16 (world w) ptr offset val))
prim_peek32 : Ptr -> Int -> IO Bits32
prim_peek32 ptr offset = MkIO (\w => prim_io_pure (prim__peek32 (world w) ptr offset))
prim_poke32 : Ptr -> Int -> Bits32 -> IO Int
prim_poke32 ptr offset val = MkIO (\w => prim_io_pure (
prim__poke32 (world w) ptr offset val))
prim_peek64 : Ptr -> Int -> IO Bits64
prim_peek64 ptr offset = MkIO (\w => prim_io_pure (prim__peek64 (world w) ptr offset))
prim_poke64 : Ptr -> Int -> Bits64 -> IO Int
prim_poke64 ptr offset val = MkIO (\w => prim_io_pure (
prim__poke64 (world w) ptr offset val))
prim_peekPtr : Ptr -> Int -> IO Ptr
prim_peekPtr ptr offset = MkIO (\w => prim_io_pure (prim__peekPtr (world w) ptr offset))
prim_pokePtr : Ptr -> Int -> Ptr -> IO Int
prim_pokePtr ptr offset val = MkIO (\w => prim_io_pure (
prim__pokePtr (world w) ptr offset val))
prim_peekDouble : Ptr -> Int -> IO Double
prim_peekDouble ptr offset = MkIO (\w => prim_io_pure (prim__peekDouble (world w) ptr offset))
prim_pokeDouble : Ptr -> Int -> Double -> IO Int
prim_pokeDouble ptr offset val = MkIO (\w => prim_io_pure (
prim__pokeDouble (world w) ptr offset val))
||| Single precision floats are marshalled to Doubles
prim_peekSingle : Ptr -> Int -> IO Double
prim_peekSingle ptr offset = MkIO (\w => prim_io_pure (prim__peekSingle (world w) ptr offset))
||| Single precision floats are marshalled to Doubles
prim_pokeSingle : Ptr -> Int -> Double -> IO Int
prim_pokeSingle ptr offset val = MkIO (\w => prim_io_pure (
prim__pokeSingle (world w) ptr offset val))