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
(===) :: AbsolutePath -> AbsolutePath -> Bool
doesFileExistCaseSensitive :: FilePath -> IO Bool
rootPath :: FilePath

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 #
Instance details Defined in Agda.Utils.FileName Methods (==) :: AbsolutePath -> AbsolutePath -> Bool # (/=) :: AbsolutePath -> AbsolutePath -> Bool #
Data AbsolutePath #
Instance details Defined in Agda.Utils.FileName 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 #
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 #
Read AbsolutePath #
Instance details Defined in Agda.Interaction.InteractionTop Methods readsPrec :: Int -> ReadS AbsolutePath # readList :: ReadS [AbsolutePath] # readPrec :: ReadPrec AbsolutePath # readListPrec :: ReadPrec [AbsolutePath] #
Show AbsolutePath #
Instance details Defined in Agda.Utils.FileName Methods showsPrec :: Int -> AbsolutePath -> ShowS # show :: AbsolutePath -> String # showList :: [AbsolutePath] -> ShowS #
Hashable AbsolutePath #
Instance details Defined in Agda.Utils.FileName Methods hashWithSalt :: Int -> AbsolutePath -> Int # hash :: AbsolutePath -> Int #
Pretty AbsolutePath #
Instance details Defined in Agda.Utils.FileName Methods pretty :: AbsolutePath -> Doc # prettyPrec :: Int -> AbsolutePath -> Doc # prettyList :: [AbsolutePath] -> Doc #
KillRange Range #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Range #
SetRange Range #
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> Range -> Range #
HasRange Range #
Instance details Defined in Agda.Syntax.Position Methods getRange :: Range -> Range #
HasRange Interval #
Instance details Defined in Agda.Syntax.Position Methods getRange :: Interval -> Range #
FreshName Range #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadState TCState m => Range -> m Name #
EmbPrj AbsolutePath #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: AbsolutePath -> S Int32 # icod_ :: AbsolutePath -> S Int32 # value :: Int32 -> R AbsolutePath #
EmbPrj Range #	Ranges are always deserialised as `noRange`.
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Range -> S Int32 # icod_ :: Range -> S Int32 # value :: Int32 -> R Range #
PrettyTCM Range #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Range -> TCM Doc #
Subst Term Range #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Range -> Range #
FreshName (Range, String) #
Instance details Defined in Agda.TypeChecking.Monad.Base 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 #