Documentation

Init.System.FilePath

structure System.FilePath :

Type

toString : String

instance System.instHashableFilePath :

Hashable System.FilePath

Equations

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

instance System.instInhabitedFilePath :

Inhabited System.FilePath

Equations

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

instance System.instDecidableEqFilePath :

DecidableEq System.FilePath

Equations

System.instDecidableEqFilePath = [anonymous]

instance System.instReprFilePath :

Repr System.FilePath

Equations

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

instance System.instToStringFilePath :

ToString System.FilePath

Equations

System.instToStringFilePath = { toString := fun p => p.toString }

def System.FilePath.pathSeparator :

Equations

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

def System.FilePath.pathSeparators :

Equations

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

def System.FilePath.extSeparator :

Equations

System.FilePath.extSeparator = Char.ofNat 46

def System.FilePath.exeExtension :

Equations

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

def System.FilePath.isCaseInsensitive :

Equations

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

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 }

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

Equations

System.FilePath.isAbsolute p = (List.contains System.FilePath.pathSeparators (String.front p.toString) || System.Platform.isWindows && decide (String.bsize p.toString ≥ 1) && String.getOp p.toString 1 == Char.ofNat 58)

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

Equations

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

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 }

instance System.FilePath.instDivFilePath :

Div System.FilePath

Equations

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

instance System.FilePath.instHDivFilePathString :

HDiv System.FilePath String System.FilePath

Equations

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

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

Option System.FilePath

Equations

System.FilePath.parent p = System.FilePath.mk <$> String.extract p.toString 0 <$> System.FilePath.posOfLastSep p

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

Equations

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

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

Equations

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

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

Equations

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

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

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)

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

Equations

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

def System.mkFilePath (parts : List String) :

System.FilePath

Equations

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

instance System.instCoeStringFilePath :

Coe String System.FilePath

Equations

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

@[inline]

abbrev System.SearchPath :

Type

Equations

System.SearchPath = List System.FilePath

def System.SearchPath.separator :

Equations

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

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)

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

Equations

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