From cda9060ab3a6807e2e6be35d8ff6a55de8d7524f Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Sun, 8 Dec 2024 18:01:22 -0500
Subject: [PATCH] feat: part 6-2

---
 advent-of-code-2024.ipkg |  2 +-
 src/AllDays.idr          |  1 +
 src/Day6/Part1.idr       | 47 +++++++++++++++++++----------
 src/Day6/Part2.idr       | 64 ++++++++++++++++++++++++++++++++++++++++
 src/Main.idr             |  2 +-
 5 files changed, 98 insertions(+), 18 deletions(-)
 create mode 100644 src/Day6/Part2.idr

diff --git a/advent-of-code-2024.ipkg b/advent-of-code-2024.ipkg
index 4a81040..4d422b0 100644
--- a/advent-of-code-2024.ipkg
+++ b/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
diff --git a/src/AllDays.idr b/src/AllDays.idr
index 0fd2978..8d9e3f0 100644
--- a/src/AllDays.idr
+++ b/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
diff --git a/src/Day6/Part1.idr b/src/Day6/Part1.idr
index 1710ef6..66ccf64 100644
--- a/src/Day6/Part1.idr
+++ b/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
 
-
-covering
-getRoute : {h, w : _} -> Direction -> Pos h w -> Map h w -> List (Pos h w)
-getRoute = go []
-  where
-    covering
-    go : List (Pos h w) -> Direction -> Pos h w -> Map h w -> List (Pos h w)
-    go route dir pos map =
-      let Just next = moveDir dir pos
-            | Nothing => pos :: route
-      in if index next map
-         then go (pos :: route) (rotate dir) pos map
-         else go (pos :: route) dir next map
+getRoute : {h, w : _} -> (Pos h w, Direction) -> Map h w
+            -> Colist (Pos h w, Direction)
+getRoute (pos, dir) mp =
+  let Just next = moveDir dir pos
+        | Nothing => [(pos, dir)]
+  in (pos, dir) ::
+      if index next mp
+      then getRoute (pos, rotate dir) mp
+      else getRoute (next, dir) mp
 
 --- 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
-  pure $ length $ nub $ getRoute dir pos mp
+  (h ** w ** (mp, g)) <- parseInput inp
+  pure $ length $ nub $ map fst $ forceList $ getRoute g mp
diff --git a/src/Day6/Part2.idr b/src/Day6/Part2.idr
new file mode 100644
index 0000000..58f09d9
--- /dev/null
+++ b/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
diff --git a/src/Main.idr b/src/Main.idr
index 3f8d2d2..ce6eeb1 100644
--- a/src/Main.idr
+++ b/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)