Day 10 Part 2

09/Main.idr

@@ -0,0 +1,201 @@
+import Data.String
+import Data.Vect
+import Data.List1
+import System.File.ReadWrite
+
+%default total
+
+data Direction = Up | Right | Left | Down
+%name Direction direction, direction2, direction3
+
+Show Direction where
+  show Up = "Up"
+  show Right = "Right"
+  show Left = "Left"
+  show Down = "Down"
+
+parseDirection : String -> Maybe Direction
+parseDirection input =
+  case trim input of
+    "U" => Just Up
+    "R" => Just Right
+    "L" => Just Left
+    "D" => Just Down
+    x => Nothing
+
+-- Apply a direction to a pair of Ints
+applyDirection : Direction -> (Int, Int) -> (Int, Int)
+applyDirection Up (x, y) = (x, y + 1)
+applyDirection Right (x, y) = (x + 1, y)
+applyDirection Left (x, y) = (x - 1, y)
+applyDirection Down (x, y) = (x, y - 1)
+
+data Motion = Move Direction Nat
+%name Motion motion, motion2, motion3
+
+Show Motion where
+  show (Move direction count) = show direction ++ " " ++ show count
+
+parseMotion : String -> Maybe Motion
+parseMotion input =
+  let components = split (== ' ') input in
+    case forget components of
+      [x, y] => do direction <- parseDirection x
+                   ammount <- parsePositive y
+                   pure (Move direction ammount)
+      _ => Nothing
+
+parseMotions : String -> Maybe (List Motion)
+parseMotions input =
+  let inputLines = lines input
+  in traverse parseMotion inputLines
+
+-- Get the distance moved by a motion
+distance : Motion -> Nat
+distance (Move _ i) = i
+
+-- Break a motion down into a list of moves-by-one
+breakdown : (motion : Motion) -> Vect (distance motion) Direction
+breakdown (Move direction 0) = []
+breakdown input@(Move direction (S k)) = direction :: breakdown (assert_smaller input (Move direction k))
+
+touching : (Int, Int) -> (Int, Int) -> Bool
+touching (x, y) (z, w) =
+  let (u, v) = (abs (x - z), abs (y - w)) in
+  u <= 1 && v <= 1
+
+data State : Nat -> Type where
+  MkState : (head : (Int, Int)) -> (tails : Vect n (Int, Int)) -> State n
+%name State state, state1, state2
+
+emptyState : {n : Nat} -> State n
+emptyState = MkState (0,0) (replicate _ (0,0))
+
+Show (State n) where
+  show (MkState head tails) = "Head: " ++ show head ++ " Tails: " ++ show tails
+
+stateTails : State n -> Vect n (Int, Int)
+stateTails (MkState head xs) = xs
+
+sign : Int -> Int
+sign i = if i == 0 then 0 else div i (abs i)
+
+mapP : (a -> b) -> (a, a) -> (b, b)
+mapP f (x, y) = (f x, f y)
+
+zipP : (a -> b -> c) -> (a, a) -> (b, b) -> (c, c)
+zipP f (x, y) (z, w) = (f x z, f y w)
+
+-- Increment the tail
+incTail : (head : (Int, Int)) -> (tail : (Int, Int)) -> (Int, Int)
+incTail head tail =
+  let diff = zipP (-) head tail
+      absDiff = mapP abs diff
+      signs = mapP sign diff
+  in if touching head tail
+     then tail
+     else zipP (+) tail signs
+
+incTails : {n: Nat} -> (head : (Int, Int)) -> (tails : Vect n (Int, Int)) -> Vect n (Int, Int)
+incTails head [] = []
+incTails head (x :: xs) =
+  let newTail = incTail head x in
+  newTail :: incTails newTail xs
+
+moveHead' : {n: Nat} -> Direction -> State n -> State n
+moveHead' direction (MkState head tails) =
+  let newHead = applyDirection direction head in
+  MkState newHead (incTails newHead tails)
+
+applyMotion' : {m: Nat} -> (motion : Motion) -> State m -> (State m, Vect (S (distance motion)) (State m))
+applyMotion' motion state = helper (breakdown motion) state
+  where helper : {m: Nat} -> (directions : Vect n Direction) -> State m -> (State m, Vect (S n) (State m))
+        helper [] state = (state, [state])
+        helper (x :: xs) state =
+          let newState = moveHead' x state
+              (resState, rest) = helper xs newState
+          in (resState, state :: rest)
+
+applyMotions' : {m : Nat} -> (motions : List Motion) -> State m -> (State m, List (State m))
+applyMotions' [] state = (state, [state])
+applyMotions' (x :: xs) state =
+  let (newState, motions) = applyMotion' x state
+      (outputState, rest) = applyMotions' xs newState
+  in (outputState, (toList motions) ++ rest)
+
+simple = """
+  R 4
+  U 4
+  L 3
+  D 1
+  R 4
+  D 1
+  L 5
+  R 2
+  """
+
+complex = """
+  R 5
+  U 8
+  L 8
+  D 3
+  R 17
+  D 10
+  L 25
+  U 20
+  """
+
+testPart : Nat -> (input : String) -> IO ()
+testPart Z input = putStrLn "No Tail!"
+testPart (S m) input =
+  case parseMotions input of
+    Nothing => putStrLn "Failed to parse motions"
+    Just motions =>
+      let (state, states) = applyMotions' motions (emptyState {n = (S m)})
+          tails = map (last . stateTails) states
+          uniqueTails = nub tails
+      in do putStrLn "Movements:"
+            traverse_ printLn motions
+            putStrLn "\nSteps:"
+            traverse_ printLn states
+            putStrLn "\nUnique Tails:"
+            printLn $ length uniqueTails
+
+testPart1 : IO ()
+testPart1 = testPart 1 simple
+
+testPart2 : IO ()
+testPart2 =
+  do testPart 9 simple
+     testPart 9 complex
+
+part : Nat -> String -> Maybe Nat
+part 0 str = ?part_rhs_0
+part (S k) input =
+  case parseMotions input of
+    Nothing => Nothing
+    Just motions =>
+      let (state, states) = applyMotions' motions (emptyState {n = (S k)})
+          tails = map (last . stateTails) states
+      in Just . length . nub $ tails
+
+
+part1 : String -> Maybe Nat
+part1 input = part 1 input
+
+part2 : String -> Maybe Nat
+part2 input = part 9 input
+
+partial main : IO ()
+main =
+  do file <- readFile "input"
+     case file of
+       Left err => printLn err
+       Right contents =>
+        case part1 contents of
+          Nothing => printLn "Error in part 1"
+          Just part1Count =>
+            do putStrLn ("Part 1: " ++ show part1Count)
+               case part2 contents of
+                 Nothing => printLn "Error in part 2"
+                 Just part2Count => putStrLn ("Part 2: " ++ show part2Count)

