Year 2015 Day 1 Part 2

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