import SDL namespace Engine structure Color where r : UInt8 g : UInt8 b : UInt8 a : UInt8 := 255 structure Camera where x : Float y : Float angle : Float speed : Float := 3.0 turnSpeed : Float := 2.0 abbrev Map := Array (Array UInt8) structure EngineState where deltaTime : Float lastTime : UInt32 running : Bool camera : Camera gameMap : Map 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], #[1,0,0,0,0,0,0,0,0,1], #[1,0,1,0,0,0,0,1,0,1], #[1,0,0,0,0,0,0,0,0,1], #[1,0,0,0,1,1,0,0,0,1], #[1,0,0,0,1,1,0,0,0,1], #[1,0,0,0,0,0,0,0,0,1], #[1,0,1,0,0,0,0,1,0,1], #[1,0,0,0,0,0,0,0,0,1], #[1,1,1,1,1,1,1,1,1,1] ] inductive Key where | W | A | S | D | Left | Right | Space | Escape def keyToScancode : Key → UInt32 | .W => SDL.SDL_SCANCODE_W | .A => SDL.SDL_SCANCODE_A | .S => SDL.SDL_SCANCODE_S | .D => SDL.SDL_SCANCODE_D | .Left => SDL.SDL_SCANCODE_LEFT | .Right => SDL.SDL_SCANCODE_RIGHT | .Space => SDL.SDL_SCANCODE_SPACE | .Escape => SDL.SDL_SCANCODE_ESCAPE def isKeyDown (key : Key) : IO Bool := SDL.getKeyState (keyToScancode key) def isWall (mapp : Map) (x y : Float) : Bool := if x < 0.0 || y < 0.0 then true else let mapX := x.floor.toUInt32.toNat 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 × Float := Id.run do let rayDirX := Float.cos angle let rayDirY := Float.sin angle let mut mapX := startX.floor let mut mapY := startY.floor let deltaDistX := if rayDirX == 0.0 then 1e30 else Float.abs (1.0 / rayDirX) let deltaDistY := if rayDirY == 0.0 then 1e30 else Float.abs (1.0 / rayDirY) let stepX := if rayDirX < 0.0 then -1 else 1 let mut sideDistX := if rayDirX < 0.0 then (startX - mapX) * deltaDistX else (mapX + 1.0 - startX) * deltaDistX let stepY := if rayDirY < 0.0 then -1 else 1 let mut sideDistY := if rayDirY < 0.0 then (startY - mapY) * deltaDistY else (mapY + 1.0 - startY) * deltaDistY let mut hit := false let mut side := 0 for _ in [0:25] do if hit then break if sideDistX < sideDistY then sideDistX := sideDistX + deltaDistX mapX := mapX + Float.ofInt stepX side := 0 else sideDistY := sideDistY + deltaDistY mapY := mapY + Float.ofInt stepY side := 1 hit := isWall map mapX mapY 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 checkCollision (map : Map) (x y : Float) (radius : Float := 0.3) : Bool := let corners := #[ (x - radius, y - radius), (x + radius, y - radius), (x - radius, y + radius), (x + radius, y + radius) ] corners.any (fun (cx, cy) => isWall map cx cy) def updateCamera (camera : Camera) (deltaTime : Float) : IO Camera := do let moveSpeed := camera.speed * deltaTime let mut newX := camera.x let mut newY := camera.y let mut newAngle := camera.angle if ← isKeyDown .W then let testX := camera.x + Float.cos camera.angle * moveSpeed let testY := camera.y + Float.sin camera.angle * moveSpeed if !checkCollision sampleMap testX camera.y then newX := testX if !checkCollision sampleMap camera.x testY then newY := testY if ← isKeyDown .S then let testX := camera.x - Float.cos camera.angle * moveSpeed let testY := camera.y - Float.sin camera.angle * moveSpeed if !checkCollision sampleMap testX camera.y then newX := testX if !checkCollision sampleMap camera.x testY then newY := testY if ← isKeyDown .A then newAngle := newAngle - camera.turnSpeed * deltaTime if ← isKeyDown .D then newAngle := newAngle + camera.turnSpeed * deltaTime pure { camera with x := newX, y := newY, angle := newAngle } def setColor (color : Color) : IO Unit := SDL.setRenderDrawColor color.r color.g color.b color.a *> pure () 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 := 135, g := 206, b := 235 } let _ ← SDL.renderClear let rayStep := FOV / SCREEN_WIDTH.toFloat for column in [0:SCREEN_WIDTH.toNatClampNeg] do 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 := (SCREEN_HEIGHT.toFloat - wallHeight) / 2 let visibleStart := max 0 wallStart let visibleEnd := min SCREEN_HEIGHT.toFloat (wallStart + wallHeight) let wallStartInt := visibleStart.toInt32 let wallEndInt := visibleEnd.toInt32 let wallHeightInt := wallEndInt - wallStartInt 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) 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 let currentTime ← SDL.getTicks let deltaTime := (currentTime - state.lastTime).toFloat / 1000.0 let newCamera ← updateCamera state.camera deltaTime engineState.set { state with deltaTime, lastTime := currentTime, camera := newCamera } partial def gameLoop (engineState : IO.Ref EngineState) : IO Unit := do updateEngineState engineState let eventType ← SDL.pollEvent if eventType == SDL.SDL_QUIT || (← isKeyDown .Escape) then engineState.modify (fun s => { s with running := false }) let state ← engineState.get if state.running then renderScene state SDL.renderPresent gameLoop engineState partial def run : IO Unit := do unless (← SDL.init SDL.SDL_INIT_VIDEO) == 1 do IO.println "Failed to initialize SDL" return unless (← SDL.createWindow "LeanDoomed" SCREEN_WIDTH SCREEN_HEIGHT SDL.SDL_WINDOW_SHOWN) != 0 do IO.println "Failed to create window" 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, camera := { x := 1.5, y := 1.5, angle := 0.0 }, gameMap := sampleMap } let engineState ← IO.mkRef initialState IO.println "Use WASD to move, A/D to turn, ESC to quit" gameLoop engineState SDL.quit def EngineState.setRunning (state : EngineState) (running : Bool) : EngineState := { state with running } end Engine