diff --git a/src/Years/Y2015.idr b/src/Years/Y2015.idr index 290f4d3..d534291 100644 --- a/src/Years/Y2015.idr +++ b/src/Years/Y2015.idr @@ -5,9 +5,11 @@ import Structures.Dependent.FreshList import Runner import Years.Y2015.Day1 +import Years.Y2015.Day2 export y2015 : Year y2015 = MkYear 2015 [ day1 + , day2 ] diff --git a/src/Years/Y2015/Day2.idr b/src/Years/Y2015/Day2.idr new file mode 100644 index 0000000..fec965d --- /dev/null +++ b/src/Years/Y2015/Day2.idr @@ -0,0 +1,47 @@ +module Years.Y2015.Day2 + +import Data.List +import Data.List1 +import Data.String + +import Control.Eff + +import Runner + +%default total + +record Box where + constructor MkBox + length, width, height : Integer + +(.area) : Box -> Integer +(.area) (MkBox length width height) = + 2 * length * width + 2 * width * height + 2 * length * height + +(.slack) : Box -> Integer +(.slack) (MkBox length width height) = + foldl1 min [length * width, width * height, length * height] + +paperNeeded : Box -> Integer +paperNeeded x = x.area + x.slack + +parseBox : Has (Except String) fs => + String -> Eff fs Box +parseBox str = do + l ::: [w, h] <- pure $ split (== 'x') str + | xs => throw "Box did not have exactly 3 components: \{show xs}" + length <- note "Failed parsing length: \{show l}" $ parsePositive l + width <- note "Failed parsing width: \{show w}" $ parsePositive w + height <- note "Failed parsing height: \{show h}" $ parsePositive h + pure $ MkBox length width height + +part1 : Eff (PartEff String) (Integer, ()) +part1 = do + input <- map lines $ askAt "input" + boxes <- traverse parseBox input + let output = sum . map paperNeeded $ boxes + pure (output, ()) + +public export +day2 : Day +day2 = First 2 part1