feat: part 5-2

advent-of-code-2024.ipkg

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

src/AllDays.idr

@@ -8,3 +8,5 @@ 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

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

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