64 lines
1.7 KiB
Agda
64 lines
1.7 KiB
Agda
module Day4
|
||
|
||
import Prelude
|
||
import Node
|
||
|
||
Round : U
|
||
Round = List Int × List Int
|
||
|
||
parseRound : String → Maybe Round
|
||
parseRound s =
|
||
let (a :: b :: Nil) = split s ": " | _ => Nothing in
|
||
let (l :: r :: Nil) = split b " | " | _ => Nothing in
|
||
Just (nums l, nums r)
|
||
where
|
||
-- Nat or Int here?
|
||
nums : String → List Int
|
||
-- catch - split returns empty strings that become zeros
|
||
nums s = map stringToInt $ filter (_/=_ "") $ split (trim s) " "
|
||
|
||
parse : String -> Maybe (List Round)
|
||
parse s = mapM parseRound (split (trim s) "\n")
|
||
|
||
pfunc pow : Int → Int → Int := `(x,y) => x ** y`
|
||
|
||
part1 : List Round → Int
|
||
part1 rounds = foldl _+_ 0 $ map score rounds
|
||
where
|
||
-- TODO we'll keep the math in Int land until we have magic Nat
|
||
score : Round → Int
|
||
score (a,b) = let count = natToInt $ length $ filter (\ n => elem n b) a
|
||
in if count == 0 then 0 else pow 2 (count - 1)
|
||
|
||
part2 : List Round → Int
|
||
part2 rounds = go 0 $ map (_,_ 1) rounds
|
||
where
|
||
mark : Int -> Nat → List (Int × Round) → List (Int × Round)
|
||
mark _ _ Nil = Nil
|
||
mark v Z rounds = rounds
|
||
mark v (S k) ((cnt, round) :: rounds) = (cnt + v, round) :: mark v k rounds
|
||
|
||
go : Int → List (Int × Round) → Int
|
||
go acc Nil = acc
|
||
go acc ((cnt, a, b) :: rounds) =
|
||
let n = length $ filter (\ n => elem n b) a
|
||
in go (acc + cnt) $ mark cnt n rounds
|
||
|
||
run : String -> IO Unit
|
||
run fn = do
|
||
putStrLn fn
|
||
text <- readFile fn
|
||
let (Just cards) = parse text
|
||
| _ => putStrLn "fail"
|
||
putStrLn "part1"
|
||
printLn (part1 cards)
|
||
putStrLn "part2"
|
||
printLn (part2 cards)
|
||
|
||
-- 13/30
|
||
-- 25004/14427616
|
||
main : IO Unit
|
||
main = do
|
||
run "aoc2023/day4/eg.txt"
|
||
run "aoc2023/day4/input.txt"
|