System.Directory.Tree

Definitions

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.

Totality: total
Visibility: export
Constructor: 

MkFileName : String -> FileName root

fileName : FileName root -> String

  Project the string out of a `FileName`.

Totality: total
Visibility: export

toRelative : FileName root -> FileName (parse "")

Totality: total
Visibility: export

toFilePath : FileName root -> Path

  Convert a filename anchored in `root` to a filepath by appending the name
  to the root path.

Totality: total
Visibility: export

directoryExists : FileName root -> IO Bool

Totality: total
Visibility: export

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
Visibility: public export

record Tree : Path -> Type

Totality: total
Visibility: public export
Constructor: 

MkTree : List (FileName root) -> List (SubTree root) -> Tree root

Projections:

.files : Tree root -> List (FileName root)

.subTrees : Tree root -> List (SubTree root)

.files : Tree root -> List (FileName root)

Totality: total
Visibility: public export

files : Tree root -> List (FileName root)

Totality: total
Visibility: public export

.subTrees : Tree root -> List (SubTree root)

Totality: total
Visibility: public export

subTrees : Tree root -> List (SubTree root)

Totality: total
Visibility: public export

emptyTree : Tree root

  An empty tree contains no files and has no sub-directories.

Totality: total
Visibility: export

toRelative : Tree root -> Tree (parse "")

  No run time information is changed,
  so we assert the identity.

Totality: total
Visibility: export

filter : (FileName root -> Bool) -> (FileName root -> Bool) -> Tree root -> Tree root

  Filter out files and directories that do not satisfy a given predicate.

Totality: total
Visibility: export

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

Totality: total
Visibility: export

sort : Tree root -> Tree root

  Sort the list of files and directories alphabetically

Totality: total
Visibility: export

explore : (root : Path) -> IO (Tree root)

  Exploring a filesystem from a given root to produce a tree

Totality: total
Visibility: export

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

Visibility: export

findFile : String -> Tree root -> IO (Maybe Path)

  Finding a file in a tree (depth first search)

Visibility: export

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.

Visibility: export

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.

Visibility: export