From d47a964c47eb76b0fe0ebfed758e2f8eca675661 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Sun, 8 Dec 2024 00:20:53 -0500
Subject: [PATCH 01/10] refactor: factor out grid code into `Utils`

---
 src/Day4/Part1.idr | 19 ++++---------------
 src/Day4/Part2.idr |  1 +
 src/Utils.idr      | 23 +++++++++++++++++++++++
 3 files changed, 28 insertions(+), 15 deletions(-)

diff --git a/src/Day4/Part1.idr b/src/Day4/Part1.idr
index 73a5b10..eb2a57f 100644
--- a/src/Day4/Part1.idr
+++ b/src/Day4/Part1.idr
@@ -3,17 +3,15 @@ module Day4.Part1
 import Data.String
 import Data.Vect
 
+import Utils
+
 %default total
 
 --- TYPES
 
 public export
 Board : Nat -> Nat -> Type
-Board h w = Vect h (Vect w Char)
-
-public export
-Pos : Nat -> Nat -> Type
-Pos h w = (Fin h, Fin w)
+Board h w = Grid h w Char
 
 
 public export
@@ -27,19 +25,10 @@ directions = [U, UR, R, DR, D, DL, L, UL]
 
 export
 parseInput : String -> Maybe (h ** w ** Board h w)
-parseInput inp =
-  let ls@(row :: _) = unpack <$> lines inp
-        | [] => Just (0 ** 0 ** [])
-      width = length row
-  in map (\l => (length l ** width ** fromList l))
-       (traverse (toVect width) ls)
+parseInput = parseGrid
 
 --- DATA
 
-export
-index : Pos h w -> Board h w -> Char
-index (i, j) = index j . index i
-
 predFin : Fin n -> Maybe (Fin n)
 predFin FZ = Nothing
 predFin (FS x) = Just $ weaken x
diff --git a/src/Day4/Part2.idr b/src/Day4/Part2.idr
index b8fd9a8..aa95510 100644
--- a/src/Day4/Part2.idr
+++ b/src/Day4/Part2.idr
@@ -4,6 +4,7 @@ import Data.String
 import Data.Vect
 
 import Day4.Part1
+import Utils
 
 %default total
 
diff --git a/src/Utils.idr b/src/Utils.idr
index 71811a4..d9b51e5 100644
--- a/src/Utils.idr
+++ b/src/Utils.idr
@@ -3,6 +3,7 @@ module Utils
 import Data.Maybe
 import Data.String
 import Data.String.Parser
+import Data.Vect
 
 %default total
 
@@ -28,3 +29,25 @@ scan p = until p *> p
 export covering
 scanWhile : Monad m => ParseT m a -> ParseT m b -> ParseT m b
 scanWhile w p = many (lookahead w *> requireFailure p *> skip (satisfy (const True))) *> p
+
+
+public export
+Grid : (h, w : Nat) -> Type -> Type
+Grid h w a = Vect h (Vect w a)
+
+public export
+Pos : (h, w : Nat) -> Type
+Pos h w = (Fin h, Fin w)
+
+export
+parseGrid : String -> Maybe (h ** w ** Grid h w Char)
+parseGrid str =
+  let ls@(row :: _) = unpack <$> lines str
+        | [] => Just (0 ** 0 ** [])
+      width = length row
+  in map (\l => (length l ** width ** fromList l))
+       (traverse (toVect width) ls)
+
+export
+index : Pos h w -> Grid h w a -> a
+index (i, j) = index j . index i

From dd51ad5d96d1c100be48cf724e0a4375a512e117 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Sun, 8 Dec 2024 00:21:18 -0500
Subject: [PATCH 02/10] feat: part 6-1

---
 advent-of-code-2024.ipkg |  3 +-
 src/AllDays.idr          |  1 +
 src/Day6/Part1.idr       | 80 ++++++++++++++++++++++++++++++++++++++++
 src/Main.idr             |  2 +-
 4 files changed, 84 insertions(+), 2 deletions(-)
 create mode 100644 src/Day6/Part1.idr

diff --git a/advent-of-code-2024.ipkg b/advent-of-code-2024.ipkg
index 1c2bd0f..4a81040 100644
--- a/advent-of-code-2024.ipkg
+++ b/advent-of-code-2024.ipkg
@@ -19,4 +19,5 @@ modules = Main, Utils, AllDays,
           Day2.Part1, Day2.Part2,
           Day3.Part1, Day3.Part2,
           Day4.Part1, Day4.Part2,
