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

Equations

System.FilePath.pathSeparator = if System.Platform.isWindows = true then Char.ofNat 92 else Char.ofNat 47

The character that separates directories. In the case where more than one character is possible, pathSeparator is the 'ideal' one.

source

def System.FilePath.pathSeparators :

List Char

Equations

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

The list of all possible separators.

source

def System.FilePath.extSeparator :

Char

Equations

System.FilePath.extSeparator = Char.ofNat 46

File extension character

source

def System.FilePath.exeExtension :

String

Equations

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

source

def System.FilePath.isCaseInsensitive :

Bool

Equations

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

Case-insensitive file system

source

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

System.FilePath

Equations

System.FilePath.normalize p normalizeCase = if (List.length System.FilePath.pathSeparators == 1 && !normalizeCase) = true then p else { toString := String.map (fun c => if List.contains System.FilePath.pathSeparators c = true then System.FilePath.pathSeparator else if normalizeCase = true then Char.toLower c else c) p.toString }

source

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

Bool

Equations

System.FilePath.isAbsolute p = (List.contains System.FilePath.pathSeparators (String.front p.toString) || System.Platform.isWindows && decide (String.length p.toString > 1) && String.Iterator.curr (String.Iterator.next (String.iter p.toString)) == Char.ofNat 58)

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

System.FilePath.fileName p = let lastPart := match System.FilePath.posOfLastSep p with | some sepPos => String.extract p.toString (sepPos + Char.ofNat 47) (String.endPos p.toString) | none => p.toString; if (String.isEmpty lastPart || lastPart == "." || lastPart == "..") = true then none else some lastPart

source

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

Option String

Equations

System.FilePath.fileStem p = Option.map (fun fname => match String.revPosOf fname (Char.ofNat 46) with | some { byteIdx := 0 } => fname | some pos => String.extract fname 0 pos | none => fname) (System.FilePath.fileName p)

Extracts the stem (non-extension) part of p.fileName.

source

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

Option String

Equations

System.FilePath.extension p = Option.bind (System.FilePath.fileName p) fun fname => match String.revPosOf fname (Char.ofNat 46) with | some { byteIdx := 0 } => none | some pos => some (String.extract fname (pos + Char.ofNat 46) (String.endPos fname)) | none => none

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

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

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

Equations

System.SearchPath.separator = if System.Platform.isWindows = true then Char.ofNat 59 else Char.ofNat 58

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

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)