advent-of-code-2024.ipkg

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

src/AllDays.idr

@@ -8,5 +8,3 @@ import public Day3.Part1
 import public Day3.Part2
 import public Day4.Part1
 import public Day4.Part2
-import public Day5.Part1
-import public Day5.Part2

src/Day4/Part1.idr

@@ -63,7 +63,7 @@ checkString board str = go (unpack str)
     go [] _ _ = True
     go (c :: cs) pos dir =
       let Just next = moveDir dir pos
-            | Nothing => False
+          | Nothing => False
       in index next board == c && go cs next dir
 
 
@@ -88,5 +88,5 @@ export
 solution : String -> Maybe Nat
 solution inp =
   let Just (_ ** _ ** board) = parseInput inp
-        | Nothing => Nothing
+      | Nothing => Nothing
   in Just $ countString board "XMAS"

src/Day4/Part2.idr

@@ -14,7 +14,7 @@ checkMS board pos =
   let Just [ul, ur, dl, dr] =
         map (map (`index` board))
           $ traverse {t=Vect _} (`moveDir` pos) [UL, UR, DL, DR]
-        | Nothing => False
+      | Nothing => False
   in ((ul == 'M' && dr == 'S') || (ul == 'S' && dr == 'M')) &&
      ((ur == 'M' && dl == 'S') || (ur == 'S' && dl == 'M'))
 
@@ -27,5 +27,5 @@ export
 solution : String -> Maybe Nat
 solution inp =
   let Just (_ ** _ ** board) = parseInput inp
-        | Nothing => Nothing
+      | Nothing => Nothing
   in Just $ countMAS board

src/Day5/Part1.idr

@@ -1,69 +0,0 @@
-module Day5.Part1
-
-import Data.Fin
-import Data.List
-import Data.List1
-import Data.String
-
-import Utils
-
-%default total
-
---- PARSING
-
-public export
-Rule : Type
-Rule = (Nat, Nat)
-
-public export
-Update : Type
-Update = List Nat
-
---- PARSING
-
-parseRule : String -> Maybe Rule
-parseRule str =
-  case split (=='|') str of
-    s ::: [s'] => (,) <$> parseNat s <*> parseNat s'
-    _ => Nothing
-
-parseUpdate : String -> Maybe Update
-parseUpdate = traverse parseNat . forget . split (==',')
-
-export
-parseInput : String -> Maybe (List Rule, List Update)
-parseInput str =
-  let ls = lines str
-      Just div = map finToNat $ findIndex null ls
-        | Nothing => Nothing
-      (rs, _ :: us) = splitAt div ls
-        | (_, []) => Nothing
-  in (,) <$> traverse parseRule rs <*> traverse parseUpdate us
-
---- DATA
-
-export
-validateRule : Rule -> Update -> Bool
-validateRule (before, after) pages =
-  fromMaybe True $
-    (<) <$> findIndex (==before) pages <*> findIndex (==after) pages
-
--- defined recursively for totality reasons
-export
-middle : Update -> Nat
-middle xs = go xs (length xs)
-  where
-    go : List Nat -> Nat -> Nat
-    go [] _ = 0
-    go (x :: _) 2 = x
-    go (_ :: xs) (S (S l)) = go xs l
-    go (x :: _) _ = x
-
-sumValidRules : List Rule -> List Update -> Nat
-sumValidRules rs us = sum $ map middle $ filter (\u => all (`validateRule` u) rs) us
-
---- SOLUTION
-
-export
-solution : String -> Maybe Nat
-solution inp = uncurry sumValidRules <$> parseInput inp

src/Day5/Part2.idr

@@ -1,46 +0,0 @@
-module Day5.Part2
-
-import Data.Fin
-import Data.List
-import Data.List1
-import Data.Maybe
-import Data.String
-
-import Day5.Part1
-import Utils
-
-%default total
-
---- DATA
-
--- This solution uses Kahn's algorithm!
--- https://en.wikipedia.org/wiki/Topological_sorting#Kahn's_algorithm
-
-orderPages : List Rule -> List Nat
-orderPages rs = go [] startVs rs
-  where
-    startVs : List Nat
-    startVs = nub $ filter (not . (`elem` map snd rs)) $ map fst rs
-
-    go : (l, s : List Nat) -> List Rule -> List Nat
-    go l [] _ = reverse l
-    go l (v :: s) rs =
-      let (vs, rs') = mapFst (map snd) $ partition ((==v) . fst) rs
-          s' = filter (not . (`elem` map snd rs')) vs ++ s
-      in assert_total $ go (v :: l) s' rs'
-
-correctUpdate : List Rule -> Update -> Update
-correctUpdate rs u =
-  let rs' = filter (\(a,b) => elem a u && elem b u) rs
-  in  orderPages rs'
-
-sumCorrectedRules : List Rule -> List Update -> Nat
-sumCorrectedRules rs us =
-  let inv = filter (\u => not $ all (`validateRule` u) rs) us
-  in sum $ map (middle . correctUpdate rs) inv
-
---- SOLUTION
-
-export
-solution : String -> Maybe Nat
-solution inp = uncurry sumCorrectedRules <$> parseInput inp

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