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

Safe HaskellNone
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
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 :: (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

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 Source # 
Instance details

Defined in Agda.Utils.FileName

Methods

showsPrec :: Int -> AbsolutePath -> ShowS

show :: AbsolutePath -> String

showList :: [AbsolutePath] -> ShowS

Hashable AbsolutePath Source # 
Instance details

Defined in Agda.Utils.FileName

Methods

hashWithSalt :: Int -> AbsolutePath -> Int

hash :: AbsolutePath -> Int

Pretty AbsolutePath Source # 
Instance details

Defined in Agda.Utils.FileName

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 #

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

FreshName Range Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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 :: Range -> TCM Doc Source #

Subst Term Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

FreshName (Range, String) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freshName_ :: MonadTCState m => (Range, String) -> m Name Source #

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.

(===) :: AbsolutePath -> AbsolutePath -> Bool infix 4 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.)

rootPath :: FilePath Source #