feat: part 4-2

advent-of-code-2024.ipkg

@@ -18,4 +18,4 @@ modules = Main, Utils, AllDays,
           Day1.Part1, Day1.Part2,
           Day2.Part1, Day2.Part2,
           Day3.Part1, Day3.Part2,
-          Day4.Part1
+          Day4.Part1, Day4.Part2

src/AllDays.idr

@@ -7,3 +7,4 @@ import public Day2.Part2
 import public Day3.Part1
 import public Day3.Part2
 import public Day4.Part1
+import public Day4.Part2

src/Day4/Part1.idr

@@ -7,20 +7,25 @@ import Data.Vect
 
 --- 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)
 
 
+public export
 data Direction = U | UR | R | DR | D | DL | L | UL
 
+export
 directions : List Direction
 directions = [U, UR, R, DR, D, DL, L, UL]
 
 --- PARSING
 
+export
 parseInput : String -> Maybe (h ** w ** Board h w)
 parseInput inp =
   let ls@(row :: _) = unpack <$> lines inp
@@ -31,6 +36,7 @@ parseInput inp =
 
 --- DATA
 
+export
 index : Pos h w -> Board h w -> Char
 index (i, j) = index j . index i
 
@@ -38,6 +44,7 @@ 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 UR (i, j) = (,) <$> predFin i <*> strengthen (FS j)
@@ -60,6 +67,7 @@ checkString board str = go (unpack str)
       in index next board == c && go cs next dir
 
 
+export
 findChar : {h, w : _} -> Board h w -> Char -> List (Pos h w)
 findChar board c = do
   i <- toList $ range {len=h}

src/Day4/Part2.idr

@@ -0,0 +1,31 @@
+module Day4.Part2
+
+import Data.String
+import Data.Vect
+
+import Day4.Part1
+
+%default total
+
+--- DATA
+
+checkMS : {h, w : _} -> Board h w -> Pos h w -> Bool
+checkMS board pos =
+  let Just [ul, ur, dl, dr] =
+        map (map (`index` board))
+          $ traverse {t=Vect _} (`moveDir` pos) [UL, UR, DL, DR]
+      | Nothing => False
+  in ((ul == 'M' && dr == 'S') || (ul == 'S' && dr == 'M')) &&
+     ((ur == 'M' && dl == 'S') || (ur == 'S' && dl == 'M'))
+
+countMAS : {h, w : _} -> Board h w -> Nat
+countMAS board = count (checkMS board) $ findChar board 'A'
+
+--- SOLUTION
+
+export
+solution : String -> Maybe Nat
+solution inp =
+  let Just (_ ** _ ** board) = parseInput inp
+      | Nothing => Nothing
+  in Just $ countMAS board

src/Main.idr

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