Today’s problem looked like it would be really hard, and I had to study for an exam, so I decided to postpone it. Even after more than two weeks, my brain’s background processing yielded no breakthroughs, so today – the last day of the year – I sat down to see how far I could get.
I created the data types, wrote the parsers for the input format, using the great lean4-parser library, and started working out how many packages I can fit inside rectangular regions.
The simple case is…well, simple: Since the packages are square, we can simply count how many places there are for packages in a region. If the number of potential places is equal to or greater than the number of packages, they will fit. No tetris-ing needed. The other simple case is when even if we could somehow optimally pack the packages and they still wouldn’t fit, well, they won’t fit.
The third case is worse. Then it’s Korobeiniki time. Let’s postpone this for now:
if numPackages <= places then
true
else
if minPackagesArea > totalArea then
false
else
panic! "Tetris time"I wonder how many of these there are!
❯ lake exec day12
Part 1: 517I…I…I’m not even mad.
And part 2? There was none! I’m done! A belated Merry Christmas to me!
Things I (re-)learned today
- Nothing, really – only that using parser combinators is fun!
“Solution”
import Parser
import Aoc
open Aoc
structure Package (n m : Nat) where
width : Nat := m
length : Nat := n
shape : Vector (Vector Char m) n
deriving Repr
def Package.maxArea {n m : Nat} (_ : Package n m) : Nat :=
n * m
def Package.minArea {n m : Nat} (p : Package n m) : Nat :=
p.shape.flatten.toArray.filter (. == '#') |>.size
structure Region where
width : Nat
length : Nat
packageCounts : List Nat
deriving Repr
namespace Parser
open Parser Char ASCII
-- 0:
-- ###
-- ##.
-- ##.
def parsePackage (n m : Nat) : SimpleParser Substring Char (Package n m) := do
let _index <- parseNat
_ <- char ':'
_ <- eol
let rowsArray <- Array.mk <$> (List.range n).mapM λ _ => do
let rowArray <- Array.mk <$> (List.range m).mapM λ _ => char '#' <|> char '.'
_ <- eol
return rowArray
let rows := Vector.ofFn (λ i => Vector.ofFn (λ j => rowsArray[i]![j]!))
return { shape := rows }
-- 4x4: 0 0 0 0 2 0
def parseRegion : SimpleParser Substring Char Region := do
let width <- parseNat
_ <- char 'x'
let length <- parseNat
_ <- char ':'
_ <- takeMany1 whitespace
let counts <- sepBy1 (char ' ') parseNat
return { width := width, length := length, packageCounts := counts.toList }
def parseInput (n m : Nat) : SimpleParser Substring Char (List (Package n m) × Array Region) := do
let packages <- sepBy1 eol (parsePackage n m)
_ <- takeMany1 eol
let regions <- sepBy eol parseRegion
return (packages.toList, regions)
end Parser
def canFit (packages : List (Package n m)) (region : Region) : Bool :=
let places := (region.width / 3) * (region.length / 3)
let packages := packages.zip region.packageCounts
|>.filter (λ (_, count) => count > 0)
|>.map (λ (p, count) => (p, count))
let numPackages := packages.foldl (λ acc (_, count) => acc + count) 0
if numPackages <= places then
true
else
let totalArea := region.width * region.length
let minPackagesArea := packages.foldl (λ acc (p, count) => acc + count * p.minArea) 0
if minPackagesArea > totalArea then
false
else
panic! "Tetris time"
def main : IO Unit := do
let input <- IO.FS.readFile "Day12/input.txt"
let (packages, regions) <- (match (Parser.parseInput 3 3).run input with
| .ok _ result => Except.ok result
| .error err _ => Except.error s!"{err}") |> IO.ofExcept
let count := regions.filter (λ r => canFit packages r) |>.size
-- part 1
IO.println s!"Part 1: {count}"