mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-23 19:54:50 +03:00
3f914889b8
Can't export a type which refers to a private name. This has caught a couple of visibility errors in the libraries, code and tests, so they've been updated too.
467 lines
14 KiB
Idris
467 lines
14 KiB
Idris
module System.Path
|
|
|
|
import Data.List
|
|
import Data.Maybe
|
|
import Data.Nat
|
|
import Data.Strings
|
|
import Data.String.Extra
|
|
|
|
import System.Info
|
|
|
|
import Text.Token
|
|
import Text.Lexer
|
|
import Text.Parser
|
|
import Text.Quantity
|
|
|
|
infixr 5 </>
|
|
infixr 7 <.>
|
|
|
|
|
|
||| The character that separates directories in the path.
|
|
export
|
|
dirSeparator : Char
|
|
dirSeparator = if isWindows then '\\' else '/'
|
|
|
|
||| The character that separates multiple paths.
|
|
export
|
|
pathSeparator : Char
|
|
pathSeparator = if isWindows then ';' else ':'
|
|
|
|
||| Windows' path prefixes of path component.
|
|
public export
|
|
data Volume
|
|
=
|
|
||| Windows' Uniform Naming Convention, e.g., a network sharing
|
|
||| directory: `\\host\c$\Windows\System32`
|
|
UNC String String |
|
|
||| The drive, e.g., "C:". The disk character is in upper case
|
|
Disk Char
|
|
|
|
||| A single body of path component.
|
|
public export
|
|
data Body
|
|
=
|
|
||| Represents "."
|
|
CurDir |
|
|
||| Represents ".."
|
|
ParentDir |
|
|
||| Common directory or file
|
|
Normal String
|
|
|
|
||| A parsed cross-platform file system path.
|
|
|||
|
|
||| The function `parse` constructs a Path component from String,
|
|
||| and the function `show` converts in reverse.
|
|
|||
|
|
||| Trailing separator is only used for display and is ignored while
|
|
||| comparing paths.
|
|
public export
|
|
record Path where
|
|
constructor MkPath
|
|
||| Windows' path prefix (only on Windows)
|
|
volume : Maybe Volume
|
|
||| Whether the path contains a root
|
|
hasRoot : Bool
|
|
||| Path bodies
|
|
body : List Body
|
|
||| Whether the path terminates with a separator
|
|
hasTrailSep : Bool
|
|
|
|
export
|
|
Eq Volume where
|
|
(==) (UNC l1 l2) (UNC r1 r2) = l1 == r1 && r1 == r2
|
|
(==) (Disk l) (Disk r) = l == r
|
|
(==) _ _ = False
|
|
|
|
export
|
|
Eq Body where
|
|
(==) CurDir CurDir = True
|
|
(==) ParentDir ParentDir = True
|
|
(==) (Normal l) (Normal r) = l == r
|
|
(==) _ _ = False
|
|
|
|
export
|
|
Eq Path where
|
|
(==) (MkPath l1 l2 l3 _) (MkPath r1 r2 r3 _) = l1 == r1
|
|
&& l2 == r2
|
|
&& l3 == r3
|
|
|
|
||| An empty path that represents "".
|
|
public export
|
|
emptyPath : Path
|
|
emptyPath = MkPath Nothing False [] False
|
|
|
|
--------------------------------------------------------------------------------
|
|
-- Show
|
|
--------------------------------------------------------------------------------
|
|
|
|
export
|
|
Show Body where
|
|
show CurDir = "."
|
|
show ParentDir = ".."
|
|
show (Normal s) = s
|
|
|
|
export
|
|
Show Volume where
|
|
show (UNC server share) = "\\\\" ++ server ++ "\\" ++ share
|
|
show (Disk disk) = singleton disk ++ ":"
|
|
|
|
||| Display the path in the format on the platform.
|
|
export
|
|
Show Path where
|
|
show p = let sep = singleton dirSeparator
|
|
volStr = fromMaybe "" (map show p.volume)
|
|
rootStr = if p.hasRoot then sep else ""
|
|
bodyStr = join sep $ map show p.body
|
|
trailStr = if p.hasTrailSep then sep else "" in
|
|
volStr ++ rootStr ++ bodyStr ++ trailStr
|
|
|
|
--------------------------------------------------------------------------------
|
|
-- Parser
|
|
--------------------------------------------------------------------------------
|
|
|
|
data PathTokenKind = PTText | PTPunct Char
|
|
|
|
Eq PathTokenKind where
|
|
(==) PTText PTText = True
|
|
(==) (PTPunct c1) (PTPunct c2) = c1 == c2
|
|
(==) _ _ = False
|
|
|
|
PathToken : Type
|
|
PathToken = Token PathTokenKind
|
|
|
|
TokenKind PathTokenKind where
|
|
TokType PTText = String
|
|
TokType (PTPunct _) = ()
|
|
|
|
tokValue PTText x = x
|
|
tokValue (PTPunct _) _ = ()
|
|
|
|
pathTokenMap : TokenMap PathToken
|
|
pathTokenMap = toTokenMap $
|
|
[ (is '/', PTPunct '/')
|
|
, (is '\\', PTPunct '\\')
|
|
, (is ':', PTPunct ':')
|
|
, (is '?', PTPunct '?')
|
|
, (some $ non $ oneOf "/\\:?", PTText)
|
|
]
|
|
|
|
lexPath : String -> List PathToken
|
|
lexPath str = let (tokens, _, _, _) = lex pathTokenMap str in
|
|
map TokenData.tok tokens
|
|
|
|
-- match both '/' and '\\' regardless of the platform.
|
|
bodySeparator : Grammar PathToken True ()
|
|
bodySeparator = (match $ PTPunct '\\') <|> (match $ PTPunct '/')
|
|
|
|
-- Example: \\?\
|
|
-- Windows can automatically translate '/' to '\\'. The verbatim prefix,
|
|
-- i.e., `\\?\`, disables the translation.
|
|
-- Here, we simply parse and then ignore it.
|
|
verbatim : Grammar PathToken True ()
|
|
verbatim = do count (exactly 2) $ match $ PTPunct '\\'
|
|
match $ PTPunct '?'
|
|
match $ PTPunct '\\'
|
|
pure ()
|
|
|
|
-- Example: \\server\share
|
|
unc : Grammar PathToken True Volume
|
|
unc = do count (exactly 2) $ match $ PTPunct '\\'
|
|
server <- match PTText
|
|
bodySeparator
|
|
share <- match PTText
|
|
Core.pure $ UNC server share
|
|
|
|
-- Example: \\?\server\share
|
|
verbatimUnc : Grammar PathToken True Volume
|
|
verbatimUnc = do verbatim
|
|
server <- match PTText
|
|
bodySeparator
|
|
share <- match PTText
|
|
Core.pure $ UNC server share
|
|
|
|
-- Example: C:
|
|
disk : Grammar PathToken True Volume
|
|
disk = do text <- match PTText
|
|
disk <- case unpack text of
|
|
(disk :: xs) => pure disk
|
|
[] => fail "Expect Disk"
|
|
match $ PTPunct ':'
|
|
pure $ Disk (toUpper disk)
|
|
|
|
-- Example: \\?\C:
|
|
verbatimDisk : Grammar PathToken True Volume
|
|
verbatimDisk = do verbatim
|
|
d <- disk
|
|
pure d
|
|
|
|
parseVolume : Grammar PathToken True Volume
|
|
parseVolume = verbatimUnc
|
|
<|> verbatimDisk
|
|
<|> unc
|
|
<|> disk
|
|
|
|
parseBody : Grammar PathToken True Body
|
|
parseBody = do text <- match PTText
|
|
the (Grammar _ False _) $
|
|
case text of
|
|
".." => pure ParentDir
|
|
"." => pure CurDir
|
|
s => pure (Normal s)
|
|
|
|
parsePath : Grammar PathToken False Path
|
|
parsePath = do vol <- optional parseVolume
|
|
root <- optional (some bodySeparator)
|
|
body <- sepBy (some bodySeparator) parseBody
|
|
trailSep <- optional (some bodySeparator)
|
|
let body = filter (\case Normal s => ltrim s /= ""
|
|
_ => True) body
|
|
let body = case body of
|
|
[] => []
|
|
(x::xs) => x :: delete CurDir xs
|
|
pure $ MkPath vol (isJust root) body (isJust trailSep)
|
|
|
|
||| Parse a String into Path component.
|
|
|||
|
|
||| Returns the path parsed as much as possible from left to right, the
|
|
||| invalid parts on the right end is ignored.
|
|
|||
|
|
||| Some kind of invalid path is accepted. Relaxing rules:
|
|
|||
|
|
||| - Both slash('/') and backslash('\\') are parsed as valid directory
|
|
||| separator, regardless of the platform;
|
|
||| - Any characters in path body in allowed, e.g., glob like "/root/*";
|
|
||| - Verbatim prefix(`\\?\`) that disables the forward
|
|
||| slash (Windows only) is ignored.
|
|
||| - Repeated separators are ignored, so "a/b" and "a//b" both have "a"
|
|
||| and "b" as bodies.
|
|
||| - Occurrences of "." are normalized away, except if they are at the
|
|
||| beginning of the path. For example, "a/./b", "a/b/", "a/b/". and
|
|
||| "a/b" all have "a" and "b" as bodies, but "./a/b" starts with an
|
|
||| additional `CurDir` body.
|
|
|||
|
|
||| ```idris example
|
|
||| parse "C:\\Windows/System32"
|
|
||| ```
|
|
||| ```idris example
|
|
||| parse "/usr/local/etc/*"
|
|
||| ```
|
|
export
|
|
parse : String -> Path
|
|
parse str = case parse parsePath (lexPath str) of
|
|
Right (p, _) => p
|
|
_ => emptyPath
|
|
|
|
--------------------------------------------------------------------------------
|
|
-- Utils
|
|
--------------------------------------------------------------------------------
|
|
|
|
isAbsolute' : Path -> Bool
|
|
isAbsolute' p = if isWindows
|
|
then case p.volume of
|
|
Just (UNC _ _) => True
|
|
Just (Disk _) => p.hasRoot
|
|
Nothing => False
|
|
else p.hasRoot
|
|
|
|
append' : (left : Path) -> (right : Path) -> Path
|
|
append' l r = if isAbsolute' r || isJust r.volume
|
|
then r
|
|
else if hasRoot r
|
|
then record { volume = l.volume } r
|
|
else record { body = l.body ++ r.body,
|
|
hasTrailSep = r.hasTrailSep } l
|
|
|
|
splitParent' : Path -> Maybe (Path, Path)
|
|
splitParent' p
|
|
= case p.body of
|
|
[] => Nothing
|
|
(x::xs) => let parentPath = record { body = init (x::xs),
|
|
hasTrailSep = False } p
|
|
lastPath = MkPath Nothing False [last (x::xs)] p.hasTrailSep in
|
|
Just (parentPath, lastPath)
|
|
|
|
parent' : Path -> Maybe Path
|
|
parent' p = map fst (splitParent' p)
|
|
|
|
fileName' : Path -> Maybe String
|
|
fileName' p = findNormal (reverse p.body)
|
|
where
|
|
findNormal : List Body -> Maybe String
|
|
findNormal ((Normal s)::xs) = Just s
|
|
findNormal (CurDir::xs) = findNormal xs
|
|
findNormal _ = Nothing
|
|
|
|
setFileName' : (name : String) -> Path -> Path
|
|
setFileName' name p = if isJust (fileName' p)
|
|
then append' (fromMaybe emptyPath $ parent' p) (parse name)
|
|
else append' p (parse name)
|
|
|
|
splitFileName : String -> (String, String)
|
|
splitFileName name
|
|
= case break (== '.') $ reverse $ unpack name of
|
|
(_, []) => (name, "")
|
|
(_, ['.']) => (name, "")
|
|
(revExt, (dot :: revStem))
|
|
=> ((pack $ reverse revStem), (pack $ reverse revExt))
|
|
|
|
--------------------------------------------------------------------------------
|
|
-- Manipulations
|
|
--------------------------------------------------------------------------------
|
|
|
|
||| Returns true if the path is absolute.
|
|
|||
|
|
||| - On Unix, a path is absolute if it starts with the root,
|
|
||| so isAbsolute and hasRoot are equivalent.
|
|
|||
|
|
||| - On Windows, a path is absolute if it has a volume and starts
|
|
||| with the root. e.g., `c:\\windows` is absolute, while `c:temp`
|
|
||| and `\temp` are not. In addition, a path with UNC volume is absolute.
|
|
export
|
|
isAbsolute : String -> Bool
|
|
isAbsolute p = isAbsolute' (parse p)
|
|
|
|
||| Returns true if the path is relative, i.e., not absolute.
|
|
export
|
|
isRelative : String -> Bool
|
|
isRelative = not . isAbsolute
|
|
|
|
||| Appends the right path to the left one.
|
|
|||
|
|
||| If the path on the right is absolute, it replaces the left path.
|
|
|||
|
|
||| On Windows:
|
|
|||
|
|
||| - If the right path has a root but no volume (e.g., `\windows`), it
|
|
||| replaces everything except for the volume (if any) of left.
|
|
||| - If the right path has a volume but no root, it replaces left.
|
|
|||
|
|
||| ```idris example
|
|
||| "/usr" </> "local/etc"
|
|
||| ```
|
|
export
|
|
(</>) : (left : String) -> (right : String) -> String
|
|
(</>) l r = show $ append' (parse l) (parse r)
|
|
|
|
||| Join path elements together.
|
|
|||
|
|
||| ```idris example
|
|
||| joinPath ["/usr", "local/etc"] == "/usr/local/etc"
|
|
||| ```
|
|
export
|
|
joinPath : List String -> String
|
|
joinPath xs = foldl (</>) "" xs
|
|
|
|
||| Returns the parent and child.
|
|
|||
|
|
||| ```idris example
|
|
||| splitParent "/usr/local/etc" == Just ("/usr/local", "etc")
|
|
||| ```
|
|
export
|
|
splitParent : String -> Maybe (String, String)
|
|
splitParent p = do (a, b) <- splitParent' (parse p)
|
|
pure $ (show a, show b)
|
|
|
|
||| Returns the path without its final component, if there is one.
|
|
|||
|
|
||| Returns Nothing if the path terminates in a root or volume.
|
|
export
|
|
parent : String -> Maybe String
|
|
parent p = map show $ parent' (parse p)
|
|
|
|
||| Returns a list of all the parents of the path, longest first,
|
|
||| self included.
|
|
|||
|
|
||| ```idris example
|
|
||| parents "/etc/kernel" == ["/etc/kernel", "/etc", "/"]
|
|
||| ```
|
|
export
|
|
parents : String -> List String
|
|
parents p = map show $ iterate parent' (parse p)
|
|
|
|
||| Determines whether base is either one of the parents of full.
|
|
|||
|
|
||| Trailing separator is ignored.
|
|
export
|
|
startWith : (base : String) -> (full : String) -> Bool
|
|
startWith base full = (parse base) `elem` (iterate parent' (parse full))
|
|
|
|
||| Returns a path that, when appended onto base, yields full.
|
|
|||
|
|
||| If base is not a prefix of full (i.e., startWith returns false),
|
|
||| returns Nothing.
|
|
export
|
|
stripPrefix : (base : String) -> (full : String) -> Maybe String
|
|
stripPrefix base full
|
|
= do let MkPath vol1 root1 body1 _ = parse base
|
|
let MkPath vol2 root2 body2 trialSep = parse full
|
|
if vol1 == vol2 && root1 == root2 then Just () else Nothing
|
|
body <- stripBody body1 body2
|
|
pure $ show $ MkPath Nothing False body trialSep
|
|
where
|
|
stripBody : (base : List Body) -> (full : List Body) -> Maybe (List Body)
|
|
stripBody [] ys = Just ys
|
|
stripBody xs [] = Nothing
|
|
stripBody (x::xs) (y::ys) = if x == y then stripBody xs ys else Nothing
|
|
|
|
||| Returns the final body of the path, if there is one.
|
|
|||
|
|
||| If the path is a normal file, this is the file name. If it's the
|
|
||| path of a directory, this is the directory name.
|
|
|||
|
|
||| Returns Nothing if the final body is "..".
|
|
export
|
|
fileName : String -> Maybe String
|
|
fileName p = fileName' (parse p)
|
|
|
|
||| Extracts the stem (non-extension) portion of the file name of path.
|
|
|||
|
|
||| The stem is:
|
|
|||
|
|
||| - Nothing, if there is no file name;
|
|
||| - The entire file name if there is no embedded ".";
|
|
||| - The entire file name if the file name begins with "." and has
|
|
||| no other "."s within;
|
|
||| - Otherwise, the portion of the file name before the final "."
|
|
export
|
|
fileStem : String -> Maybe String
|
|
fileStem p = pure $ fst $ splitFileName !(fileName p)
|
|
|
|
||| Extracts the extension of the file name of path.
|
|
|||
|
|
||| The extension is:
|
|
|||
|
|
||| - Nothing, if there is no file name;
|
|
||| - Nothing, if there is no embedded ".";
|
|
||| - Nothing, if the file name begins with "." and has no other "."s within;
|
|
||| - Otherwise, the portion of the file name after the final "."
|
|
export
|
|
extension : String -> Maybe String
|
|
extension p = pure $ snd $ splitFileName !(fileName p)
|
|
|
|
||| Updates the file name of the path.
|
|
|||
|
|
||| If no file name, this is equivalent to appending the name;
|
|
||| Otherwise it is equivalent to appending the name to the parent.
|
|
export
|
|
setFileName : (name : String) -> String -> String
|
|
setFileName name p = show $ setFileName' name (parse p)
|
|
|
|
||| Append a extension to the path.
|
|
|||
|
|
||| Returns the path as it is if no file name.
|
|
|||
|
|
||| If `extension` of the path is Nothing, the extension is added; otherwise
|
|
||| it is replaced.
|
|
|||
|
|
||| If the ext is empty, the extension is dropped.
|
|
export
|
|
(<.>) : String -> (ext : String) -> String
|
|
(<.>) p ext = let p' = parse p
|
|
ext = pack $ dropWhile (== '.') (unpack ext)
|
|
ext = if ltrim ext == "" then "" else "." ++ ext in
|
|
case fileName' p' of
|
|
Just name => let (stem, _) = splitFileName name in
|
|
show $ setFileName' (stem ++ ext) p'
|
|
Nothing => p
|