FFI good practices

Stream: lean4

[Thomas Vigouroux]

Hey there !

I am in the process of wrapping the ncurses library in lean, and I am wondering about the "good practices" of making suck a wrapper.

Here are my questions:

1. Many types in ncurses are actually standard types representing other things. I'd like to expose them as disctinct types in lean to haev better type guarantees. Is it necessary to always box them (even if the type is say short) ? What is the process ?
2. I know lean_external_class and the likes exist but I don't understand what they do. Is there documentation about that somewhere ?

[Thomas Vigouroux]

The source code of the bindings is available here by the way: https://git.sr.ht/~vigoux/lcurses/tree

[Daniil Kisel]

1. Some types are unboxed as function arguments/return types, e.g. UInts. Trivial wrappers around them (inductive with only one relevant type, e.g. Char) are treated similarly. But when stored in an inductive any wrappers are stored as lean_object*.
2. External class is required to create external objects that hold a user supplied pointer that can be anything. The class stores free and foreach callbacks (foreach is used to mark owned lean_object*s as multithreaded etc).

See manual and this guide.

[Daniil Kisel]

Wrapper example:

structure A where
  val : UInt32

@[extern "func"]
opaque func : A -> A

LEAN_EXPORT uint32_t func(uint32_t x)
{
  return x;
}

[Daniil Kisel]

Class example:

@[extern "my_init"]
opaque init : BaseIO Unit
builtin_initialize init

opaque BPointed : NonemptyType
def B := BPointed.type
instance : Nonempty B := BPointed.property

@[extern "my_func"]
opaque func : IO B

lean_external_class* my_class;

static void my_finalize(void* user_ptr) {}
static void my_foreach(void* user_ptr, b_lean_obj_arg f) {}

LEAN_EXPORT lean_obj_res my_init(lean_obj_arg io_world)
{
  my_class = lean_register_external_class(my_finalize, my_foreach);
  return lean_io_result_mk_ok(lean_box(0));
}

LEAN_EXPORT lean_obj_res my_func(lean_obj_arg io_world)
{
  return lean_io_result_mk_ok(lean_alloc_external(my_class, NULL));
}

[haowei chen]

@Daniil Kisel Is there any example about the foreachcallback? i don't quite understand how it can "mark owned lean_object*s as multithreaded etc"

[Daniil Kisel]

You need to apply the supplied function to every owned lean_object*. For example, if the pointer stored in the external object points to a structure:

typedef struct
{
  lean_object* x;
  lean_object* y;
} A;

Then the foreach callback should apply f to x and to y:

static void my_foreach(void* user_ptr, b_lean_obj_arg f)
{
  A* a = user_ptr;
  lean_inc(f);
  lean_inc(a->x);
  lean_apply_1(f, a->x);
  lean_inc(f);
  lean_inc(a->y);
  lean_apply_1(f, a->y);
}

And the free callback should probably call lean_dec on a->x and a->y to free them.