Compare commits
No commits in common. "85263e08a1240dcdd1f000dabe86428b1bfce334" and "e7c7a3fc9de905cc208881b40c429b2abddf82e3" have entirely different histories.
85263e08a1
...
e7c7a3fc9d
201
09/Main.idr
201
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)
|
||||
151
10/Main.idr
151
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
|
||||
137
10/input
137
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
|
||||
Loading…
Reference in New Issue