ModuleAgda-2.8.0.2Haskell2010

Agda.Interaction.Library.Base

Basic data types for library management.

Contents

Lenses
Lenses for ProjectConfig
Lenses for AgdaLibFile
Library warnings and errors
Position information
Warnings
Errors
Raising warnings and errors
Library Monad
Prettyprinting errors and warnings

Synopsis

data LibName
value parseLibName
data LibrariesFile
type ExeName
type ExeMap
data ExecutablesFile
value libNameForCurrentDir
data ProjectConfig
data OptionsPragma
data AgdaLibFile
value emptyLibFile
value lensConfigAbove
value libName
value libFile
value libAbove
value libIncludes
value libDepends
value libPragmas
type LineNumber
data LibPositionInfo
data LibWarning
data LibWarning'
value libraryWarningName
data LibError
data LibError'
data LibParseError
type LibErrWarns
value warnings
value warnings'
value raiseErrors'
value raiseErrors
type LibErrorIO
type LibM
type LibState
data LibCache
data LibErrors
value runLibM
value getCachedProjectConfig
value storeCachedProjectConfig
value getCachedAgdaLibFile
value storeCachedAgdaLibFile
value formatLibError
value formatLibErrors
value hasLineNumber
value formatLibPositionInfo
value prettyInstalledLibraries

PackageAgda-2.8.0.2
Exports46
LanguageHaskell2010
LicenceMIT
SourceBase.hs

datadata LibName

Source#

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
- libNameBase :: Text
  Actual library name.
- libNameVersion :: [Integer]
  Major version, minor version, subminor version, etc., all non-negative.

Instances9Eq, Ord, Show, Generic, NFData, Hashable, …

