0 | module Days.Day15

  2 | import Data.String

  3 | import Data.Vect

  4 | import Data.List1

  5 | import System

  7 | import Control.Eff

  8 | import Control.Eff.Except

 10 | import Util

 12 | data ErrorL = LParse | LSolve

 14 | Show ErrorL where

 15 |   show LParse = "parsing"

 16 |   show LSolve = "solving"

 18 | ParseError : Type -> Type

 19 | ParseError = ExceptL LParse String

 21 | SolveError : Type -> Type

 22 | SolveError = ExceptL LSolve String

 24 | data Cell = Box | BoxR | BoxL | Wall | Empty

 26 | data Move = Up | Down | Left | Right

 28 | Eq Move where

 29 |   (==) Up Up = True

 30 |   (==) Down Down = True

 31 |   (==) Left Left = True

 32 |   (==) Right Right = True

 33 |   (==) _ _ = False

 35 | Show Move where

 36 |   show Up = "^"

 37 |   show Down = "v"

 38 |   show Left = "<"

 39 |   show Right = ">"

 41 | isBox : Cell -> Bool

 42 | isBox Box = True

 43 | isBox BoxL = True

 44 | isBox BoxR = True

 45 | isBox _ = False

 48 | cellToChar : Cell -> Char

 49 | cellToChar Box = 'O'

 50 | cellToChar Wall = '#'

 51 | cellToChar BoxL = '['

 52 | cellToChar BoxR = ']'

 53 | cellToChar Empty = '.'

 55 | parseCell : Has ParseError fs => Char -> Eff fs Cell

 56 | parseCell 'O' = pure Box

 57 | parseCell '#' = pure Wall

 58 | parseCell '.' = pure Empty

 59 | parseCell '@' = pure Empty -- Actually the robot, but we extract it elsewhere

 60 | parseCell c = throwAt LParse "Invalid cell character: \{show c}"

 62 | parseMove : Has ParseError fs => Char -> Eff fs Move

 63 | parseMove '^' = pure Up

 64 | parseMove 'v' = pure Down

 65 | parseMove '<' = pure Left

 66 | parseMove '>' = pure Right

 67 | parseMove c = throwAt LParse "Invalid move character: \{show c}"

 69 | moveToDirection : Move -> (Integer, Integer)

 70 | moveToDirection Up = (-1, 0)

 71 | moveToDirection Down = (1, 0)

 72 | moveToDirection Left = (0, -1)

 73 | moveToDirection Right = (0, 1)

 75 | record Input where

 76 |   constructor MkInput

 77 |   rows, cols : Nat

 78 |   room : Grid rows cols Cell

 79 |   robot_pos : Coord rows cols

 80 |   moves : List Move

 82 | pushBox : Has SolveError fs =>

 83 |         {rows, cols : Nat} -> (room : Grid rows cols Cell)

 84 |         -> (box : Coord rows cols) -> (move : Move)

 85 |         -> Eff fs $ Maybe (Grid rows cols Cell)

 86 | pushBox room box move = do

 87 |   let box_val = box `index` room

 88 |   next_pos <- noteAt LSolve "Box out of bounds" $

 89 |     step box (moveToDirection move)

 90 |   let next_val = next_pos `index` room

 91 |   True <- pure $ isBox box_val

 92 |     | _ => throwAt LSolve "Called on non-box"

 93 |   case next_val of

 94 |     -- Hitting a wall means we can't move

 95 |     Wall => pure $ Nothing

 96 |     -- If we hit an empty cell, move forward into it

 97 |     Empty =>

 98 |       let room = replaceAt next_pos box_val room

 99 |           room = replaceAt box next_val room

100 |       in pure $ Just room

101 |     -- If we hit another box, recurse

102 |     box_type => do

103 |       Just room <- pushBox room next_pos move

104 |         | _ => pure Nothing

105 |       let next_val = next_pos `index` room

106 |       let room = replaceAt next_pos box_val room

107 |       let room = replaceAt box next_val room

108 |       -- If this is a double sided box, and we are going up or down, push our

109 |       -- partner, if we have one

110 |       if move == Up || move == Down

