doc-next-gen

Init.System.FilePath

Module docstring

{}

System.FilePath structure
Full source 
/--
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`).
-/
structure FilePath where
  /-- The string representation of the path. -/
  toString : String
  deriving Inhabited, DecidableEq, Hashable
File Path
Informal description
A structure representing a file path in a file system. File paths consist of a sequence of directories followed by a file or directory name, with components separated by platform-specific separator characters.
System.instInhabitedFilePath instance
: Inhabited✝ (@System.FilePath)
Full source 
Inhabited, DecidableEq, Hashable
File Path Type is Inhabited
Informal description
The type `System.FilePath` is inhabited, meaning there exists at least one file path.
System.instDecidableEqFilePath instance
: DecidableEq✝ (@System.FilePath✝)
Full source 
DecidableEq, Hashable
Decidable Equality for File Paths
Informal description
For any two file paths, there exists a decidable equality relation between them.
System.instHashableFilePath instance
: Hashable✝ (@System.FilePath✝)
Full source 
Hashable
Hashable File Path Structure
Informal description
The type `System.FilePath` has a hashable structure, meaning it can be used with hash-based data structures and algorithms.
System.instReprFilePath instance
: Repr FilePath
Full source 
instance : Repr FilePath where
  reprPrec p := Repr.addAppParen ("FilePath.mk " ++ repr p.toString)
Representation Instance for File Paths
Informal description
The type `System.FilePath` has a representation instance, allowing file paths to be displayed in a human-readable format.
System.instToStringFilePath instance
: ToString FilePath
Full source 
instance : ToString FilePath where
  toString p := p.toString
String Representation for File Paths
Informal description
The type `System.FilePath` has a string representation, allowing file paths to be converted to strings.
System.FilePath.pathSeparator definition
: Char
Full source 
/--
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 pathSeparator : Char :=
  if isWindows then '\\' else '/'
Directory separator character
Informal description
The character used to separate directories in file paths. On Windows systems, it is the backslash `\`, while on other systems it is the forward slash `/`.
System.FilePath.pathSeparators definition
: List Char
Full source 
/--
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 pathSeparators : List Char :=
  if isWindows then ['\\', '/'] else ['/']
Path separator characters
Informal description
The list of all path separator characters supported on the current platform. On Windows, it includes both backslash `\` and forward slash `/`, while on other platforms it contains only forward slash `/`.
System.FilePath.extSeparator definition
: Char
Full source 
/--
The character that separates file extensions from file names.
-/
def extSeparator : Char := '.'
File extension separator character
Informal description
The character `'.'` (period) is used to separate file extensions from file names.
System.FilePath.exeExtension definition
: String
Full source 
/--
The file extension expected for executable binaries on the current platform, or `""` if there is no
such extension.
-/
def exeExtension : String :=
  if isWindows then "exe" else ""
Executable file extension
Informal description
The string representing the file extension for executable binaries on the current platform (e.g., `"exe"` on Windows), or an empty string if no such extension exists.
System.FilePath.normalize definition
(p : FilePath) : FilePath
Full source 
/--
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.
-/
-- TODO: normalize `a/`, `a//b`, etc.
def normalize (p : FilePath) : FilePath := Id.run do
  let mut p := p
  -- normalize drive letter
  if isWindows && p.toString.length >= 2 && (p.toString.get 0).isLower && p.toString.get ⟨1⟩ == ':' then
    p := ⟨p.toString.set 0 (p.toString.get 0).toUpper⟩
  -- normalize separator
  unless pathSeparators.length == 1 do
    p := ⟨p.toString.map fun c => if pathSeparators.contains c then pathSeparator else c⟩
  return p
Path normalization function
Informal description
The function takes a file path `p` and returns an equivalent path that follows platform-specific conventions. On Windows, it converts drive letters to uppercase. On platforms with multiple path separators, it replaces alternative separators with the preferred one. Note that equivalent paths may not normalize to identical results.
System.FilePath.isAbsolute definition
(p : FilePath) : Bool
Full source 
/--
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 isAbsolute (p : FilePath) : Bool :=
  pathSeparatorspathSeparators.contains p.toString.front || (isWindows && p.toString.length > 1 && p.toString.iter.next.curr == ':')
