[feature] Support for a single wall texture

Engine.lean

@@ -27,6 +27,7 @@ structure EngineState where
 def SCREEN_WIDTH : Int32 := 1280
 def SCREEN_HEIGHT : Int32 := 720
 def FOV : Float := 1.047 -- ~60 degrees in radians
+def TEXTURE_SIZE : Float := 64.0
 
 def sampleMap : Map := #[
   #[1,1,1,1,1,1,1,1,1,1],
@@ -57,7 +58,7 @@ def isWall (mapp : Map) (x y : Float) : Bool :=
     let mapY := y.floor.toUInt32.toNat
     mapY >= mapp.size || mapX >= mapp[mapY]!.size || mapp[mapY]![mapX]! == 1
 
-def castRay (map : Map) (startX startY angle : Float) : Float := Id.run do
+def castRay (map : Map) (startX startY angle : Float): Float × Float := Id.run do
   let rayDirX := Float.cos angle
   let rayDirY := Float.sin angle
   let mut mapX := startX.floor
@@ -87,9 +88,16 @@ def castRay (map : Map) (startX startY angle : Float) : Float := Id.run do
 
     hit := isWall map mapX mapY
 
-  if side == 0
-  then (mapX - startX + (1.0 - Float.ofInt stepX) / 2.0) / rayDirX
-  else (mapY - startY + (1.0 - Float.ofInt stepY) / 2.0) / rayDirY
+  let distance := if side == 0
+    then (mapX - startX + (1.0 - Float.ofInt stepX) / 2.0) / rayDirX
+    else (mapY - startY + (1.0 - Float.ofInt stepY) / 2.0) / rayDirY
+
+  let wallX := if side == 0
+    then startY + distance * rayDirY
+    else startX + distance * rayDirX
+
+  let texX := (wallX - wallX.floor) * TEXTURE_SIZE
+  (distance, texX)
 
 def updateCamera (camera : Camera) (deltaTime : Float) : IO Camera := do
   let moveSpeed := camera.speed * deltaTime
@@ -115,35 +123,37 @@ def fillRect (x y w h : Int32) : IO Unit :=
   SDL.renderFillRect x y w h *> pure ()
 
 def renderScene (state : EngineState) : IO Unit := do
-  setColor { r := 87, g := 127, b := 137 }
+  setColor { r := 135, g := 206, b := 235 }
   let _ ← SDL.renderClear
 
-  let camera := state.camera
-  let rayAngleStep := FOV / SCREEN_WIDTH.toFloat
-
+  let rayStep := FOV / SCREEN_WIDTH.toFloat
   for column in [0:SCREEN_WIDTH.toNatClampNeg] do
-    let rayAngle := camera.angle - FOV/2 + column.toFloat * rayAngleStep
-    let distance := max 0.1 (castRay state.gameMap camera.x camera.y rayAngle)
-    let wallHeight := (SCREEN_HEIGHT.toFloat / distance) * 1.5
+    let rayAngle := state.camera.angle - FOV/2 + column.toFloat * rayStep
+    let (distance, texX) := castRay state.gameMap state.camera.x state.camera.y rayAngle
+    let wallHeight := (SCREEN_HEIGHT.toFloat / max 0.1 distance) * 1.5
 
-    let wallStart := max 0 ((SCREEN_HEIGHT.toFloat - wallHeight) / 2).toInt32
-    let wallEnd := min (SCREEN_HEIGHT - 1) (wallStart + wallHeight.toInt32)
-    let xPos := column.toInt32
+    let wallStart := (SCREEN_HEIGHT.toFloat - wallHeight) / 2
+    let visibleStart := max 0 wallStart
+    let visibleEnd := min SCREEN_HEIGHT.toFloat (wallStart + wallHeight)
 
-    if wallStart > 0 then
-      setColor { r := 135, g := 206, b := 235 }
-      fillRect xPos 0 1 wallStart
+    let wallStartInt := visibleStart.toInt32
+    let wallEndInt := visibleEnd.toInt32
+    let wallHeightInt := wallEndInt - wallStartInt
 
-    if wallStart < wallEnd then
-      let lightIntensity := max 0.3 (1.0 - distance / 8.0)
-      let col := (200.0 * lightIntensity).toUInt8
-      setColor { r := col, g := col, b := col + 20 }
-      fillRect xPos wallStart 1 (wallEnd - wallStart)
+    if wallHeightInt > 0 then
+      let (texYStart, texYEnd) :=
+        if wallHeight <= SCREEN_HEIGHT.toFloat then (0, TEXTURE_SIZE.toInt32)
+        else
+          let zoom := wallHeight / SCREEN_HEIGHT.toFloat
+          let visible := TEXTURE_SIZE / zoom
+          let start := 0.5 + (TEXTURE_SIZE - visible) / 2
+          (start.toInt32, (start + visible).toInt32)
 
