Initial commit

.gitignore

@@ -0,0 +1 @@
+.lake/

Engine.lean

@@ -0,0 +1,197 @@
+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 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 := 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
+
+  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
+
+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
+    newX := newX + Float.cos camera.angle * moveSpeed
+    newY := newY + Float.sin camera.angle * moveSpeed
+  if ← isKeyDown .S then
+    newX := newX - Float.cos camera.angle * moveSpeed
+    newY := newY - Float.sin camera.angle * moveSpeed
+  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 := 87, g := 127, b := 137 }
+  let _ ← SDL.renderClear
+
+  let camera := state.camera
+  let rayAngleStep := 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 wallStart := max 0 ((SCREEN_HEIGHT.toFloat - wallHeight) / 2).toInt32
+    let wallEnd := min (SCREEN_HEIGHT - 1) (wallStart + wallHeight.toInt32)
+    let xPos := column.toInt32
+
+    if wallStart > 0 then
+      setColor { r := 135, g := 206, b := 235 }
+      fillRect xPos 0 1 wallStart
+
+    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 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)
+
+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) == 0 do
+    IO.println "Failed to initialize SDL"
+    return
+
+  unless (← SDL.createWindow "LeanDoomed" 100 100 SCREEN_WIDTH SCREEN_HEIGHT SDL.SDL_WINDOW_SHOWN) != 0 do
+    IO.println "Failed to create window"
+    SDL.quit
+    return
+
+  unless (← SDL.createRenderer 4294967295 SDL.SDL_RENDERER_ACCELERATED) != 0 do
+    IO.println "Failed to create renderer"
+    SDL.quit
+    return
+
+  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

Main.lean

@@ -0,0 +1,4 @@
+import Engine
+
+def main : IO Unit := do
+  Engine.run

README.md

@@ -0,0 +1,21 @@
+# Lean SDL2 Bindings Example
+
+Playing around with SDL2 bindings in Lean4 to learn about the FFI.
+
+Simple real-time Doom-style raycasting engine in Lean4:
+
+![Screenshot](screenshots/screenshot1.png)
+
+## Run
+
+This is just an experiment and the build is currently specific to my system (Ubuntu 24.04.2).
+
+**You need to install dependencies and adjust paths in lakefile.lean!**
+
+```bash
+lake exe LeanDoomed
+```
+
+## License
+
+MIT

SDL.lean

@@ -0,0 +1,53 @@
+namespace SDL
+
+def SDL_INIT_VIDEO : UInt32 := 0x00000020
+def SDL_WINDOW_SHOWN : UInt32 := 0x00000004
+def SDL_RENDERER_ACCELERATED : UInt32 := 0x00000002
+def SDL_QUIT : UInt32 := 0x100
+
+def SDL_SCANCODE_W : UInt32 := 26
+def SDL_SCANCODE_A : UInt32 := 4
+def SDL_SCANCODE_S : UInt32 := 22
+def SDL_SCANCODE_D : UInt32 := 7
+def SDL_SCANCODE_LEFT : UInt32 := 80
+def SDL_SCANCODE_RIGHT : UInt32 := 79
+def SDL_SCANCODE_SPACE : UInt32 := 44
+def SDL_SCANCODE_ESCAPE : UInt32 := 41
+
+@[extern "sdl_init"]
+opaque init : UInt32 → IO UInt32
+
+@[extern "sdl_quit"]
+opaque quit : IO Unit
+
+@[extern "sdl_create_window"]
+opaque createWindow : String → Int32 → Int32 → Int32 → Int32 → UInt32 → IO UInt32
+
+@[extern "sdl_create_renderer"]
+opaque createRenderer : UInt32 → UInt32 → IO UInt32
+
+@[extern "sdl_set_render_draw_color"]
+opaque setRenderDrawColor : UInt8 → UInt8 → UInt8 → UInt8 → IO Int32
+
+@[extern "sdl_render_clear"]
+opaque renderClear : IO Int32
+
+@[extern "sdl_render_present"]
+opaque renderPresent : IO Unit
+
+@[extern "sdl_render_fill_rect"]
+opaque renderFillRect : Int32 → Int32 → Int32 → Int32 → IO Int32
+
+@[extern "sdl_delay"]
+opaque delay : UInt32 → IO Unit
+
+@[extern "sdl_poll_event"]
+opaque pollEvent : IO UInt32
+
+@[extern "sdl_get_ticks"]
+opaque getTicks : IO UInt32
+
+@[extern "sdl_get_key_state"]
+opaque getKeyState : UInt32 → IO Bool
+
+end SDL

c/sdl.c

