Changes
1 changed files (+87/-63)
-
-
@@ -13,8 +13,8 @@namespace Raylean -- https://github.com/raysan5/raylib/blob/aaacda6e147031f2af0cfb6c1fd7e64d761ddb1f/src/raylib.h#L567 def Flags.window_resizable : UInt64 :=0x00000004 def Flags.window_highdpi : UInt64 :=0x00002000 def Flags.window_resizable : UInt64 := 0x00000004 def Flags.window_highdpi : UInt64 := 0x00002000 -- Helpful for debugging instance : ToString Vector3 := ⟨fun a ↦ s!"({a.x}, {a.y}, {a.z})"⟩
-
@@ -144,10 +144,10 @@ | .shop => Color.Raylean.purple| .factory => Color.Raylean.green def cost (b : Building) := b.size.x * b.size.y * b.size.z * b.size.z * 100 * b.size.x * b.size.y * b.size.z * b.size.z * match b.variant with | .house => 5 | .apartment => 1 | .house => 1 | .apartment => 2 | .office => 2 | .shop => 5 | .factory => 10
-
@@ -164,19 +164,6 @@ #guard !checkCollide ⟨10, 10, 10⟩ ⟨5, 5, 5⟩ ⟨0, 8, 14⟩ ⟨5, 5, 5⟩end Building /- instance : Lean.ToJson (Fin n) where toJson := Lean.toJson ∘ Fin.val instance : Lean.FromJson (Fin n) where fromJson? j := do let m ← Lean.fromJson? j if h : m < n then return ⟨m, h⟩ else throw s!"expected val less than {n}, got {m}" -/ structure Peep where home : Nat work : Nat
-
@@ -227,8 +214,8 @@ def Road.cost (r : Road) (dir y : Nat) :=(if y == 0 && dy dir == 0 then 1 else 10) * match r with | none => 0 | low => 1 | high => 5 | low => 2 | high => 10 instance [Lean.ToJson α] : Lean.ToJson (Vector α n) where toJson := Array.toJson ∘ Vector.toArray
-
@@ -398,7 +385,7 @@ if p.dest == p.home then-- At home, go to work or shops if (← rand 1000) == 0 then p' := { p' with dest := p.work } else if h : (← rand 1000) == 0 && !s.shops.isEmpty then else if h : (← rand 500) == 0 && !s.shops.isEmpty then let shopIdx ← rand s.shops.size p' := { p' with dest := shopIdx } else if p.dest == p.work then
-
@@ -447,6 +434,10 @@ pure ()neighbors := neighbors.qsort (fun a b ↦ a.1 < b.1 || (a.1 == b.1 && a.2 < b.2)) let mut moved := false for (d, i) in neighbors do -- if d ≥ min (neighbors[0]!.1 + 100) (2 * neighbors[0]!.1 + 5) then -- Don't move if this makes us take a really long detour -- TODO better heuristic -- break let v := u.appd i if i < 27 then if s.occupied.contains v || occupied.contains v || occupiedMid.contains (u + v) then
-
@@ -611,8 +602,11 @@ if (← get).grid.contains u then-- Yeah this is not ideal but Lean doesn't know the two `← get`s are the same name := (← get).grid[u]!.name if name == "" then have : 0 < street_names.size := by native_decide name := street_names[← rand street_names.size] if isHigh then name := s!"Highway {(← rand 998) + 1}" else have : 0 < street_names.size := by native_decide name := s!"{street_names[← rand street_names.size]} Street" for i in List.range (length + 1) do let v := start.appdk dir i modifyf grid fun g ↦ Id.run do
-
@@ -624,15 +618,44 @@ if i < length then { p with e := p.e.set! dir road } else p)mkDists def addYield (pos : Nat3) : StateT State IO Unit := do spend 10 if !(← get).grid.contains pos then throw <| .userError s!"Could not place yield at {pos}" modifyf grid (·.modify pos fun p ↦ { p with isYield := true }) def addTrafficLight (pos : Nat3) (t : TrafficLight) : StateT State IO Unit := do spend 100 if !(← get).grid.contains pos then throw <| .userError s!"Could not place traffic light at {pos}" modifyf grid (·.modify pos fun p ↦ { p with trafficLight := some t }) def addIntersection (pos : Nat3) : StateT State IO Unit := do -- Main roads addRoad (pos + ⟨0, 0, 3⟩) (pos + ⟨5, 0, 3⟩) false addRoad (pos + ⟨5, 0, 2⟩) (pos + ⟨0, 0, 2⟩) false addRoad (pos + ⟨2, 0, 0⟩) (pos + ⟨2, 0, 5⟩) false addRoad (pos + ⟨3, 0, 5⟩) (pos + ⟨3, 0, 0⟩) false -- Right turns addRoad (pos + ⟨2, 0, 0⟩) (pos + ⟨0, 0, 2⟩) false addRoad (pos + ⟨0, 0, 3⟩) (pos + ⟨2, 0, 5⟩) false addRoad (pos + ⟨3, 0, 5⟩) (pos + ⟨5, 0, 3⟩) false addRoad (pos + ⟨5, 0, 2⟩) (pos + ⟨3, 0, 0⟩) false -- Left turns addRoad (pos + ⟨2, 0, 2⟩) (pos + ⟨3, 0, 3⟩) false addRoad (pos + ⟨3, 0, 3⟩) (pos + ⟨2, 0, 2⟩) false addRoad (pos + ⟨2, 0, 3⟩) (pos + ⟨3, 0, 2⟩) false addRoad (pos + ⟨3, 0, 2⟩) (pos + ⟨2, 0, 3⟩) false -- Traffic lights addTrafficLight (pos + ⟨1, 0, 3⟩) ⟨10, 10, 0⟩ addTrafficLight (pos + ⟨4, 0, 2⟩) ⟨10, 10, 0⟩ addTrafficLight (pos + ⟨2, 0, 1⟩) ⟨10, 10, 10⟩ addTrafficLight (pos + ⟨3, 0, 4⟩) ⟨10, 10, 10⟩ -- Yields addYield (pos + ⟨1, 0, 1⟩) addYield (pos + ⟨4, 0, 1⟩) addYield (pos + ⟨1, 0, 4⟩) addYield (pos + ⟨4, 0, 4⟩) def handleCmd (cmd : String) : StateT State IO Unit := do match cmd.split ' ' |>.toStringList with | ["s", path] =>
-
@@ -640,7 +663,7 @@ IO.FS.writeFile path <| Lean.toJson (← get) |>.compress| ["l", path] => set <| ← loadState path | ["v", speed] => setf speed (String.toNat! speed) setf speed (sensitivity * String.toNat! speed) | "d" :: dims => if h : dims.length = 6 then let dims := dims.map String.toNat!
-
@@ -671,6 +694,11 @@ if h : dims.length = 6 thenlet dims := dims.map String.toNat! have : dims.length = 6 := by grind addTrafficLight ⟨dims[0], dims[1], dims[2]⟩ ⟨dims[3], dims[4], dims[5]⟩ | "i" :: dims => if h : dims.length = 3 then let dims := dims.map String.toNat! have : dims.length = 3 := by grind addIntersection ⟨dims[0], dims[1], dims[2]⟩ | ["n", oldName, newName] => modifyf grid (·.map fun _ p ↦ if p.name == oldName then { p with name := newName } else p)
-
@@ -687,9 +715,9 @@def Nat3.toVector3Shift (pos : Nat3) (s : State) : Vector3 := pos.toVector3 - s.origin.toVector3 /-- `speed == 0` means paused -/ /-- Low `speed` means paused -/ def maxFrames (speed : Nat) := if speed == 0 then 2 ^ 32 else fps / ticksPerSecond / speed if speed < sensitivity then 2 ^ 32 else fps / ticksPerSecond / (speed / sensitivity) /-- Draw the game state -/ def render (s : State) (camera : Camera3D) (frames : Nat) : IO Unit := do
-
@@ -710,15 +738,8 @@ let pos2D ← getWorldToScreen (posV3 + ⟨0, 0.2, 0⟩) cameraendMode3D let address := if b.entrance.x == b.pos.x || b.entrance.x == b.pos.x + b.size.x then b.entrance.z else b.entrance.x drawText s!"{address} {name} Street" pos2D.x.toUInt64.toNat pos2D.y.toUInt64.toNat 10 Color.black drawText s!"{address} {name}" pos2D.x.toUInt64.toNat pos2D.y.toUInt64.toNat 10 Color.black beginMode3D camera -- Render road names -- for (pos, pt) in s.grid do -- if (2 * pos.x + pos.z) % 20 == 0 then -- -- https://www.raylib.com/examples/core/loader.html?name=core_world_screen -- let pos2D ← getWorldToScreen (pos.toVector3Shift s) camera -- let dir := pt.eout[di 1 0 0] != .none || pt.eout[di (-1) 0 0] != .none -- drawText s!"{if dir then pos.x else pos.z} {pt.name} Street" pos2D.x.toUInt64.toNat pos2D.y.toUInt64.toNat 10 Color.black -- Render roads for (pos, pt) in s.grid do let posV3 := pos.toVector3Shift s
-
@@ -754,7 +775,7 @@ | some i =>let m := (maxFrames s.speed).toFloat let ivec : Vector3 := ⟨.ofInt (dx i) / scale, .ofInt (dy i) / scale, .ofInt (dz i) / scale⟩ peep.pos.toVector3Shift s - (m - frames.toFloat - 1) / m * (if i < 27 then 1 else 2) * ivec drawCube (posV3 + ⟨0, 0.0025, 0⟩) 0.075 0.075 0.075 Color.Raylean.lime drawCube (posV3 + ⟨0, 0.0025, 0⟩) 0.075 0.075 0.075 Color.Raylean.skyblue drawCubeWires (posV3 + ⟨0, 0.0025, 0⟩) 0.075 0.075 0.075 .black /-- Get 3D coordinates at level `y` of 2D screen position
-
@@ -809,31 +830,31 @@ let randPos : StateT State IO Nat3 := doreturn ⟨(← get).origin.x - 50 + (← rand 100), 10, (← get).origin.z - 50 + (← rand 100)⟩ let randPosExt : StateT State IO Nat3 := do repeat let x ← rand 300 let z ← rand 300 if 100 < x && x < 200 && 100 < z && z < 200 then let x ← rand 200 let z ← rand 200 if 50 < x && x < 150 && 50 < z && z < 150 then continue return ⟨(← get).origin.x - 150 + x, 10, (← get).origin.z - 150 + z⟩ return ⟨(← get).origin.x - 100 + x, 10, (← get).origin.z - 100 + z⟩ -- Spawn the commerical buildings first so peeps' workplaces get evenly distributed among them for i in [:3] do let side ← rand 4 try addBuilding .office (← randPos) ⟨10, 2, 10⟩ (side, 5) (side, 6) addBuilding .office (← randPos) ⟨10, 2, 5⟩ (side, 2) (side, 3) catch e => IO.println e for i in [:5] do for i in [:10] do let side ← rand 4 try addBuilding .shop (← randPos) ⟨5, 1, 10⟩ (side, 3) (side, 4) catch e => IO.println e for i in [:2] do for i in [:5] do let side ← rand 4 try addBuilding .factory (← randPosExt) ⟨10, 4, 10⟩ (side, 5) (side, 6) addBuilding .factory (← randPosExt) ⟨10, 5, 10⟩ (side, 5) (side, 6) catch e => IO.println e for i in [:40] do for i in [:100] do let side ← rand 4 try addBuilding .house (← randPosExt) ⟨5, 1, 5⟩ (side, 2) (side, 3)
-
@@ -861,7 +882,6 @@ let mut task ← IO.asTask <| getInput stdinlet mut start : Option Nat3 := none let mut curAction := 1 let mut y : Int := 0 let mut speed' := sensitivity let mut frames := 0 while !(← windowShouldClose) do -- Fix `up` to prevent the Q and E keys from messing it up
-
@@ -880,27 +900,27 @@ | _, 4 =>addTrafficLight mousePos ⟨10, 10, 0⟩ | _, 5 => addTrafficLight mousePos ⟨10, 10, 10⟩ | _, 6 => addIntersection mousePos | none, _ => start := some mousePos | some pos', 1 => addRoad pos' mousePos false | some pos, 1 => addRoad pos mousePos false start := none | some pos', 2 => addRoad pos' mousePos true | some pos, 2 => addRoad pos mousePos true start := none | some pos', _ => delete pos' mousePos | some pos, _ => delete pos mousePos start := none catch e => IO.println e if (← isMouseButtonPressed MouseButton.right) then do start := none if (← isKeyDown Key.left) then do speed' := speed' - 1 setf speed (speed' / sensitivity) modifyf speed (· - 1) if (← isKeyDown Key.right) then do speed' := speed' + 1 setf speed (speed' / sensitivity) modifyf speed (· + 1) for i in [:10] do if (← isKeyDown <| '0'.toNat + i) then do curAction := i
-
@@ -918,17 +938,19 @@ elseframes := frames + 1 let s ← get renderFrame do drawFPS ((← getScreenWidth) - 100) 10 clearBackground Color.white let mousePosV3 ← getMouse3D y camera let mousePos := mousePosV3.toNat3Shift s let mousePosV3Snap := mousePos.toVector3Shift s renderWithCamera camera do render s camera frames -- For debugging: -- drawCubeV mousePosV3 ⟨0.1, 0.1, 0.1⟩ Color.Raylean.pink drawGrid (s.origin.x / scaleN * 2) 1 match start, curAction with | none, _ | _, 3 => | _, 3 | _, 4 | _, 5 => drawCubeV (mousePosV3Snap + ⟨0, 0.075, 0⟩) ⟨0.02, 0.02, 0.02⟩ Color.Raylean.lime | _, 6 => drawCubeV (mousePosV3Snap + ⟨0.25, 0, 0.25⟩) ⟨0.5, 0, 0.5⟩ Color.Raylean.gray | none, _ => pure () | some pos, 1 | some pos, 2 => let (length, dir) := endpointsToRoad pos mousePos
-
@@ -950,15 +972,17 @@ | 2 => "Build highway"| 3 => "Build yield" | 4 => "Build traffic light (phase 1)" | 5 => "Build traffic light (phase 2)" | 6 => "Build simple intersection" | _ => "Delete" drawText s!"Active control: {actionText}" 10 10 20 .black drawText s!"Time: {s.ticks / ticksPerSecond / 60 / 60}:{padTime <| s.ticks / ticksPerSecond / 60 % 60}:{padTime <| s.ticks / ticksPerSecond % 60}" 10 40 20 .black drawText s!"Money: ${s.money}" 10 70 20 .black drawText s!"Population: {s.peeps.size}" 10 100 20 .black drawText s!"Speed: {s.speed}" 10 130 20 .black drawText s!"Speed: {s.speed / sensitivity}" 10 130 20 .black drawText s!"{mousePos}" 10 160 20 .black if s.grid.contains mousePos then drawText s!"{s.grid[mousePos]!.name} Street" 10 190 20 .black drawText s!"{s.grid[mousePos]!.name}" 10 190 20 .black drawFPS ((← getScreenWidth) - 100) 10 closeWindow def main : IO Unit := do
-
@@ -968,9 +992,9 @@ setTargetFPS fpsgameLoop.run' { rng := mkStdGen (← IO.rand 0 (2 ^ 32)) ticks := 0 speed := 1 speed := sensitivity money := 2 ^ 32 -- The initial value doesn't matter since we spawn a bunch of buildings first origin := ⟨200, 10, 200⟩ origin := ⟨300, 10, 300⟩ grid := .ofList [] buildings := #[] unfull := #v[#[], #[]]
-