Somewhat playable now

Changes

4 changed files (+357/-187)

• .gitignore
  • @@ -1,2 +1,3 @@
    /.lake result + save*
• Main.lean
  • @@ -1,12 +1,18 @@
    import Lean.Data.Json import Raylean + -- This fixes the "unexpected error when elaborating 'let'" bug + set_option backward.do.legacy false + open Raylean Types + /- + ## Stuff missing from Raylean + -/ + namespace Raylean -- https://github.com/raysan5/raylib/blob/aaacda6e147031f2af0cfb6c1fd7e64d761ddb1f/src/raylib.h#L567 - def Types.Key.c := 67 def Flags.window_resizable : UInt64 :=0x00000004 def Flags.window_highdpi : UInt64 :=0x00002000
  • @@ -50,6 +56,10 @@ def Vector.modify (V : Vector α n) (i : Nat) (f : α → α) : Vector α n := by
    have : (V.toArray.modify i f).size = n := by grind exact this ▸ (V.toArray.modify i f |>.toVector) + /- + ## Basic utilities + -/ + /-- Scale factor for grid to Raylib coordinates The purpose of this is ~~to give me headaches~~ because the Raylib third-person camera has a fixed speed -/ def scaleN := 10
  • @@ -57,6 +67,9 @@ def scale := scaleN.toFloat
    def fps := 60 + -- Each cell of the grid corresponds to 5m, so peeps move at 15m/s (≈33 mph) + def ticksPerSecond := 3 + def initialScreenWidth := 960 def initialScreenHeight := 640
  • @@ -78,13 +91,17 @@
    instance : Sub Nat3 where sub a b := ⟨a.x - b.x, a.y - b.y, a.z - b.z⟩ + /- + ## MonotonoCity types + -/ + inductive BuildingVariant | house | apartment | office | shop | factory - deriving Inhabited, Lean.ToJson, Lean.FromJson + deriving Inhabited, BEq, Lean.ToJson, Lean.FromJson def BuildingVariant.ofString? : String → Option BuildingVariant | "h" | "house" => some .house
  • @@ -101,6 +118,7 @@ size : Nat3
    entrance : Nat3 exit : Nat3 spots : Nat + deleted : Bool deriving Inhabited, Lean.ToJson, Lean.FromJson namespace Building
  • @@ -134,9 +152,15 @@ | .office => 2
    | .shop => 5 | .factory => 10 - def collides (pos size pos' size' : Nat3) := - let f (a b c d : Nat) := c ≤ b || a ≤ d - !(f pos.x (pos.x + size.x) pos'.x (pos'.x + size'.x) && f pos.y (pos.y + size.y) pos'.y (pos'.y + size'.y) && f pos.z (pos.z + size.z) pos'.z (pos'.z + size'.z)) + def checkCollide (pos size pos' size' : Nat3) := + -- 1D collision + let f (a b c d : Nat) := !(b ≤ c || d ≤ a) + -- Do it for all 3 dimensions + (f pos.x (pos.x + size.x) pos'.x (pos'.x + size'.x) && f pos.y (pos.y + size.y) pos'.y (pos'.y + size'.y) && f pos.z (pos.z + size.z) pos'.z (pos'.z + size'.z)) + + #guard checkCollide ⟨10, 10, 10⟩ ⟨5, 5, 5⟩ ⟨12, 8, 14⟩ ⟨5, 5, 5⟩ + + #guard !checkCollide ⟨10, 10, 10⟩ ⟨5, 5, 5⟩ ⟨0, 8, 14⟩ ⟨5, 5, 5⟩ end Building
  • @@ -159,7 +183,7 @@ work : Nat
    pos : Nat3 dest : Nat dir : Option Nat - deriving Lean.ToJson, Lean.FromJson + deriving BEq, Lean.ToJson, Lean.FromJson /-- Grid helper functions -/ def dx (i : Nat) := Int.ofNat (i / 9 % 3) - 1
  • @@ -184,6 +208,15 @@
    def Nat3.appd (p : Nat3) (i : Nat) : Nat3 := appdk p i 1 + structure TrafficLight where + redLen : Nat + greenLen : Nat + shift : Nat + deriving Lean.ToJson, Lean.FromJson + + def TrafficLight.isRed (t : TrafficLight) (ticks : Nat) : Bool := + (ticks / ticksPerSecond - t.shift) % (t.redLen + t.greenLen) < t.redLen + inductive Road | none | low
  • @@ -210,6 +243,8 @@ throw s!"expected size {n}, got {A.size}"
    structure Point where name : String + isYield : Bool + trafficLight : Option TrafficLight e : Vector Road 27 deriving Inhabited, Lean.ToJson, Lean.FromJson
  • @@ -237,18 +272,21 @@ structure State where
    rng : StdGen ticks : Nat speed : Nat - day : Nat - time : Nat money : Nat origin : Nat3 grid : Std.HashMap Nat3 Point buildings : Array Building unfull : Vector (Array Nat) 2 + shops : Array Nat dists : Array (Std.HashMap Nat3 Nat) peeps : Array Peep occupied : Std.HashSet Nat3 deriving Lean.ToJson, Lean.FromJson + /- + ## doTick and friends + -/ + instance [Monad m] : MonadLift (StateM σ ·) (StateT σ m ·) where monadLift x := modifyGet <| StateT.run x
  • @@ -317,7 +355,8 @@ /-- Precompute all distances -/
    def mkDists : StateM State Unit := do setf dists #[] for building in (← get).buildings do - modifyf dists (·.push <| mkDist (← get).grid building.entrance) + if !building.deleted then + modifyf dists (·.push <| mkDist (← get).grid building.entrance) /-- Generate a random nat in [0, n) (with a slight bias towards smaller numbers) `randNat` is more sophisticated but doesn't bundle a bounds proof, so let's just use modulo for simplicity
  • @@ -335,19 +374,48 @@ let j ← rand (i + 1)
    A' := A'.swap i j return A'.toArray - -- TODO stop signs, traffic lights, yield signs - -- TODO don't need IO /-- Run one iteration of the game -/ - def doTick : StateT State IO Unit := do + def doTick : StateM State Unit := do let mut peeps := #[] let mut occupied : Std.HashSet Nat3 := .ofList [] - for p in (← (← get).peeps.shuffle) do + let origPeeps := + let g := (← get).grid + (← (← get).peeps.shuffle).partition (fun p ↦ + if h : g.contains p.pos then !g[p.pos].isYield else true) + for p in origPeeps.1 ++ origPeeps.2 do let u := p.pos let s := ← get if u == s.buildings[p.dest]!.entrance then - -- TODO: Randomly set new dest - peeps := peeps.push p - continue + if p.dir.isSome then + modifyf money (· + 100) + let mut p' := { p with dir := none, pos := s.buildings[p.dest]!.exit } + 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 + let shopIdx ← rand s.shops.size + p' := { p' with dest := shopIdx } + else if p.dest == p.work then + -- At work, go to shops if factory worker else go home + if h : (← rand 100) == 0 && s.buildings[p.work]!.variant == .factory && !s.shops.isEmpty then + let shopIdx ← rand s.shops.size + p' := { p' with dest := shopIdx } + else if (← rand 1000) == 0 then + p' := { p with dest := p.home } + 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 } + else if (← rand 100) == 0 then + p' := { p with dest := p.home } + if p' == p then + p' := { p' with pos := u } + peeps := peeps.push p' + else if (if h : s.grid.contains u then (if h : s.grid[u].trafficLight.isSome then s.grid[u].trafficLight.get h |>.isRed s.ticks else false) else false) then + -- Traffic light + occupied := occupied.insert u + peeps := peeps.push ({ p with dir := none }) else let dist := s.dists[p.dest]! let mut neighbors := #[]
  • @@ -373,6 +441,7 @@ 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 + -- TODO: Handle diagonally crossing roads and other fun stuff (actually not too hard to handle, just check occupancy of midpoints too) let v := u.appd i if s.occupied.contains v || occupied.contains v then continue
  • @@ -392,11 +461,11 @@ occupied := occupied.insert u
    peeps := peeps.push { p with pos := u, dir := none } setf peeps peeps setf occupied occupied - if 12 * 60 * 60 < (← get).time then - setf time 0 - modifyf day (· + 1) - else - modifyf time (· + 1) + modifyf ticks (· + 1) + + /- + ## Commands + -/ /-- Load game state from file -/ def loadState (path : String) : IO State := do
  • @@ -404,6 +473,23 @@ let serialized ← IO.FS.readFile path
    let json ← .ofExcept <| Lean.Json.parse serialized .ofExcept <| Lean.fromJson? json + /-- Delete roads in a region -/ + def delete (start stop : Nat3) : StateM State Unit := do + for x in [min start.x stop.x:max start.x stop.x + 1] do + for y in [min start.y stop.y:max start.y stop.y + 1] do + for z in [min start.z stop.z:max start.z stop.z + 1] do + modifyf grid (·.erase ⟨x, y, z⟩) + modifyf buildings (·.map fun b ↦ + if Building.checkCollide b.pos b.size start (stop - start) then { b with deleted := true} else b) + let buildings := (← get).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) + else + none) + -- TODO unfull, shops + mkDists + /-- Spend some money! Probably can use a slightly weaker monad here but I don't want to fight more monad transformers ddd-/ def spend (cost : Nat) : StateT State IO Unit := do
  • @@ -411,8 +497,28 @@ if cost > (← get).money then
    throw <| .userError s!"Need ${cost}, only have ${(← get).money}" modifyf money (· - cost) + /-- Counterclockwise thingy -/ + def sideToPos (pos size : Nat3) (side : Nat × Nat) := + pos + + (match side.1 with + | 0 => ⟨side.2, 0, 0⟩ + | 1 => ⟨size.x, 0, side.2⟩ + | 2 => ⟨size.x - side.2, 0, size.z⟩ + | _ => ⟨0, 0, size.z - side.2⟩ : Nat3) + /-- Add a building to the state -/ - def addBuilding (b : Building) : StateT State IO Unit := do + def addBuilding (variant : BuildingVariant) (pos size : Nat3) (entrance exit : Nat × Nat) : StateT State IO Unit := do + if entrance == exit then + throw <| .userError "Building entrance cannot be in same position as exit" + let b : Building := { + variant + pos + size + entrance := sideToPos pos size entrance + exit := sideToPos pos size exit + spots := Building.capacity size variant + deleted := false + } spend b.cost for x in [b.pos.x:b.pos.x + b.size.x + 1] do for y in [b.pos.y:b.pos.y + b.size.y + 1] do
  • @@ -420,7 +526,7 @@ for z in [b.pos.z:b.pos.z + b.size.z + 1] do
    if (← get).grid.contains ⟨x, y, z⟩ then throw <| IO.userError "Building collides with existing road" for b' in (← get).buildings do - if Building.collides b.pos b.size b'.pos b'.size then + if Building.checkCollide b.pos b.size b'.pos b'.size then throw <| IO.userError "Building collides with existing building" -- Randomly iterate through empty spots in buildings of the opposite kind and create new peeps let mut spots := b.spots
  • @@ -456,6 +562,8 @@ let newIdx := (← get).buildings.size
    modifyf buildings (·.push { b with spots }) if spots > 0 then modifyf unfull (·.modify (!b.isResidential).toNat (·.push newIdx)) + if b.variant == .shop then + modifyf shops (·.push newIdx) modifyf dists (·.push <| mkDist (← get).grid b.entrance) def max3 (a b c : Nat) := max a (max b c)
  • @@ -501,27 +609,20 @@ let v := start.appdk dir i
    modifyf grid fun g ↦ Id.run do let mut g := g if !g.contains v then - g := g.insert v ⟨name, .replicate 27 .none⟩ + g := g.insert v ⟨name, false, none, .replicate 27 .none⟩ g.modify v (fun p ↦ if i < length then { p with e := p.e.set! dir road } else p) mkDists - -- TODO delete buildings - /-- Delete roads in a region -/ - def delete (start stop : Nat3) : StateM State Unit := do - for x in [min start.x stop.x:max start.x stop.x + 1] do - for y in [min start.y stop.y:max start.y stop.y + 1] do - for z in [min start.z stop.z:max start.z stop.z + 1] do - modifyf grid (·.erase ⟨x, y, z⟩) - mkDists + def addYield (pos : Nat3) : StateT State IO Unit := do + 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 sideToPos (pos size : Nat3) (side dist : Nat) := - pos + - (match side with - | 0 => ⟨dist, 0, 0⟩ - | 1 => ⟨dist, 0, size.z⟩ - | 2 => ⟨0, 0, dist⟩ - | _ => ⟨size.x, 0, dist⟩ : Nat3) + def addTrafficLight (pos : Nat3) (t : TrafficLight) : StateT State IO Unit := do + 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 handleCmd (cmd : String) : StateT State IO Unit := do match cmd.split ' ' |>.toStringList with
  • @@ -531,20 +632,17 @@ | ["l", path] =>
    set <| ← loadState path | ["v", speed] => setf speed (String.toNat! speed) + | "d" :: dims => + if h : dims.length = 6 then + let dims := dims.map String.toNat! + have : dims.length = 6 := by grind + delete ⟨dims[0], dims[1], dims[2]⟩ ⟨dims[3], dims[4], dims[5]⟩ | "b" :: variant :: dims => let variant := BuildingVariant.ofString? variant if h : dims.length = 10 && variant.isSome then let dims := dims.map String.toNat! have : dims.length = 10 := by grind - let variant := variant.get (by grind) - let pos := ⟨dims[0], dims[1], dims[2]⟩ - let size := ⟨dims[3], dims[4], dims[5]⟩ - if dims[6] == dims[8] && dims[7] == dims[9] then - throw <| .userError "Building entrance cannot be in same position as exit" - let entrance := sideToPos pos size dims[6] dims[7] - let exit := sideToPos pos size dims[8] dims[9] - let spots := Building.capacity size variant - addBuilding ⟨variant, pos, size, entrance, exit, spots⟩ + addBuilding (variant.get (by grind)) ⟨dims[0], dims[1], dims[2]⟩ ⟨dims[3], dims[4], dims[5]⟩ (dims[6], dims[7]) (dims[8], dims[9]) else throw <| .userError "Failed to parse build command" | "r" :: dims =>
  • @@ -554,17 +652,26 @@ have : dims.length = 7 := by grind
    addRoad ⟨dims[0], dims[1], dims[2]⟩ ⟨dims[3], dims[4], dims[5]⟩ (dims[6] == 1) else throw <| .userError "Road cannot go straight up or down" - | "d" :: dims => + | "y" :: dims => + if h : dims.length = 3 then + let dims := dims.map String.toNat! + have : dims.length = 3 := by grind + addYield ⟨dims[0], dims[1], dims[2]⟩ + | "t" :: dims => if h : dims.length = 6 then let dims := dims.map String.toNat! have : dims.length = 6 := by grind - delete ⟨dims[0], dims[1], dims[2]⟩ ⟨dims[3], dims[4], dims[5]⟩ + addTrafficLight ⟨dims[0], dims[1], dims[2]⟩ ⟨dims[3], dims[4], dims[5]⟩ | ["n", oldName, newName] => modifyf grid (·.map fun _ p ↦ if p.name == oldName then { p with name := newName } else p) | _ => throw <| .userError "Command not found" + /- + ## Rendering and UI + -/ + def Nat3.toVector3 (pos : Nat3) : Vector3 := ⟨pos.x.toFloat / scale, pos.y.toFloat / scale, pos.z.toFloat / scale⟩
  • @@ -572,29 +679,30 @@ def Nat3.toVector3Shift (pos : Nat3) (s : State) : Vector3 :=
    pos.toVector3 - s.origin.toVector3 /-- `speed == 0` means paused -/ - def maxTicks (speed : Nat) := - if speed == 0 then 2 ^ 32 else fps / 3 / speed + def maxFrames (speed : Nat) := + if speed == 0 then 2 ^ 32 else fps / ticksPerSecond / speed /-- Draw the game state -/ - def render (s : State) (camera : Camera3D) : IO Unit := do + def render (s : State) (camera : Camera3D) (frames : Nat) : IO Unit := do -- Render buildings for b in s.buildings do - let sizeV3 := b.size.toVector3 - let posV3 := b.pos.toVector3Shift s + sizeV3 / 2.0 - let entranceV3 := b.entrance.toVector3Shift s + (Vector3.mk 0 0.05 0) - let exitV3 := b.exit.toVector3Shift s + (Vector3.mk 0 0.05 0) - drawCubeV posV3 sizeV3 b.color - drawCubeWiresV posV3 sizeV3 .black - drawCubeV entranceV3 ⟨0.1, 0.1, 0.1⟩ .green - drawCubeV exitV3 ⟨0.1, 0.1, 0.1⟩ .red - if h : s.grid.contains b.entrance then - let name := s.grid[b.entrance].name - let pos2D ← getWorldToScreen (posV3 + ⟨0, 0.2, 0⟩) camera - endMode3D - let address := - if b.entrance.x == b.pos.x || b.entrance.x == b.pos.x + b.size.x then b.entrance.y else b.entrance.x - drawText s!"{address} {name} Street" pos2D.x.toUInt64.toNat pos2D.y.toUInt64.toNat 10 Color.black - beginMode3D camera + if !b.deleted then + let sizeV3 := b.size.toVector3 + let posV3 := b.pos.toVector3Shift s + sizeV3 / 2.0 + let entranceV3 := b.entrance.toVector3Shift s + (Vector3.mk 0 0.05 0) + let exitV3 := b.exit.toVector3Shift s + (Vector3.mk 0 0.05 0) + drawCubeV posV3 sizeV3 b.color + drawCubeWiresV posV3 sizeV3 .black + drawCubeV entranceV3 ⟨0.1, 0.1, 0.1⟩ .green + drawCubeV exitV3 ⟨0.1, 0.1, 0.1⟩ .red + if h : s.grid.contains b.entrance then + let name := s.grid[b.entrance].name + let pos2D ← getWorldToScreen (posV3 + ⟨0, 0.2, 0⟩) camera + endMode3D + 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 + beginMode3D camera -- Render road names -- for (pos, pt) in s.grid do -- if (2 * pos.x + pos.z) % 20 == 0 then
  • @@ -621,6 +729,11 @@ drawCylinderEx posV3 stopV3 0.02 0 32 Color.Raylean.gold
    -- Fake shadows if pos.y != s.origin.y || stop.y != s.origin.y then drawLine3D { posV3 with y := 0 } { stopV3 with y := 0 } Color.Raylean.gray + if pt.isYield then + drawCubeV (posV3 + ⟨0, 0.075, 0⟩) ⟨0.02, 0.02, 0.02⟩ .yellow + if h : pt.trafficLight.isSome then + let t := pt.trafficLight.get h + drawCubeV (posV3 + ⟨0, 0.075, 0⟩) ⟨0.02, 0.02, 0.02⟩ (if t.isRed s.ticks then .red else .green) -- Render peeps for peep in s.peeps do if peep.pos != s.buildings[peep.dest]!.entrance then
  • @@ -630,10 +743,11 @@ match peep.dir with
    | none => peep.pos.toVector3Shift s | some i => - let m := (maxTicks s.speed).toFloat + 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 - s.ticks.toFloat - 1) / m * (if i < 27 then 1 else 2) * ivec - drawCube posV3 0.075 0.075 0.075 Color.Raylean.lime + 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 + drawCubeWires (posV3 + ⟨0, 0.0025, 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` -/
  • @@ -679,7 +793,54 @@ def getInput (stdin : IO.FS.Stream) := do
    IO.print "> " return (← stdin.getLine).trimAsciiEnd.toString + def padTime (n : Nat) := + if n < 10 then s!"0{n}" else s!"{n}" + + def spawnInitBuildings : StateT State IO Unit := do + let randPos : StateT State IO Nat3 := do + return ⟨(← get).origin.x - 50 + (← rand 100), 10, (← get).origin.z - 50 + (← rand 100)⟩ + let randPosExt : StateT State IO Nat3 := do + repeat + let x ← rand 200 + let z ← rand 200 + if 50 < x && x < 150 && 50 < z && z < 150 then + continue + return ⟨(← get).origin.x - 100 + x, 10, (← get).origin.z - 100 + z⟩ + for i in [:20] do + let side ← rand 4 + try + addBuilding .house (← randPosExt) ⟨5, 1, 5⟩ (side, 2) (side, 3) + catch e => + IO.println e + -- TODO bump up these numbers + for i in [:2] do + let side ← rand 4 + try + addBuilding .apartment (← randPos) ⟨10, 3, 5⟩ (side, 1) (side, 2) + catch e => + IO.println e + for i in [:2] do + let side ← rand 4 + try + addBuilding .office (← randPos) ⟨10, 3, 10⟩ (side, 5) (side, 6) + catch e => + IO.println e + for i in [:0] do + let side ← rand 4 + try + addBuilding .shop (← randPos) ⟨5, 1, 10⟩ (side, 3) (side, 4) + catch e => + IO.println e + for i in [:0] do + let side ← rand 4 + try + addBuilding .factory (← randPosExt) ⟨10, 4, 10⟩ (side, 5) (side, 6) + catch e => + IO.println e + def gameLoop : StateT State IO Unit := do + spawnInitBuildings + setf money 50000 let mut camera : Camera3D := { position := ⟨scale, scale, scale⟩ target := ⟨0, 0, 0⟩
  • @@ -689,9 +850,11 @@ projection := .perspective
    } let stdin ← IO.getStdin let mut task ← IO.asTask <| getInput stdin + let mut start : Option Nat3 := none + let mut curAction := 1 let mut y : Int := 0 let mut speed' := sensitivity - let mut start : Option (Nat3 × Road) := none + let mut frames := 0 while !(← windowShouldClose) do -- Fix `up` to prevent the Q and E keys from messing it up camera := { ← updateCamera camera .thirdPerson with up := ⟨0, 1, 0⟩ }
  • @@ -701,35 +864,30 @@ if ← isKeyDown Key.down then
    y := y - 1 if (← isMouseButtonPressed MouseButton.left) then do let mousePos := (← getMouse3D y camera).toNat3Shift (← get) - match start with - | some (pos', .low) => - try + try + match start, curAction with + | none, 1 | none, 2 => + start := some mousePos + | _, 3 => + addYield mousePos + | _, 4 => + addTrafficLight mousePos ⟨10, 10, 0⟩ + | _, 5 => + addTrafficLight mousePos ⟨10, 10, 10⟩ + | some pos', 1 => addRoad pos' mousePos false - catch e => - IO.println e - start := none - | _ => - start := some (mousePos, .low) - if (← isMouseButtonPressed MouseButton.middle) then do - let mousePos := (← getMouse3D y camera).toNat3Shift (← get) - match start with - | some (pos', .none) => - delete pos' mousePos - start := none - | _ => - start := some (mousePos, .none) + start := none + | some pos', 2 => + addRoad pos' mousePos true + start := none + | some pos', _ => + delete pos' mousePos + start := none + | _, _ => + pure () + catch e => + IO.println e if (← isMouseButtonPressed MouseButton.right) then do - let mousePos := (← getMouse3D y camera).toNat3Shift (← get) - match start with - | some (pos', .high) => - try - addRoad pos' mousePos true - catch e => - IO.println e - start := none - | _ => - start := some (mousePos, .high) - if (← isKeyDown Key.c) then do start := none if (← isKeyDown Key.left) then do speed' := speed' - 1
  • @@ -737,6 +895,9 @@ setf speed (speed' / sensitivity)
    if (← isKeyDown Key.right) then do speed' := speed' + 1 setf speed (speed' / sensitivity) + for i in [:10] do + if (← isKeyDown <| '0'.toNat + i) then do + curAction := i if ← IO.hasFinished task then let cmd ← (.ofExcept task.get) try
  • @@ -744,42 +905,53 @@ handleCmd cmd
    catch e => IO.println e task ← IO.asTask <| getInput stdin - if (← get).ticks ≥ maxTicks (← get).speed then + if frames ≥ maxFrames (← get).speed then doTick - setf ticks 0 + frames := 0 else - modifyf ticks (· + 1) + frames := frames + 1 + let s ← get renderFrame do drawFPS ((← getScreenWidth) - 100) 10 clearBackground Color.white let mousePosV3 ← getMouse3D y camera - let mousePos := mousePosV3.toNat3Shift (← get) + let mousePos := mousePosV3.toNat3Shift s renderWithCamera camera do - render (← get) camera + render s camera frames -- For debugging: -- drawCubeV mousePosV3 ⟨0.1, 0.1, 0.1⟩ Color.Raylean.pink - drawGrid ((← get).origin.x / scaleN * 2) 1 - match start with - | some (pos, .none) => - let posV3 := pos.toVector3Shift (← get) - drawCubeV ((posV3 + mousePosV3) / 2.0) (mousePosV3 - posV3) Color.Raylean.maroon - | some (pos, road) => + drawGrid (s.origin.x / scaleN * 2) 1 + match start, curAction with + | none, _ | _, 3 => + pure () + | some pos, 1 | some pos, 2 => let (length, dir) := endpointsToRoad pos mousePos let stop := pos.appdk dir length - let posV3 := pos.toVector3Shift (← get) - let stopV3 := stop.toVector3Shift (← get) - drawLine3D posV3 stopV3 (if road == .low then Color.Raylean.pink else Color.Raylean.gold) + let posV3 := pos.toVector3Shift s + let stopV3 := stop.toVector3Shift s + drawLine3D posV3 stopV3 (if curAction == 1 then Color.Raylean.pink else Color.Raylean.gold) -- Fake shadows - if pos.y != (← get).origin.y || stop.y != (← get).origin.y then + if pos.y != s.origin.y || stop.y != s.origin.y then drawLine3D { posV3 with y := 0 } { stopV3 with y := 0 } Color.Raylean.gray - | none => - pure () - drawText s!"Money: ${(← get).money}" 10 10 20 .black - drawText s!"Population: {(← get).peeps.size}" 10 40 20 .black - drawText s!"Speed: {(← get).speed}" 10 70 20 .black - drawText s!"{mousePos}" 10 100 20 .black - if (← get).grid.contains mousePos then - drawText s!"{(← get).grid[mousePos]!.name} Street" 10 130 20 .black + | some pos, _ => + let posV3 := pos.toVector3Shift s + drawCubeV ((posV3 + mousePosV3) / 2.0) (mousePosV3 - posV3) Color.Raylean.maroon + let actionText := + match curAction with + | 1 => "Build road" + | 2 => "Build highway" + | 3 => "Build yield" + | 4 => "Build traffic light (phase 1)" + | 5 => "Build traffic light (phase 2)" + | _ => "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!"{mousePos}" 10 160 20 .black + if s.grid.contains mousePos then + drawText s!"{s.grid[mousePos]!.name} Street" 10 190 20 .black closeWindow def main : IO Unit := do
  • @@ -790,13 +962,12 @@ gameLoop.run' {
    rng := mkStdGen (← IO.rand 0 (2 ^ 32)) ticks := 0 speed := 1 - day := 0 - time := 0 - money := 50000 + money := 2 ^ 32 -- The initial value doesn't matter since we spawn a bunch of buildings first origin := ⟨200, 10, 200⟩ grid := .ofList [] buildings := #[] unfull := #v[#[], #[]] + shops := #[] dists := #[] occupied := .ofList [] peeps := #[]
• README.md
  • @@ -2,6 +2,8 @@ # MonotoniCity
    A city-building and transport simulation game written in Lean + For learning the controls... uh, read the source code? + ## Building To build this using Nix (least painful trust me), just run `nix build`.
  • @@ -13,67 +15,6 @@
    To build a (huge) precompiled bundle that can run on any Linux distro, run `nix bundle .#packages.x86_64-linux.default`. I recommend running the game with `rlwrap` for a slightly nicer console. - - ## Random notes - - Rewrite (a small subset of) OpenTTD in Lean! - - - Focus on road vehicles for now for simplicity - - Top-down rectangular grid instead of isometric - - Basically it'll be a probalistic cellular automata - - Use https://github.com/funexists/raylean/ - - So anyways we have a rectangular grid of points 5m apart and you can add a directed road between a point and any of its 8 neighbors (24 once I add bridges and tunnels, or maybe I should add them right from the beginning?). At any time, at most one vehicle occupies each point. - - Buildings are rectangles with top right and bottom left corners in this grid. - - By default, vehicles move at a realistic speed (3 ticks per second) but we can run the simulation faster too - - Two kinds of roads, regular and highway. Vehicles can move two segments at a time on highways but only in the same direction (TODO: how to make the pathfinder exit on a multilane highway?) - - If only one possible road out of a point, then the vehicle just goes ahead. Otherwise it runs a BFS pathfinder to its destination and checks if each road going out is occupied in order of distance until it finds one that's not (TODO: don't use a road if its distance exceeds the shortest path by a huge factor?) - - It's probalistic because the order that the vehicles are processed during each tick is random, so for instance a random vehicle moves at a 4-way stop rather than the one that has been there the longest. This also makes merges random. You can use a yield sign to push a vehicle to the bottom of this order. A vehicle cannot move to a spot that is occupied during the current grid state or the next state (TODO: handle crossing diagonal roads) - - Traffic lights are kinda janky but shouldn't be too hard to support. - - Vehicles seat exactly one person and at the beginning of the day they randomly leave houses or apartments for workplaces in the city and there are also trucks between factories and stores and stuff - - Time starts at 8 AM and ends at midnight each day - - The internal data representation of the game is a 2D vector for the grid for fast access for info about a point and arrays of vehicles, buildings etc to easily iterate over all those objects. To save the game we dump all these to JSON and vice versa for loading a save (unfortunately this bloats up the binary ugh). I don't really need to plan this out in advance but rather just add more fields as needed - - 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 - - - https://www.raylib.com/cheatsheet/cheatsheet.html - - - The street names are from https://github.com/rossburton/barnum/blob/master/source-data/street-names.txt - ## Why the name?
• notes (new)
  • @@ -0,0 +1,57 @@
    + Rewrite (a small subset of) OpenTTD in Lean! + + - Focus on road vehicles for now for simplicity + - Top-down rectangular grid instead of isometric + - Basically it'll be a probalistic cellular automata + - Use https://github.com/funexists/raylean/ + + So anyways we have a rectangular grid of points 5m apart and you can add a directed road between a point and any of its 8 neighbors (24 once I add bridges and tunnels, or maybe I should add them right from the beginning?). At any time, at most one vehicle occupies each point. + + Buildings are rectangles with top right and bottom left corners in this grid. + + By default, vehicles move at a realistic speed (3 ticks per second) but we can run the simulation faster too + + Two kinds of roads, regular and highway. Vehicles can move two segments at a time on highways but only in the same direction (TODO: how to make the pathfinder exit on a multilane highway?) + + If only one possible road out of a point, then the vehicle just goes ahead. Otherwise it runs a BFS pathfinder to its destination and checks if each road going out is occupied in order of distance until it finds one that's not (TODO: don't use a road if its distance exceeds the shortest path by a huge factor?) + + It's probalistic because the order that the vehicles are processed during each tick is random, so for instance a random vehicle moves at a 4-way stop rather than the one that has been there the longest. This also makes merges random. You can use a yield sign to push a vehicle to the bottom of this order. A vehicle cannot move to a spot that is occupied during the current grid state or the next state (TODO: handle crossing diagonal roads) + + Traffic lights are kinda janky but shouldn't be too hard to support. + + Vehicles seat exactly one person and at the beginning of the day they randomly leave houses or apartments for workplaces in the city and there are also trucks between factories and stores and stuff + + Time starts at 8 AM and ends at midnight each day + + The internal data representation of the game is a 2D vector for the grid for fast access for info about a point and arrays of vehicles, buildings etc to easily iterate over all those objects. To save the game we dump all these to JSON and vice versa for loading a save (unfortunately this bloats up the binary ugh). I don't really need to plan this out in advance but rather just add more fields as needed + + 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 + + + https://www.raylib.com/cheatsheet/cheatsheet.html + + + The street names are from https://github.com/rossburton/barnum/blob/master/source-data/street-names.txt