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
- data AgdaLibFile = AgdaLibFile {
- _libName :: LibName
- _libFile :: FilePath
- _libIncludes :: [FilePath]
- _libDepends :: [LibName]
- _libPragmas :: [String]
- emptyLibFile :: AgdaLibFile
- libName :: Lens' LibName AgdaLibFile
- libFile :: Lens' FilePath AgdaLibFile
- libIncludes :: Lens' [FilePath] AgdaLibFile
- libDepends :: Lens' [LibName] AgdaLibFile
- libPragmas :: Lens' [String] AgdaLibFile
- 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 |
data ExecutablesFile Source #
Constructors
ExecutablesFile | |
Instances
EmbPrj ExecutablesFile Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Errors | |
Generic ExecutablesFile Source # | |
Defined in Agda.Interaction.Library.Base Methods from :: ExecutablesFile -> Rep ExecutablesFile x Source # to :: Rep ExecutablesFile x -> ExecutablesFile Source # | |
Show ExecutablesFile Source # | |
Defined in Agda.Interaction.Library.Base | |
NFData ExecutablesFile Source # | |
Defined in Agda.Interaction.Library.Base Methods rnf :: ExecutablesFile -> () Source # | |
type Rep ExecutablesFile Source # | |
Defined in Agda.Interaction.Library.Base type Rep ExecutablesFile = D1 ('MetaData "ExecutablesFile" "Agda.Interaction.Library.Base" "Agda-2.6.3-F91ij4KwIR0JAPMMfugHqV" '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 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 Methods from :: ProjectConfig -> Rep ProjectConfig x Source # to :: Rep ProjectConfig x -> ProjectConfig Source # | |
NFData ProjectConfig Source # | |
Defined in Agda.Interaction.Library.Base Methods rnf :: ProjectConfig -> () Source # | |
type Rep ProjectConfig Source # | |
Defined in Agda.Interaction.Library.Base type Rep ProjectConfig = D1 ('MetaData "ProjectConfig" "Agda.Interaction.Library.Base" "Agda-2.6.3-F91ij4KwIR0JAPMMfugHqV" '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 Source #
Content of a .agda-lib
file.
Constructors
AgdaLibFile | |
Fields
|
Instances
libDepends :: Lens' [LibName] AgdaLibFile Source #
libPragmas :: Lens' [String] AgdaLibFile 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
EmbPrj LibWarning' Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Errors | |
Pretty LibWarning' Source # | |
Defined in Agda.Interaction.Library.Base Methods pretty :: LibWarning' -> Doc Source # prettyPrec :: Int -> LibWarning' -> Doc Source # prettyList :: [LibWarning'] -> Doc Source # | |
Generic LibWarning' Source # | |
Defined in Agda.Interaction.Library.Base Methods from :: LibWarning' -> Rep LibWarning' x Source # to :: Rep LibWarning' x -> LibWarning' Source # | |
Show LibWarning' Source # | |
Defined in Agda.Interaction.Library.Base | |
NFData LibWarning' Source # | |
Defined in Agda.Interaction.Library.Base Methods rnf :: LibWarning' -> () Source # | |
type Rep LibWarning' Source # | |
Defined in Agda.Interaction.Library.Base type Rep LibWarning' = D1 ('MetaData "LibWarning'" "Agda.Interaction.Library.Base" "Agda-2.6.3-F91ij4KwIR0JAPMMfugHqV" 'False) (C1 ('MetaCons "UnknownField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) |
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 LibError
s and LibWarning
s.
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 LibError
s and LibWarning
s.
type LibM = ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) Source #
Throws Doc
exceptions, still collects LibWarning
s.
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
libraries
file and a line inside it, - or give the name of the
.agda-lib
file.
prettyInstalledLibraries :: [AgdaLibFile] -> Doc Source #