Agda.Utils.FileName

Operations on file names.

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

Defined in Agda.Utils.FileName

Methods

(==) :: AbsolutePath -> AbsolutePath -> Bool

(/=) :: AbsolutePath -> AbsolutePath -> Bool

Data AbsolutePath

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

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

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS AbsolutePath

readList :: ReadS [AbsolutePath]

readPrec :: ReadPrec AbsolutePath

readListPrec :: ReadPrec [AbsolutePath]

Show AbsolutePath

Defined in Agda.Utils.FileName

Methods

showsPrec :: Int -> AbsolutePath -> ShowS

show :: AbsolutePath -> String

showList :: [AbsolutePath] -> ShowS

Hashable AbsolutePath

Defined in Agda.Utils.FileName

Methods

hashWithSalt :: Int -> AbsolutePath -> Int

hash :: AbsolutePath -> Int

Pretty AbsolutePath

Defined in Agda.Utils.FileName

Methods

pretty :: AbsolutePath -> Doc

prettyPrec :: Int -> AbsolutePath -> Doc

prettyList :: [AbsolutePath] -> Doc

KillRange Range

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Range

SetRange Range

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> Range -> Range

HasRange Range

Defined in Agda.Syntax.Position

Methods

getRange :: Range -> Range

HasRange Interval

Defined in Agda.Syntax.Position

Methods

getRange :: Interval -> Range

FreshName Range

Defined in Agda.TypeChecking.Monad.Base

Methods

freshName_ :: MonadFresh NameId m => Range -> m Name

EmbPrj AbsolutePath

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.

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Range -> S Int32

icod_ :: Range -> S Int32

value :: Int32 -> R Range

PrettyTCM Range

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Range -> m Doc

ToJSON AbsolutePath

Defined in Agda.Interaction.JSON

Methods

toJSON :: AbsolutePath -> Value

toEncoding :: AbsolutePath -> Encoding

toJSONList :: [AbsolutePath] -> Value

toEncodingList :: [AbsolutePath] -> Encoding

ToJSON Range

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: Range -> Value

toEncoding :: Range -> Encoding

toJSONList :: [Range] -> Value

toEncodingList :: [Range] -> Encoding

EncodeTCM Range

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: Range -> TCM Value

Subst Term Range

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' Term -> Range -> Range

LensClosure Range MetaInfo

Defined in Agda.TypeChecking.Monad.Base

Methods

lensClosure :: Lens' (Closure Range) MetaInfo

LensClosure Range MetaVariable

Defined in Agda.TypeChecking.Monad.Base

Methods

lensClosure :: Lens' (Closure Range) MetaVariable

FreshName (Range, String)

Defined in Agda.TypeChecking.Monad.Base

Methods

freshName_ :: MonadFresh NameId 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