feat: part 4-2

advent-of-code-2024.ipkg

@@ -17,4 +17,5 @@ modules = Main, Utils, AllDays,
           Data.Problem,
           Day1.Part1, Day1.Part2,
           Day2.Part1, Day2.Part2,
-          Day3.Part1, Day3.Part2
+          Day3.Part1, Day3.Part2,
+          Day4.Part1, Day4.Part2

src/AllDays.idr

@@ -6,3 +6,5 @@ import public Day2.Part1
 import public Day2.Part2
 import public Day3.Part1
 import public Day3.Part2
+import public Day4.Part1
+import public Day4.Part2

src/Data/Problem.idr

@@ -80,24 +80,26 @@ solutionName (Pr day part) =
 
 public export
 fetchSolution : Problem -> Elab (String -> String)
-fetchSolution pr = do
+fetchSolution pr =
   let name = solutionName pr
-  check `(\s => show (~(IVar EmptyFC name) s))
+  in check `(\s => Prelude.show (~(IVar EmptyFC name) s))
-    <|> fail "\{show name} does not exist as a valid solution"
+      <|> fail "\{show name} does not exist as a valid solution"
 
 public export
 fetchAllSols : (latest : Problem) -> Elab (SortedMap Problem (String -> String))
 fetchAllSols pr =
   let prs = allProblems pr
-      list = foldr (\pr,tt => `(Prelude.(::)
+      list = foldr
-                                (Builtin.MkPair
+              (\pr,tt =>
-                                 (Data.Problem.Pr
+                `(Prelude.(::)
-                                  (Prelude.fromInteger
+                  (Builtin.MkPair
-                                   ~(IPrimVal EmptyFC $ BI $ natToInteger pr.day))
+                    (Data.Problem.Pr
-                                  ~(case pr.part of
+                    (Prelude.fromInteger
-                                      Part1 => `(Data.Problem.Part1)
+                      ~(IPrimVal EmptyFC $ BI $ natToInteger pr.day))
-                                      Part2 => `(Data.Problem.Part2)))
+                    ~(case pr.part of
-                                 (\s => show (~(IVar EmptyFC $ solutionName pr) s)))
+                        Part1 => `(Data.Problem.Part1)
-                                ~(tt))) `(Prelude.Nil) prs
+                        Part2 => `(Data.Problem.Part2)))
+                    (\s => Prelude.show (~(IVar EmptyFC $ solutionName pr) s)))
+                  ~(tt))) `(Prelude.Nil) prs
       ttimp = `(Data.SortedMap.fromList ~(list))
   in check ttimp

src/Day4/Part1.idr

@@ -0,0 +1,92 @@
+module Day4.Part1
+
+import Data.String
+import Data.Vect
+
+%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)
+
+
+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
+        | [] => Just (0 ** 0 ** [])
+      width = length row
+  in map (\l => (length l ** width ** fromList l))
+       (traverse (toVect width) ls)
+
+--- 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
+
+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)
+moveDir R (i, j) = (i,) <$> strengthen (FS j)
+moveDir DR (i, j) = (,) <$> strengthen (FS i) <*> strengthen (FS j)
+moveDir D (i, j) = (,j) <$> strengthen (FS i)
+moveDir DL (i, j) = (,) <$> strengthen (FS i) <*> predFin j
+moveDir L (i, j) = (i,) <$> predFin j
+moveDir UL (i, j) = (,) <$> predFin i <*> predFin j
+
+checkString : {h, w : _}
+              -> Board h w -> String -> Pos h w -> Direction -> Bool
+checkString board str = go (unpack str)
+  where
+    go : List Char -> Pos h w -> Direction -> Bool
+    go [] _ _ = True
+    go (c :: cs) pos dir =
+      let Just next = moveDir dir pos
+          | Nothing => False
+      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}
+  j <- toList $ range {len=w}
+  guard (index (i, j) board == c)
+  pure (i, j)
+
+countString : {h, w : _} -> Board h w -> String -> Nat
+countString board str with (strUncons str)
+  _ | Nothing = 0
+  _ | Just (c, str') =
+    count (uncurry $ checkString board str')
+      $ (,) <$> findChar board c <*> directions
+
+--- SOLUTION
+
+export
+solution : String -> Maybe Nat
+solution inp =
+  let Just (_ ** _ ** board) = parseInput inp
+      | Nothing => Nothing
+  in Just $ countString board "XMAS"

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 3 Part2
+latest = Pr 4 Part2
 
 
 solMap : SortedMap Problem (String -> String)