diff --git a/advent-of-code-2024.ipkg b/advent-of-code-2024.ipkg index 058ebfb..1c2bd0f 100644 --- a/advent-of-code-2024.ipkg +++ b/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 diff --git a/src/AllDays.idr b/src/AllDays.idr index 00a8f58..dfbce34 100644 --- a/src/AllDays.idr +++ b/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 diff --git a/src/Day5/Part1.idr b/src/Day5/Part1.idr index bbb46d0..951a406 100644 --- a/src/Day5/Part1.idr +++ b/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 diff --git a/src/Day5/Part2.idr b/src/Day5/Part2.idr new file mode 100644 index 0000000..b34fffb --- /dev/null +++ b/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 diff --git a/src/Main.idr b/src/Main.idr index f6d2785..b0be7e9 100644 --- a/src/Main.idr +++ b/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)