-          Day5.Part1, Day5.Part2
+          Day5.Part1, Day5.Part2,
+          Day6.Part1
diff --git a/src/AllDays.idr b/src/AllDays.idr
index dfbce34..0fd2978 100644
--- a/src/AllDays.idr
+++ b/src/AllDays.idr
@@ -10,3 +10,4 @@ import public Day4.Part1
 import public Day4.Part2
 import public Day5.Part1
 import public Day5.Part2
+import public Day6.Part1
diff --git a/src/Day6/Part1.idr b/src/Day6/Part1.idr
new file mode 100644
index 0000000..1710ef6
--- /dev/null
+++ b/src/Day6/Part1.idr
@@ -0,0 +1,80 @@
+module Day6.Part1
+
+import Data.List
+import Data.Maybe
+import Data.Vect
+import Data.Vect.Quantifiers
+
+import Utils
+
+%default total
+
+--- TYPES
+
+data Direction = U | R | D | L
+
+-- True if there is a wall
+Map : Nat -> Nat -> Type
+Map h w = Grid h w Bool
+
+--- PARSING
+
+parseDir : Char -> Maybe Direction
+parseDir '^' = Just U
+parseDir '>' = Just R
+parseDir 'v' = Just D
+parseDir '<' = Just L
+parseDir _ = Nothing
+
+parseInput : String -> Maybe (h ** w ** (Map h w, Pos h w, Direction))
+parseInput inp = do
+  (h ** w ** grid) <- parseGrid inp
+  g <- findGuard grid
+  pure (h ** w ** ((map . map) (=='#') grid, g))
+  where
+    findGuard : Vect h (Vect w Char) -> Maybe (Pos h w, Direction)
+    findGuard [] = Nothing
+    findGuard (row :: vs) =
+      case any (\c => isItJust (parseDir c)) row of
+        Yes p => Just ((FZ, cast $ anyToFin p), fromJust _ @{anyToFinCorrect p})
+        No _ => map (mapFst (mapFst FS)) $ findGuard vs
+
+--- DATA
+
+predFin : Fin n -> Maybe (Fin n)
+predFin FZ = Nothing
+predFin (FS x) = Just $ weaken x
+
+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
+
+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
+
+--- SOLUTION
+
+export covering
+solution : String -> Maybe Nat
+solution inp = do
+  (h ** w ** (mp, pos, dir)) <- parseInput inp
+  pure $ length $ nub $ getRoute dir pos mp
diff --git a/src/Main.idr b/src/Main.idr
index 1902a56..3f8d2d2 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 5 Part2
+latest = Pr 6 Part1
 
 
 solMap : SortedMap Problem (String -> String)

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 03/10] 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)

From d87cb7d7ee13d7cf4c116671fdd1316347ed756f Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 9 Dec 2024 00:33:28 -0500
Subject: [PATCH 04/10] fix: remove unnecessary module list from ipkg

This is apparently only necessary for libraries, not for executables.
Good to know!
---
 advent-of-code-2024.ipkg | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/advent-of-code-2024.ipkg b/advent-of-code-2024.ipkg
index 4d422b0..36c2a5b 100644
--- a/advent-of-code-2024.ipkg
+++ b/advent-of-code-2024.ipkg
@@ -13,11 +13,3 @@ depends = contrib
 
 executable = advent-of-code-2024
 main = Main
-modules = Main, Utils, AllDays,
-          Data.Problem,
-          Day1.Part1, Day1.Part2,
-          Day2.Part1, Day2.Part2,
-          Day3.Part1, Day3.Part2,
-          Day4.Part1, Day4.Part2,
-          Day5.Part1, Day5.Part2,
-          Day6.Part1, Day6.Part2

From 2196df1811ea7d3a3a953c41555416fe0026ebe3 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 9 Dec 2024 00:34:47 -0500
Subject: [PATCH 05/10] feat: part 7-1

---
 src/AllDays.idr    |  1 +
 src/Day7/Part1.idr | 41 +++++++++++++++++++++++++++++++++++++++++
 src/Main.idr       |  2 +-
 3 files changed, 43 insertions(+), 1 deletion(-)
 create mode 100644 src/Day7/Part1.idr

diff --git a/src/AllDays.idr b/src/AllDays.idr
index 8d9e3f0..fcb187f 100644
--- a/src/AllDays.idr
+++ b/src/AllDays.idr
@@ -12,3 +12,4 @@ import public Day5.Part1
 import public Day5.Part2
 import public Day6.Part1
 import public Day6.Part2
