| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.Library.Base
Description
Basic data types for library management.
Synopsis
- type LibName = String
- data LibrariesFile = LibrariesFile {}
- type ExeName = Text
- data ExecutablesFile = ExecutablesFile {}
- libNameForCurrentDir :: LibName
- data ProjectConfig
- = ProjectConfig {
- configRoot :: FilePath
- configAgdaLibFiles :: [FilePath]
- configAbove :: !Int
- | DefaultProjectConfig
- = ProjectConfig {
- data OptionsPragma = OptionsPragma {
- pragmaStrings :: [String]
- pragmaRange :: Range
- data AgdaLibFile = AgdaLibFile {
- _libName :: LibName
- _libFile :: FilePath
- _libAbove :: !Int
- _libIncludes :: [FilePath]
- _libDepends :: [LibName]
- _libPragmas :: OptionsPragma
- emptyLibFile :: AgdaLibFile
- libName :: Lens' AgdaLibFile LibName
- libFile :: Lens' AgdaLibFile FilePath
- libAbove :: Lens' AgdaLibFile Int
- libIncludes :: Lens' AgdaLibFile [FilePath]
- libDepends :: Lens' AgdaLibFile [LibName]
- libPragmas :: Lens' AgdaLibFile OptionsPragma
- type LineNumber = Int
- data LibPositionInfo = LibPositionInfo {}
- data LibWarning = LibWarning (Maybe LibPositionInfo) LibWarning'
- data LibWarning' = UnknownField String
- libraryWarningName :: LibWarning -> WarningName
- data LibError = LibError (Maybe LibPositionInfo) LibError'
- data LibError'
- data LibParseError
- type LibErrWarns = [Either LibError LibWarning]
- warnings :: MonadWriter LibErrWarns m => List1 LibWarning -> m ()
- warnings' :: MonadWriter LibErrWarns m => List1 LibWarning' -> m ()
- raiseErrors' :: MonadWriter LibErrWarns m => List1 LibError' -> m ()
- raiseErrors :: MonadWriter LibErrWarns m => List1 LibError -> m ()
- type LibErrorIO = WriterT LibErrWarns (StateT LibState IO)
- type LibM = ExceptT Doc (WriterT [LibWarning] (StateT LibState IO))
- type LibState = (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
- 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 ()
- formatLibError :: [AgdaLibFile] -> LibError -> Doc
- hasLineNumber :: LibParseError -> Maybe LineNumber
- formatLibPositionInfo :: LibPositionInfo -> LibParseError -> Doc
- prettyInstalledLibraries :: [AgdaLibFile] -> Doc
Documentation
data LibrariesFile Source #
Constructors
| LibrariesFile | |
Instances
| Show LibrariesFile Source # | |
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibrariesFile -> ShowS # show :: LibrariesFile -> String # showList :: [LibrariesFile] -> ShowS # | |
data ExecutablesFile Source #
Constructors
| ExecutablesFile | |
Instances
libNameForCurrentDir :: LibName Source #
The special name "." is used to indicated that the current directory
should count as a project root.
data ProjectConfig Source #
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
| |
| DefaultProjectConfig | |
Instances
| Generic ProjectConfig Source # | |
Defined in Agda.Interaction.Library.Base Associated Types type Rep ProjectConfig :: Type -> Type # | |
| NFData ProjectConfig Source # | |
Defined in Agda.Interaction.Library.Base Methods rnf :: ProjectConfig -> () # | |
| type Rep ProjectConfig Source # | |
Defined in Agda.Interaction.Library.Base type Rep ProjectConfig = D1 ('MetaData "ProjectConfig" "Agda.Interaction.Library.Base" "Agda-2.6.3.20230805-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]) :*: S1 ('MetaSel ('Just "configAbove") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))) :+: C1 ('MetaCons "DefaultProjectConfig" 'PrefixI 'False) (U1 :: Type -> Type)) | |
data OptionsPragma Source #
The options from an OPTIONS pragma (or a .agda-lib file).
In the future it might be nice to switch to a more structured representation. Note that, currently, there is not a one-to-one correspondence between list elements and options.
Constructors
| OptionsPragma | |
Fields
| |
Instances
| EmbPrj OptionsPragma Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common | |
| Monoid OptionsPragma Source # | |
Defined in Agda.Interaction.Library.Base Methods mempty :: OptionsPragma # mappend :: OptionsPragma -> OptionsPragma -> OptionsPragma # mconcat :: [OptionsPragma] -> OptionsPragma # | |
| Semigroup OptionsPragma Source # | |
Defined in Agda.Interaction.Library.Base Methods (<>) :: OptionsPragma -> OptionsPragma -> OptionsPragma # sconcat :: NonEmpty OptionsPragma -> OptionsPragma # stimes :: Integral b => b -> OptionsPragma -> OptionsPragma # | |
| Show OptionsPragma Source # | |
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> OptionsPragma -> ShowS # show :: OptionsPragma -> String # showList :: [OptionsPragma] -> ShowS # | |
| NFData OptionsPragma Source # | Ranges are not forced. |
Defined in Agda.Interaction.Library.Base Methods rnf :: OptionsPragma -> () # | |
data AgdaLibFile Source #
Content of a .agda-lib file.
Constructors
| AgdaLibFile | |
Fields
| |
Instances
libDepends :: Lens' AgdaLibFile [LibName] Source #
Library warnings and errors
Position information
type LineNumber = Int Source #
data LibPositionInfo Source #
Information about which .agda-lib file we are reading
and from where in the libraries file it came from.
Constructors
| LibPositionInfo | |
Fields
| |
Instances
Warnings
data LibWarning Source #
Constructors
| LibWarning (Maybe LibPositionInfo) LibWarning' |
Instances
data LibWarning' Source #
Library Warnings.
Constructors
| UnknownField String |
Instances
Errors
Collected errors while processing library files.
Constructors
| LibrariesFileNotFound FilePath | The user specified replacement for the default |
| LibNotFound LibrariesFile LibName | Raised when a library name could not successfully be resolved
to an |
| AmbiguousLib LibName [AgdaLibFile] | Raised when a library name is defined in several |
| LibParseError LibParseError | The |
| ReadError | An I/O Error occurred when reading a file. |
Fields
| |
| DuplicateExecutable | The |
data LibParseError Source #
Exceptions thrown by the .agda-lib parser.
Constructors
| BadLibraryName String | An invalid library name, e.g., containing spaces. |
| ReadFailure FilePath IOException | I/O error while reading file. |
| MissingFields (List1 String) | Missing these mandatory fields. |
| DuplicateFields (List1 String) | These fields occur each more than once. |
| MissingFieldName LineNumber | At the given line number, a field name is missing before the |
| BadFieldName LineNumber String | At the given line number, an invalid field name is encountered before the |
| MissingColonForField LineNumber String | At the given line number, the given field is not followed by |
| ContentWithoutField LineNumber | At the given line number, indented text (content) is not preceded by a field. |
Instances
| Pretty LibParseError Source # | Print library file parse error without position info. |
Defined in Agda.Interaction.Library.Base Methods pretty :: LibParseError -> Doc Source # prettyPrec :: Int -> LibParseError -> Doc Source # prettyList :: [LibParseError] -> Doc Source # | |
Raising warnings and errors
type LibErrWarns = [Either LibError LibWarning] Source #
Collection of LibErrors and LibWarnings.
warnings :: MonadWriter LibErrWarns m => List1 LibWarning -> m () Source #
warnings' :: MonadWriter LibErrWarns m => List1 LibWarning' -> m () Source #
raiseErrors' :: MonadWriter LibErrWarns m => List1 LibError' -> m () Source #
raiseErrors :: MonadWriter LibErrWarns m => List1 LibError -> m () Source #
Library Monad
type LibErrorIO = WriterT LibErrWarns (StateT LibState IO) Source #
Collects LibErrors and LibWarnings.
type LibM = ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) Source #
Throws Doc exceptions, still collects LibWarnings.
type LibState = (Map FilePath ProjectConfig, Map FilePath AgdaLibFile) Source #
Cache locations of project configurations and parsed .agda-lib files.
getCachedProjectConfig :: (MonadState LibState m, MonadIO m) => FilePath -> m (Maybe ProjectConfig) Source #
storeCachedProjectConfig :: (MonadState LibState m, MonadIO m) => FilePath -> ProjectConfig -> m () Source #
getCachedAgdaLibFile :: (MonadState LibState m, MonadIO m) => FilePath -> m (Maybe AgdaLibFile) Source #
storeCachedAgdaLibFile :: (MonadState LibState m, MonadIO m) => FilePath -> AgdaLibFile -> m () Source #
Prettyprinting errors and warnings
formatLibError :: [AgdaLibFile] -> LibError -> Doc Source #
Pretty-print LibError.
hasLineNumber :: LibParseError -> Maybe LineNumber Source #
Does a parse error contain a line number?
formatLibPositionInfo :: LibPositionInfo -> LibParseError -> Doc Source #
Compute a position position prefix.
Depending on the error to be printed, it will
- either give the name of the
librariesfile and a line inside it, - or give the name of the
.agda-libfile.
prettyInstalledLibraries :: [AgdaLibFile] -> Doc Source #