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