Don't hardcode origin in Road.cost

Changes

1 changed files (+7/-6)

• Main.lean
  • @@ -235,14 +235,12 @@ | low
    | high deriving Inhabited, BEq, Lean.ToJson, Lean.FromJson - 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)) * + (if y == 0 && y' == 0 then 1 else 10 * (y ^ 2 + y' ^ 2)) * match r with | none => 0 - | low => 1 - | high => 5 + | low => 10 + | high => 50 instance [Lean.ToJson α] : Lean.ToJson (Vector α n) where toJson := Array.toJson ∘ Vector.toArray
  • @@ -640,6 +638,8 @@ 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,8 @@ 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 start.y stop.y + let originy := (← get).origin.y + spend <| length * road.cost (diff start.y originy) (diff stop.y originy) -- TODO: Better heuristic here let mut name := "" let stop := start.appdk dir length