Libraries.Utils.Path

Definitions

dirSeparator : Char

  The character that separates directories in the path.

Totality: total
Visibility: export

pathSeparator : Char

  The character that separates multiple paths.

Totality: total
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).

Totality: total
Visibility: public export

volume : Path -> Maybe Volume

  Windows path prefix (only for Windows).

Totality: total
Visibility: public export

.hasRoot : Path -> Bool

  Whether the path contains root.

Totality: total
Visibility: public export

hasRoot : Path -> Bool

  Whether the path contains root.

Totality: total
Visibility: public export

.body : Path -> List Body

  Path bodies.

Totality: total
Visibility: public export

body : Path -> List Body

  Path bodies.

Totality: total
Visibility: public export

.hasTrailSep : Path -> Bool

  Whether the path terminates with a separator.

Totality: total
Visibility: public export

hasTrailSep : Path -> Bool

  Whether the path terminates with a separator.

Totality: total
Visibility: public export

emptyPath : Path

  An empty path, which represents "".

Totality: total
Visibility: public 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/*"
  ```

Totality: total
Visibility: export

splitFileName : String -> (String, String)

Totality: total
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"])
  ```

Totality: total
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.

Totality: total
Visibility: export

isRelative : String -> Bool

  Returns true if the path is relative.

Totality: total
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"
  ```

Totality: total
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"
  ```

Totality: total
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"
  ```

Totality: total
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"]
  ```

Totality: total
Visibility: export

splitParent : String -> Maybe (String, String)

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

Totality: total
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.

Totality: total
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"
  ```

Totality: total
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.

Totality: total
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.

Totality: total
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 ".".

Totality: total
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 ".".

Totality: total
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).

Totality: total
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.

Totality: total
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"
  ```

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

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

  Appends a extension to the path, replacing multiple extensions.
  
  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, all of the extensions of the path will be dropped;
  otherwise, the extensions will be replaced.
  
  ```idris example
  "/tmp/Foo.lidr.md" <.> "idr" == "/tmp/Foo.idr"
  ```

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

dropExtension : String -> String

  Drops the extension of the path.

Totality: total
Visibility: export

dropExtensions : String -> String

  Drops all of the extensions of a path.
  ```idris example
  "/tmp/Foo.lidr.md" == "/tmp/Foo"

Totality: total
Visibility: export

pathLookup : List String -> IO (Maybe String)

  Looks up an executable from a list of candidate names in the PATH

Totality: total
Visibility: export