Eq LibNameDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Ord LibNameDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
In comparisons, a missing version number is assumed to be infinity. E.g. foo > foo-2.2 > foo-2.0.1 > foo-2 > foo-1.0.
Show LibNameDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Generic LibNameDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
NFData LibNameDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Hashable LibNameDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Pretty LibNameDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Null LibNameDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
type Rep LibName = D1 ('MetaData "LibName" "Agda.Interaction.Library.Base" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "LibName" 'PrefixI 'True) (S1 ('MetaSel ('Just "libNameBase") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :*: S1 ('MetaSel ('Just "libNameVersion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Integer])))Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base

valueparseLibName :: 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.)

datadata LibrariesFile

Constructors

LibrariesFile
- lfPath :: FilePath
  E.g. ~.agdalibraries.
- lfExists :: Bool
  The libraries file might not exist, but we may print its assumed location in error messages.

Instances4Show, Generic, NFData, Rep

Show LibrariesFileDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Generic LibrariesFileDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
NFData LibrariesFileDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
type Rep LibrariesFile = D1 ('MetaData "LibrariesFile" "Agda.Interaction.Library.Base" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "LibrariesFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "lfPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "lfExists") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base

typetype ExeName = Text

Source#

A symbolic executable name.

typetype ExeMap = Map ExeName FilePath

datadata ExecutablesFile

Constructors

ExecutablesFile
- efPath :: FilePath
  E.g. ~.agdaexecutables.
- efExists :: Bool
  The executables file might not exist, but we may print its assumed location in error messages.

Instances5Show, Generic, NFData, EmbPrj, Rep

Show ExecutablesFileDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Generic ExecutablesFileDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
NFData ExecutablesFileDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
EmbPrj ExecutablesFileDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep ExecutablesFile = D1 ('MetaData "ExecutablesFile" "Agda.Interaction.Library.Base" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "ExecutablesFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "efPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "efExists") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base

valuelibNameForCurrentDir :: LibName

Source#

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

datadata 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
- configRoot :: FilePath
  Directory which contains the .agda-lib file for the current project.
- configAgdaLibFile :: FilePath
  .agda-lib file relative to configRoot (filename only, no directory).
- configAbove :: !Int
  How many directories above the Agda file is the .agda-lib file located?
DefaultProjectConfig

Instances3Generic, NFData, Rep

Generic ProjectConfigDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
NFData ProjectConfigDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
type Rep ProjectConfig = D1 ('MetaData "ProjectConfig" "Agda.Interaction.Library.Base" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" '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 'DecidedUnpack) (Rec0 Int))) :+: C1 ('MetaCons "DefaultProjectConfig" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base

datadata 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
- pragmaStrings :: [String]
  The options.
- pragmaRange :: Range
  The range of the options in the pragma (not including things like an OPTIONS keyword).

Instances5Show, Semigroup, Monoid, NFData, EmbPrj

Show OptionsPragmaDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Semigroup OptionsPragmaDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Monoid OptionsPragmaDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
NFData OptionsPragmaDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Ranges are not forced.
EmbPrj OptionsPragmaDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

datadata AgdaLibFile

Source#

Content of a .agda-lib file.

Constructors

AgdaLibFile
- _libName :: LibName
  The symbolic name of the library.
- _libFile :: FilePath
  Path to this .agda-lib file (not content of the file).
- _libAbove :: !Int
  How many directories above the Agda file is the .agda-lib file located?
- _libIncludes :: [FilePath]
  Roots where to look for the modules of the library.
- _libDepends :: [LibName]
  Dependencies.
- _libPragmas :: OptionsPragma
  Default pragma options for all files in the library.

Instances4Show, Generic, NFData, Rep

Show AgdaLibFileDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Generic AgdaLibFileDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
NFData AgdaLibFileDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
type Rep AgdaLibFile = D1 ('MetaData "AgdaLibFile" "Agda.Interaction.Library.Base" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" '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 'DecidedUnpack) (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)))))Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base

valueemptyLibFile :: AgdaLibFile

Lenses

Lenses for ProjectConfig

valuelensConfigAbove :: Lens' ProjectConfig Int

Lenses for AgdaLibFile

valuelibName :: Lens' AgdaLibFile LibName

valuelibFile :: Lens' AgdaLibFile FilePath

valuelibAbove :: Lens' AgdaLibFile Int

valuelibIncludes :: Lens' AgdaLibFile [FilePath]

valuelibDepends :: Lens' AgdaLibFile [LibName]

valuelibPragmas :: Lens' AgdaLibFile OptionsPragma

Library warnings and errors

Position information

typetype LineNumber = Int

datadata LibPositionInfo

Source#

Information about which .agda-lib file we are reading and from where in the libraries file it came from.

Constructors

LibPositionInfo
- libFilePos :: Maybe FilePath
  Name of libraries file.
- lineNumPos :: LineNumber
  Line number in libraries file.
- filePos :: FilePath
  Library file.

Instances5Show, Generic, NFData, EmbPrj, Rep

Show LibPositionInfoDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Generic LibPositionInfoDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
NFData LibPositionInfoDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
EmbPrj LibPositionInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep LibPositionInfo = D1 ('MetaData "LibPositionInfo" "Agda.Interaction.Library.Base" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" '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))))Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base

Warnings

datadata LibWarning

Constructors

LibWarning (Maybe LibPositionInfo) LibWarning'

Instances6Show, Generic, NFData, Pretty, EmbPrj, Rep

Show LibWarningDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Generic LibWarningDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
NFData LibWarningDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Pretty LibWarningDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
EmbPrj LibWarningDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep LibWarning = D1 ('MetaData "LibWarning" "Agda.Interaction.Library.Base" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "LibWarning" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe LibPositionInfo)) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibWarning')))Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base

datadata LibWarning'

Source#

Library Warnings.

Constructors

UnknownField String

Instances6Show, Generic, NFData, Pretty, EmbPrj, Rep

Show LibWarning'Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Generic LibWarning'Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
NFData LibWarning'Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Pretty LibWarning'Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
EmbPrj LibWarning'Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep LibWarning' = D1 ('MetaData "LibWarning'" "Agda.Interaction.Library.Base" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "UnknownField" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base

valuelibraryWarningName :: LibWarning -> WarningName

Errors

datadata LibError

Constructors

LibError (Maybe LibPositionInfo) LibError'

Instances4Show, Generic, NFData, Rep

Show LibErrorDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Generic LibErrorDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
NFData LibErrorDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
type Rep LibError = D1 ('MetaData "LibError" "Agda.Interaction.Library.Base" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "LibError" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe LibPositionInfo)) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibError')))Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base

datadata LibError'

Source#

Collected errors while processing library files.

Constructors

