mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-22 06:29:37 +03:00
d5377be628
More documentation to follow, but in brief: - IO is now a synonym of IO' FFI_C - IO' is parameterised over an ffi description, which explains which types are allowed in foreign calls, and what a foreign call target is (in C, that's a String giving the function name, for example) - New function "foreign" for building a foreign call, given an ffi description, call target, and the type of the call. The type is enough to build a structure which the compiler uses to generate the call. The type of main now needs to be IO' x (), where x can be any FFI description. There is currently only an ffi description for C; Javascript will follow. FFI_C should also work for the llvm backend (it's really about the calling convention, not the backend specifically). Small changes will be needed to the various code generators.
10 lines
164 B
Idris
10 lines
164 B
Idris
module Main
|
|
|
|
%dynamic "dummy", "libm", "msvcrt"
|
|
|
|
x : Float
|
|
x = unsafePerformIO (foreign FFI_C "sin" (Float -> IO Float) 1.6)
|
|
|
|
main : IO ()
|
|
main = putStrLn (show x)
|