Safe Haskell	Safe-Inferred
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

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 #
Read AbsolutePath
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS AbsolutePath readList :: ReadS [AbsolutePath] readPrec :: ReadPrec AbsolutePath readListPrec :: ReadPrec [AbsolutePath]
Show AbsolutePath Source #
Instance details Defined in Agda.Utils.FileName Methods showsPrec :: Int -> AbsolutePath -> ShowS show :: AbsolutePath -> String showList :: [AbsolutePath] -> ShowS
NFData AbsolutePath Source #
Instance details Defined in Agda.Utils.FileName Methods rnf :: AbsolutePath -> ()
Eq AbsolutePath Source #
Instance details Defined in Agda.Utils.FileName Methods (==) :: AbsolutePath -> AbsolutePath -> Bool (/=) :: AbsolutePath -> AbsolutePath -> Bool
Ord AbsolutePath Source #
Instance details Defined in Agda.Utils.FileName Methods compare :: AbsolutePath -> AbsolutePath -> Ordering (<) :: AbsolutePath -> AbsolutePath -> Bool (<=) :: AbsolutePath -> AbsolutePath -> Bool (>) :: AbsolutePath -> AbsolutePath -> Bool (>=) :: AbsolutePath -> AbsolutePath -> Bool max :: AbsolutePath -> AbsolutePath -> AbsolutePath min :: AbsolutePath -> AbsolutePath -> AbsolutePath
Hashable AbsolutePath Source #
Instance details Defined in Agda.Utils.FileName Methods hashWithSalt :: Int -> AbsolutePath -> Int hash :: AbsolutePath -> Int
ToJSON AbsolutePath Source #
Instance details Defined in Agda.Interaction.JSON Methods toJSON :: AbsolutePath -> Value # toEncoding :: AbsolutePath -> Encoding # toJSONList :: [AbsolutePath] -> Value # toEncodingList :: [AbsolutePath] -> Encoding # omitField :: AbsolutePath -> Bool #

filePath :: AbsolutePath -> FilePath Source #

Extract the AbsolutePath to be used as FilePath.

mkAbsolute :: FilePath -> AbsolutePath Source #

Constructs AbsolutePaths.

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 see 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.