2020-05-20 17:36:50 +03:00
|
|
|
module System.Path
|
|
|
|
|
|
|
|
import Data.List
|
|
|
|
import Data.Maybe
|
Fix import loading
This was taking too long, and adding too many things, because it was
going too deep in the name of having everything accessible at the REPL
and for the compiler. So, it's done a bit differently now, only chasing
everything on a "full" load (i.e., final load at the REPL)
This has some effects:
+ As systems get bigger, load time gets better (on my machine, checking
Idris.Main now takes 52s from scratch, down from 76s)
+ You might find import errors that you didn't previously get, because
things were being imported that shouldn't have been. The new way is
correct!
An unfortunate effect is that sometimes you end up getting "undefined
name" errors even if you didn't explicitly use the name, because
sometimes a module uses a name from another module in a type, which then
gets exported, and eventually needs to be reduced. This mostly happens
because there is a compile time check that should be done which I
haven't implemented yet. That is, public export definitions should only
be allowed to use names that are also public export. I'll get to this
soon.
2020-05-27 17:49:03 +03:00
|
|
|
import Data.Nat
|
2021-06-28 15:48:37 +03:00
|
|
|
import Data.String
|
2020-05-20 17:36:50 +03:00
|
|
|
import Data.String.Extra
|
2020-05-30 16:51:12 +03:00
|
|
|
|
2020-05-20 17:36:50 +03:00
|
|
|
import Text.Token
|
|
|
|
import Text.Lexer
|
|
|
|
import Text.Parser
|
|
|
|
import Text.Quantity
|
|
|
|
|
2020-12-06 21:57:32 +03:00
|
|
|
import System.Info
|
|
|
|
|
2021-04-15 16:08:50 +03:00
|
|
|
infixr 5 </>, />
|
2020-05-30 16:51:12 +03:00
|
|
|
infixr 7 <.>
|
|
|
|
|
|
|
|
|
2020-05-21 01:37:55 +03:00
|
|
|
||| The character that separates directories in the path.
|
2020-05-20 17:36:50 +03:00
|
|
|
export
|
2020-05-21 01:37:55 +03:00
|
|
|
dirSeparator : Char
|
|
|
|
dirSeparator = if isWindows then '\\' else '/'
|
2020-05-20 17:36:50 +03:00
|
|
|
|
2020-05-21 01:37:55 +03:00
|
|
|
||| The character that separates multiple paths.
|
2020-05-20 17:36:50 +03:00
|
|
|
export
|
2020-05-21 01:37:55 +03:00
|
|
|
pathSeparator : Char
|
|
|
|
pathSeparator = if isWindows then ';' else ':'
|
2020-05-20 17:36:50 +03:00
|
|
|
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Windows path prefix.
|
2020-05-20 17:36:50 +03:00
|
|
|
public export
|
2021-01-14 00:05:59 +03:00
|
|
|
data Volume
|
|
|
|
=
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Windows Uniform Naming Convention, consisting of server name and share
|
|
|
|
||| directory.
|
|
|
|
|||
|
|
|
|
||| Example: `\\localhost\share`
|
2020-05-30 16:51:12 +03:00
|
|
|
UNC String String |
|
2020-12-06 21:57:32 +03:00
|
|
|
||| The drive.
|
|
|
|
|||
|
|
|
|
||| Example: `C:`
|
2020-05-30 16:51:12 +03:00
|
|
|
Disk Char
|
|
|
|
|
2020-12-06 21:57:32 +03:00
|
|
|
||| A single body in path.
|
2020-05-20 17:36:50 +03:00
|
|
|
public export
|
2021-01-14 00:05:59 +03:00
|
|
|
data Body
|
|
|
|
=
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Represents ".".
|
2020-05-30 16:51:12 +03:00
|
|
|
CurDir |
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Represents "..".
|
2020-05-30 16:51:12 +03:00
|
|
|
ParentDir |
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Directory or file.
|
2020-05-30 16:51:12 +03:00
|
|
|
Normal String
|
|
|
|
|
|
|
|
||| A parsed cross-platform file system path.
|
2020-05-20 17:36:50 +03:00
|
|
|
|||
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Use the function `parse` to constructs a Path from String, and use the
|
|
|
|
||| function `show` to convert in reverse.
|
2020-05-20 17:36:50 +03:00
|
|
|
|||
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Trailing separator is only used for display and is ignored when comparing
|
|
|
|
||| paths.
|
2020-05-20 17:36:50 +03:00
|
|
|
public export
|
|
|
|
record Path where
|
|
|
|
constructor MkPath
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Windows path prefix (only for Windows).
|
2020-05-30 16:51:12 +03:00
|
|
|
volume : Maybe Volume
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Whether the path contains root.
|
2020-05-20 17:36:50 +03:00
|
|
|
hasRoot : Bool
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Path bodies.
|
2020-05-20 17:36:50 +03:00
|
|
|
body : List Body
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Whether the path terminates with a separator.
|
2020-05-20 17:36:50 +03:00
|
|
|
hasTrailSep : Bool
|
|
|
|
|
|
|
|
export
|
2020-05-30 16:51:12 +03:00
|
|
|
Eq Volume where
|
2020-05-20 17:36:50 +03:00
|
|
|
(==) (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
|
2020-12-06 21:57:32 +03:00
|
|
|
(==) (MkPath l1 l2 l3 _) (MkPath r1 r2 r3 _) =
|
|
|
|
l1 == r1 && l2 == r2 && l3 == r3
|
2020-05-20 17:36:50 +03:00
|
|
|
|
2020-12-06 21:57:32 +03:00
|
|
|
||| An empty path, which represents "".
|
2020-05-20 17:36:50 +03:00
|
|
|
public export
|
|
|
|
emptyPath : Path
|
|
|
|
emptyPath = MkPath Nothing False [] False
|
|
|
|
|
|
|
|
--------------------------------------------------------------------------------
|
|
|
|
-- Show
|
|
|
|
--------------------------------------------------------------------------------
|
|
|
|
|
|
|
|
export
|
|
|
|
Show Body where
|
|
|
|
show CurDir = "."
|
|
|
|
show ParentDir = ".."
|
2020-12-06 21:57:32 +03:00
|
|
|
show (Normal normal) = normal
|
2020-05-20 17:36:50 +03:00
|
|
|
|
|
|
|
export
|
2020-05-30 16:51:12 +03:00
|
|
|
Show Volume where
|
2020-05-20 17:36:50 +03:00
|
|
|
show (UNC server share) = "\\\\" ++ server ++ "\\" ++ share
|
2021-06-28 15:48:37 +03:00
|
|
|
show (Disk disk) = String.singleton disk ++ ":"
|
2020-05-20 17:36:50 +03:00
|
|
|
|
2021-01-14 00:26:42 +03:00
|
|
|
||| Displays the path in the format of this platform.
|
2020-05-20 17:36:50 +03:00
|
|
|
export
|
|
|
|
Show Path where
|
2021-01-16 10:03:45 +03:00
|
|
|
show path =
|
|
|
|
let
|
2021-06-28 15:48:37 +03:00
|
|
|
sep = String.singleton dirSeparator
|
2020-12-06 21:57:32 +03:00
|
|
|
showVol = maybe "" show path.volume
|
|
|
|
showRoot = if path.hasRoot then sep else ""
|
|
|
|
showBody = join sep $ map show path.body
|
|
|
|
showTrail = if path.hasTrailSep then sep else ""
|
|
|
|
in
|
|
|
|
showVol ++ showRoot ++ showBody ++ showTrail
|
2020-05-20 17:36:50 +03:00
|
|
|
|
|
|
|
--------------------------------------------------------------------------------
|
|
|
|
-- 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
|
2020-05-20 21:09:14 +03:00
|
|
|
pathTokenMap = toTokenMap $
|
2020-05-20 17:36:50 +03:00
|
|
|
[ (is '/', PTPunct '/')
|
|
|
|
, (is '\\', PTPunct '\\')
|
|
|
|
, (is ':', PTPunct ':')
|
|
|
|
, (is '?', PTPunct '?')
|
|
|
|
, (some $ non $ oneOf "/\\:?", PTText)
|
|
|
|
]
|
|
|
|
|
2021-08-06 12:03:13 +03:00
|
|
|
lexPath : String -> List (WithBounds PathToken)
|
2021-01-16 10:03:45 +03:00
|
|
|
lexPath str =
|
2020-12-06 21:57:32 +03:00
|
|
|
let
|
2021-01-16 10:03:45 +03:00
|
|
|
(tokens, _, _, _) = lex pathTokenMap str
|
2020-12-06 21:57:32 +03:00
|
|
|
in
|
2021-08-06 12:03:13 +03:00
|
|
|
tokens -- TokenData.tok tokens
|
2020-05-20 17:36:50 +03:00
|
|
|
|
|
|
|
-- match both '/' and '\\' regardless of the platform.
|
2021-08-06 12:03:13 +03:00
|
|
|
bodySeparator : Grammar state PathToken True ()
|
2020-05-21 01:37:55 +03:00
|
|
|
bodySeparator = (match $ PTPunct '\\') <|> (match $ PTPunct '/')
|
2020-05-20 17:36:50 +03:00
|
|
|
|
2020-12-06 21:57:32 +03:00
|
|
|
-- Windows will automatically translate '/' to '\\'. And the verbatim prefix,
|
|
|
|
-- i.e., `\\?\`, can be used to disable the translation.
|
|
|
|
-- However, we just parse it and ignore it.
|
|
|
|
--
|
2020-05-20 17:36:50 +03:00
|
|
|
-- Example: \\?\
|
2021-08-06 12:03:13 +03:00
|
|
|
verbatim : Grammar state PathToken True ()
|
2020-12-06 21:57:32 +03:00
|
|
|
verbatim =
|
2021-01-16 10:03:45 +03:00
|
|
|
do
|
2021-02-24 14:07:16 +03:00
|
|
|
ignore $ count (exactly 2) $ match $ PTPunct '\\'
|
2020-12-06 21:57:32 +03:00
|
|
|
match $ PTPunct '?'
|
|
|
|
match $ PTPunct '\\'
|
|
|
|
pure ()
|
2020-05-20 17:36:50 +03:00
|
|
|
|
|
|
|
-- Example: \\server\share
|
2021-08-06 12:03:13 +03:00
|
|
|
unc : Grammar state PathToken True Volume
|
2020-12-06 21:57:32 +03:00
|
|
|
unc =
|
|
|
|
do
|
2021-02-24 14:07:16 +03:00
|
|
|
ignore $ count (exactly 2) $ match $ PTPunct '\\'
|
2020-12-06 21:57:32 +03:00
|
|
|
server <- match PTText
|
|
|
|
bodySeparator
|
|
|
|
share <- match PTText
|
|
|
|
pure $ UNC server share
|
2020-05-20 17:36:50 +03:00
|
|
|
|
|
|
|
-- Example: \\?\server\share
|
2021-08-06 12:03:13 +03:00
|
|
|
verbatimUnc : Grammar state PathToken True Volume
|
2020-12-06 21:57:32 +03:00
|
|
|
verbatimUnc =
|
|
|
|
do
|
|
|
|
verbatim
|
|
|
|
server <- match PTText
|
|
|
|
bodySeparator
|
|
|
|
share <- match PTText
|
|
|
|
pure $ UNC server share
|
2020-05-20 17:36:50 +03:00
|
|
|
|
|
|
|
-- Example: C:
|
2021-08-06 12:03:13 +03:00
|
|
|
disk : Grammar state PathToken True Volume
|
2020-12-06 21:57:32 +03:00
|
|
|
disk =
|
|
|
|
do
|
|
|
|
text <- match PTText
|
|
|
|
disk <- case unpack text of
|
|
|
|
(disk :: xs) => pure disk
|
|
|
|
[] => fail "Expects disk"
|
|
|
|
match $ PTPunct ':'
|
|
|
|
pure $ Disk (toUpper disk)
|
2020-05-20 17:36:50 +03:00
|
|
|
|
|
|
|
-- Example: \\?\C:
|
2021-08-06 12:03:13 +03:00
|
|
|
verbatimDisk : Grammar state PathToken True Volume
|
2020-12-06 21:57:32 +03:00
|
|
|
verbatimDisk =
|
|
|
|
do
|
|
|
|
verbatim
|
|
|
|
disk <- disk
|
|
|
|
pure disk
|
2020-05-20 17:36:50 +03:00
|
|
|
|
2021-08-06 12:03:13 +03:00
|
|
|
parseVolume : Grammar state PathToken True Volume
|
2020-12-06 21:57:32 +03:00
|
|
|
parseVolume =
|
|
|
|
verbatimUnc
|
|
|
|
<|> verbatimDisk
|
|
|
|
<|> unc
|
|
|
|
<|> disk
|
2020-05-20 17:36:50 +03:00
|
|
|
|
2021-08-06 12:03:13 +03:00
|
|
|
parseBody : Grammar state PathToken True Body
|
2020-12-06 21:57:32 +03:00
|
|
|
parseBody =
|
2021-01-16 10:03:45 +03:00
|
|
|
do
|
2020-12-06 21:57:32 +03:00
|
|
|
text <- match PTText
|
2021-06-28 14:49:33 +03:00
|
|
|
pure $ case text of
|
|
|
|
".." => ParentDir
|
|
|
|
"." => CurDir
|
|
|
|
normal => Normal normal
|
2020-05-20 17:36:50 +03:00
|
|
|
|
2021-08-06 12:03:13 +03:00
|
|
|
parsePath : Grammar state PathToken False Path
|
2020-12-06 21:57:32 +03:00
|
|
|
parsePath =
|
|
|
|
do
|
|
|
|
vol <- optional parseVolume
|
|
|
|
root <- optional (some bodySeparator)
|
|
|
|
body <- sepBy (some bodySeparator) parseBody
|
|
|
|
trailSep <- optional (some bodySeparator)
|
2020-12-07 06:36:30 +03:00
|
|
|
let body = filter (\case Normal s => ltrim s /= ""; _ => True) body
|
2020-12-06 21:57:32 +03:00
|
|
|
let body = case body of
|
|
|
|
[] => []
|
|
|
|
(x::xs) => x :: delete CurDir xs
|
|
|
|
pure $ MkPath vol (isJust root) body (isJust trailSep)
|
|
|
|
|
2021-01-14 00:26:42 +03:00
|
|
|
||| Parses a String into Path.
|
2020-05-20 17:36:50 +03:00
|
|
|
|||
|
2021-01-16 10:03:45 +03:00
|
|
|
||| The string is parsed as much as possible from left to right, and the invalid
|
2020-12-06 21:57:32 +03:00
|
|
|
||| parts on the right is ignored.
|
2020-05-20 17:36:50 +03:00
|
|
|
|||
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Some kind of invalid paths are accepted. The relax rules:
|
2020-05-20 17:36:50 +03:00
|
|
|
|||
|
2020-12-06 21:57:32 +03:00
|
|
|
||| - Both slash('/') and backslash('\\') are parsed as valid directory separator,
|
|
|
|
||| regardless of the platform;
|
|
|
|
||| - Any characters in the body in allowed, e.g., glob like "/root/*";
|
|
|
|
||| - Verbatim prefix(`\\?\`) that disables the forward slash is ignored (for
|
|
|
|
||| Windows only).
|
2020-12-06 23:22:03 +03:00
|
|
|
||| - Repeated separators are ignored, therefore, "a/b" and "a//b" both have "a"
|
2020-05-30 16:51:12 +03:00
|
|
|
||| and "b" as bodies.
|
2020-12-06 21:57:32 +03:00
|
|
|
||| - "." in the body are removed, unless they are at the beginning of the path.
|
|
|
|
||| For example, "a/./b", "a/b/", "a/b/." and "a/b" will have "a" and "b" as
|
|
|
|
||| bodies, and "./a/b" will starts with `CurDir`.
|
2020-05-20 17:36:50 +03:00
|
|
|
|||
|
|
|
|
||| ```idris example
|
|
|
|
||| parse "C:\\Windows/System32"
|
|
|
|
||| parse "/usr/local/etc/*"
|
|
|
|
||| ```
|
|
|
|
export
|
2020-05-30 16:51:12 +03:00
|
|
|
parse : String -> Path
|
2020-12-06 21:57:32 +03:00
|
|
|
parse str =
|
|
|
|
case parse parsePath (lexPath str) of
|
|
|
|
Right (path, _) => path
|
|
|
|
_ => emptyPath
|
2020-05-30 16:51:12 +03:00
|
|
|
|
|
|
|
--------------------------------------------------------------------------------
|
|
|
|
-- Utils
|
|
|
|
--------------------------------------------------------------------------------
|
|
|
|
|
|
|
|
isAbsolute' : Path -> Bool
|
2020-12-06 21:57:32 +03:00
|
|
|
isAbsolute' path =
|
|
|
|
if isWindows then
|
|
|
|
case path.volume of
|
|
|
|
Just (UNC _ _) => True
|
|
|
|
Just (Disk _) => path.hasRoot
|
|
|
|
Nothing => False
|
|
|
|
else
|
|
|
|
path.hasRoot
|
2020-05-30 16:51:12 +03:00
|
|
|
|
|
|
|
append' : (left : Path) -> (right : Path) -> Path
|
2020-12-06 21:57:32 +03:00
|
|
|
append' left right =
|
|
|
|
if isAbsolute' right || isJust right.volume then
|
|
|
|
right
|
|
|
|
else if hasRoot right then
|
|
|
|
record { volume = left.volume } right
|
2021-01-16 10:03:45 +03:00
|
|
|
else
|
2020-12-06 21:57:32 +03:00
|
|
|
record { body = left.body ++ right.body, hasTrailSep = right.hasTrailSep } left
|
2020-05-30 16:51:12 +03:00
|
|
|
|
2020-12-07 00:18:58 +03:00
|
|
|
splitPath' : Path -> List Path
|
|
|
|
splitPath' path =
|
|
|
|
case splitRoot path of
|
|
|
|
(Just root, other) => root :: iterateBody (path.body) (path.hasTrailSep)
|
|
|
|
(Nothing, other) => iterateBody (path.body) (path.hasTrailSep)
|
|
|
|
where
|
|
|
|
splitRoot : Path -> (Maybe Path, Path)
|
|
|
|
splitRoot path@(MkPath Nothing False _ _) = (Nothing, path)
|
|
|
|
splitRoot (MkPath vol root xs trailSep) =
|
|
|
|
(Just $ MkPath vol root [] False, MkPath Nothing False xs trailSep)
|
|
|
|
|
|
|
|
iterateBody : List Body -> (trailSep : Bool) -> List Path
|
|
|
|
iterateBody [] _ = []
|
|
|
|
iterateBody [x] trailSep = [MkPath Nothing False [x] trailSep]
|
|
|
|
iterateBody (x::y::xs) trailSep =
|
|
|
|
(MkPath Nothing False [x] False) :: iterateBody (y::xs) trailSep
|
|
|
|
|
2020-05-30 16:51:12 +03:00
|
|
|
splitParent' : Path -> Maybe (Path, Path)
|
2020-12-07 00:18:58 +03:00
|
|
|
splitParent' path =
|
|
|
|
case path.body of
|
|
|
|
[] => Nothing
|
2021-01-16 10:03:45 +03:00
|
|
|
(x::xs) =>
|
2020-12-07 00:18:58 +03:00
|
|
|
let
|
|
|
|
parent = record { body = init (x::xs), hasTrailSep = False } path
|
2021-01-16 10:03:45 +03:00
|
|
|
child = MkPath Nothing False [last (x::xs)] path.hasTrailSep
|
2020-12-07 00:18:58 +03:00
|
|
|
in
|
|
|
|
Just (parent, child)
|
2020-05-30 16:51:12 +03:00
|
|
|
|
|
|
|
parent' : Path -> Maybe Path
|
2021-01-14 00:05:59 +03:00
|
|
|
parent' = map fst . splitParent'
|
2020-05-30 16:51:12 +03:00
|
|
|
|
|
|
|
fileName' : Path -> Maybe String
|
2020-12-06 21:57:32 +03:00
|
|
|
fileName' path =
|
|
|
|
findNormal $ reverse path.body
|
|
|
|
where
|
|
|
|
findNormal : List Body -> Maybe String
|
|
|
|
findNormal ((Normal normal)::xs) = Just normal
|
|
|
|
findNormal (CurDir::xs) = findNormal xs
|
|
|
|
findNormal _ = Nothing
|
2021-01-16 10:03:45 +03:00
|
|
|
|
2020-05-30 16:51:12 +03:00
|
|
|
setFileName' : (name : String) -> Path -> Path
|
2020-12-06 21:57:32 +03:00
|
|
|
setFileName' name path =
|
|
|
|
if isJust (fileName' path) then
|
|
|
|
append' (fromMaybe emptyPath $ parent' path) (parse name)
|
|
|
|
else
|
|
|
|
append' path (parse name)
|
2021-01-16 10:03:45 +03:00
|
|
|
|
2021-04-15 16:08:50 +03:00
|
|
|
export
|
2020-05-30 16:51:12 +03:00
|
|
|
splitFileName : String -> (String, String)
|
2020-12-06 21:57:32 +03:00
|
|
|
splitFileName name =
|
|
|
|
case break (== '.') $ reverse $ unpack name of
|
|
|
|
(_, []) => (name, "")
|
|
|
|
(_, ['.']) => (name, "")
|
|
|
|
(revExt, (dot :: revStem)) =>
|
|
|
|
((pack $ reverse revStem), (pack $ reverse revExt))
|
2020-05-30 16:51:12 +03:00
|
|
|
|
|
|
|
--------------------------------------------------------------------------------
|
2020-12-06 21:57:32 +03:00
|
|
|
-- Methods
|
2020-05-30 16:51:12 +03:00
|
|
|
--------------------------------------------------------------------------------
|
|
|
|
|
|
|
|
||| Returns true if the path is absolute.
|
|
|
|
|||
|
2020-12-06 21:57:32 +03:00
|
|
|
||| - On Unix, a path is absolute if it starts with the root, so `isAbsolute` and
|
|
|
|
||| `hasRoot` are equivalent.
|
2020-05-30 16:51:12 +03:00
|
|
|
|||
|
2020-12-06 23:22:03 +03:00
|
|
|
||| - On Windows, a path is absolute if it starts with a disk and has root or
|
|
|
|
||| starts with UNC. For example, `c:\\windows` is absolute, while `c:temp`
|
|
|
|
||| and `\temp` are not.
|
2020-05-30 16:51:12 +03:00
|
|
|
export
|
|
|
|
isAbsolute : String -> Bool
|
2021-01-14 00:05:59 +03:00
|
|
|
isAbsolute = isAbsolute' . parse
|
2020-05-30 16:51:12 +03:00
|
|
|
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Returns true if the path is relative.
|
2020-05-30 16:51:12 +03:00
|
|
|
export
|
|
|
|
isRelative : String -> Bool
|
|
|
|
isRelative = not . isAbsolute
|
|
|
|
|
2021-04-15 16:08:50 +03:00
|
|
|
||| Appends the right path to the left path.
|
|
|
|
|||
|
|
|
|
||| 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
|
|
|
|
||| parse "/usr" /> "local/etc" == "/usr/local/etc"
|
|
|
|
||| ```
|
|
|
|
export
|
|
|
|
(/>) : (left : Path) -> (right : String) -> Path
|
|
|
|
(/>) left right = append' left (parse right)
|
|
|
|
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Appends the right path to the left path.
|
2020-05-30 16:51:12 +03:00
|
|
|
|||
|
|
|
|
||| If the path on the right is absolute, it replaces the left path.
|
|
|
|
|||
|
|
|
|
||| On Windows:
|
|
|
|
|||
|
2020-12-06 21:57:32 +03:00
|
|
|
||| - If the right path has a root but no volume (e.g., `\windows`), it replaces
|
|
|
|
||| everything except for the volume (if any) of left.
|
2020-05-30 16:51:12 +03:00
|
|
|
||| - If the right path has a volume but no root, it replaces left.
|
|
|
|
|||
|
|
|
|
||| ```idris example
|
2020-12-06 21:57:32 +03:00
|
|
|
||| "/usr" </> "local/etc" == "/usr/local/etc"
|
2020-05-30 16:51:12 +03:00
|
|
|
||| ```
|
|
|
|
export
|
|
|
|
(</>) : (left : String) -> (right : String) -> String
|
2021-04-15 16:08:50 +03:00
|
|
|
(</>) left right = show $ parse left /> right
|
2020-05-30 16:51:12 +03:00
|
|
|
|
2021-01-14 00:26:42 +03:00
|
|
|
||| Joins path components into one.
|
2020-05-20 17:36:50 +03:00
|
|
|
|||
|
|
|
|
||| ```idris example
|
2020-05-30 16:51:12 +03:00
|
|
|
||| joinPath ["/usr", "local/etc"] == "/usr/local/etc"
|
2020-05-20 17:36:50 +03:00
|
|
|
||| ```
|
|
|
|
export
|
2020-05-30 16:51:12 +03:00
|
|
|
joinPath : List String -> String
|
2021-04-15 16:08:50 +03:00
|
|
|
joinPath xs = show $ foldl (/>) (parse "") xs
|
2020-05-30 16:51:12 +03:00
|
|
|
|
2021-01-14 00:26:42 +03:00
|
|
|
||| Splits path into components.
|
2020-12-06 21:57:32 +03:00
|
|
|
|||
|
|
|
|
||| ```idris example
|
|
|
|
||| splitPath "/usr/local/etc" == ["/", "usr", "local", "etc"]
|
2020-12-07 00:18:58 +03:00
|
|
|
||| splitPath "tmp/Foo.idr" == ["tmp", "Foo.idr"]
|
2020-12-06 21:57:32 +03:00
|
|
|
||| ```
|
|
|
|
export
|
|
|
|
splitPath : String -> List String
|
2021-01-14 00:05:59 +03:00
|
|
|
splitPath = map show . splitPath' . parse
|
2020-12-06 21:57:32 +03:00
|
|
|
|
2021-01-14 00:26:42 +03:00
|
|
|
||| Splits the path into parent and child.
|
2020-05-30 16:51:12 +03:00
|
|
|
|||
|
|
|
|
||| ```idris example
|
|
|
|
||| splitParent "/usr/local/etc" == Just ("/usr/local", "etc")
|
|
|
|
||| ```
|
|
|
|
export
|
|
|
|
splitParent : String -> Maybe (String, String)
|
2020-12-06 21:57:32 +03:00
|
|
|
splitParent path =
|
|
|
|
do
|
|
|
|
(parent, child) <- splitParent' (parse path)
|
|
|
|
pure (show parent, show child)
|
2020-05-30 16:51:12 +03:00
|
|
|
|
2021-01-14 00:26:42 +03:00
|
|
|
||| Returns the path without its final component, if there is one.
|
2020-05-30 16:51:12 +03:00
|
|
|
|||
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Returns Nothing if the path terminates by a root or volume.
|
2020-05-30 16:51:12 +03:00
|
|
|
export
|
|
|
|
parent : String -> Maybe String
|
2021-01-16 10:03:45 +03:00
|
|
|
parent = map show . parent' . parse
|
2020-05-30 16:51:12 +03:00
|
|
|
|
2021-01-14 00:26:42 +03:00
|
|
|
||| Returns the list of all parents of the path, longest first, self included.
|
2020-05-30 16:51:12 +03:00
|
|
|
|||
|
|
|
|
||| ```idris example
|
|
|
|
||| parents "/etc/kernel" == ["/etc/kernel", "/etc", "/"]
|
|
|
|
||| ```
|
|
|
|
export
|
|
|
|
parents : String -> List String
|
2021-01-14 00:05:59 +03:00
|
|
|
parents = map show . List.iterate parent' . parse
|
2020-05-30 16:51:12 +03:00
|
|
|
|
2021-01-14 00:26:42 +03:00
|
|
|
||| Determines whether the base is one of the parents of target.
|
2020-05-30 16:51:12 +03:00
|
|
|
|||
|
|
|
|
||| Trailing separator is ignored.
|
2020-12-07 06:36:30 +03:00
|
|
|
|||
|
|
|
|
||| ```idris example
|
|
|
|
||| "/etc" `isBaseOf` "/etc/kernel"
|
|
|
|
||| ```
|
2020-05-30 16:51:12 +03:00
|
|
|
export
|
2020-12-07 06:36:30 +03:00
|
|
|
isBaseOf : (base : String) -> (target : String) -> Bool
|
|
|
|
isBaseOf base target =
|
2021-01-16 10:03:45 +03:00
|
|
|
let
|
2020-12-07 06:36:30 +03:00
|
|
|
MkPath baseVol baseRoot baseBody _ = parse base
|
|
|
|
MkPath targetVol targetRoot targetBody _ = parse target
|
|
|
|
in
|
|
|
|
baseVol == targetVol
|
|
|
|
&& baseRoot == targetRoot
|
|
|
|
&& (baseBody `isPrefixOf` targetBody)
|
2020-05-30 16:51:12 +03:00
|
|
|
|
2021-01-14 00:26:42 +03:00
|
|
|
||| Returns a path that, when appended to base, yields target.
|
2020-05-30 16:51:12 +03:00
|
|
|
|||
|
2020-12-07 06:36:30 +03:00
|
|
|
||| Returns Nothing if the base is not a prefix of the target.
|
2020-05-30 16:51:12 +03:00
|
|
|
export
|
2020-12-07 06:36:30 +03:00
|
|
|
dropBase : (base : String) -> (target : String) -> Maybe String
|
|
|
|
dropBase base target =
|
2020-12-06 21:57:32 +03:00
|
|
|
do
|
|
|
|
let MkPath baseVol baseRoot baseBody _ = parse base
|
|
|
|
let MkPath targetVol targetRoot targetBody targetTrialSep = parse target
|
|
|
|
if baseVol == targetVol && baseRoot == targetRoot then Just () else Nothing
|
2020-12-07 06:36:30 +03:00
|
|
|
body <- dropBody baseBody targetBody
|
2020-12-06 21:57:32 +03:00
|
|
|
pure $ show $ MkPath Nothing False body targetTrialSep
|
2020-05-30 16:51:12 +03:00
|
|
|
where
|
2020-12-07 06:36:30 +03:00
|
|
|
dropBody : (base : List Body) -> (target : List Body) -> Maybe (List Body)
|
|
|
|
dropBody [] ys = Just ys
|
|
|
|
dropBody xs [] = Nothing
|
|
|
|
dropBody (x::xs) (y::ys) = if x == y then dropBody xs ys else Nothing
|
2020-05-30 16:51:12 +03:00
|
|
|
|
2020-12-06 21:57:32 +03:00
|
|
|
||| Returns the last body of the path.
|
2020-05-30 16:51:12 +03:00
|
|
|
|||
|
2021-01-16 10:03:45 +03:00
|
|
|
||| If the last body is a file, this is the file name;
|
|
|
|
||| if it's a directory, this is the directory name;
|
2020-12-06 21:57:32 +03:00
|
|
|
||| if it's ".", it recurses on the previous body;
|
|
|
|
||| if it's "..", returns Nothing.
|
2020-05-30 16:51:12 +03:00
|
|
|
export
|
|
|
|
fileName : String -> Maybe String
|
2021-01-14 00:05:59 +03:00
|
|
|
fileName = fileName' . parse
|
2020-05-30 16:51:12 +03:00
|
|
|
|
2021-01-14 00:26:42 +03:00
|
|
|
||| Extracts the file name in the path without extension.
|
2020-05-30 16:51:12 +03:00
|
|
|
|||
|
|
|
|
||| The stem is:
|
|
|
|
|||
|
|
|
|
||| - Nothing, if there is no file name;
|
|
|
|
||| - The entire file name if there is no embedded ".";
|
2020-12-06 21:57:32 +03:00
|
|
|
||| - The entire file name if the file name begins with a "." and has no other ".";
|
|
|
|
||| - Otherwise, the portion of the file name before the last ".".
|
2020-05-30 16:51:12 +03:00
|
|
|
export
|
|
|
|
fileStem : String -> Maybe String
|
2020-12-06 21:57:32 +03:00
|
|
|
fileStem path = pure $ fst $ splitFileName !(fileName path)
|
2020-05-30 16:51:12 +03:00
|
|
|
|
2021-01-14 00:26:42 +03:00
|
|
|
||| Extracts the extension of the file name in the path.
|
2020-05-30 16:51:12 +03:00
|
|
|
|||
|
|
|
|
||| The extension is:
|
|
|
|
|||
|
|
|
|
||| - Nothing, if there is no file name;
|
|
|
|
||| - Nothing, if there is no embedded ".";
|
2020-12-06 21:57:32 +03:00
|
|
|
||| - Nothing, if the file name begins with a "." and has no other ".";
|
|
|
|
||| - Otherwise, the portion of the file name after the last ".".
|
2020-05-30 16:51:12 +03:00
|
|
|
export
|
|
|
|
extension : String -> Maybe String
|
2021-04-25 11:13:55 +03:00
|
|
|
extension path = fileName path >>=
|
|
|
|
filter (/= "") . Just . snd . splitFileName
|
2020-05-30 16:51:12 +03:00
|
|
|
|
2021-01-14 00:26:42 +03:00
|
|
|
||| Updates the file name in the path.
|
2020-05-30 16:51:12 +03:00
|
|
|
|||
|
2020-12-06 21:57:32 +03:00
|
|
|
||| If there is no file name, it appends the name to the path;
|
|
|
|
||| otherwise, it appends the name to the parent of the path.
|
2020-05-30 16:51:12 +03:00
|
|
|
export
|
|
|
|
setFileName : (name : String) -> String -> String
|
2020-12-06 21:57:32 +03:00
|
|
|
setFileName name path = show $ setFileName' name (parse path)
|
2020-05-30 16:51:12 +03:00
|
|
|
|
2021-01-14 00:26:42 +03:00
|
|
|
||| Appends a extension to the path.
|
2020-05-30 16:51:12 +03:00
|
|
|
|||
|
2020-12-06 21:57:32 +03:00
|
|
|
||| If there is no file name, the path will not change;
|
|
|
|
||| if the path has no extension, the extension will be appended;
|
|
|
|
||| if the given extension is empty, the extension of the path will be dropped;
|
|
|
|
||| otherwise, the extension will be replaced.
|
2020-05-30 16:51:12 +03:00
|
|
|
|||
|
2020-12-06 21:57:32 +03:00
|
|
|
||| ```idris example
|
|
|
|
||| "/tmp/Foo" <.> "idr" == "/tmp/Foo.idr"
|
|
|
|
||| ```
|
|
|
|
export
|
|
|
|
(<.>) : String -> (extension : String) -> String
|
|
|
|
(<.>) path ext =
|
2021-01-16 10:03:45 +03:00
|
|
|
let
|
2020-12-06 21:57:32 +03:00
|
|
|
path' = parse path
|
|
|
|
ext = pack $ dropWhile (\char => char == '.' || isSpace char) (unpack ext)
|
|
|
|
ext = if ext == "" then "" else "." ++ ext
|
|
|
|
in
|
|
|
|
case fileName' path' of
|
2021-01-16 10:03:45 +03:00
|
|
|
Just name =>
|
2020-12-06 21:57:32 +03:00
|
|
|
let (stem, _) = splitFileName name in
|
|
|
|
show $ setFileName' (stem ++ ext) path'
|
|
|
|
Nothing => path
|
|
|
|
|
2021-01-14 00:26:42 +03:00
|
|
|
||| Drops the extension of the path.
|
2020-05-30 16:51:12 +03:00
|
|
|
export
|
2020-12-06 21:57:32 +03:00
|
|
|
dropExtension : String -> String
|
2020-12-06 23:11:44 +03:00
|
|
|
dropExtension path = path <.> ""
|