Compare commits
4 Commits
e7c7a3fc9d
...
85263e08a1
Author | SHA1 | Date |
---|---|---|
Nathan McCarty | 85263e08a1 | |
Nathan McCarty | 383b504a89 | |
Nathan McCarty | 532634d1f3 | |
Nathan McCarty | 755b570063 |
|
@ -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)
|
|
@ -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
|
|
@ -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
|
Loading…
Reference in New Issue