Data.FilePath

(source)

A small API for working with file and directory
paths, with the ability to distinguish between relative
and absolute paths at the type level.

Reexports

import public Data.FilePath.Body
import public Data.List1
import public Data.Maybe
import public Data.String

Definitions

record DriveLetter : Type

Totality: total
Visibility: public export
Constructor:

MkDriveLetter : (letter : Char) -> (0 _ : isAlpha letter = True) -> DriveLetter

Projections:

.letter : DriveLetter -> Char
0 .prf : ({rec:0} : DriveLetter) -> isAlpha (letter {rec:0}) = True

Hints:

Eq DriveLetter
Interpolation DriveLetter
Show DriveLetter

.letter : DriveLetter -> Char

Totality: total
Visibility: public export

letter : DriveLetter -> Char

Totality: total
Visibility: public export

0 .prf : ({rec:0} : DriveLetter) -> isAlpha (letter {rec:0}) = True

Totality: total
Visibility: public export

0 prf : ({rec:0} : DriveLetter) -> isAlpha (letter {rec:0}) = True

Totality: total
Visibility: public export

fromChar : (c : Char) -> {auto 0 _ : isAlpha c = True} -> DriveLetter

Totality: total
Visibility: export

parse : Char -> Maybe DriveLetter

Totality: total
Visibility: public export

data AbsType : Type

Totality: total
Visibility: public export
Constructors:

Unix : AbsType
Disk : DriveLetter -> AbsType
UNC : Body -> Body -> AbsType

Hints:

Eq AbsType
Interpolation AbsType
Show AbsType

data PathType : Type

  A path in the file system is either relative
  or absolute.

Totality: total
Visibility: public export
Constructors:

Rel : PathType
Abs : PathType

Hints:

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

data Path : PathType -> Type

  A path in the file system.
  
  Right now, only Unix-style paths are supported.

Totality: total
Visibility: public export
Constructors:

PAbs : AbsType -> SnocList Body -> Path Abs

  An absolute path

PRel : SnocList Body -> Path Rel

  A relative path

Hints:

Eq (Path t)
Interpolation (Path t)
Monoid (Path Rel)
Ord (Path t)
Semigroup (Path Rel)
Show (Path t)

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

  Concatenate two paths, the second of which must be
  relative.

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

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

  Append a file or directory to a path.

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

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

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

Totality: total
Visibility: public export

(<.>) : Path t -> Body -> Path 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

root : Path Abs

  The root of the file system. (unix)

Totality: total
Visibility: public export

disk : DriveLetter -> Path Abs

  The root of the given disk. (windows)

Totality: total
Visibility: public export

network : Body -> Body -> Path Abs

  The root of the given network share. (windows)

Totality: total
Visibility: public export

isAbsolute : Path t -> Bool

  Checks whether an unknown path is absolute or not.

Totality: total
Visibility: export

basename : Path t -> Maybe Body

  Tries to extract the basename from a path.

Totality: total
Visibility: export

parentDir : Path t -> Maybe (Path t)

  Tries to extract the parent directory from a path.

Totality: total
Visibility: export

parentDirs : Path t -> List (Path t)

  Returns a list of parent directories of the given path.

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

fileStem : Path t -> Maybe Body

  Try and extract the file stem from a path.

Totality: total
Visibility: export

extension : Path t -> Maybe Body

  Try and extract the extension from a file.

Totality: total
Visibility: export

normalize : Path t -> Path 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

isHidden : Path b -> Bool

  True if the path's basename starts with a dot

Totality: total
Visibility: export

heq : Path t1 -> Path t2 -> Bool

  Heterogeneous equality for paths

Totality: total
Visibility: export

hcomp : Path t1 -> Path t2 -> Ordering

  Heterogeneous comparison of paths

Totality: total
Visibility: export

record FilePath : Type

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

Totality: total
Visibility: public export
Constructor:

FP : Path pathType -> FilePath

Projections:

.path : ({rec:0} : FilePath) -> Path (pathType {rec:0})
0 .pathType : FilePath -> PathType

Hints:

Eq FilePath
FromString FilePath
Interpolation FilePath
Ord FilePath
Show FilePath

0 .pathType : FilePath -> PathType

Totality: total
Visibility: public export

0 pathType : FilePath -> PathType

Totality: total
Visibility: public export

.path : ({rec:0} : FilePath) -> Path (pathType {rec:0})

Totality: total
Visibility: public export

path : ({rec:0} : FilePath) -> Path (pathType {rec:0})

Totality: total
Visibility: public export

(/>) : FilePath -> Body -> FilePath

  Append a file or directory to a path.

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

(</>) : FilePath -> Path Rel -> FilePath

  Append a relative path do a file path.

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

split : FilePath -> Maybe (FilePath, Body)

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

Totality: total
Visibility: public export

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

  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

root : FilePath

  The root of the file system.

Totality: total
Visibility: public export

isAbsolute : FilePath -> Bool

  Checks whether an unknown path is absolute or not.

Totality: total
Visibility: export

basename : FilePath -> Maybe Body

  Tries to extract the basename from a path.

Totality: total
Visibility: export

parentDir : FilePath -> Maybe FilePath

  Tries to extract the parent directory from a path.

Totality: total
Visibility: export

parentDirs : FilePath -> List FilePath

  Returns a list of parent directories of the given path.

Totality: total
Visibility: export

splitFileName : FilePath -> Maybe (FilePath, Body)

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

Totality: total
Visibility: export

stemAndExt : FilePath -> Maybe (Body, Body)

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

Totality: total
Visibility: export

fileStem : FilePath -> Maybe Body

  Try and extract the file stem from a path.

Totality: total
Visibility: export

extension : FilePath -> Maybe Body

  Try and extract the extension from a file.

Totality: total
Visibility: export

isHidden : FilePath -> Bool

  True if the path's basename starts with a dot

Totality: total
Visibility: export

data IsAbs : FilePath -> Type

  Witness that the given file path is an absolute path

Totality: total
Visibility: public export
Constructor:

ItIsAbs : IsAbs (FP (PAbs at sx))

toAbs : (fp : FilePath) -> {auto 0 _ : IsAbs fp} -> Path Abs

Totality: total
Visibility: public export

data IsRel : FilePath -> Type

  Witness that the given file path is an absolute path

Totality: total
Visibility: public export
Constructor:

ItIsRel : IsRel (FP (PRel sx))

toRel : (fp : FilePath) -> {auto 0 _ : IsRel fp} -> Path Rel

Totality: total
Visibility: public export

parse : String -> Maybe (Path Abs)

  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

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

Totality: total
Visibility: public export

parse : String -> Maybe (Path Rel)

  A quite strict function for parsing relative 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)} -> Path Rel

Totality: total
Visibility: public export

parse : String -> Maybe FilePath

  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