source
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.

Instances For

source
instance System.instInhabitedFilePath :
Inhabited FilePath
Equations

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

source
def System.instInhabitedFilePath.default :
FilePath
Equations

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

Instances For

source
instance System.instDecidableEqFilePath :
DecidableEq FilePath
Equations

- System.instDecidableEqFilePath = System.instDecidableEqFilePath.decEq

source
def System.instDecidableEqFilePath.decEq (x✝ x✝¹ : FilePath) :
Decidable (x✝ = x✝¹)
Equations

- System.instDecidableEqFilePath.decEq { toString := a } { toString := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

source
def System.instHashableFilePath.hash :
FilePath → UInt64
Equations

- System.instHashableFilePath.hash { toString := a } = mixHash 0 (hash a)

Instances For

source
instance System.instHashableFilePath :
Hashable FilePath
Equations

- System.instHashableFilePath = { hash := System.instHashableFilePath.hash }

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

Instances For

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

Instances For

source
def System.FilePath.extSeparator :
Char

The character that separates file extensions from file names.

Equations

- System.FilePath.extSeparator = '.'

Instances For

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

Instances For

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.

Instances For

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

Instances For

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

Instances For

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 }

Instances For

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.

Instances For

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.

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

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)

Instances For

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

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

Instances For

source
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

Instances For

source
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 }

Instances For

source
instance System.instCoeStringFilePath :
Coe String FilePath
Equations

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

source
@[reducible, inline]
abbrev System.SearchPath :
Type
Equations

- System.SearchPath = List System.FilePath

Instances For

source
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 ':'

Instances For

source
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.splitToList fun (c : Char) => System.SearchPath.separator == c)

Instances For

source
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)

Instances For