Improve Road.cost, add fake soundtrack

Changes

3 changed files (+19/-7)

• Main.lean
  • @@ -235,12 +235,14 @@ | 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) * + def diff (a b : Nat) := if a < b then b - a else a - b + + def Road.cost (r : Road) (y y' : Nat) := + 10 * (if y == 10 && y' == 10 then 1 else 10 * ((diff y 10) ^ 2 + (diff y' 10) ^ 2)) * match r with | none => 0 - | low => 2 - | high => 10 + | low => 1 + | high => 5 instance [Lean.ToJson α] : Lean.ToJson (Vector α n) where toJson := Array.toJson ∘ Vector.toArray
  • @@ -638,8 +640,6 @@ modifyf dists (·.push <| mkDist (← get).grid b.entrance)
    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 - /-- Snap `a` to the nearest small `b` multiple -/ def snap (a : Int) (b : Nat) := if a ≤ -b / 2 then
  • @@ -663,7 +663,7 @@ let (length, dir) := endpointsToRoad start stop
    if dir == di 0 0 0 || dir == di 0 1 0 || dir == di 0 (-1) 0 then throw "Road cannot go straight up or down" let road : Road := if isHigh then .high else .low - spend <| length * road.cost dir start.y + spend <| length * road.cost start.y stop.y -- TODO: Better heuristic here let mut name := "" let stop := start.appdk dir length
• README.md
  • @@ -22,6 +22,8 @@ MonotoniCity has both a console and a GUI window. Type `help` in the console to get a list of hotkeys for the GUI (TODO: document all the commands).
    I recommend running the game with `rlwrap` for a slightly nicer console. + There's no soundtrack currently but you can play some nice tracks from the Simutrans soundtrack using `mpv --playlist=soundtrack --shuffle --loop-playlist --no-video`. + ## Why the name? `monotonicity` is a tactic in Lean.
• soundtrack (new)
  • @@ -0,0 +1,10 @@
    + -- Simutrans Float On By + https://www.youtube.com/watch?v=PFDXA7HaMuQ&list=PLzRXNerdR1xM1qAkIQANJeDmWgyJc6KBa&index=26 + -- Simutrans Above the Sky + https://www.youtube.com/watch?v=fR4vQfkSYxg&list=PLzRXNerdR1xM1qAkIQANJeDmWgyJc6KBa&index=44 + -- Simutrans Salty Breeze + https://www.youtube.com/watch?v=gjVUW82DTSo&list=PLzRXNerdR1xM1qAkIQANJeDmWgyJc6KBa&index=47 + -- Simutrans Techno Movement + https://www.youtube.com/watch?v=74O3Lcg0fPk&list=PLzRXNerdR1xM1qAkIQANJeDmWgyJc6KBa&index=48 + -- Simutrans Last Sunday + https://www.youtube.com/watch?v=OQro79efFPo&list=PLzRXNerdR1xM1qAkIQANJeDmWgyJc6KBa&index=49