It's 3D!

Changes

3 changed files (+66/-47)

• Main.lean
  • @@ -3,48 +3,47 @@ import Raylean
    open Raylean Types - def screenWidth := 1280 - def screenHeight := 720 - - private def initialBallPosition : Vector2 := { x := screenWidth.toFloat / 2, y := screenHeight.toFloat / 2 } - - inductive Move where - | up - | down - | left - | right - | stay - - def updateBallPosition (d : Move) (p : Vector2) : Vector2 := match d with - | Move.right => { p with x := p.x + 2.0 } - | Move.left => { p with x := p.x - 2.0 } - | Move.up => { p with y := p.y - 2.0 } - | Move.down => { p with y := p.y + 2.0 } - | Move.stay => p + def fps := 60 + def screenWidth := 960 + def screenHeight := 640 + + structure Nat3 where + x : Nat + y : Nat + z : Nat + + def initialBallPosition : Vector3 := ⟨0, 0, 0⟩ + + structure Move where + up : Bool + down : Bool + left : Bool + right : Bool + + def updateBallPosition (d : Move) (p : Vector3) := Id.run do + let mut p := p + if d.up then + p := { p with z := p.z - 0.1 } + if d.down then + p := { p with z := p.z + 0.1 } + if d.left then + p := { p with x := p.x - 0.1 } + if d.right then + p := { p with x := p.x + 0.1 } + return p def getMove : IO Move := do - if (← isKeyDown Key.right) then return Move.right - else if (← isKeyDown Key.left) then return Move.left - else if (← isKeyDown Key.up) then return Move.up - else if (← isKeyDown Key.down) then return Move.down - else return Move.stay - - def doRender : IO Unit := do - let mut ballPosition := initialBallPosition - while not (← windowShouldClose) do - let d ← getMove - ballPosition := updateBallPosition d ballPosition - renderFrame do - drawFPS (screenWidth - 100) 10 - clearBackground Color.white - drawText "Move the ball with arrow keys" 10 10 20 Color.blue - drawCircleV ballPosition 50 Color.red - closeWindow + return { + up := ← isKeyDown Key.up, + down := ← isKeyDown Key.down, + left := ← isKeyDown Key.left, + right := ← isKeyDown Key.right + } structure Vehicle where - pos : Nat × Nat - dest : Nat × Nat + pos : Nat3 + dest : Nat3 inductive Road
  • @@ -77,11 +76,30 @@ def serialized := Lean.toJson myroad |>.compress
    def blah : Except String Road := Lean.Json.parse serialized >>= Lean.fromJson? - def main : IO Unit := do - -- This constant is FLAG_WINDOW_HIGHDPI + -- This constant is FLAG_WINDOW_HIGHDPI || FLAG_WINDOW_RESIZABLE -- https://github.com/raysan5/raylib/blob/aaacda6e147031f2af0cfb6c1fd7e64d761ddb1f/src/raylib.h#L567 - setConfigFlags 0x00002000 + setConfigFlags 0x00002004 initWindow screenWidth screenHeight "LeanTTD" - setTargetFPS 60 - doRender + setTargetFPS fps + let mut camera : Camera3D := { + position := ⟨10, 10, 10⟩ + target := ⟨0, 0, 0⟩ + up := ⟨0, 1, 0⟩ + fovy := 45 + projection := .perspective + } + let mut ballPosition := initialBallPosition + while not (← windowShouldClose) do + camera ← updateCamera camera .thridPerson + let d ← getMove + ballPosition := updateBallPosition d ballPosition + renderFrame do + drawFPS (screenWidth - 100) 10 + clearBackground Color.white + drawText "Move the ball with arrow keys" 10 10 20 Color.blue + renderWithCamera camera do + drawCube ballPosition 2 2 2 Color.red + drawCubeWires ballPosition 2 2 2 Color.blue + drawGrid 100 1 + closeWindow
• flake.nix
  • @@ -19,12 +19,13 @@
    # This fixes a linker error hardeningDisable = [ "bindnow" ]; postConfigure = '' - # Patch Raylean to fix a compilation error - patch -p1 < ./raylean.patch # Make sure the linker can find libraylib.so substituteInPlace lakefile.toml --replace-fail \ '["-lraylib"]' \ '["-L${pkgs.raylib}/lib", "-lraylib"]' + # Patch Raylean to fix a compilation error + cd .lake/packages/raylean + patch -p1 < ./raylean.patch ''; }; apps.${system}.default = {
• raylean.patch
  • @@ -1,7 +1,7 @@
    - diff --git a/.lake/packages/raylean/c/raylib_bindings.c b/.lake/packages/raylean/c/raylib_bindings.c + diff --git a/c/raylib_bindings.c b/c/raylib_bindings.c index 902a945..7539506 100644 - --- a/.lake/packages/raylean/c/raylib_bindings.c - +++ b/.lake/packages/raylean/c/raylib_bindings.c + --- a/c/raylib_bindings.c + +++ b/c/raylib_bindings.c @@ -314,11 +314,11 @@ static inline Camera2D camera2D_of_arg(lean_obj_arg camera) { return (Camera2D){offset, target, rotation, zoom}; }