LibrariesFileNotFound FilePath
The user specified replacement for the default libraries file does not exist.
LibNotFound LibrariesFile LibName
Raised when a library name could not successfully be resolved to an .agda-lib file.
AmbiguousLib LibName (List2 AgdaLibFile)
Raised when a library name is defined in several .agda-lib files.
SeveralAgdaLibFiles FilePath (List2 FilePath)
The given project root contains more than one .agda-lib file.
LibParseError LibParseError
The .agda-lib file could not be parsed.
ReadError IOException String
An I/O Error occurred when reading a file.
DuplicateExecutable FilePath Text (List2 (LineNumber, FilePath))
The executables file contains duplicate entries.

Instances5Show, Generic, NFData, Pretty, Rep

Show LibError'Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Generic LibError'Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
NFData LibError'Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Pretty LibError'Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Pretty-print library management error without position info.
type Rep LibError' = D1 ('MetaData "LibError'" "Agda.Interaction.Library.Base" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) ((C1 ('MetaCons "LibrariesFileNotFound" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath)) :+: (C1 ('MetaCons "LibNotFound" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibrariesFile) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibName)) :+: C1 ('MetaCons "AmbiguousLib" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibName) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List2 AgdaLibFile))))) :+: ((C1 ('MetaCons "SeveralAgdaLibFiles" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List2 FilePath))) :+: C1 ('MetaCons "LibParseError" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibParseError))) :+: (C1 ('MetaCons "ReadError" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IOException) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "DuplicateExecutable" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List2 (LineNumber, FilePath))))))))Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base

datadata 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 :. (E.g., containing spaces.)
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.

Instances5Show, Generic, NFData, Pretty, Rep

Show LibParseErrorDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Generic LibParseErrorDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
NFData LibParseErrorDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Pretty LibParseErrorDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Print library file parse error without position info.
type Rep LibParseError = D1 ('MetaData "LibParseError" "Agda.Interaction.Library.Base" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (((C1 ('MetaCons "BadLibraryName" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "ReadFailure" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IOException))) :+: (C1 ('MetaCons "MissingFields" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 String))) :+: C1 ('MetaCons "DuplicateFields" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 String))))) :+: ((C1 ('MetaCons "MissingFieldName" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LineNumber)) :+: C1 ('MetaCons "BadFieldName" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LineNumber) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: (C1 ('MetaCons "MissingColonForField" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LineNumber) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "ContentWithoutField" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LineNumber)))))Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base

Raising warnings and errors

typetype LibErrWarns = [Either LibError LibWarning]

Source#

Collection of LibErrors and LibWarnings.

valuewarnings :: MonadWriter LibErrWarns m => List1 LibWarning -> m ()

valuewarnings' :: MonadWriter LibErrWarns m => List1 LibWarning' -> m ()

valueraiseErrors' :: MonadWriter LibErrWarns m => List1 LibError' -> m ()

valueraiseErrors :: MonadWriter LibErrWarns m => List1 LibError -> m ()

Library Monad

typetype LibErrorIO = WriterT LibErrWarns (StateT LibState IO)

Source#

Collects LibErrors and LibWarnings.

typetype LibM = ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO))

Source#

Throws LibErrors exceptions, still collects LibWarnings.

typetype LibState = LibCache

datadata LibCache

Source#

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

Constructors

LibCache
- projectConfigs :: !Map FilePath ProjectConfig
  Map from directories to paths of closest enclosing .agda-lib files (or DefaultProjectConfig if there are none).
- agdaLibFiles :: !Map FilePath AgdaLibFile
  Contents of .agda-lib files that have already been parsed.

Instances4Generic, NFData, Null, Rep

Generic LibCacheDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
NFData LibCacheDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Null LibCacheDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
type Rep LibCache = D1 ('MetaData "LibCache" "Agda.Interaction.Library.Base" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" '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))))Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base

datadata LibErrors

Source#

Collected errors when processing an .agda-lib file.

Constructors

LibErrors
- libErrorsInstalledLibraries :: [AgdaLibFile]
- libErrors :: List1 LibError

Instances4Show, Generic, NFData, Rep

Show LibErrorsDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
Generic LibErrorsDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
NFData LibErrorsDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
type Rep LibErrors = D1 ('MetaData "LibErrors" "Agda.Interaction.Library.Base" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" '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))))Defined in Agda-2.8.0.2 · Agda.Interaction.Library.Base