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

Equations

• System.instInhabitedFilePath = { default := { toString := default } }

instance System.instDecidableEqFilePath : DecidableEq FilePath

Equations

• System.instDecidableEqFilePath = System.decEqFilePath✝

instance System.instHashableFilePath : Hashable FilePath

Equations

• System.instHashableFilePath = { hash := System.hashFilePath✝ }

instance System.instReprFilePath : Repr FilePath

Equations

• System.instReprFilePath = { reprPrec := fun (p : System.FilePath) => Repr.addAppParen (Std.Format.text "FilePath.mk " ++ repr p.toString) }

instance System.instToStringFilePath : ToString FilePath

Equations

• System.instToStringFilePath = { toString := fun (p : System.FilePath) => p.toString }

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.

Equations

• System.FilePath.pathSeparator = if System.Platform.isWindows = true then '\\' else '/'

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.

Equations

• System.FilePath.pathSeparators = if System.Platform.isWindows = true then ['\\', '/'] else ['/']

def System.FilePath.extSeparator : Char

The character that separates file extensions from file names.

Equations

• System.FilePath.extSeparator = '.'

def System.FilePath.exeExtension : String

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

Equations

• System.FilePath.exeExtension = if System.Platform.isWindows = true then "exe" else ""

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• p.isAbsolute = (System.FilePath.pathSeparators.contains p.toString.front || System.Platform.isWindows && decide (p.toString.length > 1) && p.toString.iter.next.curr == ':')

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.

Equations

• p.isRelative = !p.isAbsolute

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.

Equations

• p.join sub = if sub.isAbsolute = true then sub else { toString := p.toString ++ System.FilePath.pathSeparator.toString ++ sub.toString }

instance System.FilePath.instDiv : Div FilePath

Equations

• System.FilePath.instDiv = { div := System.FilePath.join }

instance System.FilePath.instHDivString : HDiv FilePath String FilePath

Equations

• System.FilePath.instHDivString = { hDiv := fun (p : System.FilePath) (sub : String) => p.join { toString := sub } }

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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"

Equations

• p.fileStem = Option.map (fun (fname : String) => match fname.revPosOf '.' with | some { } => fname | some pos => fname.extract 0 pos | none => fname) p.fileName

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"

Equations

• p.extension = p.fileName.bind fun (fname : String) => match fname.revPosOf '.' with | some { } => none | some pos => some (fname.extract (pos + '.') fname.endPos) | none => none

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.

Equations

• p.withFileName fname = match p.parent with | none => { toString := fname } | some p => p / fname

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.

Equations

• p.addExtension ext = match p.fileName with | none => p | some fname => p.withFileName (if ext.isEmpty = true then fname else fname ++ "." ++ ext)

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"⟩

Equations

• p.withExtension ext = match p.fileStem with | none => p | some stem => p.withFileName (if ext.isEmpty = true then stem else stem ++ "." ++ ext)

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

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

Equations

• p.components = p.normalize.toString.splitOn System.FilePath.pathSeparator.toString

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.

Equations

• System.mkFilePath parts = { toString := System.FilePath.pathSeparator.toString.intercalate parts }

instance System.instCoeStringFilePath : Coe String FilePath

Equations

• System.instCoeStringFilePath = { coe := System.FilePath.mk }

@[reducible, inline]

abbrev System.SearchPath : Type

Equations

• System.SearchPath = List System.FilePath

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.

Equations

• System.SearchPath.separator = if System.Platform.isWindows = true then ';' else ':'

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

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

Equations

• System.SearchPath.parse s = List.map System.FilePath.mk (s.split fun (c : Char) => System.SearchPath.separator == c)

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.

Equations

• path.toString = System.SearchPath.separator.toString.intercalate (List.map System.FilePath.toString path)