structure System.FilePath : Type

A path on the file system.

Paths consist of a sequence of directories followed by the name of a file or directory. They are delimited by a platform-dependent separator character (see System.FilePath.pathSeparator).

• toString : String

  The string representation of the path.

instance System.instInhabitedFilePath : Inhabited FilePath

instance System.instDecidableEqFilePath : DecidableEq FilePath

instance System.instHashableFilePath : Hashable FilePath

instance System.instReprFilePath : Repr FilePath

instance System.instToStringFilePath : ToString FilePath

def System.FilePath.pathSeparator : Char

The character that separates directories.

On platforms that support multiple separators, System.FilePath.pathSeparator is the “ideal” one expected by users on the platform. System.FilePath.pathSeparators lists all supported separators.

def System.FilePath.pathSeparators : List Char

The list of all path separator characters supported on the current platform.

On platforms that support multiple separators, System.FilePath.pathSeparator is the “ideal” one expected by users on the platform.

def System.FilePath.extSeparator : Char

The character that separates file extensions from file names.

def System.FilePath.exeExtension : String

The file extension expected for executable binaries on the current platform, or "" if there is no such extension.

def System.FilePath.normalize (p : FilePath) : FilePath

Normalizes a path, returning an equivalent path that may better follow platform conventions.

In particular:

• On Windows, drive letters are made uppercase.
• On platforms that support multiple path separators (that is, where System.FilePath.pathSeparators has length greater than one), alternative path separators are replaced with the preferred path separator.

There is no guarantee that two equivalent paths normalize to the same path.

def System.FilePath.isAbsolute (p : FilePath) : Bool

An absolute path starts at the root directory or a drive letter. Accessing files through an absolute path does not depend on the current working directory.

def System.FilePath.isRelative (p : FilePath) : Bool

A relative path is one that depends on the current working directory for interpretation. Relative paths do not start with the root directory or a drive letter.

def System.FilePath.join (p sub : FilePath) : FilePath

Appends two paths, taking absolute paths into account. This operation is also accessible via the / operator.

If sub is an absolute path, then p is discarded and sub is returned. If sub is a relative path, then it is attached to p with the platform-specific path separator.

instance System.FilePath.instDiv : Div FilePath

instance System.FilePath.instHDivString : HDiv FilePath String FilePath

def System.FilePath.parent (p : FilePath) : Option FilePath

Returns the parent directory of a path, if there is one.

If the path is that of the root directory or the root of a drive letter, none is returned. Otherwise, the path's parent directory is returned.

def System.FilePath.fileName (p : FilePath) : Option String

Extracts the last element of a path if it is a file or directory name.

Returns none if the last entry is a special name (such as . or ..) or if the path is the root directory.

def System.FilePath.fileStem (p : FilePath) : Option String

Extracts the stem (non-extension) part of p.fileName.

If the filename contains multiple extensions, then only the last one is removed. Returns none if there is no file name at the end of the path.

Examples:

• ("app.exe" : System.FilePath).fileStem = some "app"
• ("file.tar.gz" : System.FilePath).fileStem = some "file.tar"
• ("files/" : System.FilePath).fileStem = none
• ("files/picture.jpg" : System.FilePath).fileStem = some "picture"

def System.FilePath.extension (p : FilePath) : Option String

Extracts the extension part of p.fileName.

If the filename contains multiple extensions, then only the last one is extracted. Returns none if there is no file name at the end of the path.

Examples:

• ("app.exe" : System.FilePath).extension = some "exe"
• ("file.tar.gz" : System.FilePath).extension = some "gz"
• ("files/" : System.FilePath).extension = none
• ("files/picture.jpg" : System.FilePath).extension = some "jpg"

def System.FilePath.withFileName (p : FilePath) (fname : String) : FilePath

Replaces the file name at the end of the path p with fname, placing fname in the parent directory of p.

If p has no parent directory, then fname is returned unmodified.

def System.FilePath.addExtension (p : FilePath) (ext : String) : FilePath

Appends the extension ext to a path p.

ext should not have leading ., as this function adds one. If ext is the empty string, no . is added.

Unlike System.FilePath.withExtension, this does not remove any existing extension.

def System.FilePath.withExtension (p : FilePath) (ext : String) : FilePath

Replaces the current extension in a path p with ext, adding it if there is no extension. If the path has multiple file extensions, only the last one is replaced. If the path has no filename, or if ext is the empty string, then the filename is returned unmodified.

ext should not have a leading ., as this function adds one.

Examples:

• ("files/picture.jpeg" : System.FilePath).withExtension "jpg" = ⟨"files/picture.jpg"⟩
• ("files/" : System.FilePath).withExtension "zip" = ⟨"files/"⟩
• ("files" : System.FilePath).withExtension "zip" = ⟨"files.zip"⟩
• ("files/archive.tar.gz" : System.FilePath).withExtension "xz" = ⟨"files.tar.xz"⟩

def System.FilePath.components (p : FilePath) : List String

Splits a path into a list of individual file names at the platform-specific path separator.

def System.mkFilePath (parts : List String) : FilePath

Constructs a path from a list of file names by interspersing them with the current platform's path separator.

instance System.instCoeStringFilePath : Coe String FilePath

@[reducible, inline]

abbrev System.SearchPath : Type

def System.SearchPath.separator : Char

The character that is used to separate the entries in the $PATH (or %PATH%) environment variable.

This value is platform dependent.

def System.SearchPath.parse (s : String) : SearchPath

Separates the entries in the $PATH (or %PATH%) environment variable by the current platform-dependent separator character.

def System.SearchPath.toString (path : SearchPath) : String

Joins a list of paths into a suitable value for the current platform's $PATH (or %PATH%) environment variable.