@@ -242,6 +242,8 @@ First, let's write a C file containing functions that we'll bind to.
242242.. code-block:: c
243243
244244 /* stattypes.c */
245+ #include <sys/stat.h>
246+
245247 int sizeof_dev_t() { return sizeof(dev_t); }
246248 int sizeof_ino_t() { return sizeof(ino_t); }
247249 /* lots more functions like this */
@@ -256,20 +258,30 @@ Next, an Idris file to define our providers:
256258 %dynamic "./stattypes.so"
257259
258260 sizeOfDevT : IO Int
259− sizeOfDevT = mkForeign (FFun "sizeof_dev_t" [] FInt)
261+ sizeOfDevT = foreign FFI_C "sizeof_dev_t" (IO Int)
260262 {- lots of similar functions -}
261263
262− -- now we have an integer, but we want a Provider FTy
263− -- since our sizeOf* functions are ordinary IO actions, we
264+ -- Indicates how many bits are used to represent various system
265+ -- stat types.
266+ data BitWidth = B8 | B16 | B32 | B64
267+
268+ instance Show BitWidth where
269+ show B8 = "8 bits"
270+ show B16 = "16 bits"
271+ show B32 = "32 bits"
272+ show B64 = "64 bits"
273+
274+ -- Now we have an integer, but we want a Provider BitWidth.
275+ -- Since our sizeOf* functions are ordinary IO actions, we
264276 -- can just map over them.
265− bytesToType : Int -> Provider FTy
266− bytesToType 1 = Provide (FIntT IT8) -- "8 bit foreign integer"
267− bytesToType 2 = Provide (FIntT IT16)
268− bytesToType 4 = Provide (FIntT IT32)
269− bytesToType 8 = Provide (FIntT IT64)
277+ bytesToType : Int -> Provider BitWidth
278+ bytesToType 1 = Provide B8 -- "8 bit value"
279+ bytesToType 2 = Provide B16
280+ bytesToType 4 = Provide B32
281+ bytesToType 8 = Provide B64
270282 bytesToType _ = Error "Unrecognised integral type."
271283
272− getDevT : IO (Provider FTy)
284+ getDevT : IO (Provider BitWidth)
273285 getDevT = map bytesToType sizeOfDevT
274286 {- lots of similar functions -}
275287
@@ -282,10 +294,8 @@ providers:
282294 module Main
283295 import Providers
284296 %language TypeProviders
285− %provide (FDevT : FTy) with getDevT
297+ %provide (DevTBitWidth : BitWidth) with getDevT
286298
287− -- interpFTy translates a foreign type to the corresponding idris type
288− DevT : Type
289− DevT = interpFTy FDevT -- on most systems, DevT = Bits64
290−
291− -- We can now use DevT in our program and FDevT in our FFun expressions!
299+ -- We can now use DevTBitWidth in our program!
300+ main : IO ()
301+ main = putStrLn $ "size of dev_t: " ++ show DevTBitWidth