0 | module Days.Day13
  1 |
  2 | import Data.String
  3 | import Data.List1
  4 | import Data.Vect
  5 | import Data.SortedMap
  6 | import Data.Primitives.Views
  7 | import System
  8 | import Debug.Trace
  9 |
 10 | import Control.Eff
 11 | import Control.Eff.Except
 12 |
 13 | import Util
 14 |
 15 | record Button where
 16 |   constructor MkButton
 17 |   x, y : Integer
 18 | %name Button b, b2, b3
 19 |
 20 | parseButton : Has (ExceptL "parse" String) fs => String -> Eff fs Button
 21 | parseButton str = do
 22 |   [_, _, x, y] <-
 23 |     noteAt "parse" "button: split" .
 24 |       toVect 4 . forget . split (== ' ') $ str
 25 |   x <-
 26 |     noteAt "parse" "button: x" .
 27 |      parsePositive . pack . filter isDigit . unpack $ x
 28 |   y <-
 29 |     noteAt "parse" "button: x" .
 30 |      parsePositive . pack . filter isDigit . unpack $ y
 31 |   pure $ MkButton x y
 32 |
 33 | record Prize where
 34 |   constructor MkPrize
 35 |   x, y : Integer
 36 | %name Prize p, p2, p3
 37 |
 38 | parsePrize : Has (ExceptL "parse" String) fs => String -> Eff fs Prize
 39 | parsePrize str = do
 40 |   [_, x, y] <-
 41 |     noteAt "parse" "prize: split" .
 42 |       toVect 3 . forget . split (== ' ') $ str
 43 |   x <-
 44 |     noteAt "parse" "prize: x" .
 45 |      parsePositive . pack . filter isDigit . unpack $ x
 46 |   y <-
 47 |     noteAt "parse" "prize: x" .
 48 |      parsePositive . pack . filter isDigit . unpack $ y
 49 |   pure $ MkPrize x y
 50 |
 51 | record Machine where
 52 |   constructor MkMachine
 53 |   a, b : Button
 54 |   prize : Prize
 55 | %name Machine m, m2, m3
 56 |
 57 | cost : (lower, upper : Integer) -> Machine -> Maybe Integer
 58 | cost lower upper m =
 59 |   let xs = mapMaybe cost' $ lazyRange' lower upper
 60 |   in case xs of
 61 |     [] => Nothing
 62 |     (y :: ys) => 
 63 |       Just (foldl1 min $ y ::: toList ys)
 64 |   where
 65 |   cost' : Integer -> Maybe Integer
 66 |   cost' a_count =
 67 |     let (a_x, a_y) = (m.a.x * a_count, m.a.y * a_count)
 68 |         (d_x, d_y) = (m.prize.x - a_x, m.prize.y - a_y)
 69 |     in if d_x < 0 || d_y < 0
 70 |       then Nothing
 71 |       else if d_x == 0 && d_y == 0
 72 |         then Just (a_count * 3)
 73 |         else
 74 |           let (div_x, rem_x) = (d_x `div` m.b.x, d_x `mod` m.b.x)
 75 |           in if rem_x == 0
 76 |             then if div_x * m.b.y + a_count * m.a.y == m.prize.y
 77 |               then Just (a_count * 3 + div_x)
 78 |               else Nothing
 79 |             else Nothing
 80 |
 81 | costAuto : Machine -> Maybe Integer
 82 | costAuto m =
 83 |   let presses : Vect _ _ =
 84 |         [
 85 |           (min (m.prize.x `div` m.a.x)
 86 |            (m.prize.x `div` m.b.x))
 87 |         , (min (m.prize.y `div` m.a.y)
 88 |            (m.prize.y `div` m.b.y))
 89 |         ]
 90 |       max_presses = foldl1 max . map (+1) $ presses
 91 |   in cost 0 max_presses m
 92 |
 93 | Show Machine where
 94 |   show (MkMachine a b prize) =
 95 |     "Button A: X+\{show a.x}, Y+\{show a.y}\nButton B: X+\{show b.x}, Y+\{show b.y}\nPrize: X=\{show prize.x}, Y=\{show prize.y}"
 96 |
 97 | parseMachine : Has (ExceptL "parse" String) fs => Vect 3 String -> Eff fs Machine
 98 | parseMachine [a, b, prize] = do
 99 |   a <- parseButton a
100 |   b <- parseButton b
101 |   prize <- parsePrize prize
102 |   pure $ MkMachine a b prize
103 |
104 | record Input where
105 |   constructor MkInput
106 |   len : Nat
107 |   machines : Vect len Machine
108 | %name Input i
109 |
110 | Show Input where
111 |   show (MkInput len machines) = joinBy "\n\n" . toList . map show $ machines
112 |
113 | parseInput : Has (ExceptL "parse" String) fs => String -> Eff fs Input
114 | parseInput str = do
115 |   groups <- noteAt "parse" "Grouping machines" .
116 |     traverse (toVect 3) . forget . split null . map trim . lines . trim $ str
117 |   machines <- traverse parseMachine $ groups
118 |   pure $ MkInput (length machines) (fromList machines)
119 |
120 | export
121 | part1 : String -> Eff [IO, Except String] (Integer, Input)
122 | part1 str = do
123 |   input <- tagAt "parse"  $ parseInput str
124 |   let res = sum . mapMaybe costAuto . toList $ input.machines
125 |   pure (res, input)
126 |
127 | export
128 | part2 : Input -> Eff [IO, Except String] Integer
129 | part2 (MkInput len machines) = do
130 |   let machines =
131 |     map (\(MkMachine a b (MkPrize x y)) =>
132 |             (MkMachine a b (MkPrize (x * 10000000000000) (y * 10000000000000)))) machines
133 |   let res = sum . mapMaybe costAuto . toList $ machines
134 |   pure res
135 |