feat: part 5-2

advent-of-code-2024.ipkg

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

src/AllDays.idr

@@ -9,3 +9,4 @@ import public Day3.Part2
 import public Day4.Part1
 import public Day4.Part2
 import public Day5.Part1
+import public Day5.Part2

src/Day5/Part1.idr

@@ -11,9 +11,11 @@ import Utils
 
 --- PARSING
 
+public export
 Rule : Type
 Rule = (Nat, Nat)
 
+public export
 Update : Type
 Update = List Nat
 
@@ -28,6 +30,7 @@ parseRule str =
 parseUpdate : String -> Maybe Update
 parseUpdate = traverse parseNat . forget . split (==',')
 
+export
 parseInput : String -> Maybe (List Rule, List Update)
 parseInput str =
   let ls = lines str
@@ -39,12 +42,14 @@ parseInput str =
 
 --- 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

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