Init.System.FilePath

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.

Instances For

source

instance System.instInhabitedFilePath :

Inhabited FilePath

Equations

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

source

instance System.instDecidableEqFilePath :

DecidableEq FilePath

Equations

System.instDecidableEqFilePath = System.decEqFilePath✝

source

instance System.instHashableFilePath :

Hashable FilePath

Equations

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

source

instance System.instReprFilePath :

Repr FilePath

Equations

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

source

instance System.instToStringFilePath :

ToString FilePath

Equations

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

source

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 '/'

source

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 ['/']

source

def System.FilePath.extSeparator :

Char

The character that separates file extensions from file names.

Equations

System.FilePath.extSeparator = '.'

source

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

source

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.

source

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 == ':')

source

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

source

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 }

source

instance System.FilePath.instDiv :

Div FilePath

Equations

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

source

instance System.FilePath.instHDivString :

HDiv FilePath String FilePath

Equations

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

source

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.

source

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.

source

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

source

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

source

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

source

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)

source

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