System.Path

Definitions

dirSeparator : Char

  The character that separates directories in the path.

Visibility: export

pathSeparator : Char

  The character that separates multiple paths.

Visibility: export

data Volume : Type

  Windows path prefix.

Totality: total
Visibility: public export
Constructors:

UNC : String -> String -> Volume

  Windows Uniform Naming Convention, consisting of server name and share
  directory.
  
  Example: `\\localhost\share`

Disk : Char -> Volume

  The drive.
  
  Example: `C:`

Hints:

Eq Volume

Show Volume

data Body : Type

  A single body in path.

Totality: total
Visibility: public export
Constructors:

CurDir : Body

  Represents ".".

ParentDir : Body

  Represents "..".

Normal : String -> Body

  Directory or file.

Hints:

Eq Body

Show Body

record Path : Type

  A parsed cross-platform file system path.
  
  Use the function `parse` to constructs a Path from String, and use the
  function `show` to convert in reverse.
  
  Trailing separator is only used for display and is ignored when comparing
  paths.

Totality: total
Visibility: public export
Constructor: 

MkPath : Maybe Volume -> Bool -> List Body -> Bool -> Path

Projections:

.body : Path -> List Body

  Path bodies.

.hasRoot : Path -> Bool

  Whether the path contains root.

.hasTrailSep : Path -> Bool

  Whether the path terminates with a separator.

.volume : Path -> Maybe Volume

  Windows path prefix (only for Windows).

Hints:

Eq Path

Show Path

.volume : Path -> Maybe Volume

  Windows path prefix (only for Windows).

Visibility: public export

volume : Path -> Maybe Volume

  Windows path prefix (only for Windows).

Visibility: public export

.hasRoot : Path -> Bool

  Whether the path contains root.

Visibility: public export

hasRoot : Path -> Bool

  Whether the path contains root.

Visibility: public export

.body : Path -> List Body

  Path bodies.

Visibility: public export

body : Path -> List Body

  Path bodies.

Visibility: public export

.hasTrailSep : Path -> Bool

  Whether the path terminates with a separator.

Visibility: public export

hasTrailSep : Path -> Bool

  Whether the path terminates with a separator.

Visibility: public export

emptyPath : Path

  An empty path, which represents "".

Visibility: public export

tryParse : String -> Maybe Path

Visibility: export

parse : String -> 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.
  
  Some kind of invalid paths are accepted. The relax rules:
  
  - 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).
  - Repeated separators are ignored, therefore, "a/b" and "a//b" both have "a"
    and "b" as bodies.
  - "." 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`.
  
  ```idris example
  parse "C:\\Windows/System32"
  parse "/usr/local/etc/*"
  ```

Visibility: export

splitFileName : String -> (String, String)

Visibility: export

splitExtensions : String -> (String, List String)

  Split a file name into a basename and a list of extensions.
  A leading dot is considered to be part of the basename.
  ```
  splitExtensions "Path.idr"           = ("Path", ["idr"])
  splitExtensions "file.latex.lidr"    = ("file", ["latex", "lidr"])
  splitExtensions ".hidden.latex.lidr" = (".hidden", ["latex", "lidr"])
  ```

Visibility: export

isAbsolute : String -> Bool

  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 starts with a disk and has root or
    starts with UNC. For example, `c:\\windows` is absolute, while `c:temp`
    and `\temp` are not.

Visibility: export

isRelative : String -> Bool

  Returns true if the path is relative.

Visibility: export

(/>) : Path -> String -> Path

  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"
  ```

Visibility: export
Fixity Declaration: infixl operator, level 5

(</>) : String -> String -> String

  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
  "/usr" </> "local/etc" == "/usr/local/etc"
  ```

Visibility: export
Fixity Declaration: infixl operator, level 5

joinPath : List String -> String

  Joins path components into one.
  
  ```idris example
  joinPath ["/usr", "local/etc"] == "/usr/local/etc"
  ```

Visibility: export

splitPath : String -> List String

  Splits path into components.
  
  ```idris example
  splitPath "/usr/local/etc" == ["/", "usr", "local", "etc"]
  splitPath "tmp/Foo.idr" == ["tmp", "Foo.idr"]
  ```

Visibility: export

splitParent : String -> Maybe (String, String)

  Splits the path into parent and child.
  
  ```idris example
  splitParent "/usr/local/etc" == Just ("/usr/local", "etc")
  ```

Visibility: export

parent : String -> Maybe String

  Returns the path without its final component, if there is one.
  
  Returns Nothing if the path terminates by a root or volume.

Visibility: export

parents : String -> List String

  Returns the list of all parents of the path, longest first, self included.
  
  ```idris example
  parents "/etc/kernel" == ["/etc/kernel", "/etc", "/"]
  ```

Visibility: export

isBaseOf : String -> String -> Bool

  Determines whether the base is one of the parents of target.
  
  Trailing separator is ignored.
  
  ```idris example
  "/etc" `isBaseOf` "/etc/kernel"
  ```

Visibility: export

dropBase : String -> String -> Maybe String

  Returns a path that, when appended to base, yields target.
  
  Returns Nothing if the base is not a prefix of the target.

Visibility: export

fileName : String -> Maybe String

  Returns the last body of the path.
  
  If the last body is a file, this is the file name;
  if it's a directory, this is the directory name;
  if it's ".", it recurses on the previous body;
  if it's "..", returns Nothing.

Visibility: export

fileStem : String -> Maybe String

  Extracts the file name in the path without extension.
  
  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 a "." and has no other ".";
  - Otherwise, the portion of the file name before the last ".".

Visibility: export

extension : String -> Maybe String

  Extracts the extension of the file name in the path.
  
  The extension is:
  
  - Nothing, if there is no file name;
  - Nothing, if there is no embedded ".";
  - Nothing, if the file name begins with a "." and has no other ".";
  - Otherwise, the portion of the file name after the last ".".

Visibility: export

extensions : String -> Maybe (List String)

  Extracts the list of extensions of the file name in the path.
  The returned value is:
  
  - Nothing, if there is no file name;
  - Just [], if there is no embedded ".";
  - Just [], if the filename begins with a "." and has no other ".";
  - Just es, the portions between the "."s (excluding a potential leading one).

Visibility: export

setFileName : String -> String -> String

  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.

Visibility: export

(<.>) : String -> String -> String

  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;
  if the given extension is empty, the extension of the path will be dropped;
  otherwise, the extension will be replaced.
  
  ```idris example
  "/tmp/Foo" <.> "idr" == "/tmp/Foo.idr"
  ```

Visibility: export
Fixity Declarations:
infixl operator, level 7
infixr operator, level 7

dropExtension : String -> String

  Drops the extension of the path.

Visibility: export