SDLRect as lean structure

SDL.lean

@@ -44,6 +44,13 @@ def SDL_TEXTUREACCESS_STATIC : UInt32 := 0x0
 def SDL_TEXTUREACCESS_STREAMING : UInt32 := 0x1
 def SDL_TEXTUREACCESS_TARGET :UInt32 := 0x2
 
+structure SDLRect where
+  x : Int32
+  y : Int32
+  w : Int32
+  h : Int32
+  deriving Repr
+
 @[extern "sdl_init"]
 opaque init : UInt32 → IO UInt32
 
@@ -83,7 +90,7 @@ opaque renderClear : @& SDLRenderer → SDLIO Int32
 opaque renderPresent : @& SDLRenderer → IO Unit
 
 @[extern "sdl_render_fill_rect"]
-opaque renderFillRect : @& SDLRenderer → Int32 → Int32 → Int32 → Int32 → SDLIO Int32
+opaque renderFillRect : @& SDLRenderer → @& SDLRect → SDLIO Int32
 
 @[extern "sdl_delay"]
 opaque delay : UInt32 → IO Unit

TestApp.lean

@@ -38,7 +38,7 @@ def setColor (renderer : SDL.SDLRenderer) (color : Color) : IO Unit :=
   SDL.setRenderDrawColor renderer color.r color.g color.b color.a *> pure ()
 
 def fillRect (renderer : SDL.SDLRenderer) (x y w h : Int32) : IO Unit :=
-  SDL.renderFillRect renderer x y w h *> pure ()
+  SDL.renderFillRect renderer { x, y, w, h } *> pure ()
 
 def renderScene (state : EngineState) : IO Unit := do
   setColor state.renderer { r := 135, g := 206, b := 235 }

WebcamApp.lean

@@ -38,7 +38,7 @@ def setColor (renderer : SDL.SDLRenderer) (color : Color) : IO Unit :=
   SDL.setRenderDrawColor renderer color.r color.g color.b color.a *> pure ()
 
 def fillRect (renderer : SDL.SDLRenderer) (x y w h : Int32) : IO Unit :=
-  SDL.renderFillRect renderer x y w h *> pure ()
+  SDL.renderFillRect renderer { x, y, w, h } *> pure ()
 
 def renderScene (state : EngineState) : IO Unit := do
   setColor state.renderer { r := 0, g := 0, b := 235 }

c/sdl.c

@@ -231,9 +231,15 @@ lean_obj_res sdl_render_present(lean_object * g_renderer, lean_obj_arg w) {
     return lean_io_result_mk_ok(lean_box(0));
 }
 
-lean_obj_res sdl_render_fill_rect(lean_object * g_renderer, uint32_t x, uint32_t y, uint32_t w, uint32_t h) {
+lean_obj_res sdl_render_fill_rect(lean_object * g_renderer, b_lean_obj_arg rect_obj) {
     SDL_Renderer* renderer = (SDL_Renderer*)lean_get_external_data(g_renderer);
     if (renderer == NULL) return lean_io_result_mk_error(lean_mk_io_user_error(lean_mk_string("C: Renderer is NULL")));
+
+    int32_t x = (int32_t)lean_ctor_get_uint32(rect_obj, 0);
+    int32_t y = (int32_t)lean_ctor_get_uint32(rect_obj, 4);
+    int32_t w = (int32_t)lean_ctor_get_uint32(rect_obj, 8);
+    int32_t h = (int32_t)lean_ctor_get_uint32(rect_obj, 12);
+
     SDL_FRect rect = {(float)x, (float)y, (float)w, (float)h};
     int32_t result = SDL_RenderFillRect(renderer, &rect);
     return lean_io_result_mk_ok(lean_box_uint32(result));