631f3db · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Error when using closure as callback in C backend

Document it.

commit631f3db4a646755ac7a03f88d9575471caedebfa authorNiklas Larsson <niklas@mm.st> dateSat 30 Jun 2018, 23:26 (8 years ago) parentc5c8ede

2 files changed+10−1

unifiedsplit

docs/reference/ffi.rst+6

@@ -178,6 +178,12 @@ compilation error:

178178 example : (Int -> ()) -> IO ()

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

180180

181+Note that the function that is used as a callback can't be a closure, that is

182+it can't be a partially applied function. This is because the mechanism used is

183+unable to pass the closed-over values through C. If we want to pass Idris values

184+to the callback we have to pass them through C explicitly. Non-primitive Idris

185+values can be passed to C via the ``Raw`` type.

186+

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

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

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

src/IRTS/CodegenC.hs+4−1

@@ -889,7 +889,10 @@ getCallback bc = getCallback' (reverse bc)

889889 getCallback' [] = []

890890 findCons (c:cs) xs = findCon c xs ++ findCons cs xs

891891 findCons [] _ = []

892− findCon c ((MKCON l loc tag args):xs) | snd c == l = [(fst c, tag)]

892+ findCon c ((MKCON l loc tag args):xs) | snd c == l =

893+ if null args

894+ then [(fst c, tag)]

895+ else error "Can't wrap a closure as callback."

893896 findCon c (_:xs) = findCon c xs

894897 findCon c [] = []

895898