111 |         then case box_type of

112 |           BoxR => do

113 |             left <- noteAt LSolve "BoxR out of bounds" $

114 |               step box (0, -1)

115 |             BoxL <- pure $ left `index` room

116 |               | _ => pure $ Just room

117 |             Just room <- pushBox room left move

118 |               | _ => pure Nothing

119 |             pure $ Just room

120 |           BoxL => do

121 |             right <- noteAt LSolve "BoxR out of bounds" $

122 |               step box (0, 1)

123 |             BoxR <- pure $ right `index` room

124 |               | _ => pure $ Just room

125 |             Just room <- pushBox room right move

126 |               | _ => pure Nothing

127 |             pure $ Just room

128 |           _ => pure $ Just room

129 |         else pure $ Just room

131 | nextMove : Has SolveError fs => Input -> Eff fs $ Maybe Input

132 | nextMove (MkInput rows cols room robot_pos []) = pure Nothing

133 | nextMove (MkInput rows cols room robot_pos (move :: moves)) = do

134 |   next_pos <- noteAt LSolve "Robot out of bounds" $

135 |     step robot_pos (moveToDirection move)

136 |   case next_pos `index` room of

137 |     Wall => pure . Just $ MkInput rows cols room robot_pos moves

138 |     Empty => pure . Just $ MkInput rows cols room next_pos moves

139 |     box_type => do

140 |       Just room <- pushBox room next_pos move

141 |         | _ => pure . Just $ MkInput rows cols room robot_pos moves

142 |       pure . Just $ MkInput rows cols room next_pos moves

144 | allMoves : Has SolveError fs => Input -> Eff fs $ LazyList Input

145 | allMoves x = do

146 |   Just next <- nextMove x

147 |     | _ => pure [x]

148 |   map (x ::) (allMoves next)

150 | sumGpsCoordinates : Input -> Integer

151 | sumGpsCoordinates x =

152 |   let xs = map (\(a,b) => (finToInteger a, finToInteger b))

153 |                . map fst . filter (isBox . snd) . flat

154 |                $ x.room

155 |       gps = map (\(r,c) => 100 * r + c) xs

156 |   in sum gps

158 | Show Input where

159 |   show i =

160 |     let grid_lines =

161 |           toList . map (joinBy "" . map singleton . toList) . replaceAt i.robot_pos '@' .

162 |           map (map cellToChar) $ i.room

163 |         rest_lines =

164 |           [ ""

165 |           , "Remaining Moves: \{show . length $ i.moves}"

166 |           , "Next Move : \{show $ head' i.moves}"]

167 |     in unlines $ grid_lines ++ rest_lines

169 | parseInput : Has ParseError fs => String -> Eff fs Input

170 | parseInput str = do

171 |   (room ::: moves :: []) <- pure . split null . lines . trim $ str

172 |     | _ => throwAt LParse "Unable to split rooms and moves"

173 |   let (room, moves) = (unlines . map trim $ room, joinBy "" . map trim $ moves)

174 |   (rows ** cols ** room_in) <- noteAt LParse "Failed reading room grid" $ stringTo2D room

175 |   room <- traverse (traverse parseCell) room_in

176 |   moves <- traverse parseMove . unpack $ moves

177 |   robot_pos <- noteAt LParse "No robot found" .

178 |     head' . map fst . filter ((== '@') . snd) . flat $ room_in

179 |   pure $ MkInput rows cols room robot_pos moves

181 | last' : LazyList a -> Maybe a

182 | last' [] = Nothing

183 | last' (x :: []) = Just x

184 | last' (x :: y :: xs) = last' (y :: xs)

187 | part1 : String -> Eff [IO, Except String] (Integer, Input)

188 | part1 str = do

189 |   input <- tagAt LParse $ parseInput str

190 |   all_moves <- tagAt LSolve $ allMoves input

191 |   -- traverse_ printLn $ toList all_moves

192 |   Just last <- pure $ last' all_moves

193 |     | _ => throw "No moves?"

194 |   let output = sumGpsCoordinates last

195 |   pure (output, input)

198 | part2 : Input -> Eff [IO, Except String] Integer