FFI - representing C structs in Lean

Stream: general

[Greg Shuflin]

I'm currently hacking on this SDL3 bindings library (https://github.com/ValorZard/lean-sdl3) that @Oliver Dressler and @Srayan Jana have contributed to, trying to understand how it works and expand its functionality. At the moment, I'm trying to get the SDL3 webcam bindings working.

I'm specifically trying to figure out how to best represent C SDL structures as types in Lean. I can see that the existing bindings are doing something like:

private opaque SDLWindow.nonemptyType : NonemptyType
def SDLWindow : Type := SDLWindow.nonemptyType.type
instance SDLWindow.instNonempty : Nonempty SDLWindow := SDLWindow.nonemptyType.property

to create a Lean equivalent of a SDL_Window structure. But I'm not sure how to create a Lean structure that has fields equivalent to a C structure, and I don't see any examples of this in these existing bindings. I specifically want to be able to represent a SDL_CameraSpec in Lean as a Lean structure and get access to the various C integer fields on it.

[Mac Malone]

If you want the C structure to also appear in the formalization, below is a brief example of how that could be done. In the example, SDL types are represented by Lean external objects with the assumption that the proper external classes are registered in the C code (e.g., g_pixelformat_external_class).

In general, I should probably explain the example a bit more, but I do not have the time at the present.

Example Code

namespace SDL

private opaque PixelFormat.nonemptyType : NonemptyType
def PixelFormat : Type := PixelFormat.nonemptyType.type
instance PixelFormat.instNonempty : Nonempty PixelFormat := PixelFormat.nonemptyType.property

private opaque Colorspace.nonemptyType : NonemptyType
def Colorspace : Type := PixelFormat.nonemptyType.type
instance Colorspace.instNonempty : Nonempty PixelFormat := PixelFormat.nonemptyType.property

structure CameraSpec.Model where
  format : PixelFormat
  colorspace : Colorspace
  width : Int32
  height : Int32
  framerateNumerator : Int32
  framerateDenominator : Int32

structure CameraSpec where
  private ofModel ::
    private toModel : CameraSpec.Model

namespace CameraSpec

@[extern "sdl_camera_spec_format"]
def format (spec : @& CameraSpec) : PixelFormat :=
  spec.toModel.format
/-
```c++
extern "C" LEAN_EXPORT lean_obj_res sdl_camera_spec_format(b_lean_obj_arg spec) {
  SDL_PixelFormat format = static_cast<SDL_CameraSpec*>(lean_get_external_data(spec))->format;
  return lean_alloc_external(g_pixelformat_external_class, format);
}
```
-/

@[extern "sdl_camera_spec_width"]
def width (spec : @& CameraSpec) : Int32 :=
  spec.toModel.width
/-
```c++
extern "C" LEAN_EXPORT int32_t sdl_camera_spec_width(b_lean_obj_arg spec) {
  return static_cast<SDL_CameraSpec*>(lean_get_external_data(spec))->width;
}
```
-/

[Greg Shuflin]

Mac Malone said:

If you want the C structure to also appear in the formalization, below is a brief example of how that could be done. In the example, SDL types are represented by Lean external objects with the assumption that the proper external classes are registered in the C code (e.g., g_pixelformat_external_class).

In general, I should probably explain the example a bit more, but I do not have the time at the present.

Example Code

namespace SDL

private opaque PixelFormat.nonemptyType : NonemptyType
def PixelFormat : Type := PixelFormat.nonemptyType.type
instance PixelFormat.instNonempty : Nonempty PixelFormat := PixelFormat.nonemptyType.property

private opaque Colorspace.nonemptyType : NonemptyType
def Colorspace : Type := PixelFormat.nonemptyType.type
instance Colorspace.instNonempty : Nonempty PixelFormat := PixelFormat.nonemptyType.property

structure CameraSpec.Model where
  format : PixelFormat
  colorspace : Colorspace
  width : Int32
  height : Int32
  framerateNumerator : Int32
  framerateDenominator : Int32

structure CameraSpec where
  private ofModel ::
    private toModel : CameraSpec.Model

namespace CameraSpec

@[extern "sdl_camera_spec_format"]
def format (spec : @& CameraSpec) : PixelFormat :=
  spec.toModel.format
/-
```c++
extern "C" LEAN_EXPORT lean_obj_res sdl_camera_spec_format(b_lean_obj_arg spec) {
  SDL_PixelFormat format = static_cast<SDL_CameraSpec*>(lean_get_external_data(spec))->format;
  return lean_alloc_external(g_pixelformat_external_class, format);
}
```
-/

@[extern "sdl_camera_spec_width"]
def width (spec : @& CameraSpec) : Int32 :=
  spec.toModel.width
/-
```c++
extern "C" LEAN_EXPORT int32_t sdl_camera_spec_width(b_lean_obj_arg spec) {
  return static_cast<SDL_CameraSpec*>(lean_get_external_data(spec))->width;
}
```
-/

yeah I think I need a bit more explanation to make sense of this, either that or this block of code as such doesn't work and I need to modify it some.