Day 7 Part 2

07/Main.idr

@@ -0,0 +1,239 @@
+import Data.List
+import Data.List1
+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
+
+minBy : Ord b => (a -> b) -> a -> a -> a
+minBy f x y =
+  let i = f x
+      j = f y
+  in if i < j then x else y
+
+part2 : String -> IO ()
+part2 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 totalSpace = 70000000
+              neededSpace = 30000000
+              freeSpace = minus totalSpace (size node)
+              deficit = minus neededSpace freeSpace
+              canidates = filter ((>= deficit) . size) (directories node)
+          in case Data.List1.fromList canidates of
+               Nothing => putStrLn "Only one canidate?"
+               (Just canidates) =>
+                 let smallest = foldl1 (minBy size) canidates
+                 in putStrLn $ "Part 2: " ++ (show (size smallest))
+
+
+partial main : IO ()
+main =
+  do file <- readFile "input"
+     case file of
+       (Right contents) =>
+         do part1 contents
+            part2 contents
+       (Left err) => printLn err