@@ -115,75 +115,19 @@ So now we can get the size of ``size_t`` as long as we're in C code.
115We'd like to be able to use this from Idris. Can we do this? It turns
115We'd like to be able to use this from Idris. Can we do this? It turns
116out we can.
116out we can.
118−``mkForeign``
118+``foreign``
119-------------
119-------------
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
122like this:
122like this:
124.. code-block:: idris
124.. code-block:: idris
126 getSizeT : IO Int
126 getSizeT : IO Int
127− getSizeT = mkForeign (FFun "sizeof_size_t" [] FInt)
127+ getSizeT = foreign FFI_C "sizeof_size_t" (IO Int)
129−Pretty simple. ``mkForeign`` takes a specification of what function it
129+Pretty simple. ``foreign`` takes a specification of what function it
130−needs to call, and we construct this specification with ``FFun``. And
130+needs to call and that function's return type.
131−``FFun`` just takes a name, a list of argument types (we have none),
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."
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.
148−- Rule 1: the name string must be a literal or constant
152−.. code-block:: idris
154− intIntToInt : String -> Int -> Int -> IO Int
155− intIntToInt name = mkForeign (FFun name [FInt, FInt] FInt)
157−You'll just have to bite the bullet and write out the whole
158−``mkForeign`` and ``FFun`` expression each time.
160−- Rule 2: the "call" to ``mkForeign`` must be fully applied
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:
168−.. code-block:: idris
170− strlen str = mkForeign (FFun "strlen" [FString] FInt) str
172−but this is not fine:
174−.. code-block:: idris
176− strlen = mkForeign (FFun "strlen" [FString] FInt)
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:
183−.. code-block:: idris
186− lengths = mapM strlen listOfStrings
188Running foreign functions
132Running foreign functions
189-------------------------
133-------------------------