Pass signed ints to and from the C FFI

[ValorZard]

Currently, Lean can only send unsigned integers

While working on the SDL3 bindings for Lean, I found something that was particularly annoying

https://github.com/ValorZard/lean-sdl3/blob/22c92150b622592cff10214ed5cb8b2001dec1aa/c/sdl.c#L322

lean_obj_res sdl_get_texture_width(lean_object * g_texture, lean_obj_arg w) {
    SDL_Texture* texture = (SDL_Texture*)lean_get_external_data(g_texture);

    SDL_PropertiesID messageTexProps = SDL_GetTextureProperties(texture);

    // get number property always returns a signed 64-bit integer
    int64_t width = SDL_GetNumberProperty(messageTexProps, SDL_PROP_TEXTURE_WIDTH_NUMBER, 0);
    
    // however, there seems to be no way to return int64_t directly to Lean
    // so we box it as uint64_t instead
    // TODO: figure out a way to return int64_t directly
    return lean_io_result_mk_ok(lean_box_uint64(width));
}

This is using this specific function: https://wiki.libsdl.org/SDL3/SDL_GetNumberProperty

and then you cast it back to a signed int https://github.com/ValorZard/lean-sdl3/blob/22c92150b622592cff10214ed5cb8b2001dec1aa/SDL.lean#L120

@[extern "sdl_get_texture_width"]
opaque getTextureWidth (texture : @& SDLTexture) : SDLIO Int64

This ... does not feel good. Is there a way for Lean to support signed integers natively?

[hargoniX]

What you are currently doing is the same way that Int64's C functions for performing fast addition using machine operations etc. work as well, for example:

static inline uint64_t lean_int64_add(uint64_t a1, uint64_t a2) {
    int64_t lhs = (int64_t)a1;
    int64_t rhs = (int64_t)a2;

    return (uint64_t)(lhs + rhs);
}

so no there is currently no way around this.

That said I do plan to eventually add support in the Lean ABI for these types in order to avoid these complications.