Year 2015 Day 2 Part 1

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
   ]

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