Agda.Utils.FileName

Operations on file names.

Documentation

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

Constructors

AbsolutePath Text

Instances

Eq AbsolutePath

Methods

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

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

Data AbsolutePath

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AbsolutePath -> c AbsolutePath

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AbsolutePath

toConstr :: AbsolutePath -> Constr

dataTypeOf :: AbsolutePath -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c AbsolutePath)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AbsolutePath)

gmapT :: (forall b. Data b => b -> b) -> AbsolutePath -> AbsolutePath

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AbsolutePath -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AbsolutePath -> r

gmapQ :: (forall d. Data d => d -> u) -> AbsolutePath -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> AbsolutePath -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AbsolutePath -> m AbsolutePath

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AbsolutePath -> m AbsolutePath

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AbsolutePath -> m AbsolutePath

Ord AbsolutePath

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

Show AbsolutePath

Methods

showsPrec :: Int -> AbsolutePath -> ShowS

show :: AbsolutePath -> String

showList :: [AbsolutePath] -> ShowS

Hashable AbsolutePath

Methods

hashWithSalt :: Int -> AbsolutePath -> Int

hash :: AbsolutePath -> Int

Pretty AbsolutePath

Methods

pretty :: AbsolutePath -> Doc

prettyPrec :: Int -> AbsolutePath -> Doc

prettyList :: [AbsolutePath] -> Doc

KillRange Range

Methods

killRange :: KillRangeT Range

SetRange Range

Methods

setRange :: Range -> Range -> Range

HasRange Range

Methods

getRange :: Range -> Range

HasRange Interval

Methods

getRange :: Interval -> Range

FreshName Range

Methods

freshName_ :: MonadState TCState m => Range -> m Name

PrettyTCM Range

Methods

prettyTCM :: Range -> TCM Doc

FreshName (Range, String)

Methods

freshName_ :: MonadState TCState m => (Range, String) -> m Name

filePath :: AbsolutePath -> FilePath

Extract the AbsolutePath to be used as FilePath.

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

rootPath :: FilePath