@@ -115,75 +115,19 @@ So now we can get the size of ``size_t`` as long as we're in C code.
115115We'd like to be able to use this from Idris. Can we do this? It turns
116116out we can.
117117
118−``mkForeign``
118+``foreign``
119119-------------
120120
121−With mkForeign, we can turn a C function into an IO action. It works
121+With foreign, we can turn a C function into an IO action. It works
122122like this:
123123
124124.. code-block:: idris
125125
126126 getSizeT : IO Int
127− getSizeT = mkForeign (FFun "sizeof_size_t" [] FInt)
127+ getSizeT = foreign FFI_C "sizeof_size_t" (IO Int)
128128
129−Pretty simple. ``mkForeign`` takes a specification of what function it
130−needs to call, and we construct this specification with ``FFun``. And
131−``FFun`` just takes a name, a list of argument types (we have none),
132−and a return type.
133−
134−One thing you might want to note: the return type we've specified is
135−``FInt``, not ``Int``. That's because ``Int`` is an idris type and C
136−functions don't return idris types. ``FInt`` is not an idris type, but
137−is just the representation of the type of a C int. It tells the
138−compiler "Treat the return value of this C function like it's a C int,
139−and when you pass it back into Idris, convert it to an Idris int."
140−
141−Caveats of mkForeign
142−--------------------
143−
144−First and foremost: ``mkForeign`` is not actually a function. It is
145−treated specially by the compiler, and there are certain rules you
146−need to follow when using it.
147−
148−- Rule 1: the name string must be a literal or constant
149−
150−This does not work:
151−
152−.. code-block:: idris
153−
154− intIntToInt : String -> Int -> Int -> IO Int
155− intIntToInt name = mkForeign (FFun name [FInt, FInt] FInt)
156−
157−You'll just have to bite the bullet and write out the whole
158−``mkForeign`` and ``FFun`` expression each time.
159−
160−- Rule 2: the "call" to ``mkForeign`` must be fully applied
161−
162−This just means that every argument appearing in the list of argument
163−types must be applied wherever you write ``mkForeign``. The arguments
164−don't have to be literals or even known at compile time; they just
165−have to be there. For example, if we have ``strlen : String -> IO
166−Int``, then this is fine:
167−
168−.. code-block:: idris
169−
170− strlen str = mkForeign (FFun "strlen" [FString] FInt) str
171−
172−but this is not fine:
173−
174−.. code-block:: idris
175−
176− strlen = mkForeign (FFun "strlen" [FString] FInt)
177−
178−Note that this only applies to places where you literally typed
179−``mkForeign``. Once you've defined it, ``strlen`` is just a normal
180−function returning an IO action, and it doesn't need to be fully
181−applied. This is okay:
182−
183−.. code-block:: idris
184−
185− lengths : IO [Int]
186− lengths = mapM strlen listOfStrings
129+Pretty simple. ``foreign`` takes a specification of what function it
130+needs to call and that function's return type.
187131
188132Running foreign functions
189133-------------------------