feat: part 6-2

advent-of-code-2024.ipkg

@@ -20,4 +20,4 @@ modules = Main, Utils, AllDays,
           Day3.Part1, Day3.Part2,
           Day4.Part1, Day4.Part2,
           Day5.Part1, Day5.Part2,
-          Day6.Part1
+          Day6.Part1, Day6.Part2

src/AllDays.idr

@@ -11,3 +11,4 @@ import public Day4.Part2
 import public Day5.Part1
 import public Day5.Part2
 import public Day6.Part1
+import public Day6.Part2

src/Day6/Part1.idr

@@ -1,5 +1,6 @@
 module Day6.Part1
 
+import Data.Colist
 import Data.List
 import Data.Maybe
 import Data.Vect
@@ -11,9 +12,19 @@ import Utils
 
 --- TYPES
 
+public export
 data Direction = U | R | D | L
 
--- True if there is a wall
+export
+Eq Direction where
+  U == U = True
+  D == D = True
+  L == L = True
+  R == R = True
+  _ == _ = False
+
+-- True if there is an obstacle
+public export
 Map : Nat -> Nat -> Type
 Map h w = Grid h w Bool
 
@@ -26,6 +37,7 @@ parseDir 'v' = Just D
 parseDir '<' = Just L
 parseDir _ = Nothing
 
+export
 parseInput : String -> Maybe (h ** w ** (Map h w, Pos h w, Direction))
 parseInput inp = do
   (h ** w ** grid) <- parseGrid inp
@@ -45,36 +57,39 @@ predFin : Fin n -> Maybe (Fin n)
 predFin FZ = Nothing
 predFin (FS x) = Just $ weaken x
 
+export
 moveDir : {h, w : _} -> Direction -> Pos h w -> Maybe (Pos h w)
 moveDir U (i, j) = (,j) <$> predFin i
 moveDir R (i, j) = (i,) <$> strengthen (FS j)
 moveDir D (i, j) = (,j) <$> strengthen (FS i)
 moveDir L (i, j) = (i,) <$> predFin j
 
+export
 rotate : Direction -> Direction
 rotate U = R
 rotate R = D
 rotate D = L
 rotate L = U
 
-
+getRoute : {h, w : _} -> (Pos h w, Direction) -> Map h w
-covering
+            -> Colist (Pos h w, Direction)
-getRoute : {h, w : _} -> Direction -> Pos h w -> Map h w -> List (Pos h w)
+getRoute (pos, dir) mp =
-getRoute = go []
+  let Just next = moveDir dir pos
-  where
+        | Nothing => [(pos, dir)]
-    covering
+  in (pos, dir) ::
-    go : List (Pos h w) -> Direction -> Pos h w -> Map h w -> List (Pos h w)
+      if index next mp
-    go route dir pos map =
+      then getRoute (pos, rotate dir) mp
-      let Just next = moveDir dir pos
+      else getRoute (next, dir) mp
-            | Nothing => pos :: route
-      in if index next map
-         then go (pos :: route) (rotate dir) pos map
-         else go (pos :: route) dir next map
 
 --- SOLUTION
 
+covering
+forceList : Colist a -> List a
+forceList [] = []
+forceList (x :: xs) = x :: forceList xs
+
 export covering
 solution : String -> Maybe Nat
 solution inp = do
-  (h ** w ** (mp, pos, dir)) <- parseInput inp
+  (h ** w ** (mp, g)) <- parseInput inp
-  pure $ length $ nub $ getRoute dir pos mp
+  pure $ length $ nub $ map fst $ forceList $ getRoute g mp

src/Day6/Part2.idr

@@ -0,0 +1,64 @@
+module Day6.Part2
+
+import Data.Colist
+import Data.List
+import Data.Maybe
+import Data.Vect
+
+import Day6.Part1
+import Utils
+
+%default total
+
+--- DATA
+
+getCollisions : {h, w : _} -> (Pos h w, Direction) -> Map h w
+            -> Colist (Pos h w, Direction)
+getCollisions (pos, dir) mp =
+  let Just next = moveDir dir pos
+        | Nothing => []
+  in if index next mp
+      then (next, dir) :: getCollisions (pos, rotate dir) mp
+      else assert_total $ getCollisions (next, dir) mp
+
+insertObs : Pos h w -> Map h w -> Map h w
+insertObs (i, j) = updateAt i (replaceAt j True)
+
+-- Must be total, as element type is finite
+checkRepeated : Colist (Pos h w, Direction) -> Bool
+checkRepeated = assert_total $ go []
+  where
+    covering
+    go : Eq a => List a -> Colist a -> Bool
+    go _ [] = False
+    go seen (x :: xs) =
+      (x `elem` seen) || go (x :: seen) xs
+
+covering
+loopPos : {h, w : _} -> (Pos h w, Direction) -> Map h w
+          -> List (Pos h w)
+loopPos g mp = do
+  i <- toList $ range {len=h}
+  j <- toList $ range {len=w}
+  let obs = (i,j)
+  guard (obs /= fst g && not (index obs mp)) -- must be empty space
+  let cols = getCollisions g $ insertObs obs mp
+  guard (collides obs cols) -- guard must collide with obstacle
+  guard (checkRepeated cols) -- must cause a loop
+  pure obs
+  where
+    -- Total in practice because routes that don't hit the new obstacle should
+    -- be finite, but we can't assume that from user input, so mark as covering
+    covering
+    collides : Pos h w -> Colist (Pos h w, Direction) -> Bool
+    collides _ [] = False
+    collides obs ((pos, _) :: cols) =
+      pos == obs || collides obs cols
+
+--- SOLUTION
+
+export covering
+solution : String -> Maybe Nat
+solution inp = do
+  (h ** w ** (mp, g)) <- parseInput inp
+  pure $ length $ loopPos g mp

src/Main.idr

@@ -13,7 +13,7 @@ import AllDays
 ||| The latest problem that has been solved.
 -- NOTE: UPDATE AFTER EACH SOLUTION
 latest : Problem
-latest = Pr 6 Part1
+latest = Pr 6 Part2
 
 
 solMap : SortedMap Problem (String -> String)