What are the correct C types to use in Idris FFI?

Viewed 37

When making an FFI to C from Idris, the following Idris types are allowed

Int
Char
Double (as double in C)
Bits8
Bits16
Bits32
Bits64
String (as char* in C)
Ptr t and AnyPtr (both as void* in C)

Return types can be any of the above, plus:

()
PrimIO t, where t is a valid return type other than a PrimIO.

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.

0 Answers
Related