Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Interaction.Library.Base
Description
Basic data types for library management.
Synopsis
- data LibName = LibName {
- libNameBase :: Text
- libNameVersion :: [Integer]
- parseLibName :: String -> LibName
- data LibrariesFile = LibrariesFile {}
- type ExeName = Text
- type ExeMap = Map ExeName FilePath
- data ExecutablesFile = ExecutablesFile {}
- libNameForCurrentDir :: LibName
- data 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
- lensConfigAbove :: Lens' ProjectConfig Int
- 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 LibErrors (WriterT [LibWarning] (StateT LibState IO))
- type LibState = LibCache
- data LibCache = LibCache {
- projectConfigs :: !(Map FilePath ProjectConfig)
- agdaLibFiles :: !(Map FilePath AgdaLibFile)
- data LibErrors = LibErrors {}
- runLibM :: LibM a -> LibState -> IO ((Either LibErrors a, [LibWarning]), LibState)
- 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
- formatLibErrors :: LibErrors -> Doc
- hasLineNumber :: LibParseError -> Maybe LineNumber
- formatLibPositionInfo :: LibPositionInfo -> LibParseError -> Doc
- prettyInstalledLibraries :: [AgdaLibFile] -> Doc
Documentation
A symbolic library name.
Library names are structured into the base name and a suffix of version
numbers, e.g. mylib-1.2.3
. The version suffix is optional.
Constructors
LibName | |
Fields
|
Instances
parseLibName :: String -> LibName Source #
Split a library name into basename and a list of version numbers.
parseLibName "foo-1.2.3" == LibName "foo" [1, 2, 3] parseLibName "foo-01.002.3" == LibName "foo" [1, 2, 3]
Note that because of leading zeros, parseLibName
is not injective.
(prettyShow . parseLibName
would produce a normal form.)
data LibrariesFile Source #
Constructors
LibrariesFile | |
Instances
NFData LibrariesFile Source # | |||||
Defined in Agda.Interaction.Library.Base Methods rnf :: LibrariesFile -> () # | |||||
Generic LibrariesFile Source # | |||||
Defined in Agda.Interaction.Library.Base Associated Types
| |||||
Show LibrariesFile Source # | |||||
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibrariesFile -> ShowS # show :: LibrariesFile -> String # showList :: [LibrariesFile] -> ShowS # | |||||
type Rep LibrariesFile Source # | |||||
Defined in Agda.Interaction.Library.Base type Rep LibrariesFile = D1 ('MetaData "LibrariesFile" "Agda.Interaction.Library.Base" "Agda-2.8.0-inplace" 'False) (C1 ('MetaCons "LibrariesFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "lfPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "lfExists") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) |
data ExecutablesFile Source #
Constructors
ExecutablesFile | |
Instances
EmbPrj ExecutablesFile Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Errors | |||||
NFData ExecutablesFile Source # | |||||
Defined in Agda.Interaction.Library.Base Methods rnf :: ExecutablesFile -> () # | |||||
Generic ExecutablesFile Source # | |||||
Defined in Agda.Interaction.Library.Base Associated Types
Methods from :: ExecutablesFile -> Rep ExecutablesFile x # to :: Rep ExecutablesFile x -> ExecutablesFile # | |||||
Show ExecutablesFile Source # | |||||
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> ExecutablesFile -> ShowS # show :: ExecutablesFile -> String # showList :: [ExecutablesFile] -> ShowS # | |||||
type Rep ExecutablesFile Source # | |||||
Defined in Agda.Interaction.Library.Base type Rep ExecutablesFile = D1 ('MetaData "ExecutablesFile" "Agda.Interaction.Library.Base" "Agda-2.8.0-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 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 an .agda-lib file, or be part of the default project.
Constructors
ProjectConfig | |
Fields
| |
DefaultProjectConfig |
Instances
NFData ProjectConfig Source # | |||||
Defined in Agda.Interaction.Library.Base Methods rnf :: ProjectConfig -> () # | |||||
Generic ProjectConfig Source # | |||||
Defined in Agda.Interaction.Library.Base Associated Types
| |||||
type Rep ProjectConfig Source # | |||||
Defined in Agda.Interaction.Library.Base type Rep ProjectConfig = D1 ('MetaData "ProjectConfig" "Agda.Interaction.Library.Base" "Agda-2.8.0-inplace" 'False) (C1 ('MetaCons "ProjectConfig" 'PrefixI 'True) (S1 ('MetaSel ('Just "configRoot") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: (S1 ('MetaSel ('Just "configAgdaLibFile") '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 | |
NFData OptionsPragma Source # | Ranges are not forced. |
Defined in Agda.Interaction.Library.Base Methods rnf :: OptionsPragma -> () # | |
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 # |
data AgdaLibFile Source #
Content of a .agda-lib
file.
Constructors
AgdaLibFile | |
Fields
|
Instances
NFData AgdaLibFile Source # | |||||
Defined in Agda.Interaction.Library.Base Methods rnf :: AgdaLibFile -> () # | |||||
Generic AgdaLibFile Source # | |||||
Defined in Agda.Interaction.Library.Base Associated Types
| |||||
Show AgdaLibFile Source # | |||||
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> AgdaLibFile -> ShowS # show :: AgdaLibFile -> String # showList :: [AgdaLibFile] -> ShowS # | |||||
type Rep AgdaLibFile Source # | |||||
Defined in Agda.Interaction.Library.Base type Rep AgdaLibFile = D1 ('MetaData "AgdaLibFile" "Agda.Interaction.Library.Base" "Agda-2.8.0-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 "_libAbove") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))) :*: (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 OptionsPragma))))) |
Lenses
Lenses for ProjectConfig
Lenses for AgdaLibFile
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
EmbPrj LibPositionInfo Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Errors | |||||
NFData LibPositionInfo Source # | |||||
Defined in Agda.Interaction.Library.Base Methods rnf :: LibPositionInfo -> () # | |||||
Generic LibPositionInfo Source # | |||||
Defined in Agda.Interaction.Library.Base Associated Types
Methods from :: LibPositionInfo -> Rep LibPositionInfo x # to :: Rep LibPositionInfo x -> LibPositionInfo # | |||||
Show LibPositionInfo Source # | |||||
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibPositionInfo -> ShowS # show :: LibPositionInfo -> String # showList :: [LibPositionInfo] -> ShowS # | |||||
type Rep LibPositionInfo Source # | |||||
Defined in Agda.Interaction.Library.Base type Rep LibPositionInfo = D1 ('MetaData "LibPositionInfo" "Agda.Interaction.Library.Base" "Agda-2.8.0-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)))) |
Warnings
data LibWarning Source #
Constructors
LibWarning (Maybe LibPositionInfo) LibWarning' |
Instances
Pretty LibWarning Source # | |||||
Defined in Agda.Interaction.Library.Base Methods pretty :: LibWarning -> Doc Source # prettyPrec :: Int -> LibWarning -> Doc Source # prettyList :: [LibWarning] -> Doc Source # | |||||
EmbPrj LibWarning Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Errors | |||||
NFData LibWarning Source # | |||||
Defined in Agda.Interaction.Library.Base Methods rnf :: LibWarning -> () # | |||||
Generic LibWarning Source # | |||||
Defined in Agda.Interaction.Library.Base Associated Types
| |||||
Show LibWarning Source # | |||||
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibWarning -> ShowS # show :: LibWarning -> String # showList :: [LibWarning] -> ShowS # | |||||
type Rep LibWarning Source # | |||||
Defined in Agda.Interaction.Library.Base type Rep LibWarning = D1 ('MetaData "LibWarning" "Agda.Interaction.Library.Base" "Agda-2.8.0-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' Source #
Library Warnings.
Constructors
UnknownField String |
Instances
Pretty LibWarning' Source # | |||||
Defined in Agda.Interaction.Library.Base Methods pretty :: LibWarning' -> Doc Source # prettyPrec :: Int -> LibWarning' -> Doc Source # prettyList :: [LibWarning'] -> Doc Source # | |||||
EmbPrj LibWarning' Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Errors | |||||
NFData LibWarning' Source # | |||||
Defined in Agda.Interaction.Library.Base Methods rnf :: LibWarning' -> () # | |||||
Generic LibWarning' Source # | |||||
Defined in Agda.Interaction.Library.Base Associated Types
| |||||
Show LibWarning' Source # | |||||
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibWarning' -> ShowS # show :: LibWarning' -> String # showList :: [LibWarning'] -> ShowS # | |||||
type Rep LibWarning' Source # | |||||
Defined in Agda.Interaction.Library.Base type Rep LibWarning' = D1 ('MetaData "LibWarning'" "Agda.Interaction.Library.Base" "Agda-2.8.0-inplace" 'False) (C1 ('MetaCons "UnknownField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) |
Errors
Constructors
LibError (Maybe LibPositionInfo) LibError' |
Instances
NFData LibError Source # | |||||
Defined in Agda.Interaction.Library.Base | |||||
Generic LibError Source # | |||||
Defined in Agda.Interaction.Library.Base Associated Types
| |||||
Show LibError Source # | |||||
type Rep LibError Source # | |||||
Defined in Agda.Interaction.Library.Base type Rep LibError = D1 ('MetaData "LibError" "Agda.Interaction.Library.Base" "Agda-2.8.0-inplace" 'False) (C1 ('MetaCons "LibError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe LibPositionInfo)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibError'))) |
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 (List2 AgdaLibFile) | Raised when a library name is defined in several |
SeveralAgdaLibFiles FilePath (List2 FilePath) | The given project root contains more than one |
LibParseError LibParseError | The |
ReadError | An I/O Error occurred when reading a file. |
Fields
| |
DuplicateExecutable | The |
Fields
|
Instances
Pretty LibError' Source # | Pretty-print library management error without position info. | ||||
NFData LibError' Source # | |||||
Defined in Agda.Interaction.Library.Base | |||||
Generic LibError' Source # | |||||
Defined in Agda.Interaction.Library.Base Associated Types
| |||||
Show LibError' Source # | |||||
type Rep LibError' Source # | |||||
Defined in Agda.Interaction.Library.Base type Rep LibError' = D1 ('MetaData "LibError'" "Agda.Interaction.Library.Base" "Agda-2.8.0-inplace" 'False) ((C1 ('MetaCons "LibrariesFileNotFound" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath)) :+: (C1 ('MetaCons "LibNotFound" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibrariesFile) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibName)) :+: C1 ('MetaCons "AmbiguousLib" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List2 AgdaLibFile))))) :+: ((C1 ('MetaCons "SeveralAgdaLibFiles" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List2 FilePath))) :+: C1 ('MetaCons "LibParseError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibParseError))) :+: (C1 ('MetaCons "ReadError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IOException) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "DuplicateExecutable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List2 (LineNumber, FilePath)))))))) |
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 # | |||||
NFData LibParseError Source # | |||||
Defined in Agda.Interaction.Library.Base Methods rnf :: LibParseError -> () # | |||||
Generic LibParseError Source # | |||||
Defined in Agda.Interaction.Library.Base Associated Types
| |||||
Show LibParseError Source # | |||||
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibParseError -> ShowS # show :: LibParseError -> String # showList :: [LibParseError] -> ShowS # | |||||
type Rep LibParseError Source # | |||||
Defined in Agda.Interaction.Library.Base type Rep LibParseError = D1 ('MetaData "LibParseError" "Agda.Interaction.Library.Base" "Agda-2.8.0-inplace" 'False) (((C1 ('MetaCons "BadLibraryName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "ReadFailure" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IOException))) :+: (C1 ('MetaCons "MissingFields" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 String))) :+: C1 ('MetaCons "DuplicateFields" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 String))))) :+: ((C1 ('MetaCons "MissingFieldName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LineNumber)) :+: C1 ('MetaCons "BadFieldName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LineNumber) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: (C1 ('MetaCons "MissingColonForField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LineNumber) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "ContentWithoutField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LineNumber))))) |
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 LibErrors (WriterT [LibWarning] (StateT LibState IO)) Source #
Throws LibErrors
exceptions, still collects LibWarning
s.
Cache locations of project configurations and parsed .agda-lib
files.
Constructors
LibCache | |
Fields
|
Instances
Null LibCache Source # | |||||
NFData LibCache Source # | |||||
Defined in Agda.Interaction.Library.Base | |||||
Generic LibCache Source # | |||||
Defined in Agda.Interaction.Library.Base Associated Types
| |||||
type Rep LibCache Source # | |||||
Defined in Agda.Interaction.Library.Base type Rep LibCache = D1 ('MetaData "LibCache" "Agda.Interaction.Library.Base" "Agda-2.8.0-inplace" 'False) (C1 ('MetaCons "LibCache" 'PrefixI 'True) (S1 ('MetaSel ('Just "projectConfigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map FilePath ProjectConfig)) :*: S1 ('MetaSel ('Just "agdaLibFiles") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map FilePath AgdaLibFile)))) |
Collected errors when processing an .agda-lib
file.
Constructors
LibErrors | |
Fields |
Instances
NFData LibErrors Source # | |||||
Defined in Agda.Interaction.Library.Base | |||||
Generic LibErrors Source # | |||||
Defined in Agda.Interaction.Library.Base Associated Types
| |||||
Show LibErrors Source # | |||||
type Rep LibErrors Source # | |||||
Defined in Agda.Interaction.Library.Base type Rep LibErrors = D1 ('MetaData "LibErrors" "Agda.Interaction.Library.Base" "Agda-2.8.0-inplace" 'False) (C1 ('MetaCons "LibErrors" 'PrefixI 'True) (S1 ('MetaSel ('Just "libErrorsInstalledLibraries") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AgdaLibFile]) :*: S1 ('MetaSel ('Just "libErrors") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 LibError)))) |
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 #
Orphan instances
NFData IOException Source # | |
Methods rnf :: IOException -> () # |