+import public Day7.Part1
diff --git a/src/Day7/Part1.idr b/src/Day7/Part1.idr
new file mode 100644
index 0000000..211a540
--- /dev/null
+++ b/src/Day7/Part1.idr
@@ -0,0 +1,41 @@
+module Day7.Part1
+
+import Data.List
+import Data.List1
+import Data.String
+import Data.Vect
+
+import Utils
+
+%default total
+
+--- TYPES
+
+Op : Type
+Op = Nat -> Nat -> Nat
+
+--- PARSING
+
+parseLine : String -> Maybe (Nat, List1 Nat)
+parseLine inp =
+  let (part1 ::: [part2]) = split (==':') inp
+        | _ => Nothing
+  in (,) <$> parseNat part1
+         <*> (traverse parseNat =<< fromList (words part2))
+
+parseInput : String -> Maybe (List (Nat, List1 Nat))
+parseInput = traverse parseLine . lines
+
+--- DATA
+
+search : List Op -> Nat -> List1 Nat -> Bool
+search _ n (x ::: []) = x == n
+search ops n (x ::: y :: xs) =
+  -- heuristic: abandon if running total is larger than target
+  x <= n && any (\op => assert_total $ search ops n (op x y ::: xs)) ops
+
+--- SOLUTION
+
+export
+solution : String -> Maybe Nat
+solution = map (sum . map fst . filter (uncurry $ search [(+),(*)])) . parseInput
diff --git a/src/Main.idr b/src/Main.idr
index ce6eeb1..8b60986 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 Part2
+latest = Pr 7 Part1
 
 
 solMap : SortedMap Problem (String -> String)

From b4391bec8697b29a65271145483b5ed9eef35c1c Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 9 Dec 2024 00:44:40 -0500
Subject: [PATCH 06/10] refactor: remove totality assertion

---
 src/Day7/Part1.idr | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/Day7/Part1.idr b/src/Day7/Part1.idr
index 211a540..ad9a0c1 100644
--- a/src/Day7/Part1.idr
+++ b/src/Day7/Part1.idr
@@ -1,9 +1,7 @@
 module Day7.Part1
 
-import Data.List
 import Data.List1
 import Data.String
-import Data.Vect
 
 import Utils
 
@@ -28,14 +26,15 @@ parseInput = traverse parseLine . lines
 
 --- DATA
 
-search : List Op -> Nat -> List1 Nat -> Bool
-search _ n (x ::: []) = x == n
-search ops n (x ::: y :: xs) =
+search : List Op -> (tg, tot : Nat) -> List Nat -> Bool
+search _ tg tot [] = tg == tot
+search ops tg tot (x :: xs) =
   -- heuristic: abandon if running total is larger than target
-  x <= n && any (\op => assert_total $ search ops n (op x y ::: xs)) ops
+  tot <= tg && any (\op => search ops tg (op tot x) xs) ops
 
 --- SOLUTION
 
 export
 solution : String -> Maybe Nat
-solution = map (sum . map fst . filter (uncurry $ search [(+),(*)])) . parseInput
+solution = map (sum . map fst . filter (\(tg,x:::xs) => search [(+),(*)] tg x xs))
+           . parseInput

From 3826a1324466ce7f8fc4858173b453652695d5a7 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 9 Dec 2024 00:46:19 -0500
Subject: [PATCH 07/10] feat: part 7-2

---
 src/AllDays.idr    |  1 +
 src/Day7/Part1.idr |  3 +++
 src/Day7/Part2.idr | 21 +++++++++++++++++++++
 src/Main.idr       |  2 +-
 4 files changed, 26 insertions(+), 1 deletion(-)
 create mode 100644 src/Day7/Part2.idr

diff --git a/src/AllDays.idr b/src/AllDays.idr
index fcb187f..e441f4c 100644
--- a/src/AllDays.idr
+++ b/src/AllDays.idr
@@ -13,3 +13,4 @@ import public Day5.Part2
 import public Day6.Part1
 import public Day6.Part2
 import public Day7.Part1
+import public Day7.Part2
diff --git a/src/Day7/Part1.idr b/src/Day7/Part1.idr
index ad9a0c1..b644d92 100644
--- a/src/Day7/Part1.idr
+++ b/src/Day7/Part1.idr
@@ -9,6 +9,7 @@ import Utils
 
 --- TYPES
 
+public export
 Op : Type
 Op = Nat -> Nat -> Nat
 
@@ -21,11 +22,13 @@ parseLine inp =
   in (,) <$> parseNat part1
          <*> (traverse parseNat =<< fromList (words part2))
 
+export
 parseInput : String -> Maybe (List (Nat, List1 Nat))
 parseInput = traverse parseLine . lines
 
 --- DATA
 
+export
 search : List Op -> (tg, tot : Nat) -> List Nat -> Bool
 search _ tg tot [] = tg == tot
 search ops tg tot (x :: xs) =
