When making an FFI to C from Idris, the following Idris types are allowed
Int
Char
Double(asdoublein C)
Bits8
Bits16
Bits32
Bits64
String(aschar*in C)
Ptr tandAnyPtr(both asvoid*in C)Return types can be any of the above, plus:
()
PrimIO t, wheretis a valid return type other than aPrimIO.
Except where the C types are mentioned (double, char* and void*), I'm unclear what C types I should be using. I'm mostly confused about numeric primitives, which I surmise must all correspond to Int in Idris.
For example*, if my C function expects or returns an unsigned int
unsigned int increment (unsigned int x) {
return x + 1;
}
should I use the increment C function as is, with Int, or should I first cast that to or from int before returning it?
int increment (int x) {
// obviously a silly example, do extrapolate to a meaningful example
return (int) ((unsigned int) x + 1);
}
and if I do, am I open to issues regarding numeric width?
*While I'm mostly interested in integer types, I'd like to know how to FFI with all types.