git.iko.soy/Idris-dev
on master help sign in
Document the FFI with docstrings
67143bdDavid Raymond Christiansen
libs/prelude/IO.idr+33−6
compare with master
unifiedsplit
@@ -6,7 +6,7 @@ import Prelude.List
6%access public
6%access public
7
7
8||| Idris's primitive IO, for building abstractions on top of
8||| Idris's primitive IO, for building abstractions on top of
9−abstract
9+abstract
10data PrimIO : Type -> Type where
10data PrimIO : Type -> Type where
11 prim__IO : a -> PrimIO a
11 prim__IO : a -> PrimIO a
12
12
@@ -20,13 +20,22 @@ world (TheWorld w) = w
20abstract WorldRes : Type -> Type
20abstract WorldRes : Type -> Type
21WorldRes x = x
21WorldRes x = x
22
22
23+||| An FFI specifier, which describes how a particular compiler
24+||| backend handles foreign function calls.
23record FFI where
25record FFI where
24 constructor MkFFI
26 constructor MkFFI
27+ ||| A family describing which types are available in the FFI
25 ffi_types : Type -> Type
28 ffi_types : Type -> Type
29+
30+ ||| The type used to specify the names of foreign functions in this FFI
26 ffi_fn : Type
31 ffi_fn : Type
32+
33+ ||| How this FFI describes exported datatypes
27 ffi_data : Type
34 ffi_data : Type
28
35
36+||| The IO type, parameterised over the FFI that is available within
37+||| it.
29−abstract
38+abstract
30data IO' : (lang : FFI) -> Type -> Type where
39data IO' : (lang : FFI) -> Type -> Type where
31 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a
40 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a
32
41
@@ -64,6 +73,19 @@ foreign_prim f fname (FRet y) env
64foreign_prim f fname (FFun arg sc) env
73foreign_prim f fname (FFun arg sc) env
65 = \x => foreign_prim f fname sc ((arg, x) :: env)
74 = \x => foreign_prim f fname sc ((arg, x) :: env)
66
75
76+||| Call a foreign function.
77+|||
78+||| The particular semantics of foreign function calls depend on the
79+||| Idris compiler backend in use. For the default C backend, see the
80+||| documentation for `FFI_C`.
81+|||
82+||| For more details, please consult [the Idris documentation](http://docs.idris-lang.org/en/latest/reference/ffi.html).
83+|||
84+||| @ f an FFI descriptor, which is specific to the compiler backend.
85+||| @ fname the name of the foreign function
86+||| @ ty the Idris type for the foreign function
87+||| @ fty an automatically-found proof that the Idris type works with
88+||| the FFI in question
67%inline
89%inline
68foreign : (f : FFI) -> (fname : ffi_fn f) -> (ty : Type) ->
90foreign : (f : FFI) -> (fname : ffi_fn f) -> (ty : Type) ->
69 {auto fty : FTy f [] ty} -> ty
91 {auto fty : FTy f [] ty} -> ty
@@ -128,7 +150,7 @@ namespace FFI_C
128 -- Tell erasure analysis not to erase the argument
150 -- Tell erasure analysis not to erase the argument
129 %used MkRaw x
151 %used MkRaw x
130
152
131− -- Supported C integer types
153+ ||| Supported C integer types
132 data C_IntTypes : Type -> Type where
154 data C_IntTypes : Type -> Type where
133 C_IntChar : C_IntTypes Char
155 C_IntChar : C_IntTypes Char
134 C_IntNative : C_IntTypes Int
156 C_IntNative : C_IntTypes Int
@@ -137,7 +159,7 @@ namespace FFI_C
137 C_IntBits32 : C_IntTypes Bits32
159 C_IntBits32 : C_IntTypes Bits32
138 C_IntBits64 : C_IntTypes Bits64
160 C_IntBits64 : C_IntTypes Bits64
139
161
140− -- Supported C foreign types
162+ ||| Supported C foreign types
141 data C_Types : Type -> Type where
163 data C_Types : Type -> Type where
142 C_Str : C_Types String
164 C_Str : C_Types String
143 C_Float : C_Types Float
165 C_Float : C_Types Float
@@ -147,6 +169,8 @@ namespace FFI_C
147 C_Any : C_Types (Raw a)
169 C_Any : C_Types (Raw a)
148 C_IntT : C_IntTypes i -> C_Types i
170 C_IntT : C_IntTypes i -> C_Types i
149
171
172+ ||| A descriptor for the C FFI. See the constructors of `C_Types`
173+ ||| and `C_IntTypes` for the concrete types that are available.
150 FFI_C : FFI
174 FFI_C : FFI
151 FFI_C = MkFFI C_Types String String
175 FFI_C = MkFFI C_Types String String
152
176
@@ -201,14 +225,17 @@ mutual
201-- pass we only have 'JsFn' and not the constructor.
225-- pass we only have 'JsFn' and not the constructor.
202%used MkJsFn x
226%used MkJsFn x
203
227
228+||| The JavaScript FFI. The strings naming functions in this API are
229+||| JavaScript code snippets, into which the arguments are substituted
230+||| for the placeholders `%0`, `%1`, etc.
204−FFI_JS : FFI
231+FFI_JS : FFI
205FFI_JS = MkFFI JS_Types String String
232FFI_JS = MkFFI JS_Types String String
206
233
207JS_IO : Type -> Type
234JS_IO : Type -> Type
208JS_IO = IO' FFI_JS
235JS_IO = IO' FFI_JS
209
236
210
237
211−--------- Foreign Exports
238+--------- Foreign Exports
212
239
213namespace FFI_Export
240namespace FFI_Export
214-- It's just like Data.List.Elem, but we don't need all the other stuff
241-- It's just like Data.List.Elem, but we don't need all the other stuff