More monad transformer fun

Changes

1 changed files (+48/-30)

• Main.lean
  • @@ -163,6 +163,7 @@ | .shop => Color.Raylean.purple
    | .factory => Color.Raylean.green def cost (b : Building) := + -- Make taller buildings quadratically more expensive 100 * b.size.x * b.size.y * b.size.y * b.size.z * match b.variant with | .house => 1
  • @@ -312,8 +313,17 @@ /-
    ## doTick and friends -/ - instance [Monad m] : MonadLift (StateM σ ·) (StateT σ m ·) where + /-- Lift vanilla `StateM` into `StateT` (state monad wrapped around something else) -/ + instance [Monad m] : MonadLift (StateM σ) (StateT σ m) where monadLift x := modifyGet <| StateT.run x + + /-- Lift exception throwing into the IO monad -/ + instance : MonadLift (Except String) IO where + monadLift x := .ofExcept x + + /-- For lifting `StateT State (Except String)` to `StateT State IO` -/ + instance [MonadLift m n] [Monad n] : MonadLift (StateT σ m) (StateT σ n) where + monadLift x s := monadLift (x s) /-- Macro for easily updating a specific field of the state -/ macro "modifyf" field:ident fn:term : term =>
  • @@ -400,6 +410,14 @@ for hi : i in [1:A'.size] do
    let j ← rand (i + 1) A' := A'.swap i j return A'.toArray + + abbrev homeToWorkProb := 1000 + abbrev toShopProb := 500 + abbrev factoryToShopProb := 25 + abbrev workToHomeProb := 1000 + abbrev breakdownProb := 5000 + abbrev shopToHomeProb := 100 + abbrev repairProb := 100 /-- Run one iteration of the game -/ def doTick : StateM State Unit := do
  • @@ -421,23 +439,23 @@ modifyf money (· + 100)
    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 + if (← rand homeToWorkProb) == 0 then p' := { p' with dest := p.work } - else if h : (← rand 500) == 0 && !s.shops.isEmpty then + else if h : (← rand toShopProb) == 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 : s.buildings[p.work]!.variant == .factory && !s.shops.isEmpty && (← rand 25) == 0 then + if h : s.buildings[p.work]!.variant == .factory && !s.shops.isEmpty && (← rand factoryToShopProb) == 0 then let shopIdx ← rand s.shops.size p' := { p' with dest := shopIdx } - else if (← rand 1000) == 0 then + else if (← rand workToHomeProb) == 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 + else if (← rand shopToHomeProb) == 0 then p' := { p with dest := p.home } -- Start the journey! if p'.dest != p.dest then
  • @@ -449,7 +467,7 @@ occupied := occupied.insert u
    peeps := peeps.push ({ p with dir := none }) else if p.brokenDown then occupied := occupied.insert u - peeps := peeps.push ({ p with dir := none, brokenDown := (← rand 100) != 0 }) + peeps := peeps.push ({ p with dir := none, brokenDown := (← rand repairProb) != 0 }) else let dist := s.dists[p.dest]! let mut neighbors := #[]
  • @@ -499,7 +517,7 @@ break
    if p' == p then occupied := occupied.insert u p' := { p with pos := u, dir := none } - peeps := peeps.push { p' with brokenDown := (← rand 5000) == 0 } + peeps := peeps.push { p' with brokenDown := (← rand breakdownProb) == 0 } setf peeps peeps setf occupied occupied modifyf ticks (· + 1)
  • @@ -535,33 +553,32 @@ 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 + /-- Spend some money! -/ + def spend (cost : Nat) : StateT State (Except String) Unit := do if cost > (← get).money then - throw <| .userError s!"Need ${cost}, only have ${(← get).money}" + throw s!"Need ${cost}, only have ${(← get).money}" modifyf money (· - cost) /-- Add a building to the state -/ - def addBuilding (variant : BuildingVariant) (pos size entrance exit : Nat3) : StateT State IO Unit := do + def addBuilding (variant : BuildingVariant) (pos size entrance exit : Nat3) : StateT State (Except String) Unit := do if entrance == exit then - throw <| .userError "Building entrance cannot be in same position as exit" + throw "Building entrance cannot be in same position as exit" let notOnSide (p : Nat3) := p.x != pos.x && p.x != pos.x + size.x && p.z != pos.z && p.z != pos.z + size.z if notOnSide entrance || notOnSide exit then - throw <| .userError "Building entrance or exit not on side of building" + throw "Building entrance or exit not on side of building" for x in [pos.x:pos.x + size.x + 1] do for y in [pos.y:pos.y + size.y + 1] do for z in [pos.z:pos.z + size.z + 1] do if (← get).grid.contains ⟨x, y, z⟩ then - throw <| IO.userError "Building collides with existing road" + throw "Building collides with existing road" for b' in (← get).buildings do if Building.checkCollide pos size b'.pos b'.size then - throw <| IO.userError "Building collides with existing building" + throw "Building collides with existing building" if Building.checkCollide (entrance - ⟨1, 0, 1⟩) ⟨2, 1, 2⟩ b'.pos b'.size then - throw <| IO.userError "Building entrance collides with existing building" + throw "Building entrance collides with existing building" if Building.checkCollide (exit - ⟨1, 0, 1⟩) ⟨2, 1, 2⟩ b'.pos b'.size then - throw <| IO.userError "Building exit collides with existing building" + throw "Building exit collides with existing building" let b : Building := { variant pos
  • @@ -634,10 +651,10 @@ -- Sanity check
    #guard endpointsToRoad ⟨5, 5, 5⟩ ⟨1, 5, 2⟩ == (4, di (-1) 0 (-1)) /-- Add roads to the state -/ - def addRoad (start stop : Nat3) (isHigh : Bool) : StateT State IO Unit := do + 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 - throw <| .userError "Road cannot go straight up or down" + throw "Road cannot go straight up or down" let road : Road := if isHigh then .high else .low spend <| length * road.cost dir start.y -- TODO: Better heuristic here
  • @@ -663,9 +680,9 @@ 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 IO Unit := do + def addMultiRoad (start stop : Nat3) (isHigh : Bool) : StateT State (Except String) Unit := do if start.y != stop.y then - throw <| .userError s!"Multilane road must remain at same level" + throw "Multilane road must remain at same level" -- We can't overwrite `start` and `stop` here since we need to preserve the direction of the road let y := start.y let swizzled := diff start.x stop.x < diff start.z stop.z
  • @@ -696,19 +713,20 @@ else
    addRoad' ⟨i - d, y, start'.z⟩ ⟨i, y, stop'.z⟩ addRoad' ⟨i - d, y, stop'.z⟩ ⟨i, y, start'.z⟩ - def addYield (pos : Nat3) : StateT State IO Unit := do + def addYield (pos : Nat3) : StateT State (Except String) Unit := do spend 10 if !(← get).grid.contains pos then - throw <| .userError s!"Could not place yield at {pos}" + throw s!"Could not place yield at {pos}" modifyf grid (·.modify pos fun p ↦ { p with control := .yield }) - def addTrafficLight (pos : Nat3) (t : TrafficLight) : StateT State IO Unit := do + def addTrafficLight (pos : Nat3) (t : TrafficLight) : StateT State (Except String) Unit := do spend 100 if !(← get).grid.contains pos then - throw <| .userError s!"Could not place traffic light at {pos}" + throw s!"Could not place traffic light at {pos}" modifyf grid (·.modify pos fun p ↦ { p with control := .trafficLight t }) - def addIntersection (pos : Nat3) : StateT State IO Unit := do + -- TODO: A simpler intersection might work better here? + def addIntersection (pos : Nat3) : StateT State (Except String) Unit := do -- Main roads addRoad (pos + ⟨0, 0, 3⟩) (pos + ⟨5, 0, 3⟩) false addRoad (pos + ⟨5, 0, 2⟩) (pos + ⟨0, 0, 2⟩) false
  • @@ -958,9 +976,9 @@ -- `.dot` is just element-wise product, not the dot product!
    return project (pos2.dot windowScale) camera (Float.ofInt (y / sensitivity) / scale) (← getScreenWidth).toFloat (← getScreenHeight).toFloat def spawnInitBuildings : StateT State IO Unit := do - let randPos : StateT State IO Nat3 := do + let randPos : StateM State Nat3 := do return ⟨(← get).origin.x - 50 + (← rand 100), 10, (← get).origin.z - 50 + (← rand 100)⟩ - let randPosExt : StateT State IO Nat3 := do + let randPosExt : StateM State Nat3 := do repeat let x ← rand 200 let z ← rand 200