Idris2Doc : System.Path

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
dataVolume : 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:
EqVolume
ShowVolume
dataBody : 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:
EqBody
ShowBody
recordPath : 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 : MaybeVolume->Bool->ListBody->Bool->Path

Projections:
.body : Path->ListBody
  Path bodies.
.hasRoot : Path->Bool
  Whether the path contains root.
.hasTrailSep : Path->Bool
  Whether the path terminates with a separator.
.volume : Path->MaybeVolume
  Windows path prefix (only for Windows).

Hints:
EqPath
ShowPath
.volume : Path->MaybeVolume
  Windows path prefix (only for Windows).

Visibility: public export
volume : Path->MaybeVolume
  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->ListBody
  Path bodies.

Visibility: public export
body : Path->ListBody
  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->MaybePath
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, ListString)
  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 : ListString->String
  Joins path components into one.

```idris example
joinPath ["/usr", "local/etc"] == "/usr/local/etc"
```

Visibility: export
splitPath : String->ListString
  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->MaybeString
  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->ListString
  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->MaybeString
  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->MaybeString
  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->MaybeString
  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->MaybeString
  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 (ListString)
  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