
  0 | module Years.Y2015.Day2
  1 | 
  2 | import Data.List
  3 | import Data.List1
  4 | import Data.String
  5 | 
  6 | import Control.Eff
  7 | 
  8 | import Runner
  9 | 
 10 | %default total
 11 | 
 12 | record Box where
 13 |   constructor MkBox
 14 |   length, width, height : Integer
 15 | 
 16 | (.area) : Box -> Integer
 17 | (.area) (MkBox length width height) =
 18 |   2 * length * width + 2 * width * height + 2 * length * height
 19 | 
 20 | (.slack) : Box -> Integer
 21 | (.slack) (MkBox length width height) =
 22 |   foldl1 min [length * width, width * height, length * height]
 23 | 
 24 | (.ribbon) : Box -> Integer
 25 | (.ribbon) (MkBox length width height) =
 26 |   foldl1 min [2 * (length + width), 2 * (length + height), 2 * (width + height)]
 27 | 
 28 | (.bow) : Box -> Integer
 29 | (.bow) (MkBox length width height) = length * width * height
 30 | 
 31 | totalRibbon : Box -> Integer
 32 | totalRibbon x = x.ribbon + x.bow
 33 | 
 34 | paperNeeded : Box -> Integer
 35 | paperNeeded x = x.area + x.slack
 36 | 
 37 | parseBox : Has (Except String) fs =>
 38 |   String -> Eff fs Box
 39 | parseBox str = do
 40 |   l ::: [w, h] <- pure $ split (== 'x') str
 41 |     | xs => throw "Box did not have exactly 3 components: \{show xs}"
 42 |   length <- note "Failed parsing length: \{show l}" $ parsePositive l
 43 |   width <- note "Failed parsing width: \{show w}" $ parsePositive w
 44 |   height <- note "Failed parsing height: \{show h}" $ parsePositive h
 45 |   pure $ MkBox length width height
 46 | 
 47 | part1 : Eff (PartEff String) (Integer, List Box)
 48 | part1 = do
 49 |   input <- map lines $ askAt "input"
 50 |   boxes <- traverse parseBox input
 51 |   let output = sum . map paperNeeded $ boxes
 52 |   pure (output, boxes)
 53 | 
 54 | part2 : (boxes : List Box) -> Eff (PartEff String) Integer
 55 | part2 boxes = pure . sum . map totalRibbon $ boxes
 56 | 
 57 | public export
 58 | day2 : Day
 59 | day2 = Both 2 part1 part2
 60 |