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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.FileName

Description

Operations on file names.

Synopsis

- newtype AbsolutePath = AbsolutePath Text
- filePath :: AbsolutePath -> FilePath
- mkAbsolute :: FilePath -> AbsolutePath
- absolute :: FilePath -> IO AbsolutePath
- canonicalizeAbsolutePath :: AbsolutePath -> IO AbsolutePath
- sameFile :: AbsolutePath -> AbsolutePath -> IO Bool
- doesFileExistCaseSensitive :: FilePath -> IO Bool
- isNewerThan :: FilePath -> FilePath -> IO Bool
- relativizeAbsolutePath :: AbsolutePath -> AbsolutePath -> Maybe FilePath
- makeRelativeCanonical :: FilePath -> FilePath -> IO FilePath
- stripAnyOfExtensions :: [String] -> FilePath -> Maybe FilePath

# Documentation

newtype AbsolutePath Source #

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.

Constructors

AbsolutePath Text |

#### Instances

Instances details

Pretty AbsolutePath Source # |
Instance details Defined in Agda.Syntax.Common.Pretty Methods pretty :: AbsolutePath -> Doc Source # prettyPrec :: Int -> AbsolutePath -> Doc Source # prettyList :: [AbsolutePath] -> Doc Source #
GetFileId FileToId Source # |
Instance details Defined in Agda.Utils.FileId Methods getFileId :: FileToId -> File -> FileId Source #
GetIdFile IdToFile Source # |
Instance details Defined in Agda.Utils.FileId Methods getIdFile :: IdToFile -> FileId -> File Source #
ToJSON AbsolutePath Source # |
Instance details Defined in Agda.Interaction.JSON Methods toJSON :: AbsolutePath -> Value Source # toEncoding :: AbsolutePath -> Encoding Source # toJSONList :: [AbsolutePath] -> Value Source # toEncodingList :: [AbsolutePath] -> Encoding Source # omitField :: AbsolutePath -> Bool Source #
NFData AbsolutePath Source # |
Instance details Defined in Agda.Utils.FileName Methods rnf :: AbsolutePath -> () Source #
Read AbsolutePath Source # |
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS AbsolutePath Source # readList :: ReadS [AbsolutePath] Source # readPrec :: ReadPrec AbsolutePath Source # readListPrec :: ReadPrec [AbsolutePath] Source #
Show AbsolutePath Source # |
Instance details Defined in Agda.Utils.FileName Methods showsPrec :: Int -> AbsolutePath -> ShowS Source # show :: AbsolutePath -> String Source # showList :: [AbsolutePath] -> ShowS Source #
Eq AbsolutePath Source # |
Instance details Defined in Agda.Utils.FileName Methods (==) :: AbsolutePath -> AbsolutePath -> Bool Source # (/=) :: AbsolutePath -> AbsolutePath -> Bool Source #
Ord AbsolutePath Source # |

Instance details

Defined in Agda.Utils.FileName

Methods

compare :: AbsolutePath -> AbsolutePath -> Ordering Source #

(<) :: AbsolutePath -> AbsolutePath -> Bool Source #

(<=) :: AbsolutePath -> AbsolutePath -> Bool Source #

(>) :: AbsolutePath -> AbsolutePath -> Bool Source #

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

max :: AbsolutePath -> AbsolutePath -> AbsolutePath Source #

min :: AbsolutePath -> AbsolutePath -> AbsolutePath Source #

Hashable AbsolutePath Source # |
Instance details Defined in Agda.Utils.FileName Methods hashWithSalt :: Int -> AbsolutePath -> Int Source # hash :: AbsolutePath -> Int Source #

filePath :: AbsolutePath -> FilePath Source #

Extract the `AbsolutePath` to be used as `FilePath`.

mkAbsolute :: FilePath -> AbsolutePath Source #

Constructs `AbsolutePath`s.

Precondition: The path must be absolute and valid.

absolute :: FilePath -> IO AbsolutePath Source #

Makes the path absolute.

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

canonicalizeAbsolutePath :: AbsolutePath -> IO AbsolutePath Source #

Resolve symlinks etc. Preserves `sameFile`.

sameFile :: AbsolutePath -> AbsolutePath -> IO Bool Source #

Tries to establish if the two file paths point to the same file (or directory). False negatives may be returned.

doesFileExistCaseSensitive :: FilePath -> IO Bool Source #

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 insensitively.)

isNewerThan :: FilePath -> FilePath -> IO Bool Source #

True if the first file is newer than the second file. If a file doesn't exist it is considered to be infinitely old.

relativizeAbsolutePath Source #

Arguments

:: AbsolutePath | The absolute path we seek to relativize.
-> AbsolutePath | The root for relativization.
-> Maybe FilePath | The relative path, if any.

A partial version of `makeRelative` with flipped arguments, returning `Nothing` if the given path cannot be relativized to the given `root`.

makeRelativeCanonical :: FilePath -> FilePath -> IO FilePath Source #

Makes a path relative to a root without assuming that either path is canonical.

stripAnyOfExtensions :: [String] -> FilePath -> Maybe FilePath Source #

Generalizes `stripExtension`.