Files
newt/aoc2023/Day6.newt

75 lines
1.9 KiB
Agda
Raw Blame History

module Day6
import Prelude
import Node
import Aoc
Problem : U
Problem = List (Int × Int)
pNums : String Either String (List Int)
pNums line =
let (_ :: line :: Nil) = split line ": "
| _ => Left "expected two parts" in
Right $ nums line
parse : String Either String Problem
parse content = do
let (a :: b :: Nil) = split (trim content) "\n"
| _ => Left "expected two lines"
times <- pNums a
dists <- pNums b
Right (zip times dists)
part1 : Problem Int
part1 prob = go 1 prob
where
run : Int -> Int -> Int Int Int
run time dist t count =
let count = if dist < t * (time - t) then count + 1 else count in
if time == t then count
else run time dist (t + 1) count
go : Int Problem Int
go acc Nil = acc
go acc ((time,dist) :: prob) = go (acc * run time dist 0 0) prob
part2 : Int × Int IO Unit
part2 (time,dist) = do
let t = intToDouble time
let d = intToDouble dist
let x = sqrtDouble (t * t - intToDouble 4 * d)
let start = (t - x) / intToDouble 2
let stop = (t + x) / intToDouble 2
let s = doubleToInt $ ceilDouble start
let e = doubleToInt $ ceilDouble stop
putStrLn $ "part2 " ++ show (e - s)
parse2 : String Either String (Int × Int)
parse2 content =
let (a :: b :: Nil) = split (trim content) "\n"
| _ => Left "too many parts" in
let time = stringToInt $ pack $ filter isDigit $ unpack a
dist = stringToInt $ pack $ filter isDigit $ unpack b
in Right (time, dist)
run : String -> IO Unit
run fn = do
putStrLn fn
text <- readFile fn
let (Right prob) = parse text | Left err => putStrLn err
putStrLn $ debugStr prob
putStrLn $ "part1 " ++ show (part1 prob)
let (Right prob) = parse2 text | Left err => putStrLn err
part2 prob
-- debugLog prob
-- part2 prob
-- 288 / 71503
-- 1413720 / 30565288
main : IO Unit
main = do
run "aoc2023/day6/eg.txt"
run "aoc2023/day6/input.txt"