09/Main.idr

@@ -1,201 +0,0 @@
-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

@@ -1,151 +0,0 @@
-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

@@ -1,137 +0,0 @@
-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