Idris2Doc : System.Directory.Tree

System.Directory.Tree

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

  Totality: total
record Tree : Path -> Type
  Totality: total
  Constructor: 
MkTree : List (FileName root) -> List (SubTree root) -> Tree root

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

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

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

  Totality: total
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
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

  Totality: total
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
toFilePath : FileName root -> Path
  Convert a filename anchored in `root` to a filepath by appending the name
  to the root path.

  Totality: total