Fix a lot of bugs

Changes

1 changed files (+34/-32)

• Main.lean
  • @@ -357,6 +357,8 @@ setf dists #[]
    for building in (← get).buildings do if !building.deleted then modifyf dists (·.push <| mkDist (← get).grid building.entrance) + else + modifyf dists (·.push <| .ofList []) /-- 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
  • @@ -391,7 +393,7 @@ let s := ← get
    if u == s.buildings[p.dest]!.entrance then if p.dir.isSome then modifyf money (· + 100) - let mut p' := { p with dir := none, pos := s.buildings[p.dest]!.exit } + let mut p' := { p with dir := none } if p.dest == p.home then -- At home, go to work or shops if (← rand 1000) == 0 then
  • @@ -412,8 +414,9 @@ 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 } + -- Start the journey! + if p'.dest != p.dest then + p' := { p' with pos := s.buildings[p.dest]!.exit } 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
  • @@ -650,14 +653,14 @@ let dims := dims.map String.toNat!
    have : dims.length = 10 := by grind 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" + throw <| .userError "Failed to parse add building command" | "r" :: dims => if h : dims.length = 7 then 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) - else - throw <| .userError "Road cannot go straight up or down" + else + throw <| .userError "Failed to parse add road command" | "y" :: dims => if h : dims.length = 3 then let dims := dims.map String.toNat!
  • @@ -742,18 +745,17 @@ 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 - -- Unfortunately we can't use `Nat3.toVector3` here because they're `Int`s - let posV3 := - match peep.dir with - | none => - peep.pos.toVector3Shift s - | 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.0025, 0⟩) 0.075 0.075 0.075 Color.Raylean.lime - drawCubeWires (posV3 + ⟨0, 0.0025, 0⟩) 0.075 0.075 0.075 .black + -- Unfortunately we can't use `Nat3.toVector3` here because they're `Int`s + let posV3 := + match peep.dir with + | none => + peep.pos.toVector3Shift s + | 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.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` -/
  • @@ -807,40 +809,40 @@ 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 + let x ← rand 300 + let z ← rand 300 + if 100 < x && x < 200 && 100 < z && z < 200 then continue - return ⟨(← get).origin.x - 100 + x, 10, (← get).origin.z - 100 + z⟩ - for i in [:20] do + return ⟨(← get).origin.x - 150 + x, 10, (← get).origin.z - 150 + z⟩ + -- Spawn the commerical buildings first so peeps' workplaces get evenly distributed among them + for i in [:3] do let side ← rand 4 try - addBuilding .house (← randPosExt) ⟨5, 1, 5⟩ (side, 2) (side, 3) + addBuilding .office (← randPos) ⟨10, 2, 10⟩ (side, 5) (side, 6) catch e => IO.println e - -- TODO bump up these numbers - for i in [:2] do + for i in [:5] do let side ← rand 4 try - addBuilding .apartment (← randPos) ⟨10, 3, 5⟩ (side, 1) (side, 2) + addBuilding .shop (← randPos) ⟨5, 1, 10⟩ (side, 3) (side, 4) 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) + addBuilding .factory (← randPosExt) ⟨10, 4, 10⟩ (side, 5) (side, 6) catch e => IO.println e - for i in [:0] do + for i in [:40] do let side ← rand 4 try - addBuilding .shop (← randPos) ⟨5, 1, 10⟩ (side, 3) (side, 4) + addBuilding .house (← randPosExt) ⟨5, 1, 5⟩ (side, 2) (side, 3) catch e => IO.println e - for i in [:0] do + for i in [:10] do let side ← rand 4 try - addBuilding .factory (← randPosExt) ⟨10, 4, 10⟩ (side, 5) (side, 6) + addBuilding .apartment (← randPos) ⟨10, 3, 5⟩ (side, 1) (side, 2) catch e => IO.println e