src/Runner.idr

@@ -13,7 +13,7 @@ PartEff err =
 ||| Model solving a single day
 public export
 record Day where
-  constructor Both
+  constructor MkDay
   day : Nat
   {0 out1, out2, err1, err2 : Type}
   {auto showOut1 : Show out1}
@@ -31,7 +31,16 @@ namespace Day
     (day : Nat) -> (part1 : Eff (PartEff err) (out, ctx'))
     -> Day
   First day part1 =
-    Both day part1 Nothing {out2 = ()} {err2 = ()}
+    MkDay day part1 Nothing {out2 = ()} {err2 = ()}
+
+  ||| Constructor for a day with both parts ready to run
+  public export
+  Both : Show o1 => Show o2 => Show e1 => Show e2 =>
+    (day : Nat) -> (part1 : Eff (PartEff e1) (o1, ctx')) ->
+    (part2 :ctx' -> Eff (PartEff e2) o2)
+    -> Day
+  Both day part1 part2 =
+    MkDay day part1 (Just part2)
 
 ||| Freshness criteria for days
 |||

src/Years/Y2015/Day1.idr

@@ -4,8 +4,37 @@ import Control.Eff
 
 import Runner
 
-part1 : Eff (PartEff String) ((), ())
+%default total
+
+trackFloor : (start : Integer) -> (xs : List Char) -> Integer
+trackFloor start [] = start
+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, ())
+
+part2 : () -> Eff (PartEff String) Nat
+part2 x = do
+  input <- map unpack $ askAt "input"
+  pure $ findBasement 1 0 input
 
 export
 day1 : Day
-day1 = First 1 part1
+day1 = Both 1 part1 part2