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