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

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

Eq AbsolutePath Source #
Instance details Defined in Agda.Utils.FileName Methods (==) :: AbsolutePath -> AbsolutePath -> Bool # (/=) :: AbsolutePath -> AbsolutePath -> Bool #
Data AbsolutePath Source #
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 :: forall r r'. (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 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 #
Read AbsolutePath Source #
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 #
Semigroup AbsolutePath Source #	To get `Semigroup Range`, we need a semigroup instance for `AbsolutePath`.
Instance details Defined in Agda.Syntax.Position Methods (<>) :: AbsolutePath -> AbsolutePath -> AbsolutePath # sconcat :: NonEmpty AbsolutePath -> AbsolutePath # stimes :: Integral b => b -> 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 #
ToJSON Range Source #
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: Range -> Value # toEncoding :: Range -> Encoding # toJSONList :: [Range] -> Value # toEncodingList :: [Range] -> Encoding #
NFData AbsolutePath Source #
Instance details Defined in Agda.Utils.FileName Methods rnf :: AbsolutePath -> () #
NFData Interval Source #
Instance details Defined in Agda.Syntax.Position Methods rnf :: Interval -> () #
NFData Position Source #
Instance details Defined in Agda.Syntax.Position Methods rnf :: Position -> () #
Pretty AbsolutePath Source #
Instance details Defined in Agda.Utils.FileName Methods pretty :: AbsolutePath -> Doc Source # prettyPrec :: Int -> AbsolutePath -> Doc Source # prettyList :: [AbsolutePath] -> Doc Source #
KillRange Range Source #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Range Source #
SetRange Range Source #
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> Range -> Range Source #
HasRange Range Source #
Instance details Defined in Agda.Syntax.Position Methods getRange :: Range -> Range Source #
HasRange Interval Source #
Instance details Defined in Agda.Syntax.Position Methods getRange :: Interval -> Range Source #
Subst Range Source #
Instance details Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg Range Source # Methods applySubst :: Substitution' (SubstArg Range) -> Range -> Range Source #
FreshName Range Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => Range -> m Name Source #
EmbPrj AbsolutePath Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: AbsolutePath -> S Int32 Source # icod_ :: AbsolutePath -> S Int32 Source # value :: Int32 -> R AbsolutePath Source #
EmbPrj Range Source #	Ranges are always deserialised as `noRange`.
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Range -> S Int32 Source # icod_ :: Range -> S Int32 Source # value :: Int32 -> R Range Source #
PrettyTCM Range Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Range -> m Doc Source #
EncodeTCM Range Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Range -> TCM Value Source #
LensClosure Range MetaInfo Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lensClosure :: Lens' (Closure Range) MetaInfo Source #
LensClosure Range MetaVariable Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lensClosure :: Lens' (Closure Range) MetaVariable Source #
FreshName (Range, String) Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => (Range, String) -> m Name Source #
type SubstArg Range Source #
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Range = Term

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

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.