f8cfb964 - monotonicity

@@ -5,9 +5,10 @@ open Raylean Types

namespace Raylean - def Float.pi := 4 * Float.atan 1 - - def Float.hypot (x y : Float) := Float.sqrt <| x ^ 2 + y ^ 2 + -- 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 -- Helpful for debugging instance : ToString Vector3 := ⟨fun a ↦ s!"({a.x}, {a.y}, {a.z})"⟩

@@ -41,9 +42,19 @@ drawCubeWires pos size.x size.y size.z color

end Raylean + def Float.pi := 4 * Float.atan 1 + + def Float.hypot (x y : Float) := Float.sqrt <| x ^ 2 + y ^ 2 + + /-- 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 + def scale := scaleN.toFloat + def fps := 60 - def screenWidth := 960 - def screenHeight := 640 + + def initialScreenWidth := 960 + def initialScreenHeight := 640 structure Nat3 where x : Nat

@@ -51,6 +62,16 @@ y : Nat

z : Nat deriving Inhabited, BEq, Hashable, Lean.ToJson, Lean.FromJson + -- Helpful for debugging + instance : ToString Nat3 := ⟨fun a ↦ s!"({a.x}, {a.y}, {a.z})"⟩ + + instance : Add Nat3 where + 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 | apartment

@@ -73,17 +94,21 @@ pos : Nat3

size : Nat3 entrance : Nat3 exit : Nat3 - occupants : Nat + -- occupants : Nat -- TODO probably want to store this in the state deriving Inhabited, Lean.ToJson, Lean.FromJson - -- TODO pick reasonable capacities for the others def Building.capacity (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 + | .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 + + def Building.isResidential (b : Building) := + match b.variant with + | .house | .apartment => true + | _ => false def Building.color (b : Building) := match b.variant with

@@ -92,6 +117,10 @@ | .apartment => Color.Raylean.orange

| .office => Color.Raylean.blue | .shop => Color.Raylean.purple | .factory => Color.Raylean.green + + def Building.collides (b b' : Building) := + 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) /- instance : Lean.ToJson (Fin n) where

@@ -153,8 +182,11 @@

-- `i` and `26 - i` should be in opposite directions #guard (List.range 27 |>.map fun i ↦ dx i == -(dx (26 - i)) && dy i == -(dy (26 - i)) && dz i == -(dz (26 - i))).and + def Nat3.appdk (p : Nat3) (i k : Nat) : Nat3 := + ⟨p.x + k * dx i |>.toNat, p.y + k * dy i |>.toNat, p.z + k * dz i |>.toNat⟩ + def Nat3.appd (p : Nat3) (i : Nat) : Nat3 := - ⟨p.x + dx i |>.toNat, p.y + dy i |>.toNat, p.z + dz i |>.toNat⟩ + appdk p i 1 instance : Lean.ToJson StdGen where toJson x := Lean.toJson (x.1, x.2)

@@ -339,33 +371,73 @@ let serialized ← IO.FS.readFile path

let json ← .ofExcept <| Lean.Json.parse serialized .ofExcept <| Lean.fromJson? json - def addBuilding (b : Building) : StateM State Unit := do + /-- Add a building to the state -/ + def addBuilding (b : Building) : StateT State IO Unit := do + 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 + throw <| IO.userError "Building collides with existing building" modifyf buildings (·.push b) - -- TODO check collisions - -- TODO update dists - -- Add peeps + modifyf dists (·.push <| mkDist (← get).grid b.entrance) + -- TODO: Add peeps - def addRoad (start : Nat3) (dir length : Nat) (isHigh : Bool) : StateM State Unit := do - -- let name := - -- (if h : (← get).grid.contains start then - -- (← get).grid[start].name - -- else - -- street_names[rand street_names.size]) - let mut u := start - -- let newp : Point := ⟨name, - -- , .replicate 27 .none⟩ - -- for i in List.range length do - -- modifyf grid (fun g ↦ - -- if h : g.contains u then - -- g.modify u fun p ↦ { p with eout := p.eout.set! dir .low } - -- else - -- g.insert u ⟨ .⟩ - -- ) + def max3 (a b c : Nat) := max a (max b c) def diff (a b : Nat) := if a < b then b - a else a - b - -- TODO: Build roads - -- TODO: rename roads + /-- Snap `a` to the nearest small `b` multiple -/ + def snap (a : Int) (b : Nat) := + if a < -b / 2 then + -1 + else if a ≤ b / 2 then + 0 + else 1 + + /-- Get direction and length between two endpoints -/ + def endpointsToRoad (start stop : Nat3) := + let length := max3 (diff start.x stop.x) (diff start.y stop.y) (diff start.z stop.z) + let dir := di (snap (Int.ofNat stop.x - start.x) length) (snap (Int.ofNat stop.y - start.y) length) (snap (Int.ofNat stop.z - start.z) length) + (length, dir) + + -- 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 -/ + 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 + 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 } + + 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) + + -- TODO: Delete buildings def handleCmd (cmd : String) : StateT State IO Unit := do match cmd.split ' ' |>.toStringList with | ["s", path] =>

