- data FileName : Path -> Type
A `Filename root` is anchored in `root`.
We use a `data` type so that Idris can easily infer `root` when passing
a `FileName` around. We do not use a `record` because we do not want to
allow users to manufacture their own `FileName`.
To get an absolute path, we need to append said filename to the root.
- MkFileName : String -> FileName root
- SubTree : Path -> Type
A `Tree root` is the representation of a directory tree anchored in `root`.
Each directory contains a list of files and a list of subtrees waiting to be
explored. The fact these subtrees are IO-bound means the subtrees will be
lazily constructed on demand.
- record Tree : Path -> Type
- Totality: total
- MkTree : List (FileName root) -> List (SubTree root) -> Tree root
- .files : Tree root -> List (FileName root)
- .subTrees : Tree root -> List (SubTree root)
- copyDir : HasIO io => Path -> Path -> io (Either FileError ())
Copy a directory and its contents recursively
Returns a FileError if the target directory already exists, or if any of
the source files fail to be copied.
- depthFirst : (FileName root -> Lazy (IO a) -> IO a) -> Tree root -> IO a -> IO a
Depth first traversal of all of the files in a tree
- directoryExists : FileName root -> IO Bool
- Totality: total
- emptyTree : Tree root
An empty tree contains no files and has no sub-directories.
- explore : (root : Path) -> IO (Tree root)
Exploring a filesystem from a given root to produce a tree
- fileName : FileName root -> String
Project the string out of a `FileName`.
- filter : (FileName root -> Bool) -> (FileName root -> Bool) -> Tree root -> Tree root
Filter out files and directories that do not satisfy a given predicate.
- findFile : String -> Tree root -> IO (Maybe Path)
Finding a file in a tree (depth first search)
- print : Tree root -> IO ()
Display a tree by printing it procedurally. Note that because directory
trees contain suspended computations corresponding to their subtrees this
has to be an `IO` function. We make it return Unit rather than a String
because we do not want to assume that the tree is finite.
- sort : Tree root -> Tree root
Sort the list of files and directories alphabetically
- sortBy : (FileName root -> FileName root -> Ordering) -> (FileName root -> FileName root -> Ordering) -> Tree root -> Tree root
Sort the lists of files and directories using the given comparison functions
- toFilePath : FileName root -> Path
Convert a filename anchored in `root` to a filepath by appending the name
to the root path.