Idris2Doc : System.Directory.Tree

System.Directory.Tree

dataFileName : 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.

Totality: total
Constructor: 
MkFileName : String -> FileNameroot
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.

Totality: total
recordTree : Path -> Type
Totality: total
Constructor: 
MkTree : List (FileNameroot) -> List (SubTreeroot) -> Treeroot

Projections:
.files : Treeroot -> List (FileNameroot)
.subTrees : Treeroot -> List (SubTreeroot)
copyDir : HasIOio => Path -> Path -> io (EitherFileError ())
  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 : (FileNameroot -> Lazy (IOa) -> IOa) -> Treeroot -> IOa -> IOa
  Depth first traversal of all of the files in a tree

directoryExists : FileNameroot -> IOBool
Totality: total
emptyTree : Treeroot
  An empty tree contains no files and has no sub-directories.

Totality: total
explore : (root : Path) -> IO (Treeroot)
  Exploring a filesystem from a given root to produce a tree

Totality: total
fileName : FileNameroot -> String
  Project the string out of a `FileName`.

Totality: total
filter : (FileNameroot -> Bool) -> (FileNameroot -> Bool) -> Treeroot -> Treeroot
  Filter out files and directories that do not satisfy a given predicate.

Totality: total
findFile : String -> Treeroot -> IO (MaybePath)
  Finding a file in a tree (depth first search)

print : Treeroot -> 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 : Treeroot -> Treeroot
  Sort the list of files and directories alphabetically

Totality: total
sortBy : (FileNameroot -> FileNameroot -> Ordering) -> (FileNameroot -> FileNameroot -> Ordering) -> Treeroot -> Treeroot
  Sort the lists of files and directories using the given comparison functions

Totality: total
toFilePath : FileNameroot -> Path
  Convert a filename anchored in `root` to a filepath by appending the name
to the root path.

Totality: total