From 09f8478c2f00cf24d529feaa77d75c8bdc97948c Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 4 Jan 2025 09:44:29 -0500
Subject: [PATCH] Year 2015 Day 1 Part 2

---
 src/Years/Y2015/Day1.idr | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

diff --git a/src/Years/Y2015/Day1.idr b/src/Years/Y2015/Day1.idr
index 09db409..405072d 100644
--- a/src/Years/Y2015/Day1.idr
+++ b/src/Years/Y2015/Day1.idr
@@ -12,12 +12,29 @@ trackFloor start ('(' :: xs) = trackFloor (start + 1) xs
 trackFloor start (')' :: xs) = trackFloor (start - 1) xs
 trackFloor start (x :: xs) = trackFloor start xs
 
+findBasement : (position : Nat) -> (currentFloor : Integer) -> (xs : List Char)
+  -> Nat
+findBasement position currentFloor [] = position
+findBasement position currentFloor ('(' :: xs) =
+  findBasement (position + 1) (currentFloor + 1) xs
+findBasement position currentFloor (')' :: xs) =
+  if currentFloor <= 0
+    then position
+    else findBasement (position + 1) (currentFloor - 1) xs
+findBasement position currentFloor (x :: xs) =
+  findBasement (position + 1) currentFloor xs
+
 part1 : Eff (PartEff String) (Integer, ())
 part1 = do
   input <- map unpack $ askAt "input"
   let output = trackFloor 0 input
   pure (output, ())
 
-export
+part2 : () -> Eff (PartEff String) Nat
+part2 x = do
+  input <- map unpack $ askAt "input"
+  pure $ findBasement 1 0 input
+
+public export
 day1 : Day
-day1 = First 1 part1
+day1 = Both 1 part1 part2