@@ -6,7 +6,7 @@ import Prelude.List
66%access public
77
88||| Idris's primitive IO, for building abstractions on top of
9−abstract
9+abstract
1010data PrimIO : Type -> Type where
1111 prim__IO : a -> PrimIO a
1212
@@ -20,13 +20,22 @@ world (TheWorld w) = w
2020abstract WorldRes : Type -> Type
2121WorldRes x = x
2222
23+||| An FFI specifier, which describes how a particular compiler
24+||| backend handles foreign function calls.
2325record FFI where
2426 constructor MkFFI
27+ ||| A family describing which types are available in the FFI
2528 ffi_types : Type -> Type
29+
30+ ||| The type used to specify the names of foreign functions in this FFI
2631 ffi_fn : Type
32+
33+ ||| How this FFI describes exported datatypes
2734 ffi_data : Type
2835
29−abstract
36+||| The IO type, parameterised over the FFI that is available within
37+||| it.
38+abstract
3039data IO' : (lang : FFI) -> Type -> Type where
3140 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a
3241
@@ -64,6 +73,19 @@ foreign_prim f fname (FRet y) env
6473foreign_prim f fname (FFun arg sc) env
6574 = \x => foreign_prim f fname sc ((arg, x) :: env)
6675
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
6789%inline
6890foreign : (f : FFI) -> (fname : ffi_fn f) -> (ty : Type) ->
6991 {auto fty : FTy f [] ty} -> ty
@@ -128,7 +150,7 @@ namespace FFI_C
128150 -- Tell erasure analysis not to erase the argument
129151 %used MkRaw x
130152
131− -- Supported C integer types
153+ ||| Supported C integer types
132154 data C_IntTypes : Type -> Type where
133155 C_IntChar : C_IntTypes Char
134156 C_IntNative : C_IntTypes Int
@@ -137,7 +159,7 @@ namespace FFI_C
137159 C_IntBits32 : C_IntTypes Bits32
138160 C_IntBits64 : C_IntTypes Bits64
139161
140− -- Supported C foreign types
162+ ||| Supported C foreign types
141163 data C_Types : Type -> Type where
142164 C_Str : C_Types String
143165 C_Float : C_Types Float
@@ -147,6 +169,8 @@ namespace FFI_C
147169 C_Any : C_Types (Raw a)
148170 C_IntT : C_IntTypes i -> C_Types i
149171
172+ ||| A descriptor for the C FFI. See the constructors of `C_Types`
173+ ||| and `C_IntTypes` for the concrete types that are available.
150174 FFI_C : FFI
151175 FFI_C = MkFFI C_Types String String
152176
@@ -201,14 +225,17 @@ mutual
201225-- pass we only have 'JsFn' and not the constructor.
202226%used MkJsFn x
203227
204−FFI_JS : FFI
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.
231+FFI_JS : FFI
205232FFI_JS = MkFFI JS_Types String String
206233
207234JS_IO : Type -> Type
208235JS_IO = IO' FFI_JS
209236
210237
211−--------- Foreign Exports
238+--------- Foreign Exports
212239
213240namespace FFI_Export
214241-- It's just like Data.List.Elem, but we don't need all the other stuff