Render buildings

Changes

2 changed files (+123/-44)

• Main.lean
  • @@ -3,43 +3,73 @@ import Raylean
    open Raylean Types + namespace Raylean + + /-- This is in Raylib but not Raylean so let's just define it ourselves -/ + def drawCubeV (pos size : Vector3) (color : Color) := + drawCube pos size.x size.y size.z color + + def drawCubeWiresV (pos size : Vector3) (color : Color) := + drawCubeWires pos size.x size.y size.z color + + end Raylean + def fps := 60 def screenWidth := 960 def screenHeight := 640 + /-- Grid side length -/ + def N := 500 + + /-- Grid height -/ + def M := 20 + + def origin : Vector3 := ⟨N.toFloat / 20, M.toFloat / 20, N.toFloat / 20⟩ + + instance : Add Vector3 where + add a b := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩ + + instance : Sub Vector3 where + sub a b := ⟨a.x - b.x, a.y - b.y, a.z - b.z⟩ + + instance : HDiv Vector3 Float Vector3 where + hDiv a b := ⟨a.x / b, a.y / b, a.z / b⟩ + structure Nat3 where x : Nat y : Nat z : Nat + deriving Lean.ToJson, Lean.FromJson - 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 - return { - up := ← isKeyDown Key.up, - down := ← isKeyDown Key.down, - left := ← isKeyDown Key.left, - right := ← isKeyDown Key.right - } + inductive BuildingVariant + | house + | apartment + | office + | shop + | factory + deriving Lean.ToJson, Lean.FromJson + + structure Building where + pos : Nat3 + size : Nat3 + variant : BuildingVariant + deriving Lean.ToJson, Lean.FromJson + def Building.occupants (b : Building) := + match b.variant with + | .house => 1 + | .apartment => b.size.x * b.size.y * b.size.z / 2 + | .office => 0 + | .shop => 0 + | .factory => 0 + + def Building.color (b : Building) := + match b.variant with + | .house => Color.Raylean.red + | .apartment => Color.Raylean.orange + | .office => Color.Raylean.blue + | .shop => Color.Raylean.purple + | .factory => Color.Raylean.green structure Vehicle where pos : Nat3
  • @@ -52,22 +82,36 @@ inductive Road
    | high deriving Lean.ToJson, Lean.FromJson + instance [Lean.ToJson α] : Lean.ToJson (Vector α n) where + toJson := Array.toJson ∘ Vector.toArray + + instance [Lean.FromJson α] : Lean.FromJson (Vector α n) where + fromJson? j := do + let A : Array α ← Array.fromJson? j + if h : A.size = n then + return h ▸ A.toVector + else + throw s!"expected size {n}, got {A.size}" + structure Point where roads : Vector Road 24 occupant : Option Nat + deriving Lean.ToJson, Lean.FromJson - def Grid h w := Vector (Vector Point w) h - - def Tick (g : Grid h w) : Grid h w := Id.run do - return g + def Point.empty : Point := + ⟨.replicate 24 .none, none⟩ + abbrev Grid := Vector (Vector (Vector Point (M + 1)) (N + 1)) (N + 1) structure State where - datetime : Std.Time.PlainDateTime - height : Nat - width : Nat - grid : Grid height width - -- deriving Lean.ToJson, Lean.FromJson + day : Nat + time : Nat + grid : Grid + buildings : Array Building + deriving Lean.ToJson, Lean.FromJson + + def tick (g : Grid) : Grid := Id.run do + return g def myroad : Road := .low
  • @@ -76,6 +120,19 @@ def serialized := Lean.toJson myroad |>.compress
    def blah : Except String Road := Lean.Json.parse serialized >>= Lean.fromJson? + def Nat3.toVector3 (p : Nat3) : Vector3 := + ⟨p.x.toFloat / 10, p.y.toFloat / 10, p.z.toFloat / 10⟩ + + instance : ToString Vector3 := ⟨fun v ↦ s!"({v.1}, {v.2}, {v.3})"⟩ + + def render (s : State) : IO Unit := do + for b in s.buildings do + let p := b.pos.toVector3 + let s := b.size.toVector3 + let o := p - origin + s / 2.0 + drawCubeV o s b.color + drawCubeWiresV o s .black + def main : IO Unit := do -- This constant is FLAG_WINDOW_HIGHDPI || FLAG_WINDOW_RESIZABLE -- https://github.com/raysan5/raylib/blob/aaacda6e147031f2af0cfb6c1fd7e64d761ddb1f/src/raylib.h#L567
  • @@ -89,17 +146,18 @@ def main : IO Unit := do
    fovy := 45 projection := .perspective } - let mut ballPosition := initialBallPosition - while not (← windowShouldClose) do + let mut s : State := { + day := 0 + time := 0 + grid := Vector.replicate _ (Vector.replicate _ (Vector.replicate _ .empty)) + buildings := #[⟨⟨250, 10, 250⟩, ⟨20, 5, 5⟩, .apartment⟩] + } + while !(← windowShouldClose) do camera ← updateCamera camera .thirdPerson - 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 + drawGrid (N / 20) 1 + render s closeWindow
• README.md
  • @@ -44,3 +44,24 @@ The internal data representation of the game is a 2D vector for the grid for fas
    First step: render the grid using raylib Street names + + + TODO: bundle seems to be missing deps? + + NFO: Initializing raylib 6.0 + INFO: Platform backend: DESKTOP (GLFW) + INFO: Supported raylib modules: + INFO: > rcore:..... loaded (mandatory) + INFO: > rlgl:...... loaded (mandatory) + INFO: > rshapes:... loaded (optional) + INFO: > rtextures:. loaded (optional) + INFO: > rtext:..... loaded (optional) + INFO: > rmodels:... loaded (optional) + INFO: > raudio:.... loaded (optional) + Fontconfig error: Cannot load default config file: No such file: (null) + Gtk-Message: 19:24:22.735: Failed to load module "colorreload-gtk-module" + Gtk-Message: 19:24:22.735: Failed to load module "window-decorations-gtk-module" + WARNING: GLFW: Error: 65542 Description: EGL: Failed to get EGL display: Success + WARNING: GLFW: Failed to initialize Window + WARNING: SYSTEM: Failed to initialize platform + INFO: TIMER: Target time per frame: 16.667 milliseconds