Constructing `lean_object *` when calling Lean code from C

Stream: general

[Qiuye Wang]

I'm trying to export a Lean model to an executable function using the FFI. My target function is def hasPermission (user: UserInfo) (resource: Resource) (perm_type: PermissionType): Bool, where UserInfo, Resource, and PermissionType are Lean structures.

I looked into the C IR generated when exporting the shared library and found that the prototype is LEAN_EXPORT uint8_t has_permission(lean_object*, lean_object*, uint8_t);. That is expected because PermissionType is an enum type. However, I do not know how to build the other two arguments, namely user and resource.

The most relevant resource I found is the reverse-ffi example, where a Lean string represented by lean_object * is built using lean_mk_string. However, it does not show how to build complex inductive types. The document mentions the memory layout here and there, but I'm still a little confused.

Is there a more detailed "reverse-ffi" example that shows how to build lean_object with complex inductive type in C?

[David Thrane Christiansen]

You could take a look at md4lean, which uses the FFI to construct ASTs. The type in question is not hugely complex, but it at least shows examples of using lean_alloc_ctor, lean_ctor_set, lean_box, and lean_box_* to allocate and populate constructors of an inductive type.

The C in question is here.

[Qiuye Wang]

David Thrane Christiansen 发言道：

You could take a look at md4lean, which uses the FFI to construct ASTs. The type in question is not hugely complex, but it at least shows examples of using lean_alloc_ctor, lean_ctor_set, lean_box, and lean_box_* to allocate and populate constructors of an inductive type.

The C in question is here.

Thanks! The reference helped a lot.

I noticed that in this project only Lean Array is built. Should I build arrays first, then convert to lists using lean_array_to_list, or is there someway I can directly build Lean List?

[David Thrane Christiansen]

Unlike arrays, lists aren't a primitive. lean_alloc_ctor and lean_box should get you List.cons and List.nil.

[David Thrane Christiansen]

It'll look a lot like this code that returns an Option.