Absolute path check
Informal description
A function that determines whether a given file path `p` is absolute. A path is considered absolute if it starts with a path separator character (like `/` or `\`) or, on Windows systems, if it begins with a drive letter followed by a colon (e.g., `C:`).
System.FilePath.isRelative definition
(p : FilePath) : Bool
Full source 
/--
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 isRelative (p : FilePath) : Bool :=
  !p.isAbsolute
Relative path check
Informal description
A function that determines whether a given file path `p` is relative. A path is considered relative if it does not start with a path separator character (like `/` or `\`) and, on Windows systems, does not begin with a drive letter followed by a colon (e.g., `C:`). In other words, a relative path is one that depends on the current working directory for interpretation.
System.FilePath.join definition
(p sub : FilePath) : FilePath
Full source 
/--
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.
-/
def join (p sub : FilePath) : FilePath :=
  if sub.isAbsolute then
    sub
  else
    ⟨p.toString ++ pathSeparator.toString ++ sub.toString⟩
File path concatenation
Informal description
The function combines two file paths `p` and `sub` into a single path. If `sub` is an absolute path, it is returned directly. Otherwise, `sub` is appended to `p` with the platform-specific path separator character in between.
System.FilePath.instDiv instance
: Div FilePath
Full source 
instance : Div FilePath where
  div := FilePath.join
Division Operation for File Paths
Informal description
The file path structure supports division-like operations, where two file paths can be combined to form a new file path.
System.FilePath.instHDivString instance
: HDiv FilePath String FilePath
Full source 
instance : HDiv FilePath String FilePath where
  hDiv p sub := FilePath.join p ⟨sub⟩
File Path Division with Strings
Informal description
The file path structure supports division-like operations with strings, where a file path can be combined with a string to form a new file path.
System.FilePath.parent definition
(p : FilePath) : Option FilePath
Full source 
/--
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 parent (p : FilePath) : Option FilePath :=
  let extractParentPath := FilePath.mkFilePath.mk <$> p.toString.extract {} <$> posOfLastSep p
  if p.isAbsolute then
    let lengthOfRootDirectory := if pathSeparators.contains p.toString.front then 1 else 3
    if p.toString.length == lengthOfRootDirectory then
      -- `p` is a root directory
      none
    else if posOfLastSep p == String.Pos.mk (lengthOfRootDirectory - 1) then
      -- `p` is a direct child of the root
      some ⟨p.toString.extract 0 ⟨lengthOfRootDirectory⟩⟩
    else
      -- `p` is an absolute path with at least two subdirectories
      extractParentPath
  else
    -- `p` is a relative path
    extractParentPath
Parent directory of a file path
Informal description
The function takes a file path `p` and returns its parent directory as a `FilePath` if it exists. If `p` is the root directory or the root of a drive letter, it returns `none`. Otherwise, it returns the path of the parent directory by removing the last component of the path.
System.FilePath.fileName definition
(p : FilePath) : Option String
Full source 
/--
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 fileName (p : FilePath) : Option String :=
  let lastPart := match posOfLastSep p with
    | somesome sepPos => p.toString.extract (sepPos + '/') p.toString.endPos
    | none        => p.toString
  if lastPart.isEmpty || lastPart == "." || lastPart == ".." then none else some lastPart
File name extraction from path
Informal description
The function takes a file path `p` and returns the last component of the path as a string if it is a valid file or directory name. Returns `none` if the last component is a special name (like `.` or `..`) or if the path is the root directory.
System.FilePath.fileStem definition
(p : FilePath) : Option String
Full source 
/--
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 fileStem (p : FilePath) : Option String :=
  p.fileName.map fun fname =>
    match fname.revPosOf '.' with
    | somesome ⟨0⟩ => fname
    | somesome pos => fname.extract 0 pos
    | none     => fname
File stem extraction from path
Informal description
The function takes a file path `p` and returns the stem (name without the last extension) of the filename component as a string, if it exists. If the filename contains multiple extensions, only the last one is removed. Returns `none` if there is no valid filename component. More precisely: - For a filename like `"app.exe"`, returns `some "app"` - For a filename like `"file.tar.gz"`, returns `some "file.tar"` - For a directory path like `"files/"`, returns `none` - For a filename like `"files/picture.jpg"`, returns `some "picture"`
System.FilePath.extension definition
(p : FilePath) : Option String
Full source 
/--
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 extension (p : FilePath) : Option String :=
  p.fileName.bind fun fname =>
    match fname.revPosOf '.' with
    | somesome 0   => none
    | somesome pos => fname.extract (pos + '.') fname.endPos
    | none     => none
File extension extraction
Informal description
The function takes a file path `p` and returns the file extension of the last component of the path as a string, if it exists. If the filename contains multiple extensions, only the last one is returned. Returns `none` if there is no extension or if the last component is not a valid filename. More precisely: - For a filename like `"app.exe"`, returns `some "exe"` - For a filename like `"file.tar.gz"`, returns `some "gz"` - For a directory path like `"files/"`, returns `none` - For a filename like `"files/picture.jpg"`, returns `some "jpg"`
System.FilePath.withFileName definition
(p : FilePath) (fname : String) : FilePath
Full source 
/--
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 withFileName (p : FilePath) (fname : String) : FilePath :=
  match p.parent with
  | none => ⟨fname⟩
  | somesome p => p / fname
Replace filename in path
Informal description
Given a file path `p` and a filename `fname`, the function constructs a new file path by replacing the filename component of `p` with `fname`. If `p` has no parent directory (i.e., it is a root path), the result is simply `fname`. Otherwise, the result is the parent directory of `p` combined with `fname`. More precisely: - For a path like `"dir/file.txt"` and `fname = "new.txt"`, returns `"dir/new.txt"` - For a path like `"file.txt"` (no parent), returns `"new.txt"`
System.FilePath.addExtension definition
(p : FilePath) (ext : String) : FilePath
Full source 
/--
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 addExtension (p : FilePath) (ext : String) : FilePath :=
  match p.fileName with
  | none => p
  | somesome fname => p.withFileName (if ext.isEmpty then fname else fname ++ "." ++ ext)
Append extension to file path
Informal description
Given a file path `p` and an extension string `ext`, this function appends the extension to the filename component of `p`. The extension should not include a leading dot. If `ext` is empty, the filename remains unchanged. Unlike `withExtension`, this function preserves any existing extensions in the filename. More precisely: - For a path like `"dir/file"` and `ext = "txt"`, returns `"dir/file.txt"` - For a path like `"dir/file.txt"` and `ext = "bak"`, returns `"dir/file.txt.bak"` - For a path like `"dir/file"` and `ext = ""`, returns `"dir/file"`
System.FilePath.withExtension definition
(p : FilePath) (ext : String) : FilePath
Full source 
/--
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 withExtension (p : FilePath) (ext : String) : FilePath :=
  match p.fileStem with
  | none => p
  | somesome stem => p.withFileName (if ext.isEmpty then stem else stem ++ "." ++ ext)
File path with replaced extension
Informal description
Given a file path `p` and a file extension `ext`, this function constructs a new file path by replacing the last extension of `p` with `ext`. If `p` has no filename component or if `ext` is empty, the path is returned unchanged. The extension `ext` should not include a leading dot. More precisely: - For a path like `"files/picture.jpeg"` and `ext = "jpg"`, returns `"files/picture.jpg"` - For a path like `"files/"` (no filename), returns `"files/"` - For a path like `"files"` (no extension), returns `"files.jpg"` if `ext = "jpg"` - For a path like `"files/archive.tar.gz"` and `ext = "xz"`, returns `"files/archive.tar.xz"`
System.FilePath.components definition
(p : FilePath) : List String
Full source 
/--
Splits a path into a list of individual file names at the platform-specific path separator.
-/
def components (p : FilePath) : List String :=
  p.normalize |>.toString.splitOn pathSeparator.toString
File path components as list
Informal description
Given a file path `p`, this function returns a list of strings representing the individual file or directory names in the path, split at the platform-specific path separator character. The path is first normalized according to platform conventions before splitting.
System.mkFilePath definition
(parts : List String) : FilePath
Full source 
/--
Constructs a path from a list of file names by interspersing them with the current platform's path
separator.
-/
def mkFilePath (parts : List String) : FilePath :=
  ⟨String.intercalate FilePath.pathSeparator.toString parts⟩
File path construction from components
Informal description
Given a list of strings representing file or directory names, this function constructs a file path by joining them with the platform's path separator character.
System.instCoeStringFilePath instance
: Coe String FilePath
Full source 
instance : Coe String FilePath where
  coe := FilePath.mk
String to File Path Coercion
Informal description
There is a canonical way to interpret a string as a file path.
System.SearchPath abbrev
Full source 
abbrev SearchPath := List FilePath
File Search Path Structure
Informal description
A search path is a list of file paths used to locate files or directories, typically represented as a string with entries separated by platform-specific separator characters (semicolon `;` on Windows and colon `:` on other systems).
System.SearchPath.separator definition
: Char
Full source 
/--
The character that is used to separate the entries in the `$PATH` (or `%PATH%`) environment variable.

This value is platform dependent.
-/
protected def separator : Char :=
  if isWindows then ';' else ':'
Path separator character
Informal description
The character used to separate entries in the `PATH` (or `%PATH%`) environment variable, which is platform-dependent: semicolon `;` on Windows and colon `:` on other systems.
System.SearchPath.parse definition
(s : String) : SearchPath
Full source 
/--
Separates the entries in the `$PATH` (or `%PATH%`) environment variable by the current
platform-dependent separator character.
-/
def parse (s : String) : SearchPath :=
  s.split (fun c => SearchPath.separator == c) |>.map FilePath.mk
Parsing of PATH environment variable into file paths
Informal description
The function takes a string `s` representing the `PATH` (or `%PATH%`) environment variable and splits it into a list of file paths, using the platform-specific separator character (semicolon `;` on Windows and colon `:` on other systems). Each resulting string is then converted into a `FilePath` structure.
System.SearchPath.toString definition
(path : SearchPath) : String
Full source 
/--
Joins a list of paths into a suitable value for the current platform's `$PATH` (or `%PATH%`)
environment variable.
-/
def toString (path : SearchPath) : String :=
  SearchPath.separator.toString.intercalate (path.map FilePath.toString)
Search path to string conversion
Informal description
The function converts a search path (a list of file paths) into a string representation suitable for the current platform's `PATH` environment variable, with entries separated by the platform-specific separator character (semicolon `;` on Windows and colon `:` on other systems).