Idris2Doc : System.Path

System.Path

(/>) : 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"
```

Fixity Declaration: infixr operator, level 5
(<.>) : 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"
```

Fixity Declaration: infixr operator, level 7
(</>) : 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"
```

Fixity Declaration: infixr operator, level 5
Body : Type
A single body in path.
Totality: total
Constructors:
CurDir : Body
Represents ".".
ParentDir : Body
Represents "..".
Normal : String -> Body
Directory or file.
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
Constructor: 
Volume : Type
Windows path prefix.
Totality: total
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:`
dirSeparator : Char
The character that separates directories in the path.
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.
dropExtension : String -> String
Drops the extension of the path.
emptyPath : Path
An empty path, which represents "".
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 ".".
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.
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 ".".
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.
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"
```
isRelative : String -> Bool
Returns true if the path is relative.
joinPath : List String -> String
Joins path components into one.

```idris example
joinPath ["/usr", "local/etc"] == "/usr/local/etc"
```
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.
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", "/"]
```
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/*"
```
pathSeparator : Char
The character that separates multiple paths.
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.
splitFileName : String -> (String, String)
splitParent : String -> Maybe (String, String)
Splits the path into parent and child.

```idris example
splitParent "/usr/local/etc" == Just ("/usr/local", "etc")
```
splitPath : String -> List String
Splits path into components.

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