Changes

2 changed files (+23/-31)

• Main.lean
  • @@ -35,8 +35,8 @@ instance : HMul Vector3 Float Vector3 where
    instance : HDiv Vector3 Float Vector3 where hDiv a c := ⟨a.x / c, a.y / c, a.z / c⟩ - def Types.Vector3.dist (a b : Vector3) := - Float.sqrt <| (a.x - b.x) ^ 2 + (a.y - b.y) ^ 2 + (a.z - b.z) ^ 2 + def Types.Vector3.length (a : Vector3) := + Float.sqrt <| a.x ^ 2 + a.y ^ 2 + a.z ^ 2 /-- This is in Raylib but not Raylean so let's just define it ourselves -/ def drawCubeV (pos size : Vector3) (color : Color) :=
  • @@ -654,7 +654,8 @@ def endpointsToRoad (start stop : Nat3) :=
    -- Sanity check #guard endpointsToRoad ⟨5, 5, 5⟩ ⟨1, 5, 2⟩ == (4, di (-1) 0 (-1)) - /-- Add roads to the state -/ + /-- Add roads to the state + Note that this DOES NOT call `mkDists` so it's your responsibility to do that! -/ def addRoad (start stop : Nat3) (isHigh : Bool) : StateT State (Except String) Unit := do let (length, dir) := endpointsToRoad start stop if dir == di 0 0 0 || dir == di 0 1 0 || dir == di 0 (-1) 0 then
  • @@ -683,7 +684,6 @@ def addRoad (start stop : Nat3) (isHigh : Bool) : StateT State (Except String) U
    g := g.insert v ⟨name, .none, .replicate 27 .none⟩ g.modify v (fun p ↦ if i < length then { p with e := p.e.set! dir road } else p) - mkDists def addMultiRoad (start stop : Nat3) (isHigh : Bool) : StateT State (Except String) Unit := do if start.y != stop.y then
  • @@ -737,10 +737,10 @@ def deleteControl (pos : Nat3) : StateT State (Except String) Unit := do
    def addIntersection (pos : Nat3) : StateT State (Except String) Unit := do -- Main roads - addRoad (pos + ⟨0, 0, 1⟩) (pos + ⟨3, 0, 1⟩) false + addRoad (pos + ⟨0, 0, 2⟩) (pos + ⟨3, 0, 2⟩) 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 + addRoad (pos + ⟨2, 0, 3⟩) (pos + ⟨2, 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
  • @@ -751,6 +751,7 @@ def addIntersection (pos : Nat3) : StateT State (Except String) Unit := do
    addTrafficLight (pos + ⟨3, 0, 1⟩) ⟨10, 10, 0⟩ addTrafficLight (pos + ⟨2, 0, 3⟩) ⟨10, 10, 10⟩ addTrafficLight (pos + ⟨1, 0, 0⟩) ⟨10, 10, 10⟩ + mkDists /-- Currently unused -/ def addIntersection' (pos : Nat3) : StateT State (Except String) Unit := do
  • @@ -779,6 +780,7 @@ def addIntersection' (pos : Nat3) : StateT State (Except String) Unit := do
    addYield (pos + ⟨4, 0, 1⟩) addYield (pos + ⟨1, 0, 4⟩) addYield (pos + ⟨4, 0, 4⟩) + mkDists inductive Action | delete
  • @@ -850,6 +852,7 @@ def handleCmd (cmd : String) : StateT State IO Unit := do
    let dims := dims.map String.toNat! have : dims.length = 7 := by grind addRoad ⟨dims[0], dims[1], dims[2]⟩ ⟨dims[3], dims[4], dims[5]⟩ (dims[6] == 1) + mkDists else throw <| .userError "Failed to parse add road command" | "m" :: dims =>
  • @@ -857,6 +860,7 @@ def handleCmd (cmd : String) : StateT State IO Unit := do
    let dims := dims.map String.toNat! have : dims.length = 7 := by grind addMultiRoad ⟨dims[0], dims[1], dims[2]⟩ ⟨dims[3], dims[4], dims[5]⟩ (dims[6] == 1) + mkDists else throw <| .userError "Failed to parse add multilane road command" | "y" :: dims =>
  • @@ -962,6 +966,8 @@ def render (s : State) (camera : Camera3D) (frames : Nat) : IO Unit := do
    -- Render peeps for peep in s.peeps do -- Unfortunately we can't use `Nat3.toVector3` here because they're `Int`s + if peep.pos == s.buildings[peep.dest]!.entrance && peep.dir.isNone then + continue let posV3 := match peep.dir with | none =>
  • @@ -970,7 +976,8 @@ def render (s : State) (camera : Camera3D) (frames : Nat) : IO Unit := do
    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.035, 0⟩) 0.075 0.075 0.075 (if peep.isCommercial then Color.Raylean.beige else Color.Raylean.skyblue) + let color := if peep.brokenDown then Color.Raylean.darkpurple else if peep.isCommercial then Color.Raylean.beige else Color.Raylean.skyblue + drawCube (posV3 + ⟨0, 0.035, 0⟩) 0.075 0.075 0.075 color drawCubeWires (posV3 + ⟨0, 0.035, 0⟩) 0.075 0.075 0.075 .black /-- Get 3D coordinates at level `y` of 2D screen position
  • @@ -992,7 +999,7 @@ def project (p : Vector2) (camera : Camera3D) (y width height : Float) : Vector3
    -- Radial move let dradial := mul * Vector3.mk (camera.target.x - camera.position.x) 0 (camera.target.z - camera.position.z) -- Now compute the tangential move - let d := camera.position.dist camera.target + let d := camera.position - camera.target |>.length -- The term `h / (h + r * .tan verta)` is intuitively how much horizontal lines get squished or stretched let mul := d * .tan hora / r * h / (h + r * .tan verta) -- Tangential move
  • @@ -1059,8 +1066,10 @@ def doAction (actionState : List Nat3) (curAction : Action) (mousePos : Nat3) (n
    delete pos mousePos | pos :: _, .road isHigh => addRoad pos mousePos isHigh + mkDists | pos :: _, .multiRoad isHigh => addMultiRoad pos mousePos isHigh + mkDists | pos :: pos' :: entrance :: _, .building variant => let (pos, size) := endpointsToPosSize pos { pos' with y := pos.y + newHeight / sensitivity } addBuilding variant pos size entrance mousePos
  • @@ -1119,8 +1128,9 @@ def getInput (stdin : IO.FS.Stream) := do
    def padTime (n : Nat) := if n < 10 then s!"0{n}" else s!"{n}" - def gameLoop : StateT State IO Unit := do - spawnInitBuildings + def gameLoop (needSpawn : Bool) : StateT State IO Unit := do + if needSpawn then + spawnInitBuildings setf money 50000 let mut camera : Camera3D := { position := ⟨scale, scale, scale⟩
  • @@ -1201,6 +1211,7 @@ def main (args : List String) : IO Unit := do
    -- The initial dimensions don't matter since we immediately resize the window to work around a HiDPI bug maximizeWindow setTargetFPS fps + let mut needSpawn := true let mut s := { rng := mkStdGen (← IO.rand 0 (2 ^ 32)) ticks := 0
  • @@ -1218,8 +1229,9 @@ def main (args : List String) : IO Unit := do
    if h : args.length > 0 then try s ← loadState args[0] + needSpawn := false catch e => IO.println s!"Failed to load save {args[0]} with error {e}" - gameLoop.run' s + gameLoop needSpawn |>.run' s -- We can't use `exit` because that won't kill the `getInput` task IO.Process.forceExit 0
• lens.patch (deleted)
  • @@ -1,20 +0,0 @@
    - diff --git a/Lens/Elab.lean b/Lens/Elab.lean - index 9d9c1bc..98a708d 100644 - --- a/Lens/Elab.lean - +++ b/Lens/Elab.lean - @@ -21,12 +21,9 @@ elab "makeLenses" structIdent:ident : command => do - let fieldNameIdent := mkIdent field.fieldName - let some decl := env.find? (field.projFn) - | throwErrorAt structIdent s!"Could not find project function {field.projFn}" - - let (some fieldTypeName, some fieldTypeArgs) := (← liftTermElabM (liftMetaM ( - - forallTelescope decl.type fun _ body - - => pure (body.getAppFn.constName?, body.getAppArgs.mapM (·.constName?))))) - - | throwErrorAt structIdent "Not a structure name" - - let d ← fieldTypeArgs.mapM fun argName => `($(mkIdent argName)) - - let fieldTypeNameIdent := Syntax.mkCApp fieldTypeName d - + let fieldTypeNameIdent : Term ← liftTermElabM <| liftMetaM <| - + forallTelescope decl.type fun _ body => - + Lean.PrettyPrinter.delab body - let lensName := mkIdent field.fieldName - let newVal := mkIdent <| Name.mkSimple "newVal" - let l ←