-    if wallEnd < SCREEN_HEIGHT - 1 then
-      let floorShade := max 20 (60 - distance * 5).toUInt8
-      setColor { r := floorShade, g := floorShade + 30, b := floorShade }
-      fillRect xPos wallEnd 1 (SCREEN_HEIGHT - 1 - wallEnd)
+      let _ ← SDL.renderTextureColumn column.toInt32 wallStartInt wallHeightInt texX.toInt32 texYStart texYEnd
+
+    let shade := max 20 (50 - distance * 5).toUInt8
+    setColor { r := shade, g := shade + 30, b := shade }
+    fillRect column.toInt32 wallEndInt 1 (SCREEN_HEIGHT - wallEndInt)
 
 private def updateEngineState (engineState : IO.Ref EngineState) : IO Unit := do
   let state ← engineState.get
@@ -175,12 +185,13 @@ partial def run : IO Unit := do
     SDL.quit
     return
 
-
   unless (← SDL.createRenderer ()) != 0 do
     IO.println "Failed to create renderer"
     SDL.quit
     return
 
+  unless (← SDL.loadTexture "wall.png") != 0 do
+    IO.println "Failed to load texture, using solid colors"
 
   let initialState : EngineState := {
     deltaTime := 0.0, lastTime := 0, running := true,

README.md

@@ -36,6 +36,8 @@ For more information on MSYS2, see: https://github.com/leanprover/lean4/blob/mas
 
 Next, follow the instructions for Unix above.
 
-## License
+## License & Attribution
 
 MIT
+
+Wall texture by [FacadeGaikan](https://opengameart.org/node/31075), licensed under CC0.

SDL.lean

@@ -50,4 +50,10 @@ opaque getTicks : IO UInt32
 @[extern "sdl_get_key_state"]
 opaque getKeyState : UInt32 → IO Bool
 
+@[extern "sdl_load_texture"]
+opaque loadTexture : String → IO UInt32
+
+@[extern "sdl_render_texture_column"]
+opaque renderTextureColumn : Int32 → Int32 → Int32 → Int32 → Int32 → Int32 → IO Int32
+
 end SDL

c/sdl.c

@@ -5,12 +5,7 @@
 
 static SDL_Window* g_window = NULL;
 static SDL_Renderer* g_renderer = NULL;
-
-uint32_t sdl_get_version(void) {
-    // from https://wiki.libsdl.org/SDL3/SDL_GetVersion
-    const int linked = SDL_GetVersion();  /* reported by linked SDL library */
-    return SDL_VERSIONNUM_MAJOR(linked) * 100 + SDL_VERSIONNUM_MINOR(linked) * 10 + SDL_VERSIONNUM_MICRO(linked);
-}
+static SDL_Texture* g_wall_texture = NULL;
 
 lean_obj_res sdl_init(uint32_t flags, lean_obj_arg w) {
     int32_t result = SDL_Init(flags);
@@ -18,6 +13,10 @@ lean_obj_res sdl_init(uint32_t flags, lean_obj_arg w) {
 }
 
 lean_obj_res sdl_quit(lean_obj_arg w) {
+    if (g_wall_texture) {
+        SDL_DestroyTexture(g_wall_texture);
+        g_wall_texture = NULL;
+    }
     if (g_renderer) {
         SDL_DestroyRenderer(g_renderer);
         g_renderer = NULL;
@@ -99,3 +98,38 @@ lean_obj_res sdl_get_key_state(uint32_t scancode, lean_obj_arg w) {
     uint8_t pressed = state[scancode];
     return lean_io_result_mk_ok(lean_box(pressed));
 }
+
+// TEXTURE SUPPORT
+// Assuming 64x64 texture
+lean_obj_res sdl_load_texture(lean_obj_arg filename, lean_obj_arg w) {
+    const char* filename_str = lean_string_cstr(filename);
+    SDL_Surface* surface = IMG_Load(filename_str);
+    if (!surface) {
+        SDL_Log("C: Failed to load texture: %s\n", SDL_GetError());
+        return lean_io_result_mk_ok(lean_box(0));
+    }
+
+    if (g_wall_texture) SDL_DestroyTexture(g_wall_texture);
+    g_wall_texture = SDL_CreateTextureFromSurface(g_renderer, surface);
+    SDL_DestroySurface(surface);
+
+    if (!g_wall_texture) {
+        SDL_Log("C: Failed to create texture: %s\n", SDL_GetError());
+        return lean_io_result_mk_ok(lean_box(0));
+    }
+
+    return lean_io_result_mk_ok(lean_box(1));
+}
+
+lean_obj_res sdl_render_texture_column(uint32_t dst_x, uint32_t dst_y, uint32_t dst_height, uint32_t src_x, uint32_t src_y_start, uint32_t src_y_end, lean_obj_arg w) {
+    if (!g_renderer || !g_wall_texture) return lean_io_result_mk_ok(lean_box_uint32(-1));
+
+    uint32_t tex_y_start = src_y_start >= 64 ? 0 : src_y_start;
+    uint32_t tex_y_end = src_y_end > 64 ? 64 : src_y_end;
+    if (tex_y_end <= tex_y_start) tex_y_end = tex_y_start + 1;
+
+    SDL_FRect src_rect = {(float)(src_x % 64), (float)tex_y_start, 1.0f, (float)(tex_y_end - tex_y_start)};
+    SDL_FRect dst_rect = {(float)dst_x, (float)dst_y, 1.0f, (float)dst_height};
+
+    return lean_io_result_mk_ok(lean_box_uint32(SDL_RenderTexture(g_renderer, g_wall_texture, &src_rect, &dst_rect)));
+}