@@ -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-------------------------
@@ -242,6 +186,8 @@ First, let's write a C file containing functions that we'll bind to.
242186.. code-block:: c
243187
244188 /* stattypes.c */
189+ #include <sys/stat.h>
190+
245191 int sizeof_dev_t() { return sizeof(dev_t); }
246192 int sizeof_ino_t() { return sizeof(ino_t); }
247193 /* lots more functions like this */
@@ -256,20 +202,30 @@ Next, an Idris file to define our providers:
256202 %dynamic "./stattypes.so"
257203
258204 sizeOfDevT : IO Int
259− sizeOfDevT = mkForeign (FFun "sizeof_dev_t" [] FInt)
205+ sizeOfDevT = foreign FFI_C "sizeof_dev_t" (IO Int)
260206 {- lots of similar functions -}
261207
262− -- now we have an integer, but we want a Provider FTy
263− -- since our sizeOf* functions are ordinary IO actions, we
208+ -- Indicates how many bits are used to represent various system
209+ -- stat types.
210+ data BitWidth = B8 | B16 | B32 | B64
211+
212+ instance Show BitWidth where
213+ show B8 = "8 bits"
214+ show B16 = "16 bits"
215+ show B32 = "32 bits"
216+ show B64 = "64 bits"
217+
218+ -- Now we have an integer, but we want a Provider BitWidth.
219+ -- Since our sizeOf* functions are ordinary IO actions, we
264220 -- 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)
221+ bytesToType : Int -> Provider BitWidth
222+ bytesToType 1 = Provide B8 -- "8 bit value"
223+ bytesToType 2 = Provide B16
224+ bytesToType 4 = Provide B32
225+ bytesToType 8 = Provide B64
270226 bytesToType _ = Error "Unrecognised integral type."
271227
272− getDevT : IO (Provider FTy)
228+ getDevT : IO (Provider BitWidth)
273229 getDevT = map bytesToType sizeOfDevT
274230 {- lots of similar functions -}
275231
@@ -282,10 +238,8 @@ providers:
282238 module Main
283239 import Providers
284240 %language TypeProviders
285− %provide (FDevT : FTy) with getDevT
286−
287− -- interpFTy translates a foreign type to the corresponding idris type
288− DevT : Type
289− DevT = interpFTy FDevT -- on most systems, DevT = Bits64
241+ %provide (DevTBitWidth : BitWidth) with getDevT
290242
291− -- We can now use DevT in our program and FDevT in our FFun expressions!
243+ -- We can now use DevTBitWidth in our program!
244+ main : IO ()
245+ main = putStrLn $ "size of dev_t: " ++ show DevTBitWidth