advent-of-code-2024.ipkg

@@ -17,5 +17,4 @@ 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,5 +6,3 @@ 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,18 +80,16 @@ solutionName (Pr day part) =
 
 public export
 fetchSolution : Problem -> Elab (String -> String)
-fetchSolution pr =
+fetchSolution pr = do
   let name = solutionName pr
-  in check `(\s => Prelude.show (~(IVar EmptyFC name) s))
+  check `(\s => show (~(IVar EmptyFC name) s))
     <|> 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
+      list = foldr (\pr,tt => `(Prelude.(::)
-              (\pr,tt =>
-                `(Prelude.(::)
                                 (Builtin.MkPair
                                  (Data.Problem.Pr
                                   (Prelude.fromInteger
@@ -99,7 +97,7 @@ fetchAllSols pr =
                                   ~(case pr.part of
                                       Part1 => `(Data.Problem.Part1)
                                       Part2 => `(Data.Problem.Part2)))
-                    (\s => Prelude.show (~(IVar EmptyFC $ solutionName pr) s)))
+                                 (\s => show (~(IVar EmptyFC $ solutionName pr) s)))
                                 ~(tt))) `(Prelude.Nil) prs
       ttimp = `(Data.SortedMap.fromList ~(list))
   in check ttimp

src/Day4/Part1.idr

@@ -1,92 +0,0 @@
-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

@@ -1,31 +0,0 @@
-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 Part2
+latest = Pr 3 Part2
 
 
 solMap : SortedMap Problem (String -> String)