102 lines
3.1 KiB
Agda
102 lines
3.1 KiB
Agda
module Day9
|
||
|
||
import Prelude
|
||
import Node
|
||
import Aoc
|
||
|
||
parsePoint : String → Maybe Point
|
||
parsePoint text = case split text "," of
|
||
a :: b :: Nil => Just (stringToInt a, stringToInt b)
|
||
_ => Nothing
|
||
|
||
parse : String → List Point
|
||
parse text = mapMaybe parsePoint $ split (trim text) "\n"
|
||
|
||
abs : Int → Int
|
||
abs x = if x < 0 then 0 - x else x
|
||
|
||
data Line : U where
|
||
VL : (x y1 y2 : Int) → Line
|
||
HL : (y x1 x2 : Int) → Line
|
||
|
||
instance Show Line where
|
||
show (VL x y1 y2) = "VL \{show (x,y1,y2)}"
|
||
show (HL x y1 y2) = "HL \{show (x,y1,y2)}"
|
||
|
||
data Box = B Int Int Int Int
|
||
|
||
instance Show Box where
|
||
show (B l r t b) = "Box \{show (l,r,t,b)}"
|
||
|
||
area : Box → Int
|
||
area (B l r t b) = (abs (l - r) + 1) * (abs (t - b) + 1)
|
||
|
||
mkbox : Point → Point → Box
|
||
mkbox (a,b) (c,d) = B (min a c) (max a c) (min b d) (max b d)
|
||
|
||
makeBoxes : List Point → List Box
|
||
makeBoxes pts = go pts Nil
|
||
where
|
||
go2 : Point → List Point → List Box → List Box
|
||
go2 pt (x :: xs) acc = go2 pt xs (mkbox pt x :: acc)
|
||
go2 pt _ acc = acc
|
||
|
||
go : List Point → List Box → List Box
|
||
go (pt :: rest) acc = go rest $ go2 pt rest acc
|
||
go Nil acc = acc
|
||
|
||
-- line intersects middle of a box
|
||
isect : Box → Line → Bool
|
||
isect (B l r t b) (VL x y1 y2) = x < r && l < x && y1 < b && t < y2
|
||
isect (B l r t b) (HL y x1 x2) = y < b && t < y && x1 < r && l < x2
|
||
|
||
getLines : List Point → List Line
|
||
getLines points = go points Nil
|
||
where
|
||
go : List Point → List Line → List Line
|
||
go ((a,b) :: rest@((c,d) :: _)) acc =
|
||
if a == c
|
||
then let seg = if b < d then VL a b d else VL a d b in go rest (seg :: acc)
|
||
else if b == d then let seg = if a < c then HL b a c else HL b c a in go rest (seg :: acc)
|
||
else Nil
|
||
go _ acc = acc
|
||
|
||
-- I'm assuming the winner isn't a single row/column
|
||
part2 : List (Int × Box) → List Line → Int
|
||
part2 boxes lines = go boxes lines 0
|
||
where
|
||
winds : Box → Line → Bool
|
||
winds (B l r t b) (VL x y1 y2) =
|
||
-- pick a point in the middle, the rest is connected because no intersection
|
||
if t == b then False else r <= x && y1 < t + 1 && t + 1 < y2
|
||
winds (B l r t b) (HL x y1 y2) = False
|
||
|
||
checkRec : Box → Bool
|
||
checkRec box =
|
||
let (Nothing) = find (isect box) lines | _ => False in
|
||
let winding = length' $ filter (winds box) lines in mod winding 2 == 1
|
||
|
||
go : List (Int × Box) → List Line → Int → Int
|
||
go Nil _ acc = acc
|
||
go ((size, box) :: rest) lines acc =
|
||
if size < acc then go rest lines acc
|
||
else if checkRec box then go rest lines size
|
||
else go rest lines acc
|
||
|
||
run : String -> IO Unit
|
||
run fn = do
|
||
putStrLn fn
|
||
text <- readFile fn
|
||
let (pts@(a :: _)) = parse text | _ => putStrLn "empty input"
|
||
let boxes = map (\box => (area box, box)) $ makeBoxes pts
|
||
let ((p1,_) :: _ ) = boxes | _ => printLn "no boxes"
|
||
let x = foldl (\ acc x => if fst x > acc then fst x else acc) 0 boxes
|
||
putStrLn $ "part1 \{show p1} \{show x}"
|
||
let vl = getLines $ a :: reverse pts
|
||
putStrLn $ "part2 " ++ show (part2 boxes vl)
|
||
|
||
main : IO Unit
|
||
main = do
|
||
run "aoc2025/day9/eg.txt"
|
||
run "aoc2025/day9/input.txt"
|