10/Main.idr

@@ -0,0 +1,151 @@
+import Data.Vect
+import Data.Fin
+import Data.String
+import Data.List
+import System.File.ReadWrite
+
+data Operation = Noop | Addx Int
+%name Operation op
+
+Show Operation where
+  show Noop = "Noop"
+  show (Addx i) = "Addx " ++ show i
+
+cycles : Operation -> Nat
+cycles Noop = 0
+cycles (Addx i) = 1
+
+parseOp : String -> Maybe Operation
+parseOp str =
+  case map trim . words $ str of
+    ["noop"] => Just Noop
+    ["addx", val] => do val <- parseInteger val
+                        pure (Addx val)
+    _ => Nothing
+
+parseOps : String -> Maybe (List Operation)
+parseOps str = traverse parseOp (lines str)
+
+data Pixel = On | Off
+%name Pixel pixel
+
+Show Pixel where
+  show On = "#"
+  show Off = " "
+
+record State where
+  constructor MkState
+  cycle : Nat
+  xRegister : Int
+  waitCycles : Nat
+  waitingOp : Maybe Operation
+%name State state
+
+Show State where
+  show (MkState cycle xRegister waitCycles waitingOp) =
+    "Cycle: " ++ show cycle ++ " X: " ++ show xRegister ++ " waitingOp: " ++ show waitingOp
+
+startState : State
+startState = MkState 0 1 0 Nothing
+
+isWaiting : State -> Bool
+isWaiting (MkState cycle xRegister waitCycles Nothing) = False
+isWaiting (MkState cycle xRegister waitCycles (Just x)) = True
+
+-- Tick the CPU, taking an operation off the stack if needed
+tick : State -> List Operation -> (State, List Operation)
+tick (MkState cycle xRegister 0 Nothing) [] =
+  (MkState (S cycle) xRegister 0 Nothing, [])
+tick (MkState cycle xRegister 0 (Just Noop)) [] =
+  (MkState (S cycle) xRegister 0 Nothing, [])
+tick (MkState cycle xRegister 0 (Just (Addx i))) [] =
+  (MkState (S cycle) (xRegister + i) 0 Nothing, [])
+tick (MkState cycle xRegister (S k) waitingOp) [] =
+  (MkState (S cycle) xRegister k waitingOp, [])
+tick (MkState cycle xRegister 0 Nothing) (x :: xs) =
+  (MkState (S cycle) xRegister (cycles x) (Just x), xs)
+tick (MkState cycle xRegister 0 (Just Noop)) (x :: xs) =
+  (MkState (S cycle) xRegister (cycles x) (Just x), xs)
+tick (MkState cycle xRegister 0 (Just (Addx i))) (x :: xs) =
+  (MkState (S cycle) (xRegister + i) (cycles x) (Just x), xs)
+tick (MkState cycle xRegister (S k) waitingOp) rest@(x :: xs) =
+  (MkState (S cycle) xRegister k waitingOp, rest)
+
+tickMultiple : State -> List Operation -> List State
+tickMultiple state [] =
+  if isWaiting state
+    then let (newState, rest) = tick state []
+             tail = tickMultiple newState rest
+         in state :: tail
+    else [state]
+tickMultiple state ops@(x :: xs) =
+  let (newState, rest) = tick state ops
+      tail = tickMultiple newState rest
+  in state :: tail
+
+data CRT : Type where
+  MkCrt : Vect 6 (Vect 40 Pixel) -> CRT
+%name CRT crt
+
+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 []
+indexes (x :: ys) xs =
+  do idx <- natToFin x (length xs)
+     let value = index' xs idx
+     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
+
+part1 : List Operation -> Maybe Int
+part1 ops =
+  let states = tickMultiple startState ops in
+  do selectedStates <- indexes (cycle 20 40 (length states)) states
+     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"
+       | Left err => printLn err
+     Just ops <- pure (parseOps file)
+       | Nothing => putStrLn "Error parsing ops"
+     Just part1Result <- pure (part1 ops)
+       | Nothing => putStrLn "Error in part1"
+     putStrLn ("Part 1: " ++ show part1Result)
+     let part2Result = part2 ops
+     putStrLn "\nPart 2:"
+     printLn part2Result

