0 | module System.Directory.Tree
  1 |
  2 | import Control.Monad.Either
  3 | import Data.DPair
  4 | import Data.List
  5 | import Data.Nat
  6 | import System.Directory
  7 | import System.File
  8 | import System.Path
  9 |
 10 | %default total
 11 |
 12 | ------------------------------------------------------------------------------
 13 | -- Filenames
 14 |
 15 | ||| A `Filename root` is anchored in `root`.
 16 | ||| We use a `data` type so that Idris can easily infer `root` when passing
 17 | ||| a `FileName` around. We do not use a `record` because we do not want to
 18 | ||| allow users to manufacture their own `FileName`.
 19 | ||| To get an absolute path, we need to append said filename to the root.
 20 | export
 21 | data FileName : Path -> Type where
 22 |   MkFileName : String -> FileName root
 23 |
 24 | ||| Project the string out of a `FileName`.
 25 | export
 26 | fileName : FileName root -> String
 27 | fileName (MkFileName str) = str
 28 |
 29 | namespace FileName
 30 |   export
 31 |   toRelative : FileName root -> FileName (parse "")
 32 |   toRelative (MkFileName x) = MkFileName x
 33 |
 34 | ||| Convert a filename anchored in `root` to a filepath by appending the name
 35 | ||| to the root path.
 36 | export
 37 | toFilePath : {root : Path} -> FileName root -> Path
 38 | toFilePath file = root /> fileName file
 39 |
 40 | export
 41 | directoryExists : {root : Path} -> FileName root -> IO Bool
 42 | directoryExists fp = do
 43 |   Right dir <- openDir (show $ toFilePath fp)
 44 |     | Left _ => pure False
 45 |   closeDir dir
 46 |   pure True
 47 |
 48 | ------------------------------------------------------------------------------
 49 | -- Directory trees
 50 |
 51 | ||| A `Tree root` is the representation of a directory tree anchored in `root`.
 52 | ||| Each directory contains a list of files and a list of subtrees waiting to be
 53 | ||| explored. The fact these subtrees are IO-bound means the subtrees will be
 54 | ||| lazily constructed on demand.
 55 | public export
 56 | SubTree : Path -> Type
 57 |
 58 | public export
 59 | record Tree (root : Path) where
 60 |   constructor MkTree
 61 |   files    : List (FileName root)
 62 |   subTrees : List (SubTree root)
 63 |
 64 | SubTree root = (dir : FileName root ** IO (Tree (root /> fileName dir)))
 65 |
 66 | ||| An empty tree contains no files and has no sub-directories.
 67 | export
 68 | emptyTree : Tree root
 69 | emptyTree = MkTree [] []
 70 |
 71 | namespace Tree
 72 |   ||| No run time information is changed,
 73 |   ||| so we assert the identity.
 74 |   export
 75 |   toRelative : Tree root -> Tree (parse "")
 76 |   toRelative x = believe_me x
 77 |
 78 | ||| Filter out files and directories that do not satisfy a given predicate.
 79 | export
 80 | filter : (filePred, dirPred : {root : _} -> FileName root -> Bool) ->
 81 |          {root : _} -> Tree root -> Tree root
 82 | filter filePred dirPred (MkTree files dirs) = MkTree files' dirs' where
 83 |
 84 |   files' : List (FileName root)
 85 |   files' = filter filePred files
 86 |
 87 |   dirs' : List (SubTree root)
 88 |   dirs' = flip List.mapMaybe dirs $ \ (dname ** iot) => do
 89 |             guard (dirPred dname)
 90 |             pure (dname ** map (assert_total (filter filePred dirPred)) iot)
 91 |
 92 | ||| Sort the lists of files and directories using the given comparison functions
 93 | export
 94 | sortBy : (fileCmp, dirCmp : {root : _} -> FileName root -> FileName root -> Ordering) ->
 95 |          {root : _} -> Tree root -> Tree root
 96 | sortBy fileCmp dirCmp (MkTree files dirs) = MkTree files' dirs' where
 97 |
 98 |   files' : List (FileName root)
 99 |   files' = sortBy fileCmp files
