Correctly implement deletion (hopefully)

Changes

2 changed files (+60/-24)

• Main.lean
  • @@ -137,7 +137,7 @@ size : Nat3
    entrance : Nat3 exit : Nat3 spots : Nat - deleted : Bool + isDeleted : Bool deriving Inhabited, Lean.ToJson, Lean.FromJson namespace Building
  • @@ -191,6 +191,7 @@ pos : Nat3
    dest : Nat dir : Option Nat brokenDown : Bool + isCommercial : Bool deriving BEq, Lean.ToJson, Lean.FromJson /-- Grid helper functions -/
  • @@ -390,7 +391,7 @@ /-- Precompute all distances -/
    def mkDists : StateM State Unit := do setf dists #[] for building in (← get).buildings do - if !building.deleted then + if !building.isDeleted then modifyf dists (·.push <| mkDist (← get).grid building.entrance) else modifyf dists (·.push <| .ofList [])
  • @@ -435,28 +436,28 @@ let u := p.pos
    let s := ← get if u == s.buildings[p.dest]!.entrance then if p.dir.isSome then - modifyf money (· + 100) + modifyf money (· + (if p.isCommercial then 1000 else 100)) let mut p' := { p with dir := none } if p.dest == p.home then -- At home, go to work or shops if (← rand homeToWorkProb) == 0 then - p' := { p' with dest := p.work } + p' := { p' with dest := p.work, isCommercial := false } else if h : (← rand toShopProb) == 0 && !s.shops.isEmpty then let shopIdx ← rand s.shops.size - p' := { p' with dest := shopIdx } + p' := { p' with dest := shopIdx, isCommercial := false } else if p.dest == p.work then -- At work, go to shops if factory worker else go home if h : s.buildings[p.work]!.variant == .factory && !s.shops.isEmpty && (← rand factoryToShopProb) == 0 then let shopIdx ← rand s.shops.size - p' := { p' with dest := shopIdx } + p' := { p' with dest := shopIdx, isCommercial := true } else if (← rand workToHomeProb) == 0 then - p' := { p with dest := p.home } + p' := { p with dest := p.home, isCommercial := false } else -- At shop, go to work if factory else go home if s.buildings[p.work]!.variant == .factory then - p' := { p with dest := p.work } + p' := { p with dest := p.work, isCommercial := false } else if (← rand shopToHomeProb) == 0 then - p' := { p with dest := p.home } + p' := { p with dest := p.home, isCommercial := false } -- Start the journey! if p'.dest != p.dest then p' := { p' with pos := s.buildings[p.dest]!.exit }
  • @@ -538,19 +539,23 @@
    /-- Delete roads in a region -/ def delete (start stop : Nat3) : StateM State Unit := do let (start, stop) := endPointsToCorners start stop + -- Delete roads for x in [start.x:stop.x + 1] do for y in [start.y:stop.y + 1] do for z in [start.z:stop.z + 1] do modifyf grid (·.erase ⟨x, y, z⟩) + -- Delete buildings if intersects center modifyf buildings (·.map fun b ↦ - if Building.checkCollide (b.pos + b.size / 2) ⟨1, 1, 1⟩ start (stop - start) then { b with deleted := true} else b) + if Building.checkCollide (b.pos + b.size / 2) ⟨1, 1, 1⟩ start (stop - start) then { b with isDeleted := true} else b) let buildings := (← get).buildings + -- Note that we don't add back spots, this is because ~~I'm lazy~~ to penalize deleting buildings modifyf peeps (·.filterMap fun p ↦ - if !buildings[p.home]!.deleted && !buildings[p.work]!.deleted then - some (if buildings[p.dest]!.deleted then { p with dest := p.home }else p) + if !buildings[p.home]!.isDeleted && !buildings[p.work]!.isDeleted then + some (if buildings[p.dest]!.isDeleted then { p with dest := p.home }else p) else none) - -- TODO unfull, shops + modifyf shops (·.filter fun idx ↦ !buildings[idx]!.isDeleted) + modifyf unfull (fun uf ↦ #v[uf[0].filter fun idx ↦ !buildings[idx]!.isDeleted, uf[1].filter fun idx ↦ !buildings[idx]!.isDeleted]) mkDists /-- Spend some money! -/
  • @@ -586,7 +591,7 @@ size
    entrance exit spots := Building.capacity size variant - deleted := false + isDeleted := false } spend b.cost -- Randomly iterate through empty spots in buildings of the opposite kind and create new peeps
  • @@ -604,6 +609,7 @@ pos := b.exit
    dest := idx dir := none brokenDown := false + isCommercial := false }) else let newIdx := (← get).buildings.size
  • @@ -614,6 +620,7 @@ pos := (← get).buildings[idx]!.exit
    dest := newIdx dir := none brokenDown := false + isCommercial := false }) spots := spots - 1 modifyf buildings (·.modify idx (fun b ↦ { b with spots := b.spots - 1 }))
  • @@ -725,9 +732,26 @@ if !(← get).grid.contains pos then
    throw s!"Could not place traffic light at {pos}" modifyf grid (·.modify pos fun p ↦ { p with control := .trafficLight t }) - -- TODO: A simpler intersection might work better here? def addIntersection (pos : Nat3) : StateT State (Except String) Unit := do -- Main roads + addRoad (pos + ⟨0, 0, 1⟩) (pos + ⟨3, 0, 1⟩) false + addRoad (pos + ⟨3, 0, 1⟩) (pos + ⟨0, 0, 1⟩) false + addRoad (pos + ⟨1, 0, 0⟩) (pos + ⟨1, 0, 3⟩) false + addRoad (pos + ⟨1, 0, 3⟩) (pos + ⟨1, 0, 0⟩) false + -- Left turns + addRoad (pos + ⟨1, 0, 1⟩) (pos + ⟨2, 0, 2⟩) false + addRoad (pos + ⟨2, 0, 2⟩) (pos + ⟨1, 0, 1⟩) false + addRoad (pos + ⟨1, 0, 2⟩) (pos + ⟨2, 0, 1⟩) false + addRoad (pos + ⟨2, 0, 1⟩) (pos + ⟨1, 0, 2⟩) false + -- Traffic lights + addTrafficLight (pos + ⟨0, 0, 2⟩) ⟨10, 10, 0⟩ + addTrafficLight (pos + ⟨3, 0, 1⟩) ⟨10, 10, 0⟩ + addTrafficLight (pos + ⟨2, 0, 3⟩) ⟨10, 10, 10⟩ + addTrafficLight (pos + ⟨1, 0, 0⟩) ⟨10, 10, 10⟩ + + /-- Currently unused -/ + def addIntersection' (pos : Nat3) : StateT State (Except String) 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
  • @@ -789,6 +813,7 @@ ('C', .trafficLight true),
    ('V', .intersection), ] + -- TODO: Add height to existing building def handleCmd (cmd : String) : StateT State IO Unit := do match cmd.split ' ' |>.toStringList with | "h" :: _ | "help" :: _ | "?" :: _ =>
  • @@ -873,7 +898,7 @@ /-- Draw the game state -/
    def render (s : State) (camera : Camera3D) (frames : Nat) : IO Unit := do -- Render buildings for b in s.buildings do - if !b.deleted then + if !b.isDeleted then let sizeV3 := b.size.toVector3 let posV3 := b.pos.toVector3Shift s + sizeV3 / 2.0 let entranceV3 := b.entrance.toVector3Shift s + ⟨0, 0.05, 0⟩
  • @@ -885,7 +910,7 @@ drawCubeV exitV3 ⟨0.1, 0.1, 0.1⟩ .red
    -- Render building names endMode3D for b in s.buildings do - if !b.deleted then + if !b.isDeleted then if h : s.grid.contains b.entrance then let name := s.grid[b.entrance].name let sizeV3 := b.size.toVector3
  • @@ -932,8 +957,8 @@ | 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.0035, 0⟩) 0.075 0.075 0.075 Color.Raylean.skyblue - drawCubeWires (posV3 + ⟨0, 0.0035, 0⟩) 0.075 0.075 0.075 .black + drawCube (posV3 + ⟨0, 0.035, 0⟩) 0.075 0.075 0.075 (if peep.isCommercial then Color.Raylean.beige else Color.Raylean.skyblue) + drawCubeWires (posV3 + ⟨0, 0.035, 0⟩) 0.075 0.075 0.075 .black /-- Get 3D coordinates at level `y` of 2D screen position This assumes `up = ⟨0, 1, 0⟩ ∧ projection = .perspective` -/
  • @@ -1002,7 +1027,7 @@ catch e =>
    IO.println e -- Spawn the commerical buildings first so peeps' workplaces get evenly distributed among them for i in [:3] do - randBuilding .office ⟨8, 2, 4⟩ 3 true + randBuilding .office ⟨8, 2, 4⟩ 2 true for i in [:15] do randBuilding .shop ⟨8, 1, 5⟩ 3 true for i in [:10] do
  • @@ -1068,7 +1093,7 @@ drawCubeV (poses[3].toVector3Shift s + ⟨0, 0.05, 0⟩) ⟨0.1, 0.1, 0.1⟩ .red
    | _, .yield | _, .trafficLight _ => drawCubeV (mousePosV3 + ⟨0, 0.075, 0⟩) ⟨0.02, 0.02, 0.02⟩ Color.Raylean.lime | _, .intersection => - drawCubeV (mousePosV3 + ⟨0.25, 0, 0.25⟩) ⟨0.5, 0, 0.5⟩ Color.Raylean.gray + drawCubeV (mousePosV3 + ⟨0.15, 0, 0.15⟩) ⟨0.3, 0, 0.3⟩ Color.Raylean.gray | _, _ => pure ()
  • @@ -1152,13 +1177,14 @@ drawText s!"{mousePos}" 10 160 20 .black
    if hs : s.grid.contains mousePos then drawText s!"{s.grid[mousePos].name} {s.grid[mousePos].control}" 10 190 20 .black drawFPS ((← getScreenWidth) - 100) 10 + -- TODO: GUI buttons? closeWindow - def main : IO Unit := do + def main (args : List String) : IO Unit := do setConfigFlags <| Flags.window_resizable ||| Flags.window_highdpi initWindow initialScreenWidth initialScreenHeight "MonotoniCity" setTargetFPS fps - gameLoop.run' { + let mut s := { rng := mkStdGen (← IO.rand 0 (2 ^ 32)) ticks := 0 speed := sensitivity
  • @@ -1172,3 +1198,11 @@ dists := #[]
    occupied := .ofList [] peeps := #[] } + if h : args.length > 0 then + try + s ← loadState args[0] + catch e => + IO.println s!"Failed to load save {args[0]} with error {e}" + gameLoop.run' s + -- We can't use `exit` because that won't kill the `getInput` task + IO.Process.forceExit 0
• README.md
  • @@ -1,6 +1,8 @@
    # MonotoniCity - A city-building and transport simulation game written in Lean, kinda like a hybrid of SimCity and OpenTTD + A city-building and transport simulation game written in Lean (like a hybrid of SimCity and OpenTTD) + + Build roads, multilane roads, controlled-access highways, roundabouts, diverging diamond interchanges, trumpet interchanges, stack interchanges, tunnels, and more! TODO screenshot