Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Utils.FileName

Description

Operations on file names.

Synopsis

- data AbsolutePath
- filePath :: AbsolutePath -> FilePath
- mkAbsolute :: FilePath -> AbsolutePath
- absolute :: FilePath -> IO AbsolutePath
- (===) :: AbsolutePath -> AbsolutePath -> Bool
- doesFileExistCaseSensitive :: FilePath -> IO Bool
- tests :: IO Bool

# Documentation

data AbsolutePath

Paths which are known to be absolute.

Note that the `Eq` and `Ord` instances do not check if different paths point to the same files or directories.

Instances

Eq AbsolutePath |
Ord AbsolutePath |
Read AbsolutePath |
Read Range |
Read Interval |
Read Position |
Show AbsolutePath |
Typeable AbsolutePath |
Arbitrary AbsolutePath |
Arbitrary Range |
KillRange Range |
SetRange Range |
HasRange Range |
HasRange Interval |
EmbPrj AbsolutePath |
EmbPrj Range |
EmbPrj Interval |
EmbPrj Position |
GenC Range |

filePath :: AbsolutePath -> FilePath

mkAbsolute :: FilePath -> AbsolutePath

Constructs `AbsolutePath`s.

Precondition: The path must be absolute and valid.

absolute :: FilePath -> IO AbsolutePath

Makes the path absolute.

This function may raise an `__IMPOSSIBLE__` error if `canonicalizePath` does not return an absolute path.

(===) :: AbsolutePath -> AbsolutePath -> Bool

Tries to establish if the two file paths point to the same file (or directory).

doesFileExistCaseSensitive :: FilePath -> IO Bool

Case-sensitive doesFileExist for Windows. This is case-sensitive only on the file name part, not on the directory part. (Ideally, path components coming from module name components should be checked case-sensitively and the other path components should be checked case insenstively.)

tests :: IO Bool