@@ -0,0 +1,102 @@
+#include <stdint.h>
+#include <SDL2/SDL.h>
+#include <SDL2/SDL_image.h>
+#include <lean/lean.h>
+
+static SDL_Window* g_window = NULL;
+static SDL_Renderer* g_renderer = NULL;
+
+uint32_t sdl_get_version(void) {
+    SDL_version compiled;
+    SDL_VERSION(&compiled);
+    return compiled.major * 100 + compiled.minor * 10 + compiled.patch;
+}
+
+lean_obj_res sdl_init(uint32_t flags, lean_obj_arg w) {
+    int32_t result = SDL_Init(flags);
+    return lean_io_result_mk_ok(lean_box_uint32(result));
+}
+
+lean_obj_res sdl_quit(lean_obj_arg w) {
+    if (g_renderer) {
+        SDL_DestroyRenderer(g_renderer);
+        g_renderer = NULL;
+    }
+    if (g_window) {
+        SDL_DestroyWindow(g_window);
+        g_window = NULL;
+    }
+    SDL_Quit();
+    return lean_io_result_mk_ok(lean_box(0));
+}
+
+lean_obj_res sdl_create_window(lean_obj_arg title, uint32_t x, uint32_t y, uint32_t w, uint32_t h, uint32_t flags, lean_obj_arg world) {
+    const char* title_str = lean_string_cstr(title);
+    g_window = SDL_CreateWindow(title_str, (int)x, (int)y, (int)w, (int)h, flags);
+    if (g_window == NULL) {
+        return lean_io_result_mk_ok(lean_box(0));
+    }
+    return lean_io_result_mk_ok(lean_box(1));
+}
+
+lean_obj_res sdl_create_renderer(uint32_t index_unsigned, uint32_t flags, lean_obj_arg w) {
+    if (g_window == NULL) {
+        printf("C: No window available for renderer creation\n");
+        return lean_io_result_mk_ok(lean_box(0));
+    }
+    int32_t index = (int32_t)index_unsigned;
+    g_renderer = SDL_CreateRenderer(g_window, index, flags);
+    if (g_renderer == NULL) {
+        const char* error = SDL_GetError();
+        printf("C: SDL_CreateRenderer failed: %s\n", error);
+        return lean_io_result_mk_ok(lean_box(0));
+    }
+    return lean_io_result_mk_ok(lean_box(1));
+}
+
+lean_obj_res sdl_set_render_draw_color(uint8_t r, uint8_t g, uint8_t b, uint8_t a, lean_obj_arg w) {
+    if (g_renderer == NULL) return lean_io_result_mk_ok(lean_box_uint32(-1));
+    int32_t result = SDL_SetRenderDrawColor(g_renderer, r, g, b, a);
+    return lean_io_result_mk_ok(lean_box_uint32(result));
+}
+
+lean_obj_res sdl_render_clear(lean_obj_arg w) {
+    if (g_renderer == NULL) return lean_io_result_mk_ok(lean_box_uint32(-1));
+    int32_t result = SDL_RenderClear(g_renderer);
+    return lean_io_result_mk_ok(lean_box_uint32(result));
+}
+
+lean_obj_res sdl_render_present(lean_obj_arg w) {
+    if (g_renderer == NULL) return lean_io_result_mk_ok(lean_box(0));
+    SDL_RenderPresent(g_renderer);
+    return lean_io_result_mk_ok(lean_box(0));
+}
+
+lean_obj_res sdl_render_fill_rect(uint32_t x, uint32_t y, uint32_t w, uint32_t h, lean_obj_arg world) {
+    if (g_renderer == NULL) return lean_io_result_mk_ok(lean_box_uint32(-1));
+    SDL_Rect rect = {(int)x, (int)y, (int)w, (int)h};
+    int32_t result = SDL_RenderFillRect(g_renderer, &rect);
+    return lean_io_result_mk_ok(lean_box_uint32(result));
+}
+
+lean_obj_res sdl_delay(uint32_t ms, lean_obj_arg w) {
+    SDL_Delay(ms);
+    return lean_io_result_mk_ok(lean_box(0));
+}
+
+lean_obj_res sdl_poll_event(lean_obj_arg w) {
+    SDL_Event event;
+    int has_event = SDL_PollEvent(&event);
+    return lean_io_result_mk_ok(lean_box_uint32(has_event ? event.type : 0));
+}
+
+lean_obj_res sdl_get_ticks(lean_obj_arg w) {
+    uint32_t ticks = SDL_GetTicks();
+    return lean_io_result_mk_ok(lean_box_uint32(ticks));
+}
+
+lean_obj_res sdl_get_key_state(uint32_t scancode, lean_obj_arg w) {
+    const uint8_t* state = SDL_GetKeyboardState(NULL);
+    uint8_t pressed = state[scancode];
+    return lean_io_result_mk_ok(lean_box(pressed));
+}

lake-manifest.json

@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "LeanDoomed",
+ "lakeDir": ".lake"}

lakefile.lean

@@ -0,0 +1,30 @@
+import Lake
+open System Lake DSL
+
+package LeanDoomed
+
+input_file sdl.c where
+  path := "c" / "sdl.c"
+  text := true
+
+target sdl.o pkg : FilePath := do
+  let srcJob ← sdl.c.fetch
+  let oFile := pkg.buildDir / "c" / "sdl.o"
+  let leanInclude := "/home/ooo/.elan/toolchains/leanprover--lean4---v4.22.0/include"
+  buildO oFile srcJob #[] #["-fPIC", "-I/usr/include/SDL2", "-D_REENTRANT", s!"-I{leanInclude}"] "cc"
+
+target libleansdl pkg : FilePath := do
+  let sdlO ← sdl.o.fetch
+  let name := nameToStaticLib "leansdl"
+  buildStaticLib (pkg.staticLibDir / name) #[sdlO]
+
+lean_lib SDL where
+  moreLinkObjs := #[libleansdl]
+  moreLinkArgs := #["-lSDL2", "-lSDL2_image"]
+
+lean_lib Engine
+
+@[default_target]
+lean_exe LeanDoomed where
+  root := `Main
+  moreLinkArgs := #["/usr/lib/x86_64-linux-gnu/libSDL2.so", "/usr/lib/x86_64-linux-gnu/libSDL2_image.so"]

lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.22.0