import Data.List import Data.Vect import Data.String import System.File.ReadWrite %default total simple = """ $ cd / $ ls dir a 14848514 b.txt 8504156 c.dat dir d $ cd a $ ls dir e 29116 f 2557 g 62596 h.lst $ cd e $ ls 584 i $ cd .. $ cd .. $ cd d $ ls 4060174 j 8033020 d.log 5626152 d.ext 7214296 k """ data DirEntry = File String Nat | Directory String Show DirEntry where show (File name len) = name ++ " (" ++ show len ++ ")" show (Directory name) = name parseDirEntry : String -> Maybe DirEntry parseDirEntry entry = let worded = words entry in do fst <- head' worded lst <- last' worded if fst == "dir" then Just (Directory lst) else do len <- parsePositive fst Just (File lst len) data Command : Type where Cd : String -> Command Ls : List DirEntry -> Command Show Command where show (Cd str) = "cd " ++ str show (Ls dirs) = "ls: " ++ (unwords . map show $ dirs) -- Parse one command from a list of lines parseCmd : List String -> Maybe (Command, List String) parseCmd [] = Nothing parseCmd (cmd :: lines) = if isPrefixOf "$ cd" cmd then case last' . words $ cmd of Just dir => Just (Cd dir, lines) Nothing => Nothing else if isPrefixOf "$ ls" cmd then let ours = takeWhile (not . isPrefixOf "$") lines theirs = dropWhile (not . isPrefixOf "$") lines in do children <- traverse parseDirEntry ours Just (Ls children, theirs) else Nothing -- Parse all the commands in a list parseCmds : List String -> Maybe (List Command) parseCmds lines = map reverse $ helper [] lines where helper : List Command -> List String -> Maybe (List Command) helper [] [] = Nothing helper cmds [] = Just cmds helper cmds lines = do (command, rest) <- parseCmd lines helper (command :: cmds) (assert_smaller lines rest) data Map : Nat -> Type -> Type -> Type where Nil : Map 0 k v (::) : (k, v) -> Map n k v -> Map (S n) k v %name Map map, map2, map3 get : Eq k => k -> Map n k v -> Maybe v get x [] = Nothing get x ((key, value) :: map) = if key == x then Just value else get x map values : Map n k v -> Vect n v values [] = [] values ((x, y) :: map) = y :: values map mapToList : Map n k v -> List (k, v) mapToList [] = [] mapToList (x :: map) = x :: mapToList map insert : k -> v -> Map n k v -> Map (S n) k v insert key value map = (key, value) :: map replace : Eq k => k -> v -> Map n k v -> Maybe (Map n k v) replace key value [] = Nothing replace key value ((x, y) :: map) = if key == x then Just $ (key, value) :: map else do rest <- replace key value map Just $ (x, y) :: rest insertPair : k -> v -> (n: Nat ** Map n k v) -> (m: Nat ** Map m k v) insertPair key value ((fst ** snd)) = (S fst ** insert key value snd) record Node where constructor MkDir name : String files : (n: Nat ** Map n String (Nat, String)) children : (m : Nat ** Map m String Node) size : Node -> Nat size self@(MkDir nodename (fileCount ** files) (childCount ** children)) = let fileTotal = sum . map fst . values $ files dirTotal = sum . map (\x => size (assert_smaller self x)) . values $ children in fileTotal + dirTotal showDepth : Nat -> Node -> List String showDepth depth self@(MkDir name (fileCount ** files) (childCount ** children)) = let fileLines = toList . map (\(size, name) => leader depth ++ name ++ " (" ++ show size ++ ")" ) . values $ files header = leader depth ++ name ++ ": (" ++ show (size self) ++ ")" childrenLines = foldMap (\x => showDepth (depth + 1) (assert_smaller self x)) . values $ children in header :: (fileLines ++ childrenLines) where leader : Nat -> String leader k = replicate k ' ' Show Node where show = unlines . showDepth 0 emptyNode : Node emptyNode = MkDir "Root" (0 ** Nil) (0 ** Nil) directories : Node -> List Node directories self@(MkDir nodename files (childCount ** children)) = self :: foldMap (\x => directories (assert_smaller self x)) (values children) insertFile : List String -> String -> Nat -> Node -> Maybe Node insertFile [] name size (MkDir nodename files children) = Just $ MkDir nodename (insertPair name (size, name) files) children insertFile (x :: xs) name size (MkDir nodename files (childCount ** children)) = case get x children of Nothing => Nothing (Just y) => do result <- insertFile xs name size y replaced <- replace x result children Just $ MkDir nodename files (childCount ** replaced) insertDir : List String -> String -> Node -> Maybe Node insertDir [] name (MkDir nodename files children) = Just $ MkDir nodename files (insertPair name (MkDir name (0 ** Nil) (0 ** Nil)) children) insertDir (x :: xs) name (MkDir nodename files (childCount ** children)) = case get x children of Nothing => Nothing (Just y) => do result <- insertDir xs name y replaced <- replace x result children Just $ MkDir nodename files (childCount ** replaced) insertEntry : List String -> Node -> DirEntry -> Maybe Node insertEntry path node (File name size) = insertFile path name size node insertEntry path node (Directory name) = insertDir path name node data PathStack = Stk (List String) current : PathStack -> List String current (Stk strs) = reverse strs pop : PathStack -> PathStack pop (Stk []) = Stk [] pop (Stk (x :: xs)) = Stk xs push : String -> PathStack -> PathStack push "/" stack = stack push ".." stack = pop stack push path (Stk strs) = Stk (path :: strs) applyCommands : List Command -> Node -> Maybe Node applyCommands xs x = helper (Stk []) xs x where helper : PathStack -> List Command -> Node -> Maybe Node helper stack [] node = Just node helper stack ((Cd name) :: ys) node = helper (push name stack) ys node helper stack ((Ls entries) :: ys) node = do result <- foldlM (insertEntry (current stack)) node entries helper stack ys result part1 : String -> IO () part1 input = case parseCmds (lines input) of Nothing => putStrLn "Failed to parse commands" (Just commands) => case applyCommands commands emptyNode of Nothing => putStrLn "Failed to apply commands" (Just node) => let wanted = sum . filter (<= 100000) . map size . directories $ node in putStrLn $ "Part 1: " ++ show wanted partial main : IO () main = do file <- readFile "input" case file of (Right contents) => part1 contents (Left err) => printLn err