100 |
101 |   dirs' : List (SubTree root)
102 |   dirs' = sortBy (\ d1, d2 => dirCmp (fst d1) (fst d2))
103 |         $ flip map dirs $ \ (dname ** iot) =>
104 |           (dname ** map (assert_total (sortBy fileCmp dirCmp)) iot)
105 |
106 | ||| Sort the list of files and directories alphabetically
107 | export
108 | sort : {root : _} -> Tree root -> Tree root
109 | sort = sortBy cmp cmp where
110 |
111 |   cmp : {root : _} -> FileName root -> FileName root -> Ordering
112 |   cmp a b = compare (fileName a) (fileName b)
113 |
114 |
115 | ||| Exploring a filesystem from a given root to produce a tree
116 | export
117 | explore : (root : Path) -> IO (Tree root)
118 |
119 | go : {root : Path} -> Directory -> Tree root -> IO (Tree root)
120 |
121 | explore root = do
122 |   Right dir <- openDir (show root)
123 |     | Left err => pure emptyTree
124 |   assert_total (go dir emptyTree)
125 |
126 | go dir acc = case !(nextDirEntry dir) of
127 |   -- If there is no next entry then we are done and can return the accumulator.
128 |   Left err      => acc <$ closeDir dir
129 |   Right Nothing => acc <$ closeDir dir
130 |   -- Otherwise we have an entry and need to categorise it
131 |   Right (Just entry) => do
132 |     -- ignore aliases for current and parent directories
133 |     let False = elem entry [".", ".."]
134 |          | _ => assert_total (go dir acc)
135 |     -- if the entry is a directory, add it to the (lazily explored)
136 |     -- list of subdirectories
137 |     let entry : FileName root = MkFileName entry
138 |     let acc = if !(directoryExists entry)
139 |                 then { subTrees $= ((entry ** explore _) ::) } acc
140 |                 else { files    $= (entry                ::) } acc
141 |     assert_total (go dir acc)
142 |
143 | ||| Depth first traversal of all of the files in a tree
144 | export
145 | covering
146 | depthFirst : ({root : Path} -> FileName root -> Lazy (IO a) -> IO a) ->
147 |              {root : Path} -> Tree root -> IO a -> IO a
148 | depthFirst check t k =
149 |   let next = foldr (\ (dir ** iot), def => depthFirst check !iot def) k t.subTrees in
150 |   foldr (\ fn, def => check fn def) next t.files
151 |
152 | ||| Finding a file in a tree (depth first search)
153 | export
154 | covering
155 | findFile : {root : Path} -> String -> Tree root -> IO (Maybe Path)
156 | findFile needle t = depthFirst check t (pure Nothing) where
157 |
158 |   check : {root : Path} -> FileName root ->
159 |           Lazy (IO (Maybe Path)) -> IO (Maybe Path)
160 |   check fn next = if fileName fn == needle
161 |                     then pure (Just (toFilePath fn))
162 |                     else next
163 |
164 | ||| Display a tree by printing it procedurally. Note that because directory
165 | ||| trees contain suspended computations corresponding to their subtrees this
166 | ||| has to be an `IO` function. We make it return Unit rather than a String
167 | ||| because we do not want to assume that the tree is finite.
168 | export
169 | covering
170 | print : Tree root -> IO ()
171 | print t = go [([], ".", Evidence root (pure t))] where
172 |
173 |   -- This implementation is unadulterated black magic.
174 |   -- Do NOT touch it if nothing is broken.
175 |
176 |   padding : Bool -> List Bool -> String
177 |   padding isDir = fastConcat . go [] where
178 |
179 |     go : List String -> List Bool -> List String
180 |     go acc [] = acc
181 |     go acc (b :: bs) = go (hd :: acc) bs where
182 |       hd : String
183 |       hd = if isDir && isNil acc
184 |            then if b then " ├ " else " └ "
185 |            else if b then " │"  else "  "
186 |
187 |   prefixes : Nat -> List Bool
188 |   prefixes n = snoc (replicate (pred n) True) False
189 |
190 |   covering
191 |   go : List (List Bool, String, Exists (IO . Tree)) -> IO ()
192 |   go [] = pure ()
193 |   go ((bs, fn, Evidence _ iot) :: iots) = do
194 |     t <- iot
195 |     putStrLn (padding True bs ++ fn)
196 |     let pad = padding False bs
197 |     let pads = prefixes (length t.files + length t.subTrees)
198 |     for_ (zip pads t.files) $ \ (b, fp) =>
199 |       putStrLn (pad ++ (if b then " ├ " else " └ ") ++ fileName fp)
200 |     let bss = map (:: bs) (prefixes (length t.subTrees))
201 |     go (zipWith (\ bs, (dir ** iot) => (bs, fileName dir, Evidence _ iot)) bss t.subTrees)
202 |     go iots
203 |
204 | ||| Copy a directory and its contents recursively
205 | ||| Returns a FileError if the target directory already exists, or if any of
206 | ||| the source files fail to be copied.
207 | export
208 | covering
209 | copyDir : HasIO io => (src : Path) -> (target : Path) -> io (Either FileError ())
210 | copyDir src target = runEitherT $ do
211 |     MkEitherT $ createDir $ show target
212 |     copyDirContents !(liftIO $ explore src) target
213 |   where
214 |     copyFile' : (srcDir : Path) -> (targetDir : Path) -> (fileName : String) -> EitherT FileError io ()
215 |     copyFile' srcDir targetDir fileName = MkEitherT $ do
216 |       Right ok <- copyFile (show $ srcDir /> fileName) (show $ targetDir /> fileName)
217 |       | Left (err, size) => pure (Left err)
218 |       pure (Right ok)
219 |
220 |     covering
221 |     copyDirContents : {srcDir : Path} -> Tree srcDir -> (targetDir : Path) -> EitherT FileError io ()
222 |     copyDirContents (MkTree files subTrees) targetDir = do
223 |       traverse_ (copyFile' srcDir targetDir) (map fileName files)
224 |       traverse_ (\(subDir ** subDirTree) => do
225 |           let targetSubDir = targetDir /> fileName subDir
226 |           MkEitherT $ createDir $ show $ targetSubDir
227 |           copyDirContents !(liftIO subDirTree) targetSubDir
228 |         ) subTrees
229 |