Init.System.FilePath

source

structure System.FilePath :

Type

toString : String

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. In the case where more than one character is possible, pathSeparator is the 'ideal' one.

Equations

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

source

def System.FilePath.pathSeparators :

List Char

The list of all possible separators.

Equations

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

source

def System.FilePath.extSeparator :

Char

File extension character

Equations

System.FilePath.extSeparator = '.'

source

def System.FilePath.exeExtension :

String

Equations

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

source

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

FilePath

Equations

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

source

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

Bool

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

Equations

p.isRelative = !p.isAbsolute

source

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

FilePath

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

Equations

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

source

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

Option String

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.

Equations

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

source

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

Option String

Equations

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

source

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

FilePath

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 contain a 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

Replace the current extension in a path p with ext.

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

Equations

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

source

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

List String

Equations

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

source

def System.mkFilePath (parts : List String) :

FilePath

Equations

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

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

source

def System.SearchPath.separator :

Char

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

Equations

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

source

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

SearchPath

Equations

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

source

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

String

Equations

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