Vehicles now move!

Changes

1 changed files (+247/-117)

• Main.lean
  • @@ -46,6 +46,10 @@ def Float.pi := 4 * Float.atan 1
    def Float.hypot (x y : Float) := Float.sqrt <| x ^ 2 + y ^ 2 + 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) + /-- 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
  • @@ -56,6 +60,9 @@
    def initialScreenWidth := 960 def initialScreenHeight := 640 + /-- Keyboard sensitivity -/ + def sensitivity := 5 + structure Nat3 where x : Nat y : Nat
  • @@ -70,7 +77,6 @@ add a b := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩
    instance : Sub Nat3 where sub a b := ⟨a.x - b.x, a.y - b.y, a.z - b.z⟩ - inductive BuildingVariant | house
  • @@ -94,23 +100,24 @@ pos : Nat3
    size : Nat3 entrance : Nat3 exit : Nat3 - -- occupants : Nat -- TODO probably want to store this in the state + spots : Nat deriving Inhabited, Lean.ToJson, Lean.FromJson - def Building.capacity (b : Building) := - match b.variant with + namespace Building + + def capacity (size : Nat3) : BuildingVariant → Nat | .house => 1 - | .apartment => b.size.x * b.size.y * b.size.z / 2 - | .office => 2 * b.size.x * b.size.y * b.size.z - | .shop => b.size.x * b.size.y * b.size.z / 4 - | .factory => b.size.x * b.size.y * b.size.z / 32 + | .apartment => size.x * size.y * size.z / 2 + | .office => 2 * size.x * size.y * size.z + | .shop => size.x * size.y * size.z / 4 + | .factory => size.x * size.y * size.z / 32 - def Building.isResidential (b : Building) := + def isResidential (b : Building) := match b.variant with | .house | .apartment => true | _ => false - def Building.color (b : Building) := + def color (b : Building) := match b.variant with | .house => Color.Raylean.red | .apartment => Color.Raylean.orange
  • @@ -118,9 +125,20 @@ | .office => Color.Raylean.blue
    | .shop => Color.Raylean.purple | .factory => Color.Raylean.green - def Building.collides (b b' : Building) := + def cost (b : Building) := + b.size.x * b.size.y * b.size.z * b.size.z * + match b.variant with + | .house => 5 + | .apartment => 1 + | .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 b.pos.x (b.pos.x + b.size.x) b'.pos.x (b'.pos.x + b'.size.x) && f b.pos.y (b.pos.y + b.size.y) b'.pos.y (b'.pos.y + b'.size.y) && f b.pos.z (b.pos.z + b.size.z) b'.pos.z (b'.pos.z + b'.size.z) + !(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)) + + end Building /- instance : Lean.ToJson (Fin n) where
  • @@ -143,29 +161,7 @@ dest : Nat
    dir : Option Nat deriving Lean.ToJson, Lean.FromJson - inductive Road - | none - | low - | high - deriving Inhabited, BEq, 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.fromJson? j - if h : A.size = n then - return h ▸ A.toVector - else - throw s!"expected size {n}, got {A.size}" - - structure Point where - name : String - ein : Vector Road 27 - eout : Vector Road 27 - deriving Inhabited, Lean.ToJson, Lean.FromJson - + /-- Grid helper functions -/ def dx (i : Nat) := Int.ofNat (i / 9 % 3) - 1 def dy (i : Nat) := Int.ofNat (i % 3) - 1
  • @@ -188,6 +184,35 @@
    def Nat3.appd (p : Nat3) (i : Nat) : Nat3 := appdk p i 1 + inductive Road + | none + | low + | high + deriving Inhabited, BEq, Lean.ToJson, Lean.FromJson + + 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 + + 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.fromJson? j + if h : A.size = n then + return h ▸ A.toVector + else + throw s!"expected size {n}, got {A.size}" + + structure Point where + name : String + e : Vector Road 27 + deriving Inhabited, Lean.ToJson, Lean.FromJson + instance : Lean.ToJson StdGen where toJson x := Lean.toJson (x.1, x.2)
  • @@ -208,16 +233,17 @@
    instance [BEq α] [Hashable α] [Lean.FromJson α] [Lean.FromJson β] : Lean.FromJson (Std.HashMap α β) where fromJson? j := .ofList <$> List.fromJson? j - -- TODO: Money? Eh can do that later 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 dists : Array (Std.HashMap Nat3 Nat) peeps : Array Peep occupied : Std.HashSet Nat3
  • @@ -261,23 +287,23 @@ let uq := q.dequeue?.get (queue_dequeue_isSome_if_not_isEmpty hq)
    let u := uq.1 q := uq.2 let d := dist[u]! - if hs : g.contains u then - for hi : i in List.range 27 do - let v := u.appd (26 - i) - match (g[u]'hs).ein[i]'(by grind) with + for hi : i in List.range 27 do + let v := u.appd (26 - i) + if hg : g.contains v then + match g[v].e[i]'(by grind) with | .low => if !dist.contains v then - dist := dist.insert u (d + 1) + dist := dist.insert v (d + 1) q := q.enqueue v | .high => if !dist.contains v then dist := dist.insert v (d + 1) q := q.enqueue v -- Try traveling another unit in direction `i` - if hs : g.contains v then - match (g[v]'hs).ein[i]'(by grind) with + let v' := v.appd (26 - i) + if hg : g.contains v' then + match g[v'].e[i]'(by grind) with | .high => - let v' := u.appd (26 - i) if !dist.contains v' then dist := dist.insert v' (d + 1) q := q.enqueue v'
  • @@ -310,8 +336,9 @@ 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 : StateM State Unit := do + def doTick : StateT State IO Unit := do let mut peeps := #[] let mut occupied : Std.HashSet Nat3 := .ofList [] for p in (← (← get).peeps.shuffle) do
  • @@ -319,6 +346,7 @@ 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 else let dist := s.dists[p.dest]!
  • @@ -326,28 +354,37 @@ let mut neighbors := #[]
    if dist.contains u then for hi : i in List.range 27 do let v := u.appd i - match s.grid[u]!.eout[i]'(by grind) with - | .none => - pure () - | .low => - neighbors := neighbors.push (dist[v]!, i) - | .high => - neighbors := neighbors.push (dist[v]!, i) - if hv : s.grid.contains v then - let v' := v.appd i - match s.grid[v]!.eout[i]'(by grind) with - | .high => - neighbors := neighbors.push (dist[v']!, 2 * i) - | _ => - pure () + if hd : dist.contains v then + match s.grid[u]!.e[i]'(by grind) with + | .none => + pure () + | .low => + neighbors := neighbors.push (dist[v], i) + | .high => + neighbors := neighbors.push (dist[v], i) + if hv : s.grid.contains v then + let v' := v.appd i + if hd : dist.contains v' then + match s.grid[v]!.e[i]'(by grind) with + | .high => + neighbors := neighbors.push (dist[v'], i + 27) + | _ => + 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 - let v := if hi : i < 27 then u.appd i else (u.appd i).appd i + let v := u.appd i if s.occupied.contains v || occupied.contains v then continue occupied := occupied.insert v - peeps := peeps.push { p with pos := v, dir := some i } + if i < 27 then + peeps := peeps.push { p with pos := v, dir := some i } + else + let v':= u.appdk i 2 + if s.occupied.contains v' || occupied.contains v' then + continue + occupied := occupied.insert v' + peeps := peeps.push { p with pos := v', dir := some i } moved := true break if !moved then
  • @@ -361,29 +398,65 @@ modifyf day (· + 1)
    else modifyf time (· + 1) - def getInput (stdin : IO.FS.Stream) := do - IO.print "> " - return (← stdin.getLine).trimAsciiEnd.toString - /-- Load game state from file -/ def loadState (path : String) : IO State := do let serialized ← IO.FS.readFile path let json ← .ofExcept <| Lean.Json.parse serialized .ofExcept <| Lean.fromJson? json + /-- 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 + if cost > (← get).money then + throw <| .userError s!"Need ${cost}, only have ${(← get).money}" + modifyf money (· - cost) + /-- Add a building to the state -/ def addBuilding (b : Building) : StateT State IO Unit := do + 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 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 b.collides b' then + if Building.collides b.pos b.size b'.pos b'.size then throw <| IO.userError "Building collides with existing building" - modifyf buildings (·.push b) + -- Randomly iterate through empty spots in buildings of the opposite kind and create new peeps + let mut spots := b.spots + while spots > 0 do + let choices := ((← get).unfull[b.isResidential.toNat]'(by grind [Bool.toNat_lt])) + if h : !choices.isEmpty then + let choiceIdx ← rand choices.size + let idx := choices[choiceIdx] + if b.isResidential then + modifyf peeps (·.push { + home := (← get).buildings.size + work := idx + pos := b.exit + dest := idx + dir := none + }) + else + let newIdx := (← get).buildings.size + modifyf peeps (·.push { + home := idx + work := newIdx + pos := (← get).buildings[idx]!.exit + dest := newIdx + dir := none + }) + spots := spots - 1 + modifyf buildings (·.modify idx (fun b ↦ { b with spots := b.spots - 1 })) + if (← get).buildings[idx]!.spots == 0 then + modifyf unfull (·.modify b.isResidential.toNat (·.eraseIdx! choiceIdx)) + else + break + let newIdx := (← get).buildings.size + modifyf buildings (·.push { b with spots }) + if spots > 0 then + modifyf unfull (·.modify (!b.isResidential).toNat (·.push newIdx)) modifyf dists (·.push <| mkDist (← get).grid b.entrance) - -- TODO: Add peeps def max3 (a b c : Nat) := max a (max b c)
  • @@ -391,7 +464,7 @@ def diff (a b : Nat) := if a < b then b - a else a - b
    /-- Snap `a` to the nearest small `b` multiple -/ def snap (a : Int) (b : Nat) := - if a < -b / 2 then + if a ≤ -b / 2 then -1 else if a ≤ b / 2 then 0
  • @@ -406,28 +479,41 @@
    -- Sanity check #guard endpointsToRoad ⟨5, 5, 5⟩ ⟨1, 5, 2⟩ == (4, di (-1) 0 (-1)) - /-- Add roads to the state - Probably can use a slightly weaker monad here but I don't want to fight more monad transformers -/ + /-- Add roads to the state -/ def addRoad (start stop : Nat3) (isHigh : Bool) : StateT State IO Unit := do - let mut name := "" - if (← get).grid.contains start then - -- Yeah this is not ideal but Lean doesn't know the two `← get`s are the same - name := (← get).grid[start]!.name - else - have : 0 < street_names.size := by native_decide - name := street_names[← rand street_names.size] let (length, dir) := endpointsToRoad start stop if dir == di 0 0 0 || dir == di 0 1 0 || dir == di 0 (-1) 0 then throw <| .userError "Road cannot go straight up or down" let road : Road := if isHigh then .high else .low + spend <| length * road.cost dir start.y + let mut name := "" + -- Subtract 1 so that we need at least one overlap to share the same street name + let stop := start.appdk dir (length - 1) + for u in [start, { start with x := start.x + 1 }, { start with z := start.z + 1 }, { start with x := start.x - 1 }, { start with z := start.z - 1 }, stop] do + 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] for i in List.range (length + 1) do 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, .replicate 27 .none⟩ - g.modify v fun p ↦ - { p with ein := if 0 < i then p.ein.set! dir .low else p.ein, eout := if i < length then p.eout.set! dir .low else p.eout } + g := g.insert v ⟨name, .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 sideToPos (pos size : Nat3) (side dist : Nat) := pos +
  • @@ -437,7 +523,6 @@ | 1 => ⟨dist, 0, size.z⟩
    | 2 => ⟨0, 0, dist⟩ | _ => ⟨size.x, 0, dist⟩ : Nat3) - -- TODO: Delete buildings def handleCmd (cmd : String) : StateT State IO Unit := do match cmd.split ' ' |>.toStringList with | ["s", path] =>
  • @@ -451,19 +536,15 @@ 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] - addBuilding { - variant := variant.get (by grind), - pos, - size, - entrance, - exit, - } + let spots := Building.capacity size variant + addBuilding ⟨variant, pos, size, entrance, exit, spots⟩ else throw <| .userError "Failed to parse build command" | "r" :: dims =>
  • @@ -473,6 +554,11 @@ 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 => + 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]⟩ | ["n", oldName, newName] => modifyf grid (·.map fun _ p ↦ if p.name == oldName then { p with name := newName } else p)
  • @@ -485,8 +571,9 @@
    def Nat3.toVector3Shift (pos : Nat3) (s : State) : Vector3 := pos.toVector3 - s.origin.toVector3 + /-- `speed == 0` means paused -/ def maxTicks (speed : Nat) := - fps / 3 / speed + if speed == 0 then 2 ^ 32 else fps / 3 / speed /-- Draw the game state -/ def render (s : State) (camera : Camera3D) : IO Unit := do
  • @@ -519,15 +606,21 @@ -- Render roads
    for (pos, pt) in s.grid do let posV3 := pos.toVector3Shift s for hi : i in List.range 27 do - -- TODO choose better colors - -- TODO draw arrows - match pt.eout[i]'(by grind) with + let stop := pos.appd i + let stopV3 := stop.toVector3Shift s + match pt.e[i]'(by grind) with | .none => pure () | .low => - drawLine3D posV3 (pos.appd i |>.toVector3Shift s) Color.Raylean.pink + drawCylinderEx posV3 stopV3 0.02 0 32 Color.Raylean.pink + -- 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 | .high => - drawLine3D posV3 (pos.appd i |>.toVector3Shift s) Color.Raylean.gold + 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 -- Render peeps for peep in s.peeps do if peep.pos != s.buildings[peep.dest]!.entrance then
  • @@ -540,7 +633,7 @@ | some i =>
    let m := (maxTicks 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.05 0.05 0.08 Color.Raylean.lime + drawCube posV3 0.075 0.075 0.075 Color.Raylean.lime /-- Get 3D coordinates at level `y` of 2D screen position This assumes `up = ⟨0, 1, 0⟩ ∧ projection = .perspective` -/
  • @@ -575,14 +668,17 @@ let posV3 := posV3 + s.origin.toVector3
    let round (f : Float) := ((scale * f).round + 1e-9).toUInt64.toNat ⟨round posV3.x, round posV3.y, round posV3.z⟩ - /-- Get position of mouse at level `y` -/ - def getMouse3D (y : Nat) (camera : Camera3D) : IO Vector3 := do + /-- Get position of mouse at level `y` (relative to origin) -/ + def getMouse3D (y : Int) (camera : Camera3D) : IO Vector3 := do let pos2 ← getMousePosition let windowScale ← getWindowScaleDPI -- `.dot` is just element-wise product, not the dot product! - return project (pos2.dot windowScale) camera (y.toFloat / scale - 1) (← getScreenWidth).toFloat (← getScreenHeight).toFloat + return project (pos2.dot windowScale) camera (Float.ofInt (y / sensitivity) / scale) (← getScreenWidth).toFloat (← getScreenHeight).toFloat + + def getInput (stdin : IO.FS.Stream) := do + IO.print "> " + return (← stdin.getLine).trimAsciiEnd.toString - -- TODO build road using mouse def gameLoop : StateT State IO Unit := do let mut camera : Camera3D := { position := ⟨scale, scale, scale⟩
  • @@ -593,8 +689,9 @@ projection := .perspective
    } let stdin ← IO.getStdin let mut task ← IO.asTask <| getInput stdin - let mut y := 10 - let mut start : Option (Nat3 × Bool) := none + let mut y : Int := 0 + let mut speed' := sensitivity + let mut start : Option (Nat3 × Road) := none 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⟩ }
  • @@ -605,21 +702,41 @@ y := y - 1
    if (← isMouseButtonPressed MouseButton.left) then do let mousePos := (← getMouse3D y camera).toNat3Shift (← get) match start with - | none => - start := some (mousePos, false) - | some (pos', isHigh) => - addRoad pos' mousePos isHigh + | some (pos', .low) => + try + 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) if (← isMouseButtonPressed MouseButton.right) then do let mousePos := (← getMouse3D y camera).toNat3Shift (← get) match start with - | none => - start := some (mousePos, true) - | some (pos', isHigh) => - addRoad pos' mousePos isHigh + | 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 + setf speed (speed' / sensitivity) + if (← isKeyDown Key.right) then do + speed' := speed' + 1 + setf speed (speed' / sensitivity) if ← IO.hasFinished task then let cmd ← (.ofExcept task.get) try
  • @@ -637,21 +754,32 @@ drawFPS ((← getScreenWidth) - 100) 10
    clearBackground Color.white let mousePosV3 ← getMouse3D y camera let mousePos := mousePosV3.toNat3Shift (← get) - drawText s!"{mousePos}" 10 10 20 Color.black - if (← get).grid.contains mousePos then - drawText s!"{(← get).grid[mousePos]!.name} Street" 10 30 20 Color.black renderWithCamera camera do + render (← get) camera -- 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, isHigh) => + | some (pos, .none) => + let posV3 := pos.toVector3Shift (← get) + drawCubeV ((posV3 + mousePosV3) / 2.0) (mousePosV3 - posV3) Color.Raylean.maroon + | some (pos, road) => let (length, dir) := endpointsToRoad pos mousePos let stop := pos.appdk dir length - drawLine3D (pos.toVector3Shift (← get)) (stop.toVector3Shift (← get)) (if isHigh then Color.Raylean.gold else Color.Raylean.pink) + let posV3 := pos.toVector3Shift (← get) + let stopV3 := stop.toVector3Shift (← get) + drawLine3D posV3 stopV3 (if road == .low then Color.Raylean.pink else Color.Raylean.gold) + -- Fake shadows + if pos.y != (← get).origin.y || stop.y != (← get).origin.y then + drawLine3D { posV3 with y := 0 } { stopV3 with y := 0 } Color.Raylean.gray | none => pure () - render (← get) camera + 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 closeWindow def main : IO Unit := do
  • @@ -664,10 +792,12 @@ ticks := 0
    speed := 1 day := 0 time := 0 + money := 50000 origin := ⟨200, 10, 200⟩ grid := .ofList [] - dists := #[] buildings := #[] + unfull := #v[#[], #[]] + dists := #[] occupied := .ofList [] peeps := #[] }