Agda.Interaction.Library.Base

Basic data types for library management.

Documentation

type LibName = String

A symbolic library name.

data LibrariesFile

Constructors

LibrariesFile

Fields

• lfPath :: FilePath

  E.g. ~.agdalibraries.

• lfExists :: Bool

  The libraries file might not exist, but we may print its assumed location in error messages.

Instances

Show LibrariesFile

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibrariesFile -> ShowS

show :: LibrariesFile -> String

showList :: [LibrariesFile] -> ShowS

type ExeName = Text

A symbolic executable name.

data ExecutablesFile

Constructors

ExecutablesFile

Fields

• efPath :: FilePath

  E.g. ~.agdaexecutables.

• efExists :: Bool

  The executables file might not exist, but we may print its assumed location in error messages.

Instances

EmbPrj ExecutablesFile

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ExecutablesFile -> S Int32

icod_ :: ExecutablesFile -> S Int32

value :: Int32 -> R ExecutablesFile

Data ExecutablesFile

Defined in Agda.Interaction.Library.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExecutablesFile -> c ExecutablesFile

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExecutablesFile

toConstr :: ExecutablesFile -> Constr

dataTypeOf :: ExecutablesFile -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExecutablesFile)

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

gmapT :: (forall b. Data b => b -> b) -> ExecutablesFile -> ExecutablesFile

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExecutablesFile -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExecutablesFile -> r

gmapQ :: (forall d. Data d => d -> u) -> ExecutablesFile -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ExecutablesFile -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExecutablesFile -> m ExecutablesFile

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExecutablesFile -> m ExecutablesFile

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExecutablesFile -> m ExecutablesFile

Generic ExecutablesFile

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep ExecutablesFile :: Type -> Type

Methods

from :: ExecutablesFile -> Rep ExecutablesFile x

to :: Rep ExecutablesFile x -> ExecutablesFile

Show ExecutablesFile

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> ExecutablesFile -> ShowS

show :: ExecutablesFile -> String

showList :: [ExecutablesFile] -> ShowS

NFData ExecutablesFile

Defined in Agda.Interaction.Library.Base

Methods

rnf :: ExecutablesFile -> ()

type Rep ExecutablesFile

Defined in Agda.Interaction.Library.Base

