import SDL structure Color where r : UInt8 g : UInt8 b : UInt8 a : UInt8 := 255 structure EngineState where window : SDL.SDLWindow renderer : SDL.SDLRenderer deltaTime : Float lastTime : UInt64 running : Bool playerX : Int32 playerY : Int32 texture : SDL.SDLTexture font : SDL.SDLFont mixer : SDL.SDLMixer track : SDL.SDLTrack audio : SDL.SDLAudio def SCREEN_WIDTH : Int32 := 1280 def SCREEN_HEIGHT : Int32 := 720 def TEXTURE_SIZE : Float := 64.0 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 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 () def renderScene (state : EngineState) : IO Unit := do setColor state.renderer { r := 135, g := 206, b := 235 } let _ ← SDL.renderClear state.renderer setColor state.renderer { r := 255, g := 0, b := 0 } fillRect state.renderer state.playerX state.playerY 100 100 let _ ← SDL.renderEntireTexture state.renderer state.texture 500 150 64 64 let _ ← SDL.renderTexture state.renderer state.texture 0 0 10 30 100 150 64 100 let message := "Hello, Lean SDL!" let textSurface ← SDL.textToSurface state.renderer state.font message 50 50 255 255 255 255 let textTexture ← SDL.createTextureFromSurface state.renderer textSurface let textWidth ← SDL.getTextureWidth textTexture let textHeight ← SDL.getTextureHeight textTexture let _ ← SDL.renderEntireTexture state.renderer textTexture 50 50 textWidth textHeight pure () 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 mut playerX := state.playerX let mut playerY := state.playerY if ← isKeyDown .A then playerX := playerX - 1 if ← isKeyDown .D then playerX := playerX + 1 if ← isKeyDown .W then playerY := playerY - 1 if ← isKeyDown .S then playerY := playerY + 1 engineState.set { state with deltaTime, lastTime := currentTime, playerX, playerY } 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 }) if eventType == SDL.SDL_MOUSEBUTTONDOWN then let (mouseX, mouseY) ← SDL.getMousePos if ← SDL.isLeftMousePressed then IO.println s!"Left click at ({mouseX}, {mouseY})" if ← SDL.isRightMousePressed then IO.println s!"Right click at ({mouseX}, {mouseY})" if ← SDL.isMiddleMousePressed then IO.println s!"Middle click at ({mouseX}, {mouseY})" let state ← engineState.get if state.running then renderScene state SDL.renderPresent state.renderer gameLoop engineState partial def run : IO Unit := do unless (← SDL.init SDL.SDL_INIT_VIDEO) == 1 do IO.println "Failed to initialize SDL" return let window ← try SDL.createWindow "LeanDoomed" SCREEN_WIDTH SCREEN_HEIGHT SDL.SDL_WINDOW_SHOWN catch sdlError => IO.println sdlError SDL.quit return let renderer ← try SDL.createRenderer window catch sdlError => IO.println sdlError SDL.quit return let texture ← try SDL.loadImageTexture renderer "assets/wall.png" catch sdlError => IO.println sdlError SDL.quit return unless (← SDL.ttfInit) do IO.println "Failed to initialize SDL_ttf" SDL.quit return let font ← try SDL.loadFont "assets/Inter-VariableFont.ttf" 24 catch sdlError => IO.println sdlError SDL.quit return unless (← SDL.mixerInit) do IO.println "Failed to initialize SDL_mixer" SDL.quit return let mixer ← try SDL.createMixer () catch sdlError => IO.println sdlError SDL.quit return let track ← try SDL.createTrack mixer catch sdlError => IO.println sdlError SDL.quit return let audio ← try SDL.loadAudio mixer "assets/In_The_Dark_Flashes.mp3" catch sdlError => IO.println sdlError SDL.quit return match (← SDL.setTrackAudio track audio) with | true => pure () | false => IO.println s!"Failed to set track audio" SDL.quit return match (← SDL.playTrack track) with | true => pure () | false => IO.println s!"Failed to play track" SDL.quit return let initialState : EngineState := { window := window, renderer := renderer deltaTime := 0.0, lastTime := 0, running := true playerX := (SCREEN_WIDTH / 2), playerY := (SCREEN_HEIGHT / 2) texture := texture, mixer := mixer, track := track, audio := audio, font := font } let engineState ← IO.mkRef initialState IO.println "Starting game loop..." gameLoop engineState SDL.quit def EngineState.setRunning (state : EngineState) (running : Bool) : EngineState := { state with running } def main : IO Unit := run