diff --git a/10/Main.idr b/10/Main.idr index 9b731ec..83a3ea5 100644 --- a/10/Main.idr +++ b/10/Main.idr @@ -31,7 +31,7 @@ data Pixel = On | Off Show Pixel where show On = "#" - show Off = "." + show Off = " " record State where constructor MkState @@ -83,160 +83,33 @@ tickMultiple state ops@(x :: xs) = tail = tickMultiple newState rest in state :: tail -extraSimple = """ - noop - addx 3 - addx -5 -""" +data CRT : Type where + MkCrt : Vect 6 (Vect 40 Pixel) -> CRT +%name CRT crt -simple = """ - addx 15 - addx -11 - addx 6 - addx -3 - addx 5 - addx -1 - addx -8 - addx 13 - addx 4 - noop - addx -1 - addx 5 - addx -1 - addx 5 - addx -1 - addx 5 - addx -1 - addx 5 - addx -1 - addx -35 - addx 1 - addx 24 - addx -19 - addx 1 - addx 16 - addx -11 - noop - noop - addx 21 - addx -15 - noop - noop - addx -3 - addx 9 - addx 1 - addx -3 - addx 8 - addx 1 - addx 5 - noop - noop - noop - noop - noop - addx -36 - noop - addx 1 - addx 7 - noop - noop - noop - addx 2 - addx 6 - noop - noop - noop - noop - noop - addx 1 - noop - noop - addx 7 - addx 1 - noop - addx -13 - addx 13 - addx 7 - noop - addx 1 - addx -33 - noop - noop - noop - addx 2 - noop - noop - noop - addx 8 - noop - addx -1 - addx 2 - addx 1 - noop - addx 17 - addx -9 - addx 1 - addx 1 - addx -3 - addx 11 - noop - noop - addx 1 - noop - addx 1 - noop - noop - addx -13 - addx -19 - addx 1 - addx 3 - addx 26 - addx -30 - addx 12 - addx -1 - addx 3 - addx 1 - noop - noop - noop - addx -9 - addx 18 - addx 1 - addx 2 - noop - noop - addx 9 - noop - noop - noop - addx -1 - addx 2 - addx -37 - addx 1 - addx 3 - noop - addx 15 - addx -21 - addx 22 - addx -6 - addx 1 - noop - addx 2 - addx 1 - noop - addx -10 - noop - noop - addx 20 - addx 1 - addx 2 - addx 2 - addx -6 - addx -11 - noop - noop - noop - """ +Show CRT where + show (MkCrt xs) = + let rows = map (concatMap show) xs + in joinBy "\n" (toList rows) + +emptyCrt : CRT +emptyCrt = MkCrt (replicate _ (replicate _ Off)) + +applyState : CRT -> State -> CRT +applyState (MkCrt xs) (MkState 0 xRegister waitCycles waitingOp) = MkCrt xs +applyState (MkCrt xs) (MkState cycle@(S k) xRegister waitCycles waitingOp) = + let crtPos = k `mod` 40 + crtRow = k `div` 40 + xDiff = xRegister - (cast crtPos) + in case (natToFin crtRow 6, natToFin crtPos 40) of + (Just row, Just col) => + if abs xDiff <= 1 + then let oldRow = index row xs + newRow = replaceAt col On oldRow + newXs = replaceAt row newRow xs + in MkCrt newXs + else MkCrt xs + _ => MkCrt xs indexes : List Nat -> List a -> Maybe (List (Nat, a)) indexes [] xs = Just [] @@ -246,26 +119,12 @@ indexes (x :: ys) xs = rest <- indexes ys xs pure ((x, value) :: rest) - cycle : (start : Nat) -> (inc : Nat) -> (end : Nat) -> List Nat cycle start inc end = if start >= end then [] else start :: cycle (assert_smaller start (start + inc)) inc end -testPart1 : IO () -testPart1 = - do Just ops <- pure $ parseOps simple - | Nothing => putStrLn "Error parsing ops" - let states = tickMultiple startState ops - let idxs = cycle 20 40 (length states) - Just selectedStates <- pure . map (map snd) $ indexes idxs states - | Nothing => putStrLn "Not enough cycles" - putStrLn "Selected States:" - traverse_ printLn selectedStates - let totalSignal = sum . map (\x => (xRegister x) * (cast (cycle x))) $ selectedStates - putStrLn ("Total Signal Strength: " ++ show totalSignal) - part1 : List Operation -> Maybe Int part1 ops = let states = tickMultiple startState ops in @@ -273,6 +132,11 @@ part1 ops = let totalSignal = sum . map (\x => (xRegister x) * (cast (cycle x))) . map snd $ selectedStates pure totalSignal +part2 : List Operation -> CRT +part2 ops = + let states = tickMultiple startState ops + in foldl applyState emptyCrt states + main : IO () main = do Right file <- readFile "input" @@ -282,3 +146,6 @@ main = Just part1Result <- pure (part1 ops) | Nothing => putStrLn "Error in part1" putStrLn ("Part 1: " ++ show part1Result) + let part2Result = part2 ops + putStrLn "\nPart 2:" + printLn part2Result