34c8e1f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added slightly to the C FFI reference, and corrected a code example i… (#3126)

* Added slightly to the C FFI reference, and corrected a code example in the type providers tutorial * Changed Sigma to DPair in the tutorial * Responded to code review comments * Corrected indentation of type-provider exmple

commit34c8e1ff220fbdb0b35e3dc9eca0c7b38040c825 authorColin Adams <colinpauladams@gmail.com> dateTue 26 Apr 2016, 13:40 (10 years ago) parentc6c47ae

3 files changed+12−7

compare with master

unifiedsplit

docs/reference/ffi.rst+5−1 docs/tutorial/miscellany.rst+3−2 docs/tutorial/typesfuns.rst+4−4

docs/reference/ffi.rst+5−1

@@ -179,7 +179,8 @@ compilation error:

179179 example f = foreign FFI_C "callbacker" (CFnPtr (Int -> ()) -> IO ()) f

180180

181181The other big limitation is that it doesn't support IO functions. Use

182−``unsafePerformIO`` to wrap them.

182+``unsafePerformIO`` to wrap them (i.e. to make an IO function usable as a callback, change the return type

183+from IOr to r, and change the = do to = unsafePerformIO $ do).

183184

184185There are two special function names:

185186``%wrapper`` returns the function pointer that wraps an Idris function. This

@@ -216,6 +217,9 @@ global variable with the following name. The type must be just ``IO Ptr``.

216217 errno : IO Ptr

217218 errno = foreign FFI_C "&errno" (IO Ptr)

218219

220+For more complicated interactions with C (such as reading and setting fields of a C struct), there is

221+a module CFFI available in the contrib package.

222+

219223FFI implementation

220224------------------

221225

docs/tutorial/miscellany.rst+3−2

@@ -276,8 +276,9 @@ type ``Int`` will be provided. Otherwise, it will provide the type

276276 strToType _ = Nat

277277

278278 fromFile : String -> IO (Provider Type)

279− fromFile fname = do str <- readFile fname

280− return (Provide (strToType (trim str)))

279+ fromFile fname = do Right str <- readFile fname

280+ | Left err => pure (Provide Void)

281+ pure (Provide (strToType (trim str)))

281282

282283We then use the ``%provide`` directive:

283284

docs/tutorial/typesfuns.rst+4−4

@@ -864,8 +864,8 @@ as “sigma types”:

864864

865865.. code-block:: idris

866866

867− data Sigma : (a : Type) -> (P : a -> Type) -> Type where

868− MkSigma : {P : a -> Type} -> (x : a) -> P x -> Sigma a P

867+ data DPair : (a : Type) -> (P : a -> Type) -> Type where

868+ MkDPair : {P : a -> Type} -> (x : a) -> P x -> DPair a P

869869

870870Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type

871871of a pair of A and P, where the name ``a`` can occur inside ``P``.

@@ -882,8 +882,8 @@ equivalent.

882882

883883.. code-block:: idris

884884

885− vec : Sigma Nat (\n => Vect n Int)

886− vec = MkSigma 2 [3, 4]

885+ vec : DPair Nat (\n => Vect n Int)

886+ vec = MkDPair 2 [3, 4]

887887

888888The type checker could of course infer the value of the first element

889889from the length of the vector. We can write an underscore ``_`` in