Agda.Utils.FileName

Operations on file names.

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.

Andreas, 2014-03-30: For efficiency of serialization, AbsolutePath is implemented as ByteString which short-cuts equality testing using pointer equality. This saves 20% of the serialization time of the standard library!

Instances

Eq AbsolutePath

Ord AbsolutePath

Read AbsolutePath

Show AbsolutePath

Arbitrary AbsolutePath

KillRange Range

SetRange Range

HasRange Range

HasRange Interval

FreshName Range

GenC Range

PrettyTCM Range

PrettyTCM Interval

PrettyTCM Position

EmbPrj AbsolutePath

EmbPrj Range

EmbPrj Interval

EmbPrj Position

Typeable * AbsolutePath

FreshName (Range, String)

filePath :: AbsolutePath -> FilePath

Extract the AbsolutePath to be used as FilePath.

rootName :: AbsolutePath -> String

maps blablablafoo.bar.xxx to foo.bar.

mkAbsolute :: FilePath -> AbsolutePath

Constructs AbsolutePaths.

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 infix 4

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