diff --git a/src/Day7/Part2.idr b/src/Day7/Part2.idr
new file mode 100644
index 0000000..9cbe7fe
--- /dev/null
+++ b/src/Day7/Part2.idr
@@ -0,0 +1,21 @@
+module Day7.Part2
+
+import Data.List1
+
+import Day7.Part1
+import Utils
+
+%default total
+
+--- DATA
+
+concat : Nat -> Nat -> Nat
+concat x y = cast $ show x ++ show y
+
+--- SOLUTION
+
+export
+solution : String -> Maybe Nat
+solution = map (sum . map fst
+                    . filter (\(tg,x:::xs) => search [(+),(*),concat] tg x xs))
+           . parseInput
diff --git a/src/Main.idr b/src/Main.idr
index 8b60986..65448ab 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 7 Part1
+latest = Pr 7 Part2
 
 
 solMap : SortedMap Problem (String -> String)

From 22423f6cf6d79ad839b8ed081d160486094891e4 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 9 Dec 2024 02:27:33 -0500
Subject: [PATCH 08/10] refactor: `Data.Vect.range` -> `Data.List.allFins`

---
 src/Day4/Part1.idr | 5 +++--
 src/Day6/Part2.idr | 4 ++--
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/Day4/Part1.idr b/src/Day4/Part1.idr
index eb2a57f..19066b2 100644
--- a/src/Day4/Part1.idr
+++ b/src/Day4/Part1.idr
@@ -1,5 +1,6 @@
 module Day4.Part1
 
+import Data.List
 import Data.String
 import Data.Vect
 
@@ -59,8 +60,8 @@ checkString board str = go (unpack str)
 export
 findChar : {h, w : _} -> Board h w -> Char -> List (Pos h w)
 findChar board c = do
-  i <- toList $ range {len=h}
-  j <- toList $ range {len=w}
+  i <- allFins h
+  j <- allFins w
   guard (index (i, j) board == c)
   pure (i, j)
 
diff --git a/src/Day6/Part2.idr b/src/Day6/Part2.idr
index 58f09d9..6f25782 100644
--- a/src/Day6/Part2.idr
+++ b/src/Day6/Part2.idr
@@ -38,8 +38,8 @@ 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}
+  i <- allFins h
+  j <- allFins w
   let obs = (i,j)
   guard (obs /= fst g && not (index obs mp)) -- must be empty space
   let cols = getCollisions g $ insertObs obs mp

From b10afe5239a3ebbe7c54273ce5036cc4de0f5208 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 9 Dec 2024 02:29:40 -0500
Subject: [PATCH 09/10] feat: part 8-1

---
 src/AllDays.idr    |  1 +
 src/Day8/Part1.idr | 54 ++++++++++++++++++++++++++++++++++++++++++++++
 src/Main.idr       |  2 +-
 3 files changed, 56 insertions(+), 1 deletion(-)
 create mode 100644 src/Day8/Part1.idr

diff --git a/src/AllDays.idr b/src/AllDays.idr
index e441f4c..884de46 100644
--- a/src/AllDays.idr
+++ b/src/AllDays.idr
@@ -14,3 +14,4 @@ import public Day6.Part1
 import public Day6.Part2
 import public Day7.Part1
 import public Day7.Part2
