idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-13 05:48:39 +03:00
Code Issues Projects Releases Wiki Activity

Use present tense in doc for Path

Browse Source
This commit is contained in:
Andy Lok 2021-01-14 05:26:42 +08:00
parent f1d6d4d6f4
commit 4f8bd22b35
2 changed files with 30 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
libs/contrib/System/Path.idr
View File

@ -109,7 +109,7 @@ Show Volume where
show (UNC server share) = "\\\\" ++ server ++ "\\" ++ share
show (Disk disk) = Strings.singleton disk ++ ":"
||| Display the path in the format of this platform.
||| Displays the path in the format of this platform.
export
Show Path where
show path =
@ -245,7 +245,7 @@ parsePath =
(x::xs) => x :: delete CurDir xs
pure $ MkPath vol (isJust root) body (isJust trailSep)
||| Parse a String into Path.
||| Parses a String into Path.
|||
||| The string is parsed as much as possible from left to right, and the invalid
||| parts on the right is ignored.
@ -390,7 +390,7 @@ export
(</>) : (left : String) -> (right : String) -> String
(</>) left right = show $ append' (parse left) (parse right)
||| Join path components into one.
||| Joins path components into one.
|||
||| ```idris example
||| joinPath ["/usr", "local/etc"] == "/usr/local/etc"
@ -399,7 +399,7 @@ export
joinPath : List String -> String
joinPath xs = foldl (</>) "" xs
||| Split path into components.
||| Splits path into components.
|||
||| ```idris example
||| splitPath "/usr/local/etc" == ["/", "usr", "local", "etc"]
@ -409,7 +409,7 @@ export
splitPath : String -> List String
splitPath = map show . splitPath' . parse
||| Split the path into parent and child.
||| Splits the path into parent and child.
|||
||| ```idris example
||| splitParent "/usr/local/etc" == Just ("/usr/local", "etc")
@ -421,14 +421,14 @@ splitParent path =
(parent, child) <- splitParent' (parse path)
pure (show parent, show child)
||| Return the path without its final component, if there is one.
||| Returns the path without its final component, if there is one.
|||
||| Returns Nothing if the path terminates by a root or volume.
export
parent : String -> Maybe String
parent = map show . parent' . parse
||| Return the list of all parents of the path, longest first, self included.
||| Returns the list of all parents of the path, longest first, self included.
|||
||| ```idris example
||| parents "/etc/kernel" == ["/etc/kernel", "/etc", "/"]
@ -437,7 +437,7 @@ export
parents : String -> List String
parents = map show . List.iterate parent' . parse
||| Determine whether the base is one of the parents of target.
||| Determines whether the base is one of the parents of target.
|||
||| Trailing separator is ignored.
|||
@ -455,7 +455,7 @@ isBaseOf base target =
&& baseRoot == targetRoot
&& (baseBody `isPrefixOf` targetBody)
||| Return a path that, when appended to base, yields target.
||| Returns a path that, when appended to base, yields target.
|||
||| Returns Nothing if the base is not a prefix of the target.
export
@ -483,7 +483,7 @@ export
fileName : String -> Maybe String
fileName = fileName' . parse
||| Extract the file name in the path without extension.
||| Extracts the file name in the path without extension.
|||
||| The stem is:
|||
@ -495,7 +495,7 @@ export
fileStem : String -> Maybe String
fileStem path = pure $ fst $ splitFileName !(fileName path)
||| Extract the extension of the file name in the path.
||| Extracts the extension of the file name in the path.
|||
||| The extension is:
|||
@ -507,7 +507,7 @@ export
extension : String -> Maybe String
extension path = pure $ snd $ splitFileName !(fileName path)
||| Update the file name in the path.
||| Updates the file name in the path.
|||
||| If there is no file name, it appends the name to the path;
||| otherwise, it appends the name to the parent of the path.
@ -515,7 +515,7 @@ export
setFileName : (name : String) -> String -> String
setFileName name path = show $ setFileName' name (parse path)
||| Append a extension to the path.
||| Appends a extension to the path.
|||
||| If there is no file name, the path will not change;
||| if the path has no extension, the extension will be appended;
@ -539,7 +539,7 @@ export
show $ setFileName' (stem ++ ext) path'
Nothing => path
||| Drop the extension of the path.
||| Drops the extension of the path.
export
dropExtension : String -> String
dropExtension path = path <.> ""

32
src/Utils/Path.idr
View File

