Compare commits

...

4 Commits

Author SHA1 Message Date
Nathan McCarty 85263e08a1
Day 10 Part 2 2022-12-10 18:16:03 -05:00
Nathan McCarty 383b504a89
Day 10 Part 1 2022-12-10 17:32:21 -05:00
Nathan McCarty 532634d1f3
Day 9 Part 2 2022-12-10 02:45:51 -05:00
Nathan McCarty 755b570063
Day 9 Part 1 2022-12-09 19:02:56 -05:00
4 changed files with 2489 additions and 0 deletions

201
09/Main.idr Normal file
View File

@ -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)

2000
09/input Normal file

File diff suppressed because it is too large Load Diff

151
10/Main.idr Normal file
View File

@ -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

137
10/input Normal file
View File

@ -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