10/input

@@ -0,0 +1,137 @@
+noop
+addx 7
+addx -1
+addx -1
+addx 5
+noop
+noop
+addx 1
+addx 3
+addx 2
+noop
+addx 2
+addx 5
+addx 2
+addx 10
+addx -9
+addx 4
+noop
+noop
+noop
+addx 3
+addx 5
+addx -40
+addx 26
+addx -23
+addx 2
+addx 5
+addx 26
+addx -35
+addx 12
+addx 2
+addx 17
+addx -10
+addx 3
+noop
+addx 2
+addx 3
+noop
+addx 2
+addx 3
+noop
+addx 2
+addx 2
+addx -39
+noop
+addx 15
+addx -12
+addx 2
+addx 10
+noop
+addx -1
+addx -2
+noop
+addx 5
+noop
+addx 5
+noop
+noop
+addx 1
+addx 4
+addx -25
+addx 26
+addx 2
+addx 5
+addx 2
+noop
+addx -3
+addx -32
+addx 1
+addx 4
+addx -2
+addx 3
+noop
+noop
+addx 3
+noop
+addx 6
+addx -17
+addx 27
+addx -7
+addx 5
+addx 2
+addx 3
+addx -2
+addx 4
+noop
+noop
+addx 5
+addx 2
+addx -39
+noop
+noop
+addx 2
+addx 5
+addx 3
+addx -2
+addx 2
+addx 11
+addx -4
+addx -5
+noop
+addx 10
+addx -18
+addx 19
+addx 2
+addx 5
+addx 2
+addx 2
+addx 3
+addx -2
+addx 2
+addx -37
+noop
+addx 5
+addx 4
+addx -1
+noop
+addx 4
+noop
+noop
+addx 1
+addx 4
+noop
+addx 1
+addx 2
+noop
+addx 3
+addx 5
+noop
+addx -3
+addx 5
+addx 5
+addx 2
+addx 3
+noop
+addx -32
+noop