mmhelloworld/idris-jvm

Example of java ffi from documentation does not compile

Closed this issue · 2 comments

jneira commented

Hi, i am exploring this awesome project and when trying to compile the example program from docs i get many errors about missing definitions amongs others:

Error: While processing type of get. Undefined name Inherits.
...
Error: While processing right hand side of get. Undefined name subtyping.
....
Error: Undefined name main.

This is using idris2-jvm-0.6.0.6 in windows.
Sorry if i am missing something obvious and thanks in advance.

mmhelloworld commented

Hi,

Those example programs require importing System.FFI module so the following code works. I will update the documentation to make it explicit. Thanks for pointing it out!

module Main

import System.FFI

%foreign "jvm:toBinaryString(int java/lang/String),java/lang/Integer"
intToBinaryString : Int -> String

main : IO ()
main = printLn $ intToBinaryString 128

By the way, I also improved FFI in the latest version to infer types from Idris signature so we don't have to explicitly provide types in FFI signature in most cases. The following simplified example works as well:

module Main

import System.FFI

%foreign "jvm:toBinaryString,java/lang/Integer"
intToBinaryString : Int -> String

main : IO ()
main = printLn $ intToBinaryString 128
  • ❤️2