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