working cameraSpec

SDL.lean

@@ -195,4 +195,28 @@ instance SDLCamera.instNonempty : Nonempty SDLCamera := SDLCamera.nonemptyType.p
 @[extern "sdl_open_camera"]
 opaque openCamera : UInt32 -> SDLIO SDLCamera
 
+-- cameraspec stuff
+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 := Colorspace.nonemptyType.type
+instance Colorspace.instNonempty : Nonempty Colorspace := Colorspace.nonemptyType.property
+
+structure CameraSpec.Model where
+  format : PixelFormat
+  colorspace : Colorspace
+  width : Int32
+  height : Int32
+  framerateNumerator : Int32
+  framerateDenominator : Int32
+
+private opaque CameraSpec.nonemptyType : NonemptyType
+def CameraSpec : Type := CameraSpec.nonemptyType.type
+instance CameraSpec.instNonempty : Nonempty CameraSpec := CameraSpec.nonemptyType.property
+
+@[extern "sdl_get_camera_format"]
+opaque getCameraFormat : @& SDLCamera -> SDLIO CameraSpec
+
 end SDL

WebcamApp.lean

@@ -171,6 +171,8 @@ partial def run : IO Unit := do
   let idx := cameraCount[0]!
   let camera <- SDL.openCamera idx
 
+  let spec <- SDL.getCameraFormat camera
+
   let initialState : EngineState := {
     window := window, renderer := renderer
     deltaTime := 0.0, lastTime := 0, running := true

c/sdl.c

@@ -102,6 +102,12 @@ static void sdl_camera_foreach(void * val, lean_obj_arg fn) {
 }
 static void sdl_camera_finalizer(void * h) {
 }
+static lean_external_class * sdl_camera_spec_external_class = NULL;
+static void sdl_camera_spec_foreach(void * val, lean_obj_arg fn) {
+
+}
+static void sdl_camera_spec_finalizer(void * h) {
+}
 
 lean_obj_res sdl_init(uint32_t flags, lean_obj_arg w) {
     int32_t result = SDL_Init(flags);
@@ -112,6 +118,7 @@ lean_obj_res sdl_init(uint32_t flags, lean_obj_arg w) {
     sdl_renderer_external_class = lean_register_external_class(sdl_renderer_finalizer, sdl_renderer_foreach);
     sdl_surface_external_class = lean_register_external_class(sdl_surface_finalizer, sdl_surface_foreach);
     sdl_camera_external_class = lean_register_external_class(sdl_camera_finalizer, sdl_camera_foreach);
+    sdl_camera_spec_external_class = lean_register_external_class(sdl_camera_spec_finalizer, sdl_camera_spec_foreach);
 
     return lean_io_result_mk_ok(lean_box_uint32(result));
 }
@@ -439,6 +446,17 @@ lean_obj_res sdl_open_camera(uint32_t instance_id) {
 }
 
 
+lean_obj_res sdl_get_camera_format(lean_object* camera_obj) {
+    SDL_Camera* camera = (SDL_Camera*)lean_get_external_data(camera_obj);
+    SDL_CameraSpec spec;
+    bool result = SDL_GetCameraFormat(camera, &spec);
+    if (!result) {
+        return lean_io_result_mk_error(lean_mk_string(SDL_GetError()));
+    }
+    lean_object* camera_spec = lean_alloc_external(sdl_camera_spec_external_class, &spec);
+    return lean_io_result_mk_ok(camera_spec);
+}
+
 
 // Mouse support (caching avoids redundant SDL calls within the same frame)
 static struct {