From 8dd697ee64f9314aaff83ce1a0a7e0a0ddf602da Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Thu, 5 Dec 2024 07:45:11 -0500
Subject: [PATCH] feat: part 5-1

---
 advent-of-code-2024.ipkg |  3 +-
 src/AllDays.idr          |  1 +
 src/Day5/Part1.idr       | 64 ++++++++++++++++++++++++++++++++++++++++
 src/Main.idr             |  2 +-
 4 files changed, 68 insertions(+), 2 deletions(-)
 create mode 100644 src/Day5/Part1.idr

diff --git a/advent-of-code-2024.ipkg b/advent-of-code-2024.ipkg
index 38ab29e..058ebfb 100644
--- a/advent-of-code-2024.ipkg
+++ b/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
diff --git a/src/AllDays.idr b/src/AllDays.idr
index 298e18d..00a8f58 100644
--- a/src/AllDays.idr
+++ b/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
diff --git a/src/Day5/Part1.idr b/src/Day5/Part1.idr
new file mode 100644
index 0000000..bbb46d0
--- /dev/null
+++ b/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
diff --git a/src/Main.idr b/src/Main.idr
index df92b07..f6d2785 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 4 Part2
+latest = Pr 5 Part1
 
 
 solMap : SortedMap Problem (String -> String)