59 lines
1.4 KiB
Agda
59 lines
1.4 KiB
Agda
module Day7
|
||
|
||
import Prelude
|
||
import Node
|
||
import Aoc
|
||
|
||
Prob : U
|
||
Prob = Int × List Int
|
||
|
||
cases : Int → Int → List Int → Bool
|
||
cases goal acc Nil = goal == acc
|
||
cases goal acc (x :: xs) =
|
||
if goal < acc then False
|
||
else if cases goal (x + acc) xs then True
|
||
else cases goal (x * acc) xs
|
||
|
||
part1 : Prob → Bool
|
||
part1 (goal, x :: xs) = cases goal x xs
|
||
part1 _ = False
|
||
|
||
cat : Int → Int → Int
|
||
cat x y = stringToInt $ show x ++ show y
|
||
|
||
cases2 : Int → Int → List Int → Bool
|
||
cases2 goal acc Nil = goal == acc
|
||
cases2 goal acc (x :: xs) =
|
||
if goal < acc then False
|
||
else if cases2 goal (x + acc) xs then True
|
||
else if cases2 goal (x * acc) xs then True
|
||
else cases2 goal (cat acc x) xs
|
||
|
||
part2 : Prob → Bool
|
||
part2 (goal, x :: xs) = cases2 goal x xs
|
||
part2 _ = False
|
||
|
||
parse : String -> Maybe (List Prob)
|
||
parse text = do
|
||
traverse parseLine $ split (trim text) "\n"
|
||
where
|
||
parseLine : String → Maybe Prob
|
||
parseLine line = do
|
||
let (a :: b :: Nil) = split line ": " | _ => Nothing
|
||
Just (stringToInt a , nums b)
|
||
|
||
run : String -> IO Unit
|
||
run fn = do
|
||
putStrLn fn
|
||
text <- readFile fn
|
||
let (Just probs) = parse text | _ => putStrLn "parse error"
|
||
let p1 = foldl _+_ 0 $ map fst $ filter part1 probs
|
||
putStrLn $ "part1 " ++ show p1
|
||
let p2 = foldl _+_ 0 $ map fst $ filter part2 probs
|
||
putStrLn $ "part2 " ++ show p2
|
||
|
||
main : IO Unit
|
||
main = do
|
||
run "aoc2024/day7/eg.txt"
|
||
run "aoc2024/day7/input.txt"
|