@@ -80,24 +80,40 @@ For C, this is:
8080.. code-block:: idris
8181
8282 ||| Supported C integer types
83+ public export
8384 data C_IntTypes : Type -> Type where
84− C_IntChar : C_IntTypes Char
85− C_IntNative : C_IntTypes Int
86− ... -- more integer types
85+ C_IntChar : C_IntTypes Char
86+ C_IntNative : C_IntTypes Int
87+ C_IntBits8 : C_IntTypes Bits8
88+ C_IntBits16 : C_IntTypes Bits16
89+ C_IntBits32 : C_IntTypes Bits32
90+ C_IntBits64 : C_IntTypes Bits64
91+
92+ ||| Supported C function types
93+ public export
94+ data C_FnTypes : Type -> Type where
95+ C_Fn : C_Types s -> C_FnTypes t -> C_FnTypes (s -> t)
96+ C_FnIO : C_Types t -> C_FnTypes (IO' FFI_C t)
97+ C_FnBase : C_Types t -> C_FnTypes t
8798
8899 ||| Supported C foreign types
100+ public export
89101 data C_Types : Type -> Type where
90− C_Str : C_Types String
91− C_Float : C_Types Float
92− C_Ptr : C_Types Ptr
93− C_MPtr : C_Types ManagedPtr
94− C_Unit : C_Types ()
95− C_Any : C_Types (Raw a)
96− C_IntT : C_IntTypes i -> C_Types i
97−
102+ C_Str : C_Types String
103+ C_Float : C_Types Double
104+ C_Ptr : C_Types Ptr
105+ C_MPtr : C_Types ManagedPtr
106+ C_Unit : C_Types ()
107+ C_Any : C_Types (Raw a)
108+ C_FnT : C_FnTypes t -> C_Types (CFnPtr t)
109+ C_IntT : C_IntTypes i -> C_Types i
110+
111+ ||| A descriptor for the C FFI. See the constructors of `C_Types`
112+ ||| and `C_IntTypes` for the concrete types that are available.
113+ %error_reverse
114+ public export
98115 FFI_C : FFI
99− FFI_C = MkFFI C_Types
100− String -- the name of the C function
116+ FFI_C = MkFFI C_Types String String
101117
102118Foreign calls
103119=============
@@ -135,6 +151,71 @@ example a shorthand for calling external JavaScript functions:
135151 {auto fty : FTy FFI_JS [] ty} -> ty
136152 jscall fname ty = foreign FFI_JS fname ty
137153
154+C callbacks
155+-----------
156+It is possible to pass an Idris function to a C function taking a function
157+pointer by using ``CFnPtr`` in the function type. The Idris function is passed
158+to ``MkCFnPtr`` in the arguments. The example below shows declaring the C standard
159+library function ``qsort`` which takes a pointer to a comparison function.
160+
161+.. code-block:: idris
162+
163+ myComparer : Ptr -> Ptr -> Int
164+ myComparer = ...
165+
166+ qsort : Ptr -> Int -> Int -> IO ()
167+ test2 data elems elsize = foreign FFI_C "qsort"
168+ (Ptr -> Int -> Int -> CFnPtr (Ptr -> Ptr -> Int) -> IO ())
169+ data elems elsize (MkCFnPtr myComparer)
170+
171+There are a few limitations to callbacks in the C FFI. The foreign function can't
172+take the function to make a callback of as an argument. This will give a
173+compilation error:
174+
175+.. code-block:: idris
176+
177+ -- This does not work
178+ example : (Int -> ()) -> IO ()
179+ example f = foreign FFI_C "callbacker" (CFnPtr (Int -> ()) -> IO ()) f
180+
181+The other big limitation is that it doesn't support IO functions. Use
182+``unsafePerformIO`` to wrap them.
183+
184+There are two special function names:
185+``%wrapper`` returns the function pointer that wraps an Idris function. This
186+is useful if the function pointer isn't taken by a C function directly but
187+should be inserted into a data structure. A foreign declaration using
188+``%wrapper`` must return ``IO Ptr``.
189+
190+.. code-block:: idris
191+
192+ -- this returns the C function pointer to a qsort comparer
193+ example_wrapper : IO Ptr
194+ example_wrapper = foreign FFI_C "%wrapper" (CFnPtr (Ptr -> Ptr -> Int) -> IO Ptr)
195+ (MkCFnPtr myComparer)
196+
197+``%dynamic`` calls a C function pointer with some arguments. This is useful if
198+a C function returns or data structure contains a C function pointer, for example
199+structs of function pointers are common in object-oriented C such as in COM or the
200+Linux kernel. The function type contains an extra ``Ptr`` at the start for the
201+function pointer. ``%dynamic`` can be seen as a pseudo-function that calls the
202+function in the first argument, passing the remaining arguments to it.
203+
204+.. code-block:: idris
205+
206+ -- we have a pointer to a function with the signature int f(int), call it
207+ example_dynamic : Ptr -> Int -> IO Int
208+ example_dynamic fn x = foreign FFI_C "%dynamic" (Ptr -> Int -> IO Int) fn x
209+
210+If the foreign name is prefixed by a ``&``, it is treated as a pointer to the
211+global variable with the following name. The type must be just ``IO Ptr``.
212+
213+.. code-block:: idris
214+
215+ -- access the global variable errno
216+ errno : IO Ptr
217+ errno = foreign FFI_C "&errno" (IO Ptr)
218+
138219FFI implementation
139220------------------
140221