src/Runner.idr

@@ -13,7 +13,7 @@ PartEff err =
 ||| Model solving a single day
 public export
 record Day where
-  constructor MkDay
+  constructor Both
   day : Nat
   {0 out1, out2, err1, err2 : Type}
   {auto showOut1 : Show out1}
@@ -31,16 +31,7 @@ namespace Day
     (day : Nat) -> (part1 : Eff (PartEff err) (out, ctx'))
     -> Day
   First day part1 =
-    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)
+    Both day part1 Nothing {out2 = ()} {err2 = ()}
 
 ||| Freshness criteria for days
 |||

src/Years/Y2015/Day1.idr

@@ -4,37 +4,8 @@ import Control.Eff
 
 import Runner
 
-%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
+part1 : Eff (PartEff String) ((), ())
 
 export
 day1 : Day
-day1 = Both 1 part1 part2
+day1 = First 1 part1