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

docs/reference/ffi.rst+5−1

compare with master

unifiedsplit

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

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

180

181The 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).

183

184

184There are two special function names:

185There are two special function names:

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

186``%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``.

216 errno : IO Ptr

217 errno : IO Ptr

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

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

218

219

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+

219FFI implementation

223FFI implementation

220------------------

224------------------

221

225

docs/tutorial/miscellany.rst+3−2

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

276 strToType _ = Nat

277

278 fromFile : String -> IO (Provider Type)

279− fromFile fname = do str <- readFile fname

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

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

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

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

281

282

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

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

283

284

docs/tutorial/typesfuns.rst+4−4

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

864

865.. code-block:: idris

866

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

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

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

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

869

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

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

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

882

883.. code-block:: idris

884

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

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

886− vec = MkSigma 2 [3, 4]

886+ vec = MkDPair 2 [3, 4]

887

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

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