Data.FilePath.File

(source)

Relative and absolute file paths, which are guaranteed
to consist of a basename plus parent directory.

Reexports

import public Data.FilePath

Definitions

record File : PathType -> Type

  A file path consists of a basename and a parent
  directory, which is either a relative or absolute
  path.

Totality: total
Visibility: public export
Constructor:

MkF : Path t -> Body -> File t

Projections:

.file : File t -> Body
.parent : File t -> Path t

Hints:

Eq (File t)
Eq (File t)
Interpolation (File t)
Interpolation (File t)
Ord (File t)
Ord (File t)
Show (File t)
Show (File t)

.parent : File t -> Path t

Totality: total
Visibility: public export

parent : File t -> Path t

Totality: total
Visibility: public export

.file : File t -> Body

Totality: total
Visibility: public export

file : File t -> Body

Totality: total
Visibility: public export

toPath : File t -> Path t

Totality: total
Visibility: public export

(</>) : Path t -> File Rel -> File t

  Concatenate a path with a relative file path.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 5

(/>) : Path t -> Body -> File t

  Append a file or directory to a path.

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 5

split : File t -> (Path t, Body)

  Split a file path into its parent directory and
  base name.

Totality: total
Visibility: public export

(<.>) : File t -> Body -> File t

  Append a file ending to a path. If the path is empty,
  this appends a hidden file/directory by prepending the
  name with a dot.

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

isAbsolute : File t -> Bool

  Checks whether an unknown path is absolute or not.

Totality: total
Visibility: export

isHidden : File t -> Bool

  True if the file's basename starts with a dot.

Totality: total
Visibility: export

basename : File t -> Body

  Extract the basename from a file path.

Totality: total
Visibility: export

parentDirs : File t -> List (Path t)

  Returns a list of parent directories of the given path.

Totality: total
Visibility: export

splitFileName : File t -> Maybe (File t, Body)

  Try and split a path into the stem and extension
  of the basename.

Totality: total
Visibility: export

stemAndExt : File t -> Maybe (Body, Body)

  Try and split a path into the stem and extension
  of the basename.

Totality: total
Visibility: export

fileStem : File t -> Maybe Body

  Try and extract the file stem from a file path.

Totality: total
Visibility: export

extension : File t -> Maybe Body

  Try and extract the extension from a file.

Totality: total
Visibility: export

normalize : File t -> File t

  Remove references to parent directories (`..`)
  by removing the according number of parent dirs.
  
  In case of absolute paths, excess `..`s will be
  silently dropped.

Totality: total
Visibility: export

parse : String -> Maybe (File Abs)

  A quite strict function for parsing absolute file paths.
  This only accepts valid file bodies, so no doubling
  of path separators or bodies starting with or ending
  on whitespace. Sorry.

Totality: total
Visibility: public export

fromString : (s : String) -> {auto 0 _ : IsJust (parse s)} -> File Abs

Totality: total
Visibility: public export

parse : String -> Maybe (File Rel)

  A quite strict function for parsing relative file paths.
  This only accepts valid file bodies, so no doubling
  of path separators or bodies starting with or ending
  on whitespace. Sorry.

Totality: total
Visibility: public export

fromString : (s : String) -> {auto 0 _ : IsJust (parse s)} -> File Rel

Totality: total
Visibility: public export

record AnyFile : Type

  A path (relative or absolute) in a file system.

Totality: total
Visibility: public export
Constructor:

AF : File pathType -> AnyFile

Projections:

.file : ({rec:0} : AnyFile) -> File (pathType {rec:0})
0 .pathType : AnyFile -> PathType

Hints:

Eq AnyFile
Eq AnyFile
Interpolation AnyFile
Interpolation AnyFile
Ord AnyFile
Ord AnyFile
Show AnyFile
Show AnyFile

0 .pathType : AnyFile -> PathType

Totality: total
Visibility: public export

0 pathType : AnyFile -> PathType

Totality: total
Visibility: public export

.file : ({rec:0} : AnyFile) -> File (pathType {rec:0})

Totality: total
Visibility: public export

file : ({rec:0} : AnyFile) -> File (pathType {rec:0})

Totality: total
Visibility: public export

parse : String -> Maybe AnyFile

  A quite strict function for parsing absolute paths.
  This only accepts valid file bodies, so no doubling
  of path separators or bodies starting with or ending
  on whitespace. Sorry.

Totality: total
Visibility: public export

split : AnyFile -> (FilePath, Body)

  Try and split a path into parent directory and
  file/directory name.

Totality: total
Visibility: public export

(<.>) : AnyFile -> Body -> AnyFile

  Append a file ending to a path. If the path is empty,
  this appends a hidden file/directory by prepending the
  name with a dot.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

isAbsolute : AnyFile -> Bool

  Checks whether an unknown path is absolute or not.

Totality: total
Visibility: export

basename : AnyFile -> Body

  Tries to extract the basename from a path.

Totality: total
Visibility: export

parentDir : AnyFile -> FilePath

  Tries to extract the parent directory from a path.

Totality: total
Visibility: export

splitFileName : AnyFile -> Maybe (AnyFile, Body)

  Try and split a path into base name and file extension.

Totality: total
Visibility: export

stemAndExt : AnyFile -> Maybe (Body, Body)

  Try and split a path into the stem and extension
  of the basename.

Totality: total
Visibility: export

fileStem : AnyFile -> Maybe Body

  Try and extract the file stem from a path.

Totality: total
Visibility: export

extension : AnyFile -> Maybe Body

  Try and extract the extension from a file.

Totality: total
Visibility: export

isHidden : AnyFile -> Bool

  True if the file's basename starts with a dot.

Totality: total
Visibility: export