@@ -242,6 +242,8 @@ First, let's write a C file containing functions that we'll bind to.
242.. code-block:: c
242.. code-block:: c
244 /* stattypes.c */
244 /* stattypes.c */
245+ #include <sys/stat.h>
245 int sizeof_dev_t() { return sizeof(dev_t); }
247 int sizeof_dev_t() { return sizeof(dev_t); }
246 int sizeof_ino_t() { return sizeof(ino_t); }
248 int sizeof_ino_t() { return sizeof(ino_t); }
247 /* lots more functions like this */
249 /* lots more functions like this */
@@ -256,20 +258,30 @@ Next, an Idris file to define our providers:
256 %dynamic "./stattypes.so"
258 %dynamic "./stattypes.so"
258 sizeOfDevT : IO Int
260 sizeOfDevT : IO Int
259− sizeOfDevT = mkForeign (FFun "sizeof_dev_t" [] FInt)
261+ sizeOfDevT = foreign FFI_C "sizeof_dev_t" (IO Int)
260 {- lots of similar functions -}
262 {- lots of similar functions -}
264+ -- Indicates how many bits are used to represent various system
266+ data BitWidth = B8 | B16 | B32 | B64
268+ instance Show BitWidth where
270+ show B16 = "16 bits"
271+ show B32 = "32 bits"
272+ show B64 = "64 bits"
262− -- now we have an integer, but we want a Provider FTy
274+ -- Now we have an integer, but we want a Provider BitWidth.
263− -- since our sizeOf* functions are ordinary IO actions, we
275+ -- Since our sizeOf* functions are ordinary IO actions, we
264 -- can just map over them.
276 -- can just map over them.
265− bytesToType : Int -> Provider FTy
277+ bytesToType : Int -> Provider BitWidth
266− bytesToType 1 = Provide (FIntT IT8) -- "8 bit foreign integer"
278+ bytesToType 1 = Provide B8 -- "8 bit value"
267− bytesToType 2 = Provide (FIntT IT16)
279+ bytesToType 2 = Provide B16
268− bytesToType 4 = Provide (FIntT IT32)
280+ bytesToType 4 = Provide B32
269− bytesToType 8 = Provide (FIntT IT64)
281+ bytesToType 8 = Provide B64
270 bytesToType _ = Error "Unrecognised integral type."
282 bytesToType _ = Error "Unrecognised integral type."
272− getDevT : IO (Provider FTy)
284+ getDevT : IO (Provider BitWidth)
273 getDevT = map bytesToType sizeOfDevT
285 getDevT = map bytesToType sizeOfDevT
274 {- lots of similar functions -}
286 {- lots of similar functions -}
@@ -282,10 +294,8 @@ providers:
282 module Main
294 module Main
283 import Providers
295 import Providers
284 %language TypeProviders
296 %language TypeProviders
285− %provide (FDevT : FTy) with getDevT
297+ %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!
299+ -- We can now use DevTBitWidth in our program!
301+ main = putStrLn $ "size of dev_t: " ++ show DevTBitWidth