@@ -374,56 +446,69 @@ | ["l", path] =>

set <| ← loadState path | ["v", speed] => setf speed (String.toNat! speed) - | ["i"] => - -- TODO - IO.println s!"Population: {(← get).peeps.size}" | "b" :: variant :: dims => -- TODO refactor into own function, check collisions, update dists let variant := BuildingVariant.ofString? variant - if h : dims.length = 6 && variant.isSome then + if h : dims.length = 10 && variant.isSome then let dims := dims.map String.toNat! - have : dims.length = 6 := by grind - -- addBuilding ⟨⟨dims[0], dims[1], dims[2]⟩, ⟨dims[3], dims[4], dims[5]⟩, variant.get (by grind), 0⟩ + have : dims.length = 10 := 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, + } else throw <| .userError "Failed to parse build command" | "r" :: dims => if h : dims.length = 7 then let dims := dims.map String.toNat! have : dims.length = 7 := by grind - let start : Nat3 := ⟨dims[0], dims[1], dims[2]⟩ - let stop : Nat3 := ⟨dims[3], dims[4], dims[5]⟩ - let isHigh := dims[6] == 1 - let length := max (diff start.x stop.x) <| max (diff start.y stop.y) (diff start.z stop.z) - let dir := di ((Int.ofNat start.x - stop.x) / length) ((Int.ofNat start.y - stop.y) / length) ((Int.ofNat start.z - stop.z) / length) - if dir != di 0 0 0 && dir != di 0 1 0 && dir != di 0 (-1) 0 then - addRoad start dir length isHigh + 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" + | ["n", oldName, newName] => + modifyf grid (·.map fun _ p ↦ + if p.name == oldName then { p with name := newName } else p) | _ => throw <| .userError "Command not found" - def Nat3.toVector3 (p : Nat3) : Vector3 := - ⟨p.x.toFloat / 10, p.y.toFloat / 10, p.z.toFloat / 10⟩ + def Nat3.toVector3 (pos : Nat3) : Vector3 := + ⟨pos.x.toFloat / scale, pos.y.toFloat / scale, pos.z.toFloat / scale⟩ - def Nat3.toVector3Shift (p : Nat3) (s : State) : Vector3 := - p.toVector3 - s.origin.toVector3 + def Nat3.toVector3Shift (pos : Nat3) (s : State) : Vector3 := + pos.toVector3 - s.origin.toVector3 def maxTicks (speed : Nat) := fps / 3 / speed /-- Draw the game state -/ def render (s : State) (camera : Camera3D) : IO Unit := do + -- Render buildings for b in s.buildings do - let size := b.size.toVector3 - let pos := b.pos.toVector3Shift s + size / 2.0 - drawCubeV pos size b.color - drawCubeWiresV pos size .black + 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⟩ Color.Raylean.beige + drawCubeV exitV3 ⟨0.1, 0.1, 0.1⟩ Color.Raylean.skyblue + -- Render roads 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 20 Color.black + -- TODO this might not work + drawText s!"{if dir then pos.x else pos.z} {pt.name} Street" pos2D.x.toUInt64.toNat pos2D.y.toUInt64.toNat 10 Color.black let posV3 := pos.toVector3Shift s for hi : i in List.range 27 do -- TODO choose better colors

@@ -435,18 +520,19 @@ | .low =>

