@@ -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-------------------------
@@ -242,6 +186,8 @@ First, let's write a C file containing functions that we'll bind to.
242.. code-block:: c
186.. code-block:: c
244 /* stattypes.c */
188 /* stattypes.c */
189+ #include <sys/stat.h>
245 int sizeof_dev_t() { return sizeof(dev_t); }
191 int sizeof_dev_t() { return sizeof(dev_t); }
246 int sizeof_ino_t() { return sizeof(ino_t); }
192 int sizeof_ino_t() { return sizeof(ino_t); }
247 /* lots more functions like this */
193 /* lots more functions like this */
@@ -256,20 +202,30 @@ Next, an Idris file to define our providers:
256 %dynamic "./stattypes.so"
202 %dynamic "./stattypes.so"
258 sizeOfDevT : IO Int
204 sizeOfDevT : IO Int
259− sizeOfDevT = mkForeign (FFun "sizeof_dev_t" [] FInt)
205+ sizeOfDevT = foreign FFI_C "sizeof_dev_t" (IO Int)
260 {- lots of similar functions -}
206 {- lots of similar functions -}
208+ -- Indicates how many bits are used to represent various system
210+ data BitWidth = B8 | B16 | B32 | B64
212+ instance Show BitWidth where
214+ show B16 = "16 bits"
215+ show B32 = "32 bits"
216+ show B64 = "64 bits"
262− -- now we have an integer, but we want a Provider FTy
218+ -- Now we have an integer, but we want a Provider BitWidth.
263− -- since our sizeOf* functions are ordinary IO actions, we
219+ -- Since our sizeOf* functions are ordinary IO actions, we
264 -- can just map over them.
220 -- can just map over them.
265− bytesToType : Int -> Provider FTy
221+ bytesToType : Int -> Provider BitWidth
266− bytesToType 1 = Provide (FIntT IT8) -- "8 bit foreign integer"
222+ bytesToType 1 = Provide B8 -- "8 bit value"
267− bytesToType 2 = Provide (FIntT IT16)
223+ bytesToType 2 = Provide B16
268− bytesToType 4 = Provide (FIntT IT32)
224+ bytesToType 4 = Provide B32
269− bytesToType 8 = Provide (FIntT IT64)
225+ bytesToType 8 = Provide B64
270 bytesToType _ = Error "Unrecognised integral type."
226 bytesToType _ = Error "Unrecognised integral type."
272− getDevT : IO (Provider FTy)
228+ getDevT : IO (Provider BitWidth)
273 getDevT = map bytesToType sizeOfDevT
229 getDevT = map bytesToType sizeOfDevT
274 {- lots of similar functions -}
230 {- lots of similar functions -}
@@ -282,10 +238,8 @@ providers:
282 module Main
238 module Main
283 import Providers
239 import Providers
284 %language TypeProviders
240 %language TypeProviders
285− %provide (FDevT : FTy) with getDevT
241+ %provide (DevTBitWidth : BitWidth) with getDevT
287− -- interpFTy translates a foreign type to the corresponding idris type
289− DevT = interpFTy FDevT -- on most systems, DevT = Bits64
291− -- We can now use DevT in our program and FDevT in our FFun expressions!
243+ -- We can now use DevTBitWidth in our program!
245+ main = putStrLn $ "size of dev_t: " ++ show DevTBitWidth