Agda-2.6.2.1.20220327: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Utils.FileName

Description

Operations on file names.

Synopsis

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

HasRange Interval Source # 
Instance details

Defined in Agda.Syntax.Position

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

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

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

EmbPrj AbsolutePath Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Subst Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Range Source #

Pretty AbsolutePath Source # 
Instance details

Defined in Agda.Utils.FileName

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 #

Semigroup AbsolutePath Source #

To get Semigroup Range', we need a semigroup instance for AbsolutePath.

Instance details

Defined in Agda.Syntax.Position

Read AbsolutePath Source # 
Instance details

Defined in Agda.Interaction.Base

Show AbsolutePath Source # 
Instance details

Defined in Agda.Utils.FileName

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 -> () #

NFData AbsolutePath Source # 
Instance details

Defined in Agda.Utils.FileName

Methods

rnf :: AbsolutePath -> () #

Eq AbsolutePath Source # 
Instance details

Defined in Agda.Utils.FileName

Ord AbsolutePath Source # 
Instance details

Defined in Agda.Utils.FileName

Hashable AbsolutePath Source # 
Instance details

Defined in Agda.Utils.FileName

ToJSON Range Source # 
Instance details

Defined in Agda.Interaction.JSONTop

ToJSON AbsolutePath Source # 
Instance details

Defined in Agda.Interaction.JSON

LensClosure Range MetaInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensClosure Range MetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

FreshName (Range, String) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type SubstArg Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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.