type Rep ExecutablesFile = D1 ('MetaData "ExecutablesFile" "Agda.Interaction.Library.Base" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "ExecutablesFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "efPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "efExists") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

libNameForCurrentDir :: LibName

The special name "." is used to indicated that the current directory should count as a project root.

data ProjectConfig

A file can either belong to a project located at a given root containing one or more .agda-lib files, or be part of the default project.

Constructors

ProjectConfig

Fields

• configRoot :: FilePath
• configAgdaLibFiles :: [FilePath]

DefaultProjectConfig

Instances

Generic ProjectConfig

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep ProjectConfig :: Type -> Type

Methods

from :: ProjectConfig -> Rep ProjectConfig x

to :: Rep ProjectConfig x -> ProjectConfig

NFData ProjectConfig

Defined in Agda.Interaction.Library.Base

Methods

rnf :: ProjectConfig -> ()

type Rep ProjectConfig

Defined in Agda.Interaction.Library.Base

type Rep ProjectConfig = D1 ('MetaData "ProjectConfig" "Agda.Interaction.Library.Base" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "ProjectConfig" 'PrefixI 'True) (S1 ('MetaSel ('Just "configRoot") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "configAgdaLibFiles") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath])) :+: C1 ('MetaCons "DefaultProjectConfig" 'PrefixI 'False) (U1 :: Type -> Type))

data AgdaLibFile

Content of a .agda-lib file.

Constructors

AgdaLibFile

Fields

• _libName :: LibName

  The symbolic name of the library.

• _libFile :: FilePath

  Path to this .agda-lib file (not content of the file).

• _libIncludes :: [FilePath]

  Roots where to look for the modules of the library.

• _libDepends :: [LibName]

  Dependencies.

• _libPragmas :: [String]

  Default pragma options for all files in the library.

Instances

Generic AgdaLibFile

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep AgdaLibFile :: Type -> Type

Methods

from :: AgdaLibFile -> Rep AgdaLibFile x

to :: Rep AgdaLibFile x -> AgdaLibFile

Show AgdaLibFile

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> AgdaLibFile -> ShowS

show :: AgdaLibFile -> String

showList :: [AgdaLibFile] -> ShowS

NFData AgdaLibFile

Defined in Agda.Interaction.Library.Base

Methods

rnf :: AgdaLibFile -> ()

type Rep AgdaLibFile

Defined in Agda.Interaction.Library.Base

type Rep AgdaLibFile = D1 ('MetaData "AgdaLibFile" "Agda.Interaction.Library.Base" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "AgdaLibFile" 'PrefixI 'True) ((S1 ('MetaSel ('Just "_libName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibName) :*: S1 ('MetaSel ('Just "_libFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath)) :*: (S1 ('MetaSel ('Just "_libIncludes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]) :*: (S1 ('MetaSel ('Just "_libDepends") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LibName]) :*: S1 ('MetaSel ('Just "_libPragmas") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])))))

emptyLibFile :: AgdaLibFile

libName :: Lens' LibName AgdaLibFile

Lenses for AgdaLibFile

libFile :: Lens' FilePath AgdaLibFile

libIncludes :: Lens' [FilePath] AgdaLibFile

libDepends :: Lens' [LibName] AgdaLibFile

libPragmas :: Lens' [String] AgdaLibFile

Library warnings and errors

type LineNumber = Int

data LibPositionInfo

Constructors

LibPositionInfo

Fields

• libFilePos :: Maybe FilePath

  Name of libraries file

• lineNumPos :: LineNumber

  Line number in libraries file.

• filePos :: FilePath

  Library file

Instances

EmbPrj LibPositionInfo

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibPositionInfo -> S Int32

icod_ :: LibPositionInfo -> S Int32

value :: Int32 -> R LibPositionInfo

Data LibPositionInfo

Defined in Agda.Interaction.Library.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LibPositionInfo -> c LibPositionInfo

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LibPositionInfo

toConstr :: LibPositionInfo -> Constr

dataTypeOf :: LibPositionInfo -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LibPositionInfo)

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

gmapT :: (forall b. Data b => b -> b) -> LibPositionInfo -> LibPositionInfo

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r

gmapQ :: (forall d. Data d => d -> u) -> LibPositionInfo -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LibPositionInfo -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LibPositionInfo -> m LibPositionInfo

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LibPositionInfo -> m LibPositionInfo

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LibPositionInfo -> m LibPositionInfo

Generic LibPositionInfo

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibPositionInfo :: Type -> Type

Methods

from :: LibPositionInfo -> Rep LibPositionInfo x

to :: Rep LibPositionInfo x -> LibPositionInfo

Show LibPositionInfo

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibPositionInfo -> ShowS

show :: LibPositionInfo -> String

showList :: [LibPositionInfo] -> ShowS

NFData LibPositionInfo

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibPositionInfo -> ()

type Rep LibPositionInfo

Defined in Agda.Interaction.Library.Base

type Rep LibPositionInfo = D1 ('MetaData "LibPositionInfo" "Agda.Interaction.Library.Base" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "LibPositionInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "libFilePos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe FilePath)) :*: (S1 ('MetaSel ('Just "lineNumPos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LineNumber) :*: S1 ('MetaSel ('Just "filePos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath))))

data LibWarning

Constructors

LibWarning (Maybe LibPositionInfo) LibWarning'

Instances

EmbPrj LibWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning -> S Int32

icod_ :: LibWarning -> S Int32

value :: Int32 -> R LibWarning

Pretty LibWarning

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibWarning -> Doc

prettyPrec :: Int -> LibWarning -> Doc

prettyList :: [LibWarning] -> Doc

Data LibWarning

Defined in Agda.Interaction.Library.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LibWarning -> c LibWarning

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LibWarning

toConstr :: LibWarning -> Constr

dataTypeOf :: LibWarning -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LibWarning)

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

gmapT :: (forall b. Data b => b -> b) -> LibWarning -> LibWarning

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LibWarning -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LibWarning -> r

gmapQ :: (forall d. Data d => d -> u) -> LibWarning -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LibWarning -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning

Generic LibWarning

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibWarning :: Type -> Type

Methods

from :: LibWarning -> Rep LibWarning x

to :: Rep LibWarning x -> LibWarning

Show LibWarning

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibWarning -> ShowS

show :: LibWarning -> String

showList :: [LibWarning] -> ShowS

NFData LibWarning

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibWarning -> ()

type Rep LibWarning

Defined in Agda.Interaction.Library.Base

type Rep LibWarning = D1 ('MetaData "LibWarning" "Agda.Interaction.Library.Base" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "LibWarning" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe LibPositionInfo)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibWarning')))

data LibWarning'

Library Warnings.

Constructors

UnknownField String

Instances

EmbPrj LibWarning'

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning' -> S Int32

icod_ :: LibWarning' -> S Int32

value :: Int32 -> R LibWarning'

Pretty LibWarning'

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibWarning' -> Doc

prettyPrec :: Int -> LibWarning' -> Doc

prettyList :: [LibWarning'] -> Doc

Data LibWarning'

Defined in Agda.Interaction.Library.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LibWarning' -> c LibWarning'

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LibWarning'

toConstr :: LibWarning' -> Constr

dataTypeOf :: LibWarning' -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LibWarning')

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LibWarning')

gmapT :: (forall b. Data b => b -> b) -> LibWarning' -> LibWarning'

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r

gmapQ :: (forall d. Data d => d -> u) -> LibWarning' -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LibWarning' -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'

Generic LibWarning'

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibWarning' :: Type -> Type

Methods

from :: LibWarning' -> Rep LibWarning' x

to :: Rep LibWarning' x -> LibWarning'

Show LibWarning'

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibWarning' -> ShowS

show :: LibWarning' -> String

showList :: [LibWarning'] -> ShowS

NFData LibWarning'

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibWarning' -> ()

type Rep LibWarning'

Defined in Agda.Interaction.Library.Base

type Rep LibWarning' = D1 ('MetaData "LibWarning'" "Agda.Interaction.Library.Base" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "UnknownField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

data LibError

Constructors

LibError (Maybe LibPositionInfo) LibError'

libraryWarningName :: LibWarning -> WarningName

data LibError'

Collected errors while processing library files.

Constructors

LibNotFound LibrariesFile LibName

Raised when a library name could not successfully be resolved to an .agda-lib file.

AmbiguousLib LibName [AgdaLibFile]

Raised when a library name is defined in several .agda-lib files.

OtherError String

Generic error.

Instances

Show LibError'

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibError' -> ShowS

show :: LibError' -> String

showList :: [LibError'] -> ShowS

type LibState = (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)

Cache locations of project configurations and parsed .agda-lib files

type LibErrorIO = WriterT [Either LibError LibWarning] (StateT LibState IO)

Collects LibErrors and LibWarnings.

type LibM = ExceptT Doc (WriterT [LibWarning] (StateT LibState IO))

Throws Doc exceptions, still collects LibWarnings.

warnings :: MonadWriter [Either LibError LibWarning] m => [LibWarning] -> m ()

warnings' :: MonadWriter [Either LibError LibWarning] m => [LibWarning'] -> m ()

raiseErrors' :: MonadWriter [Either LibError LibWarning] m => [LibError'] -> m ()

raiseErrors :: MonadWriter [Either LibError LibWarning] m => [LibError] -> m ()

getCachedProjectConfig :: (MonadState LibState m, MonadIO m) => FilePath -> m (Maybe ProjectConfig)

storeCachedProjectConfig :: (MonadState LibState m, MonadIO m) => FilePath -> ProjectConfig -> m ()

getCachedAgdaLibFile :: (MonadState LibState m, MonadIO m) => FilePath -> m (Maybe AgdaLibFile)

storeCachedAgdaLibFile :: (MonadState LibState m, MonadIO m) => FilePath -> AgdaLibFile -> m ()

Prettyprinting errors and warnings

formatLibPositionInfo :: LibPositionInfo -> String -> Doc

formatLibError :: [AgdaLibFile] -> LibError -> Doc

Pretty-print LibError.