drawLine3D posV3 (pos.appd i |>.toVector3Shift s) Color.black | .high => drawLine3D posV3 (pos.appd i |>.toVector3Shift s) Color.Raylean.gray - for p in s.peeps do - if p.pos != s.buildings[p.dest]!.entrance then + -- Render peeps + for peep in s.peeps do + if peep.pos != s.buildings[peep.dest]!.entrance then -- Unfortunately we can't use `Nat3.toVector3` here because they're `Int`s - let pos := - match p.dir with + let posV3 := + match peep.dir with | none => - p.pos.toVector3Shift s + peep.pos.toVector3Shift s | some i => let m := (maxTicks s.speed).toFloat - let ivec : Vector3 := Vector3.mk (.ofInt (dx i) / 10) (.ofInt (dy i) / 10) (.ofInt (dz i) / 10) - p.pos.toVector3Shift s - (m - s.ticks.toFloat - 1) / m * (if i < 27 then 1 else 2) * ivec - drawCube pos 0.05 0.05 0.08 Color.Raylean.lime + 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 /-- Get 3D coordinates at level `y` of 2D screen position This assumes `up = ⟨0, 1, 0⟩ ∧ projection = .perspective` -/

@@ -475,15 +561,23 @@ let dtang := mul * Vector3.mk (camera.target.z - camera.position.z) 0 (camera.position.x - camera.target.x)

-- Now scale to level `y` (dradial - dtang) * (camera.position.y - y) / (camera.position.y - camera.target.y) + ⟨camera.position.x, y, camera.position.z⟩ - def Raylean.Types.Vector3.toNat3Shift (p : Vector3) (s : State) : Nat3 := - let p := p + s.origin.toVector3 - let round (f : Float) := ((10 * f).round + 1e-9).toUInt64.toNat - ⟨round p.x, round p.y, round p.z⟩ + /-- Inverse of `Nat3.toVector3Shift` -/ + def Raylean.Types.Vector3.toNat3Shift (posV3 : Vector3) (s : State) : Nat3 := + 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 + 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 -- TODO build road using mouse def gameLoop : StateT State IO Unit := do let mut camera : Camera3D := { - position := ⟨10, 10, 10⟩ + position := ⟨scale, scale, scale⟩ target := ⟨0, 0, 0⟩ up := ⟨0, 1, 0⟩ fovy := 45

@@ -491,23 +585,33 @@ projection := .perspective

} let stdin ← IO.getStdin let mut task ← IO.asTask <| getInput stdin + let mut y := 10 let mut start : Option (Nat3 × Bool) := none while !(← windowShouldClose) do - camera ← updateCamera camera .thirdPerson + -- Fix `up` to prevent the Q and E keys from messing it up + camera := { ← updateCamera camera .thirdPerson with up := ⟨0, 1, 0⟩ } + if ← isKeyDown Key.up then + y := y + 1 + if ← isKeyDown Key.down then + y := y - 1 if (← isMouseButtonPressed MouseButton.left) then do - let pos2 ← getMousePosition - let scale ← getWindowScaleDPI - -- TODO move camera up and down - -- `.dot` is just element-wise product, not the dot product! - let pos := project (pos2.dot scale) camera 0 (← getScreenWidth).toFloat (← getScreenHeight).toFloat |>.toNat3Shift (← get) - start := some (pos, true) - -- match start with - -- | none => - -- start := some (pos, true) - -- | some _ => - -- start := some (pos, true) + let mousePos := (← getMouse3D y camera).toNat3Shift (← get) + match start with + | none => + start := some (mousePos, false) + | some (pos', isHigh) => + addRoad pos' mousePos isHigh + start := none if (← isMouseButtonPressed MouseButton.right) then do - let pos ← getMousePosition + let mousePos := (← getMouse3D y camera).toNat3Shift (← get) + match start with + | none => + start := some (mousePos, true) + | some (pos', isHigh) => + addRoad pos' mousePos isHigh + start := none + if (← isKeyDown Key.c) then do + start := none if ← IO.hasFinished task then let cmd ← (.ofExcept task.get) try

@@ -523,23 +627,26 @@ modifyf ticks (· + 1)

renderFrame do 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 renderWithCamera camera do - let s ← get - drawGrid (s.origin.x / 10) 1 + -- 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 => - drawCubeV (pos.1.toVector3Shift (← get)) ⟨0.1, 0.1, 0.1⟩ Color.Raylean.pink + | some (pos, isHigh) => + 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) | none => pure () - -- TODO if start then render temporary line - render s camera + render (← get) camera closeWindow 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 - setConfigFlags 0x00002004 - initWindow screenWidth screenHeight "MonotoniCity" + setConfigFlags <| Flags.window_resizable ||| Flags.window_highdpi + initWindow initialScreenWidth initialScreenHeight "MonotoniCity" setTargetFPS fps gameLoop.run' { rng := mkStdGen (← IO.rand 0 (2 ^ 32))

Changes