System.Path


   0 | module System.Path
   1 | 
   2 | import Data.List
   3 | import Data.Maybe
   4 | import Data.Nat
   5 | import Data.String
   6 | import Data.String.Extra
   7 | 
   8 | import Text.Token
   9 | import Text.Lexer
  10 | import Text.Parser
  11 | import Text.Quantity
  12 | 
  13 | import System.Info
  14 | 
  15 | export infixl 5 </>, />
  16 | export infixr 7 <.>
  17 | 
  18 | 
  19 | ||| The character that separates directories in the path.
  20 | export
  21 | dirSeparator : Char
  22 | dirSeparator = if isWindows then '\\' else '/'
  23 | 
  24 | ||| The character that separates multiple paths.
  25 | export
  26 | pathSeparator : Char
  27 | pathSeparator = if isWindows then ';' else ':'
  28 | 
  29 | ||| Windows path prefix.
  30 | public export
  31 | data Volume
  32 |   =
  33 |   ||| Windows Uniform Naming Convention, consisting of server name and share
  34 |   ||| directory.
  35 |   |||
  36 |   ||| Example: `\\localhost\share`
  37 |   UNC String String |
  38 |   ||| The drive.
  39 |   |||
  40 |   ||| Example: `C:`
  41 |   Disk Char
  42 | 
  43 | ||| A single body in path.
  44 | public export
  45 | data Body
  46 |   =
  47 |   ||| Represents ".".
  48 |   CurDir |
  49 |   ||| Represents "..".
  50 |   ParentDir |
  51 |   ||| Directory or file.
  52 |   Normal String
  53 | 
  54 | ||| A parsed cross-platform file system path.
  55 | |||
  56 | ||| Use the function `parse` to constructs a Path from String, and use the
  57 | ||| function `show` to convert in reverse.
  58 | |||
  59 | ||| Trailing separator is only used for display and is ignored when comparing
  60 | ||| paths.
  61 | public export
  62 | record Path where
  63 |     constructor MkPath
  64 |     ||| Windows path prefix (only for Windows).
  65 |     volume : Maybe Volume
  66 |     ||| Whether the path contains root.
  67 |     hasRoot : Bool
  68 |     ||| Path bodies.
  69 |     body : List Body
  70 |     ||| Whether the path terminates with a separator.
  71 |     hasTrailSep : Bool
  72 | 
  73 | export
  74 | Eq Volume where
  75 |   (==) (UNC l1 l2) (UNC r1 r2) = l1 == r1 && r1 == r2
  76 |   (==) (Disk l) (Disk r) = l == r
  77 |   (==) _ _ = False
  78 | 
  79 | export
  80 | Eq Body where
  81 |   (==) CurDir CurDir = True
  82 |   (==) ParentDir ParentDir = True
  83 |   (==) (Normal l) (Normal r) = l == r
  84 |   (==) _ _ = False
  85 | 
  86 | export
  87 | Eq Path where
  88 |   (==) (MkPath l1 l2 l3 _) (MkPath r1 r2 r3 _) =
  89 |     l1 == r1 && l2 == r2 && l3 == r3
  90 | 
  91 | ||| An empty path, which represents "".
  92 | public export
  93 | emptyPath : Path
  94 | emptyPath = MkPath Nothing False [] False
  95 | 
  96 | --------------------------------------------------------------------------------
  97 | -- Show
  98 | --------------------------------------------------------------------------------
  99 | 
 100 | export
 101 | Show Body where
 102 |   show CurDir = "."
 103 |   show ParentDir = ".."
 104 |   show (Normal normal) = normal
 105 | 
 106 | export
 107 | Show Volume where
 108 |   show (UNC server share) = "\\\\" ++ server ++ "\\" ++ share
 109 |   show (Disk disk) = String.singleton disk ++ ":"
 110 | 
 111 | ||| Displays the path in the format of this platform.
 112 | export
 113 | Show Path where
 114 |   show path =
 115 |     let
 116 |       sep = String.singleton dirSeparator
 117 |       showVol = maybe "" show path.volume
 118 |       showRoot = if path.hasRoot then sep else ""
 119 |       showBody = join sep $ map show path.body
 120 |       showTrail = if path.hasTrailSep then sep else ""
 121 |     in
 122 |       showVol ++ showRoot ++ showBody ++ showTrail
 123 | 
 124 | --------------------------------------------------------------------------------
 125 | -- Parser
 126 | --------------------------------------------------------------------------------
 127 | 
 128 | data PathTokenKind = PTText | PTPunct Char
 129 | 
 130 | Eq PathTokenKind where
 131 |   (==) PTText PTText = True
 132 |   (==) (PTPunct c1) (PTPunct c2) = c1 == c2
 133 |   (==) _ _ = False
 134 | 
 135 | PathToken : Type
 136 | PathToken = Token PathTokenKind
 137 | 
 138 | TokenKind PathTokenKind where
 139 |   TokType PTText = String
 140 |   TokType (PTPunct _) = ()
 141 | 
 142 |   tokValue PTText x = x
 143 |   tokValue (PTPunct _) _ = ()
 144 | 
 145 | pathTokenMap : TokenMap PathToken
 146 | pathTokenMap = toTokenMap $
 147 |   [ (is '/', PTPunct '/')
 148 |   , (is '\\', PTPunct '\\')
 149 |   , (is ':', PTPunct ':')
 150 |   , (is '?', PTPunct '?')
 151 |   , (some $ non $ oneOf "/\\:?", PTText)
 152 |   ]
 153 | 
 154 | lexPath : String -> List (WithBounds PathToken)
 155 | lexPath str =
 156 |   let
 157 |     (tokens, _, _, _) = lex pathTokenMap str
 158 |   in
 159 |     tokens -- TokenData.tok tokens
 160 | 
 161 | -- match both '/' and '\\' regardless of the platform.
 162 | bodySeparator : Grammar state PathToken True ()
 163 | bodySeparator = (match $ PTPunct '\\') <|> (match $ PTPunct '/')
 164 | 
 165 | -- Windows will automatically translate '/' to '\\'. And the verbatim prefix,
 166 | -- i.e., `\\?\`, can be used to disable the translation.
 167 | -- However, we just parse it and ignore it.
 168 | --
 169 | -- Example: \\?\
 170 | verbatim : Grammar state PathToken True ()
 171 | verbatim =
 172 |   do
 173 |     ignore $ count (exactly 2) $ match $ PTPunct '\\'
 174 |     match $ PTPunct '?'
 175 |     match $ PTPunct '\\'
 176 |     pure ()
 177 | 
 178 | -- Example: \\server\share
 179 | unc : Grammar state PathToken True Volume
 180 | unc =
 181 |   do
 182 |     ignore $ count (exactly 2) $ match $ PTPunct '\\'
 183 |     server <- match PTText
 184 |     bodySeparator
 185 |     share <- match PTText
 186 |     pure $ UNC server share
 187 | 
 188 | -- Example: \\?\server\share
 189 | verbatimUnc : Grammar state PathToken True Volume
 190 | verbatimUnc =
 191 |   do
 192 |     verbatim
 193 |     server <- match PTText
 194 |     bodySeparator
 195 |     share <- match PTText
 196 |     pure $ UNC server share
 197 | 
 198 | -- Example: C:
 199 | disk : Grammar state PathToken True Volume
 200 | disk =
 201 |   do
 202 |     text <- match PTText
 203 |     disk <- case unpack text of
 204 |               (disk :: xs) => pure disk
 205 |               [] => fail "Expects disk"
 206 |     match $ PTPunct ':'
 207 |     pure $ Disk (toUpper disk)
 208 | 
 209 | -- Example: \\?\C:
 210 | verbatimDisk : Grammar state PathToken True Volume
 211 | verbatimDisk =
 212 |   do
 213 |     verbatim
 214 |     disk <- disk
 215 |     pure disk
 216 | 
 217 | parseVolume : Grammar state PathToken True Volume
 218 | parseVolume =
 219 |       verbatimUnc
 220 |   <|> verbatimDisk
 221 |   <|> unc
 222 |   <|> disk
 223 | 
 224 | parseBody : Grammar state PathToken True Body
 225 | parseBody =
 226 |   do
 227 |     text <- match PTText
 228 |     pure $ case text of
 229 |       ".." => ParentDir
 230 |       "." => CurDir
 231 |       normal => Normal normal
 232 | 
 233 | parsePath : Grammar state PathToken False Path
 234 | parsePath =
 235 |   do
 236 |     vol <- optional parseVolume
 237 |     root <- optional (some bodySeparator)
 238 |     body <- sepBy (some bodySeparator) parseBody
 239 |     trailSep <- optional (some bodySeparator)
 240 |     let body = filter (\case Normal s => ltrim s /= ""; _ => True) body
 241 |     let body = case body of
 242 |                 [] => []
 243 |                 (x::xs) => x :: delete CurDir xs
 244 |     pure $ MkPath vol (isJust root) body (isJust trailSep)
 245 | 
 246 | export
 247 | tryParse : String -> Maybe Path
 248 | tryParse str =
 249 |   case parse parsePath (lexPath str) of
 250 |     Right (path, []) => Just path
 251 |     _ => Nothing
 252 | 
 253 | ||| Parses a String into Path.
 254 | |||
 255 | ||| The string is parsed as much as possible from left to right, and the invalid
 256 | ||| parts on the right is ignored.
 257 | |||
 258 | ||| Some kind of invalid paths are accepted. The relax rules:
 259 | |||
 260 | ||| - Both slash('/') and backslash('\\') are parsed as valid directory separator,
 261 | |||   regardless of the platform;
 262 | ||| - Any characters in the body in allowed, e.g., glob like "/root/*";
 263 | ||| - Verbatim prefix(`\\?\`) that disables the forward slash is ignored (for
 264 | |||   Windows only).
 265 | ||| - Repeated separators are ignored, therefore, "a/b" and "a//b" both have "a"
 266 | |||   and "b" as bodies.
 267 | ||| - "." in the body are removed, unless they are at the beginning of the path.
 268 | |||   For example, "a/./b", "a/b/", "a/b/." and "a/b" will have "a" and "b" as
 269 | |||   bodies, and "./a/b" will starts with `CurDir`.
 270 | |||
 271 | ||| ```idris example
 272 | ||| parse "C:\\Windows/System32"
 273 | ||| parse "/usr/local/etc/*"
 274 | ||| ```
 275 | export
 276 | parse : String -> Path
 277 | parse str =
 278 |   case parse parsePath (lexPath str) of
 279 |     Right (path, _) => path
 280 |     _ => emptyPath
 281 | 
 282 | --------------------------------------------------------------------------------
 283 | -- Utils
 284 | --------------------------------------------------------------------------------
 285 | 
 286 | isAbsolute' : Path -> Bool
 287 | isAbsolute' path =
 288 |   if isWindows then
 289 |     case path.volume of
 290 |       Just (UNC _ _) => True
 291 |       Just (Disk _) => path.hasRoot
 292 |       Nothing => False
 293 |   else
 294 |     path.hasRoot
 295 | 
 296 | append' : (left : Path) -> (right : Path) -> Path
 297 | append' left right =
 298 |   if isAbsolute' right || isJust right.volume then
 299 |     right
 300 |   else if hasRoot right then
 301 |     { volume := left.volume } right
 302 |   else
 303 |     { body := left.body ++ right.body, hasTrailSep := right.hasTrailSep } left
 304 | 
 305 | splitPath' : Path -> List Path
 306 | splitPath' path =
 307 |   case splitRoot path of
 308 |     (Just root, other) => root :: iterateBody (path.body) (path.hasTrailSep)
 309 |     (Nothing, other) => iterateBody (path.body) (path.hasTrailSep)
 310 |   where
 311 |     splitRoot : Path -> (Maybe Path, Path)
 312 |     splitRoot path@(MkPath Nothing False _ _) = (Nothing, path)
 313 |     splitRoot (MkPath vol root xs trailSep) =
 314 |       (Just $ MkPath vol root [] False, MkPath Nothing False xs trailSep)
 315 | 
 316 |     iterateBody : List Body -> (trailSep : Bool) -> List Path
 317 |     iterateBody [] _ = []
 318 |     iterateBody [x] trailSep = [MkPath Nothing False [x] trailSep]
 319 |     iterateBody (x::y::xs) trailSep =
 320 |       (MkPath Nothing False [x] False) :: iterateBody (y::xs) trailSep
 321 | 
 322 | splitParent' : Path -> Maybe (Path, Path)
 323 | splitParent' path =
 324 |   case path.body of
 325 |     [] => Nothing
 326 |     (x::xs) =>
 327 |       let
 328 |         parent = { body := init (x::xs), hasTrailSep := False } path
 329 |         child = MkPath Nothing False [last (x::xs)] path.hasTrailSep
 330 |       in
 331 |         Just (parent, child)
 332 | 
 333 | parent' : Path -> Maybe Path
 334 | parent' = map fst . splitParent'
 335 | 
 336 | fileName' : Path -> Maybe String
 337 | fileName' path =
 338 |   findNormal $ reverse path.body
 339 | where
 340 |   findNormal : List Body -> Maybe String
 341 |   findNormal ((Normal normal)::xs) = Just normal
 342 |   findNormal (CurDir::xs) = findNormal xs
 343 |   findNormal _ = Nothing
 344 | 
 345 | setFileName' : (name : String) -> Path -> Path
 346 | setFileName' name path =
 347 |   if isJust (fileName' path) then
 348 |     append' (fromMaybe emptyPath $ parent' path) (parse name)
 349 |   else
 350 |     append' path (parse name)
 351 | 
 352 | export
 353 | splitFileName : String -> (String, String)
 354 | splitFileName name =
 355 |   case break (== '.') $ reverse $ unpack name of
 356 |     (_, []) => (name, "")
 357 |     (_, ['.']) => (name, "")
 358 |     (revExt, (dot :: revStem)) =>
 359 |       ((pack $ reverse revStem), (pack $ reverse revExt))
 360 | 
 361 | ||| Split a file name into a basename and a list of extensions.
 362 | ||| A leading dot is considered to be part of the basename.
 363 | ||| ```
 364 | ||| splitExtensions "Path.idr"           = ("Path", ["idr"])
 365 | ||| splitExtensions "file.latex.lidr"    = ("file", ["latex", "lidr"])
 366 | ||| splitExtensions ".hidden.latex.lidr" = (".hidden", ["latex", "lidr"])
 367 | ||| ```
 368 | export
 369 | splitExtensions : String -> (String, List String)
 370 | splitExtensions name = case map pack $ split (== '.') (unpack name) of
 371 |   ("" ::: base :: exts) => ("." ++ base, exts)
 372 |   (base ::: exts) => (base, exts)
 373 | 
 374 | --------------------------------------------------------------------------------
 375 | -- Methods
 376 | --------------------------------------------------------------------------------
 377 | 
 378 | ||| Returns true if the path is absolute.
 379 | |||
 380 | ||| - On Unix, a path is absolute if it starts with the root, so `isAbsolute` and
 381 | |||   `hasRoot` are equivalent.
 382 | |||
 383 | ||| - On Windows, a path is absolute if it starts with a disk and has root or
 384 | |||   starts with UNC. For example, `c:\\windows` is absolute, while `c:temp`
 385 | |||   and `\temp` are not.
 386 | export
 387 | isAbsolute : String -> Bool
 388 | isAbsolute = isAbsolute' . parse
 389 | 
 390 | ||| Returns true if the path is relative.
 391 | export
 392 | isRelative : String -> Bool
 393 | isRelative = not . isAbsolute
 394 | 
 395 | ||| Appends the right path to the left path.
 396 | |||
 397 | ||| If the path on the right is absolute, it replaces the left path.
 398 | |||
 399 | ||| On Windows:
 400 | |||
 401 | ||| - If the right path has a root but no volume (e.g., `\windows`), it replaces
 402 | |||   everything except for the volume (if any) of left.
 403 | ||| - If the right path has a volume but no root, it replaces left.
 404 | |||
 405 | ||| ```idris example
 406 | ||| parse "/usr" /> "local/etc" == "/usr/local/etc"
 407 | ||| ```
 408 | export
 409 | (/>) : (left : Path) -> (right : String) -> Path
 410 | (/>) left right = append' left (parse right)
 411 | 
 412 | ||| Appends the right path to the left path.
 413 | |||
 414 | ||| If the path on the right is absolute, it replaces the left path.
 415 | |||
 416 | ||| On Windows:
 417 | |||
 418 | ||| - If the right path has a root but no volume (e.g., `\windows`), it replaces
 419 | |||   everything except for the volume (if any) of left.
 420 | ||| - If the right path has a volume but no root, it replaces left.
 421 | |||
 422 | ||| ```idris example
 423 | ||| "/usr" </> "local/etc" == "/usr/local/etc"
 424 | ||| ```
 425 | export
 426 | (</>) : (left : String) -> (right : String) -> String
 427 | (</>) left right = show $ parse left /> right
 428 | 
 429 | ||| Joins path components into one.
 430 | |||
 431 | ||| ```idris example
 432 | ||| joinPath ["/usr", "local/etc"] == "/usr/local/etc"
 433 | ||| ```
 434 | export
 435 | joinPath : List String -> String
 436 | joinPath xs = show $ foldl (/>) (parse "") xs
 437 | 
 438 | ||| Splits path into components.
 439 | |||
 440 | ||| ```idris example
 441 | ||| splitPath "/usr/local/etc" == ["/", "usr", "local", "etc"]
 442 | ||| splitPath "tmp/Foo.idr" == ["tmp", "Foo.idr"]
 443 | ||| ```
 444 | export
 445 | splitPath : String -> List String
 446 | splitPath = map show . splitPath' . parse
 447 | 
 448 | ||| Splits the path into parent and child.
 449 | |||
 450 | ||| ```idris example
 451 | ||| splitParent "/usr/local/etc" == Just ("/usr/local", "etc")
 452 | ||| ```
 453 | export
 454 | splitParent : String -> Maybe (String, String)
 455 | splitParent path =
 456 |   do
 457 |     (parent, child) <- splitParent' (parse path)
 458 |     pure (show parent, show child)
 459 | 
 460 | ||| Returns the path without its final component, if there is one.
 461 | |||
 462 | ||| Returns Nothing if the path terminates by a root or volume.
 463 | export
 464 | parent : String -> Maybe String
 465 | parent = map show . parent' . parse
 466 | 
 467 | ||| Returns the list of all parents of the path, longest first, self included.
 468 | |||
 469 | ||| ```idris example
 470 | ||| parents "/etc/kernel" == ["/etc/kernel", "/etc", "/"]
 471 | ||| ```
 472 | export
 473 | parents : String -> List String
 474 | parents = map show . List.iterate parent' . parse
 475 | 
 476 | ||| Determines whether the base is one of the parents of target.
 477 | |||
 478 | ||| Trailing separator is ignored.
 479 | |||
 480 | ||| ```idris example
 481 | ||| "/etc" `isBaseOf` "/etc/kernel"
 482 | ||| ```
 483 | export
 484 | isBaseOf : (base : String) -> (target : String) -> Bool
 485 | isBaseOf base target =
 486 |   let
 487 |     MkPath baseVol baseRoot baseBody _ = parse base
 488 |     MkPath targetVol targetRoot targetBody _ = parse target
 489 |   in
 490 |        baseVol == targetVol
 491 |     && baseRoot == targetRoot
 492 |     && (baseBody `isPrefixOf` targetBody)
 493 | 
 494 | ||| Returns a path that, when appended to base, yields target.
 495 | |||
 496 | ||| Returns Nothing if the base is not a prefix of the target.
 497 | export
 498 | dropBase : (base : String) -> (target : String) -> Maybe String
 499 | dropBase base target =
 500 |   do
 501 |     let MkPath baseVol baseRoot baseBody _ = parse base
 502 |     let MkPath targetVol targetRoot targetBody targetTrialSep = parse target
 503 |     if baseVol == targetVol && baseRoot == targetRoot then Just () else Nothing
 504 |     body <- dropBody baseBody targetBody
 505 |     pure $ show $ MkPath Nothing False body targetTrialSep
 506 |   where
 507 |     dropBody : (base : List Body) -> (target : List Body) -> Maybe (List Body)
 508 |     dropBody [] ys = Just ys
 509 |     dropBody xs [] = Nothing
 510 |     dropBody (x::xs) (y::ys) = if x == y then dropBody xs ys else Nothing
 511 | 
 512 | ||| Returns the last body of the path.
 513 | |||
 514 | ||| If the last body is a file, this is the file name;
 515 | ||| if it's a directory, this is the directory name;
 516 | ||| if it's ".", it recurses on the previous body;
 517 | ||| if it's "..", returns Nothing.
 518 | export
 519 | fileName : String -> Maybe String
 520 | fileName  = fileName' . parse
 521 | 
 522 | ||| Extracts the file name in the path without extension.
 523 | |||
 524 | ||| The stem is:
 525 | |||
 526 | ||| - Nothing, if there is no file name;
 527 | ||| - The entire file name if there is no embedded ".";
 528 | ||| - The entire file name if the file name begins with a "." and has no other ".";
 529 | ||| - Otherwise, the portion of the file name before the last ".".
 530 | export
 531 | fileStem : String -> Maybe String
 532 | fileStem path = pure $ fst $ splitFileName !(fileName path)
 533 | 
 534 | ||| Extracts the extension of the file name in the path.
 535 | |||
 536 | ||| The extension is:
 537 | |||
 538 | ||| - Nothing, if there is no file name;
 539 | ||| - Nothing, if there is no embedded ".";
 540 | ||| - Nothing, if the file name begins with a "." and has no other ".";
 541 | ||| - Otherwise, the portion of the file name after the last ".".
 542 | export
 543 | extension : String -> Maybe String
 544 | extension path = fileName path >>=
 545 |   filter (/= "") . Just . snd . splitFileName
 546 | 
 547 | ||| Extracts the list of extensions of the file name in the path.
 548 | ||| The returned value is:
 549 | |||
 550 | ||| - Nothing, if there is no file name;
 551 | ||| - Just [], if there is no embedded ".";
 552 | ||| - Just [], if the filename begins with a "." and has no other ".";
 553 | ||| - Just es, the portions between the "."s (excluding a potential leading one).
 554 | export
 555 | extensions : String -> Maybe (List String)
 556 | extensions path = snd . splitExtensions <$> fileName path
 557 | 
 558 | ||| Updates the file name in the path.
 559 | |||
 560 | ||| If there is no file name, it appends the name to the path;
 561 | ||| otherwise, it appends the name to the parent of the path.
 562 | export
 563 | setFileName : (name : String) -> String -> String
 564 | setFileName name path = show $ setFileName' name (parse path)
 565 | 
 566 | ||| Appends a extension to the path.
 567 | |||
 568 | ||| If there is no file name, the path will not change;
 569 | ||| if the path has no extension, the extension will be appended;
 570 | ||| if the given extension is empty, the extension of the path will be dropped;
 571 | ||| otherwise, the extension will be replaced.
 572 | |||
 573 | ||| ```idris example
 574 | ||| "/tmp/Foo" <.> "idr" == "/tmp/Foo.idr"
 575 | ||| ```
 576 | export
 577 | (<.>) : String -> (extension : String) -> String
 578 | (<.>) path ext =
 579 |   let
 580 |     path' = parse path
 581 |     ext = pack $ dropWhile (\char => char == '.' || isSpace char) (unpack ext)
 582 |     ext = if ext == "" then "" else "." ++ ext
 583 |   in
 584 |     case fileName' path' of
 585 |       Just name =>
 586 |         let (stem, _) = splitFileName name in
 587 |           show $ setFileName' (stem ++ ext) path'
 588 |       Nothing => path
 589 | 
 590 | ||| Drops the extension of the path.
 591 | export
 592 | dropExtension : String -> String
 593 | dropExtension path = path <.> ""
 594 |