feat: part 5-1

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

src/AllDays.idr

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

src/Day5/Part1.idr

@@ -0,0 +1,64 @@
+module Day5.Part1
+
+import Data.Fin
+import Data.List
+import Data.List1
+import Data.String
+
+import Utils
+
+%default total
+
+--- PARSING
+
+Rule : Type
+Rule = (Nat, Nat)
+
+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 (==',')
+
+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
+
+validateRule : Rule -> Update -> Bool
+validateRule (before, after) pages =
+  fromMaybe True $
+    (<) <$> findIndex (==before) pages <*> findIndex (==after) pages
+
+-- defined recursively for totality reasons
+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/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 Part1
 
 
 solMap : SortedMap Problem (String -> String)