git.iko.soy/Idris-dev
on master help sign in
Idris-dev/test/ffi009/Good.idr
37 lines 727 B history raw
1module Good
3%include c "ffi009.h"
5private
6get_allocation_size : Ptr -> IO Int
7get_allocation_size = foreign FFI_C "get_allocation_size" (Ptr -> IO Int)
9-- [ NOTE ]
10--
11-- As `commen_call` is a partial function and not inline, Idris should complain.
13private
14%inline
15common_call : String -> Int -> IO ManagedPtr
16common_call f l = do
17 ptr <- foreign FFI_C
18 f
19 (Int -> IO Ptr)
20 l
21 len <- get_allocation_size ptr
22 pure (prim__registerPtr ptr len)
24func_foo : IO ManagedPtr
25func_foo = common_call "foo" 4
27func_bar : IO ManagedPtr
28func_bar = common_call "bar" 8
31namespace Main
32 main : IO ()
33 main = do
34 foo <- func_foo
35 bar <- func_bar
37 printLn "I should be seen."