Init.System.FilePath

source

structure System.FilePath:

Type

toString : String

source

instance System.instInhabitedFilePath:

Inhabited System.FilePath

Equations

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

source

instance System.instDecidableEqFilePath:

DecidableEq System.FilePath

Equations

System.instDecidableEqFilePath = [anonymous]

source

instance System.instHashableFilePath:

Hashable System.FilePath

Equations

System.instHashableFilePath = { hash := [anonymous] }

source

instance System.instReprFilePath:

Repr System.FilePath

Equations

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

source

instance System.instToStringFilePath:

ToString System.FilePath

Equations

System.instToStringFilePath = { toString := fun p => 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 Char.ofNat 92 else Char.ofNat 47

source

def System.FilePath.pathSeparators:

List Char

The list of all possible separators.

Equations

System.FilePath.pathSeparators = if System.Platform.isWindows = true then [Char.ofNat 92, Char.ofNat 47] else [Char.ofNat 47]

source

def System.FilePath.extSeparator:

Char

File extension character

Equations

System.FilePath.extSeparator = Char.ofNat 46

source

def System.FilePath.exeExtension:

String

Equations

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

source

def System.FilePath.isCaseInsensitive:

Bool

Case-insensitive file system

Equations

System.FilePath.isCaseInsensitive = (System.Platform.isWindows || System.Platform.isOSX)

source

def System.FilePath.normalize (p : System.FilePath) (normalizeCase : optParam Bool System.FilePath.isCaseInsensitive) :

System.FilePath

Equations

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

source

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

Bool

Equations

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

source

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

Bool

Equations

System.FilePath.isRelative p = !System.FilePath.isAbsolute p

source

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

System.FilePath

Equations

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

source

instance System.FilePath.instDivFilePath:

Div System.FilePath

Equations

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

source

instance System.FilePath.instHDivFilePathString:

HDiv System.FilePath String System.FilePath

Equations

System.FilePath.instHDivFilePathString = { hDiv := fun p sub => System.FilePath.join p { toString := sub } }

source

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

Option System.FilePath

Equations

System.FilePath.parent p = System.FilePath.mk <$> String.extract p.toString { byteIdx := 0 } <$> System.FilePath.posOfLastSep p

source

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

Option String

Equations

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

source

def System.FilePath.fileStem (p : System.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 : System.FilePath) :

Option String

Equations

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

source

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

System.FilePath

Equations

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

source

def System.FilePath.withExtension (p : System.FilePath) (ext : String) :

System.FilePath

Equations

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

source

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

List String

Equations

System.FilePath.components p = String.splitOn (System.FilePath.normalize p false).toString (Char.toString System.FilePath.pathSeparator)

source

def System.mkFilePath (parts : List String) :

System.FilePath

Equations

System.mkFilePath parts = { toString := String.intercalate (Char.toString System.FilePath.pathSeparator) parts }

source

instance System.instCoeStringFilePath:

Coe String System.FilePath

Equations

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

source

@[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 Char.ofNat 59 else Char.ofNat 58

source

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

System.SearchPath

Equations

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

source

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

String

Equations

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