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] 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)