@ -30,7 +30,7 @@ pathSeparator = if isWindows then ';' else ':'
||| Windows path prefix.
public export
data Volume
=
=
||| Windows Uniform Naming Convention, consisting of server name and share
||| directory.
|||
@ -44,7 +44,7 @@ data Volume
||| A single body in path.
public export
data Body
=
=
||| Represents ".".
CurDir |
||| Represents "..".
@ -109,7 +109,7 @@ Show Volume where
show (UNC server share) = "\\\\" ++ server ++ "\\" ++ share
show (Disk disk) = Strings.singleton disk ++ ":"
||| Display the path in the format of this platform.
||| Displays the path in the format of this platform.
export
Show Path where
show path =
@ -241,7 +241,7 @@ parsePath =
(x::xs) => x :: delete CurDir xs
pure $ MkPath vol (isJust root) body (isJust trailSep)
||| Parse a String into Path.
||| Parses a String into Path.
|||
||| The string is parsed as much as possible from left to right, and the invalid
||| parts on the right is ignored.
@ -386,7 +386,7 @@ export
(</>) : (left : String) -> (right : String) -> String
(</>) left right = show $ append' (parse left) (parse right)
||| Join path components into one.
||| Joins path components into one.
|||
||| ```idris example
||| joinPath ["/usr", "local/etc"] == "/usr/local/etc"
@ -395,7 +395,7 @@ export
joinPath : List String -> String
joinPath xs = foldl (</>) "" xs
||| Split path into components.
||| Splits path into components.
|||
||| ```idris example
||| splitPath "/usr/local/etc" == ["/", "usr", "local", "etc"]
@ -405,7 +405,7 @@ export
splitPath : String -> List String
splitPath = map show . splitPath' . parse
||| Split the path into parent and child.
||| Splits the path into parent and child.
|||
||| ```idris example
||| splitParent "/usr/local/etc" == Just ("/usr/local", "etc")
@ -417,14 +417,14 @@ splitParent path =
(parent, child) <- splitParent' (parse path)
pure (show parent, show child)
||| Return the path without its final component, if there is one.
||| Returns the path without its final component, if there is one.
|||
||| Returns Nothing if the path terminates by a root or volume.
export
parent : String -> Maybe String
parent = map show . parent' . parse
||| Return the list of all parents of the path, longest first, self included.
||| Returns the list of all parents of the path, longest first, self included.
|||
||| ```idris example
||| parents "/etc/kernel" == ["/etc/kernel", "/etc", "/"]
@ -433,7 +433,7 @@ export
parents : String -> List String
parents = map show . List.iterate parent' . parse
||| Determine whether the base is one of the parents of target.
||| Determines whether the base is one of the parents of target.
|||
||| Trailing separator is ignored.
|||
@ -451,7 +451,7 @@ isBaseOf base target =
&& baseRoot == targetRoot
&& (baseBody `isPrefixOf` targetBody)
||| Return a path that, when appended to base, yields target.
||| Returns a path that, when appended to base, yields target.
|||
||| Returns Nothing if the base is not a prefix of the target.
export
@ -479,7 +479,7 @@ export
fileName : String -> Maybe String
fileName = fileName' . parse
||| Extract the file name in the path without extension.
||| Extracts the file name in the path without extension.
|||
||| The stem is:
|||
@ -491,7 +491,7 @@ export
fileStem : String -> Maybe String
fileStem path = pure $ fst $ splitFileName !(fileName path)
||| Extract the extension of the file name in the path.
||| Extracts the extension of the file name in the path.
|||
||| The extension is:
|||
@ -503,7 +503,7 @@ export
extension : String -> Maybe String
extension path = pure $ snd $ splitFileName !(fileName path)
||| Update the file name in the path.
||| Updates the file name in the path.
|||
||| If there is no file name, it appends the name to the path;
||| otherwise, it appends the name to the parent of the path.
@ -511,7 +511,7 @@ export
setFileName : (name : String) -> String -> String
setFileName name path = show $ setFileName' name (parse path)
||| Append a extension to the path.
||| Appends a extension to the path.
|||
||| If there is no file name, the path will not change;
||| if the path has no extension, the extension will be appended;
@ -535,7 +535,7 @@ export
show $ setFileName' (stem ++ ext) path'
Nothing => path
||| Drop the extension of the path.
||| Drops the extension of the path.
export
dropExtension : String -> String
dropExtension path = path <.> ""