diff --git a/src/Runner.idr b/src/Runner.idr index c6a2712..7347fee 100644 --- a/src/Runner.idr +++ b/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 ||| diff --git a/src/Years/Y2015/Day1.idr b/src/Years/Y2015/Day1.idr index 9b01045..cbe81d0 100644 --- a/src/Years/Y2015/Day1.idr +++ b/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