+import public Day8.Part1
diff --git a/src/Day8/Part1.idr b/src/Day8/Part1.idr
new file mode 100644
index 0000000..864e239
--- /dev/null
+++ b/src/Day8/Part1.idr
@@ -0,0 +1,54 @@
+module Day8.Part1
+
+import Data.List
+import Data.Vect
+
+import Utils
+
+%default total
+
+--- TYPES
+
+Map : (h, w : Nat) -> Type
+Map h w = Grid h w (Maybe Char)
+
+--- PARSING
+
+parseInput : String -> Maybe (h ** w ** Map h w)
+parseInput inp = do
+  (h ** w ** grid) <- parseGrid inp
+  pure (h ** w ** map (map (filter (/='.') . Just)) grid)
+
+--- DATA
+
+frequencies : Map h w -> List Char
+frequencies mp = nub $ do
+  row <- toList mp
+  Just c <- toList row
+    | Nothing => empty
+  pure c
+
+antinodePos : {h, w : _} -> (a, b : Pos h w) -> Maybe (Pos h w)
+antinodePos (x, y) (x', y') =
+  (,) <$> integerToFin (cast x * 2 - cast x') h
+      <*> integerToFin (cast y * 2 - cast y') w
+
+antinodes : {h, w : _} -> Map h w -> Char -> List (Pos h w)
+antinodes mp c = do
+  let poss = do
+        i <- allFins h
+        j <- allFins w
+        guard (index (i, j) mp == Just c)
+        pure (i, j)
+  p1 <- poss
+  p2 <- poss
+  guard (p1 /= p2)
+  toList (antinodePos p1 p2) <|> toList (antinodePos p2 p1)
+
+--- SOLUTION
+
+export
+solution : String -> Maybe Nat
+solution inp = do
+  (h ** w ** mp) <- parseInput inp
+  pure $ length $ nub $ frequencies mp >>= antinodes mp
diff --git a/src/Main.idr b/src/Main.idr
index 65448ab..3f1f3e8 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 7 Part2
+latest = Pr 8 Part1
 
 
 solMap : SortedMap Problem (String -> String)

From 68a806b2918acb62bc9e7882a61a8770722fb2fb Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 9 Dec 2024 02:30:01 -0500
Subject: [PATCH 10/10] feat: part 8-2

---
 src/AllDays.idr    |  1 +
 src/Day8/Part1.idr |  3 +++
 src/Day8/Part2.idr | 49 ++++++++++++++++++++++++++++++++++++++++++++++
 src/Main.idr       |  2 +-
 4 files changed, 54 insertions(+), 1 deletion(-)
 create mode 100644 src/Day8/Part2.idr

diff --git a/src/AllDays.idr b/src/AllDays.idr
index 884de46..898b247 100644
--- a/src/AllDays.idr
+++ b/src/AllDays.idr
@@ -15,3 +15,4 @@ import public Day6.Part2
 import public Day7.Part1
 import public Day7.Part2
 import public Day8.Part1
+import public Day8.Part2
diff --git a/src/Day8/Part1.idr b/src/Day8/Part1.idr
index 864e239..501566f 100644
--- a/src/Day8/Part1.idr
+++ b/src/Day8/Part1.idr
@@ -9,11 +9,13 @@ import Utils
 
 --- TYPES
 
+public export
 Map : (h, w : Nat) -> Type
 Map h w = Grid h w (Maybe Char)
 
 --- PARSING
 
+export
 parseInput : String -> Maybe (h ** w ** Map h w)
 parseInput inp = do
   (h ** w ** grid) <- parseGrid inp
@@ -21,6 +23,7 @@ parseInput inp = do
 
 --- DATA
 
+export
 frequencies : Map h w -> List Char
 frequencies mp = nub $ do
   row <- toList mp
diff --git a/src/Day8/Part2.idr b/src/Day8/Part2.idr
new file mode 100644
index 0000000..4ca6f60
--- /dev/null
+++ b/src/Day8/Part2.idr
@@ -0,0 +1,49 @@
+module Day8.Part2
+
+import Data.List
+import Data.Vect
+
+import Day8.Part1
+import Utils
+
+%default total
+
+--- DATA
+
+antinodePos : {h, w : _} -> (a, b : Pos h w) -> List (Pos h w)
+antinodePos (x, y) (x', y') = do
+  let dx = cast x' - cast x
+      dy = cast y' - cast y
+      (dx', dy') = reduce (dx, dy)
+  n <- [-(cast $ max h w)..(cast $ max h w)]
+  toList $
+    (,) <$> integerToFin (cast x + dx' * n) h
+        <*> integerToFin (cast y + dy' * n) w
+  where
+    reduce : (Integer, Integer) -> (Integer, Integer)
+    reduce (a, b) with (cast {to=Nat} $ abs a) | (cast {to=Nat} $ abs b)
+      _ | Z | _ = (a, b)
+      _ | _ | Z = (a, b)
+      _ | a'@(S _) | b'@(S _) =
+        let g = assert_total $ gcd a' b'
+        in (a `div` cast g, b `div` cast g)
+
+antinodes : {h, w : _} -> Map h w -> Char -> List (Pos h w)
+antinodes mp c = do
+  let poss = do
+        i <- allFins h
+        j <- allFins w
+        guard (index (i, j) mp == Just c)
+        pure (i, j)
+  p1 <- poss
+  p2 <- poss
+  guard (p1 /= p2)
+  antinodePos p1 p2
+
+--- SOLUTION
+
+export
+solution : String -> Maybe Nat
+solution inp = do
+  (h ** w ** mp) <- parseInput inp
+  pure $ length $ nub $ frequencies mp >>= antinodes mp
diff --git a/src/Main.idr b/src/Main.idr
index 3f1f3e8..17b048c 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 8 Part1
+latest = Pr 8 Part2
 
 
 solMap : SortedMap Problem (String -> String)