diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index 188c94e150..b36ceea747 100644 --- a/library/init/data/string/basic.lean +++ b/library/init/data/string/basic.lean @@ -131,6 +131,16 @@ partial def posOfAux (s : String) (c : Char) (stopPos : Pos) : Pos → Pos @[inline] def posOf (s : String) (c : Char) : Pos := posOfAux s c s.bsize 0 +partial def revPosOfAux (s : String) (c : Char) : Pos → Option Pos +| pos := + if s.get pos == c then some pos + else if pos == 0 then none + else revPosOfAux (s.prev pos) + +def revPosOf (s : String) (c : Char) : Option Pos := +if s.bsize == 0 then none +else revPosOfAux s c (s.prev s.bsize) + private def utf8ExtractAux₂ : List Char → Pos → Pos → List Char | [] _ _ := [] | (c::cs) i e := if i = e then [] else c :: utf8ExtractAux₂ cs (i + csize c) e diff --git a/library/init/system/filepath.lean b/library/init/system/filepath.lean index 7abc4d8b1b..483cd3a3a3 100644 --- a/library/init/system/filepath.lean +++ b/library/init/system/filepath.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ prelude import init.system.platform -import init.data.char.basic +import init.data.string.basic namespace System namespace FilePath @@ -27,5 +27,10 @@ if isWindows then ';' else ':' def extSeparator : Char := '.' +def dirName (fname : String) : String := +match fname.revPosOf pathSeparator with +| none => "." +| some pos => { Substring . str := fname, startPos := 0, stopPos := pos }.toString + end FilePath end System