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

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

# 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

EncodeTCM Range Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Range -> TCM Value Source #
HasRange Interval Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: Interval -> Range Source #
HasRange Range Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: Range -> Range 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 #
FreshName Range Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => Range -> m Name Source #
PrettyTCM Range Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Range -> m Doc 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 #
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 #
Subst Range Source # |
Instance details Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg Range Source # Methods applySubst :: Substitution' (SubstArg Range) -> Range -> Range Source #
Pretty AbsolutePath Source # |
Instance details Defined in Agda.Utils.FileName Methods pretty :: AbsolutePath -> Doc Source # prettyPrec :: Int -> AbsolutePath -> Doc Source # prettyList :: [AbsolutePath] -> Doc Source #
ToJSON Range Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: Range -> Value # toEncoding :: Range -> Encoding # toJSONList :: [Range] -> Value # toEncodingList :: [Range] -> Encoding #
ToJSON AbsolutePath Source # |
Instance details Defined in Agda.Interaction.JSON Methods toJSON :: AbsolutePath -> Value # toEncoding :: AbsolutePath -> Encoding # toJSONList :: [AbsolutePath] -> Value # toEncodingList :: [AbsolutePath] -> Encoding #
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 Source #

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

toConstr :: AbsolutePath -> Constr Source #

dataTypeOf :: AbsolutePath -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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 Source # sconcat :: NonEmpty AbsolutePath -> AbsolutePath Source # stimes :: Integral b => b -> AbsolutePath -> 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 #
NFData Interval Source # |
Instance details Defined in Agda.Syntax.Position Methods rnf :: Interval -> () Source #
NFData Position Source # |
Instance details Defined in Agda.Syntax.Position Methods rnf :: Position -> () Source #
NFData AbsolutePath Source # |
Instance details Defined in Agda.Utils.FileName Methods rnf :: AbsolutePath -> () 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 #
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 `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).

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.