197 lines
7.2 KiB
Idris
197 lines
7.2 KiB
Idris
import Data.Vect
|
|
import Data.List1
|
|
import Data.SnocList
|
|
import Data.String
|
|
import Data.Fin
|
|
import System.File.ReadWrite
|
|
|
|
allFins' : (n : Nat) -> List (Fin n)
|
|
allFins' n = toList (allFins'' n)
|
|
where
|
|
allFins'' : (n : Nat) -> SnocList (Fin n)
|
|
allFins'' 0 = Lin
|
|
allFins'' 1 = Lin :< FZ
|
|
allFins'' (S k) = map weaken (allFins'' k) :< last
|
|
|
|
data Data : Type where
|
|
-- An atom, in this case, a nat, for now
|
|
MkAtom : (atom : Nat) -> Data
|
|
-- A list of sub-datas
|
|
MkList : (n : Nat) -> (contents : Vect n Data) -> Data
|
|
|
|
Show Data where
|
|
show (MkAtom atom) = show atom
|
|
show input@(MkList n contents) =
|
|
let inner = joinBy "," . toList . map (\x => show (assert_smaller input x)) $ contents in
|
|
"[" ++ inner ++ "]"
|
|
|
|
Eq Data where
|
|
(==) (MkAtom atom) (MkAtom k) = atom == k
|
|
(==) (MkAtom atom) (MkList n contents) = False
|
|
(==) (MkList n contents) (MkAtom atom) = False
|
|
(==) (MkList n contents) (MkList k xs) = helper (toList contents) (toList xs)
|
|
where helper : List Data -> List Data -> Bool
|
|
helper [] [] = True
|
|
helper (x :: xs) [] = False
|
|
helper [] (x :: xs) = False
|
|
helper ((MkAtom atom) :: xs) ((MkAtom j) :: ys) =
|
|
if atom == j
|
|
then helper xs ys
|
|
else False
|
|
helper ((MkAtom atom) :: xs) ((MkList j zs) :: ys) = False
|
|
helper ((MkList j zs) :: xs) ((MkAtom atom) :: ys) = False
|
|
helper input1@((MkList j zs) :: xs) ((MkList i ws) :: ys) =
|
|
if helper (assert_smaller input1 (toList zs)) (toList ws)
|
|
then helper xs ys
|
|
else False
|
|
|
|
atomToList : Nat -> Data
|
|
atomToList i = MkList 1 [MkAtom i]
|
|
|
|
splitNonNesting : String -> Maybe (List String)
|
|
splitNonNesting str =
|
|
do result <- splitNonNesting' (== ',') (unpack (trim str)) 0 Lin
|
|
let packed = map pack result
|
|
pure packed
|
|
where splitNonNesting' : (test : (Char -> Bool)) -> (input: List Char) -> (depth : Nat)
|
|
-> (buffer : SnocList Char) -> Maybe (List (List Char))
|
|
splitNonNesting' test (['[', ']']) depth buffer = Just [[]]
|
|
splitNonNesting' test ('[' :: xs) 0 buffer =
|
|
splitNonNesting' test xs 1 buffer
|
|
splitNonNesting' test ('[' :: xs) depth@(S k) buffer =
|
|
splitNonNesting' test xs (S depth) (buffer :< '[')
|
|
splitNonNesting' test ([']']) 0 [<] = Just []
|
|
splitNonNesting' test ([']']) 0 buffer = Nothing
|
|
splitNonNesting' test ([']']) 1 buffer@(sx :< x) =
|
|
let buffer = toList buffer in Just [buffer]
|
|
splitNonNesting' test ([']']) (S k) buffer = Nothing
|
|
splitNonNesting' test [] 0 [<] = Just []
|
|
splitNonNesting' test [] 0 buffer@(sx :< x) =
|
|
let buffer = toList buffer in Just [buffer]
|
|
splitNonNesting' test [] (S k) buffer = Nothing
|
|
splitNonNesting' test (']' :: xs) 0 buffer = Nothing
|
|
splitNonNesting' test (']' :: xs) (S k) buffer =
|
|
splitNonNesting' test xs k (buffer :< ']')
|
|
splitNonNesting' test (x :: xs) 0 buffer = Nothing
|
|
splitNonNesting' test (x :: xs) 1 buffer =
|
|
if test x
|
|
then do let buffer = toList buffer
|
|
rest <- splitNonNesting' test xs 1 Lin
|
|
pure $ buffer :: rest
|
|
else splitNonNesting' test xs 1 (buffer :< x)
|
|
splitNonNesting' test (x :: xs) (S k) buffer =
|
|
splitNonNesting' test xs (S k) (buffer :< x)
|
|
|
|
parseAtom : String -> Maybe Data
|
|
parseAtom = map MkAtom . parsePositive
|
|
|
|
mutual
|
|
parseList : String -> Maybe Data
|
|
parseList str =
|
|
do components <- splitNonNesting str
|
|
parsed <- traverse parseData components
|
|
let n = length parsed
|
|
list <- toVect n parsed
|
|
pure (MkList n list)
|
|
|
|
parseData : String -> Maybe Data
|
|
parseData str =
|
|
-- Attempt to parse as an atom first, then a list
|
|
case parseAtom str of
|
|
Just atom => Just atom
|
|
Nothing =>
|
|
-- Then attempt to parse as a list
|
|
parseList str
|
|
|
|
checkOrder' : (left : Data) -> (right : Data) -> Maybe Bool
|
|
checkOrder' (MkAtom atom) (MkAtom k) = if atom == k then Nothing else Just (atom < k)
|
|
checkOrder' (MkAtom atom) list@(MkList n contents) = checkOrder' (atomToList atom) list
|
|
checkOrder' list@(MkList n contents) (MkAtom atom) = checkOrder' list (atomToList atom)
|
|
checkOrder' (MkList 0 []) (MkList 0 []) = Nothing
|
|
checkOrder' (MkList 0 []) (MkList m ys) = Just True
|
|
checkOrder' (MkList (S n) xs) (MkList 0 []) = Just False
|
|
checkOrder' (MkList (S n) (x :: xs)) (MkList (S m) (y :: ys)) =
|
|
case checkOrder' x y of
|
|
Nothing => checkOrder' (MkList n xs) (MkList m ys)
|
|
Just z => Just z
|
|
-- For some reason idris thinks this isn't covering
|
|
checkOrder' _ _ = Nothing
|
|
|
|
-- Returns true of the two datas are in the correct order
|
|
checkOrder : (left : Data) -> (right : Data) -> Bool
|
|
checkOrder left right =
|
|
case checkOrder' left right of
|
|
Nothing => True
|
|
Just x => x
|
|
|
|
parsePairs : String -> Maybe (n : Nat ** Vect n (Data, Data))
|
|
parsePairs str =
|
|
do let lines = map trim . lines $ str
|
|
let groups = split (=="") lines
|
|
pairs <- traverse toPair (toList groups)
|
|
pairs <- traverse handlePairs pairs
|
|
let n = length pairs
|
|
pairs <- toVect n pairs
|
|
pure (n ** pairs)
|
|
where toPair : List String -> Maybe (String, String)
|
|
toPair [a, b] = Just (a, b)
|
|
toPair strs = Nothing
|
|
handlePairs : (String, String) -> Maybe (Data, Data)
|
|
handlePairs (x, y) =
|
|
do x <- parseData x
|
|
y <- parseData y
|
|
pure (x, y)
|
|
|
|
parseVect : String -> Maybe (m : Nat ** Vect m Data)
|
|
parseVect str =
|
|
do let lines = filter (not . (=="")). map trim . lines $ str
|
|
datas <- traverse parseData lines
|
|
let m = length datas
|
|
datas <- toVect m datas
|
|
pure (m ** datas)
|
|
|
|
part1 : (pairs : (n : Nat ** Vect n (Data, Data))) -> Nat
|
|
part1 (n ** pairs) =
|
|
let indicies = allFins' n
|
|
correct_order =
|
|
map S .
|
|
map finToNat .
|
|
filter (\x =>
|
|
let (x,y) = index x pairs
|
|
in checkOrder x y) $
|
|
indicies
|
|
in sum correct_order
|
|
|
|
sort : {n : Nat} -> Vect n Data -> Vect n Data
|
|
sort [] = []
|
|
sort (x :: xs) = insert x (sort xs)
|
|
where insert : {m : Nat} -> Data -> Vect m Data -> Vect (S m) Data
|
|
insert x [] = [x]
|
|
insert x rest@(y :: xs) =
|
|
if checkOrder x y
|
|
then x :: y :: xs
|
|
else y :: insert x xs
|
|
|
|
part2 : (datas : (m : Nat ** Vect m Data)) -> Maybe Nat
|
|
part2 (m ** datas) =
|
|
do let divider_packets =
|
|
(MkList 1 [MkList 1 [MkAtom 2]]) :: (MkList 1 [MkList 1 [MkAtom 6]]) :: datas
|
|
let sorted = sort divider_packets
|
|
divider_1 <- findIndex (== MkList 1 [MkList 1 [MkAtom 2]]) sorted
|
|
divider_2 <- findIndex (== MkList 1 [MkList 1 [MkAtom 6]]) sorted
|
|
let (divider_1, divider_2) = (1 + finToNat divider_1, 1 + finToNat divider_2)
|
|
pure (divider_1 * divider_2)
|
|
|
|
main : IO ()
|
|
main =
|
|
do Right file <- readFile "input"
|
|
| Left err => printLn err
|
|
Just pairs <- pure (parsePairs file)
|
|
| Nothing => putStrLn "Failed parsing input"
|
|
putStrLn $ "Part 1: " ++ show (part1 pairs)
|
|
Just datas <- pure (parseVect file)
|
|
| Nothing => putStrLn "Failed parsing input"
|
|
Just part2Result <- pure (part2 datas)
|
|
| Nothing => putStrLn "Error in part2"
|
|
putStrLn $ "Part 2: " ++ show part2Result
|