ModuleAgda-2.7.0.1Haskell2010

Agda.Interaction.Library.Base

Basic data types for library management.

19 types
22 values

PackageAgda-2.7.0.1
Exports41
LanguageHaskell2010
LicenceMIT
SourceBase.hs

typetype LibName = String

A symbolic library name.

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.7.0.1 · Agda.Interaction.Library.Base
Generic LibrariesFileDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
NFData LibrariesFileDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
type Rep LibrariesFile = D1 ('MetaData "LibrariesFile" "Agda.Interaction.Library.Base" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" '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.7.0.1 · Agda.Interaction.Library.Base

typetype ExeName = Text

A symbolic executable name.

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.7.0.1 · Agda.Interaction.Library.Base
Generic ExecutablesFileDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
NFData ExecutablesFileDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
EmbPrj ExecutablesFileDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep ExecutablesFile = D1 ('MetaData "ExecutablesFile" "Agda.Interaction.Library.Base" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" '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.7.0.1 · Agda.Interaction.Library.Base

valuelibNameForCurrentDir :: LibName

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

datadata 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
- configRoot :: FilePath
- configAgdaLibFiles :: [FilePath]
- configAbove :: !Int
  How many directories above the Agda file is the .agda-lib file located?
DefaultProjectConfig

Instances3Generic, NFData, Rep

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

datadata OptionsPragma

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.7.0.1 · Agda.Interaction.Library.Base
Semigroup OptionsPragmaDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
Monoid OptionsPragmaDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
NFData OptionsPragmaDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
Ranges are not forced.
EmbPrj OptionsPragmaDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan

datadata AgdaLibFile

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.7.0.1 · Agda.Interaction.Library.Base
Generic AgdaLibFileDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
NFData AgdaLibFileDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
type Rep AgdaLibFile = D1 ('MetaData "AgdaLibFile" "Agda.Interaction.Library.Base" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" '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.7.0.1 · Agda.Interaction.Library.Base

valueemptyLibFile :: AgdaLibFile

valuelibName :: Lens' AgdaLibFile LibName

Lenses for AgdaLibFile

valuelibFile :: Lens' AgdaLibFile FilePath

valuelibAbove :: Lens' AgdaLibFile Int

valuelibIncludes :: Lens' AgdaLibFile [FilePath]

valuelibDepends :: Lens' AgdaLibFile [LibName]

valuelibPragmas :: Lens' AgdaLibFile OptionsPragma

Library warnings and errors

0 declarations

Position information

typetype LineNumber = Int

datadata LibPositionInfo

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.7.0.1 · Agda.Interaction.Library.Base
Generic LibPositionInfoDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
NFData LibPositionInfoDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
EmbPrj LibPositionInfoDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep LibPositionInfo = D1 ('MetaData "LibPositionInfo" "Agda.Interaction.Library.Base" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" '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.7.0.1 · Agda.Interaction.Library.Base

Warnings

datadata LibWarning

Constructors

LibWarning (Maybe LibPositionInfo) LibWarning'

Instances6Show, Generic, NFData, Pretty, EmbPrj, Rep

Show LibWarningDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
Generic LibWarningDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
NFData LibWarningDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
Pretty LibWarningDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
EmbPrj LibWarningDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep LibWarning = D1 ('MetaData "LibWarning" "Agda.Interaction.Library.Base" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" '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.7.0.1 · Agda.Interaction.Library.Base

datadata LibWarning'

Library Warnings.

Constructors

UnknownField String

Instances6Show, Generic, NFData, Pretty, EmbPrj, Rep

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

valuelibraryWarningName :: LibWarning -> WarningName

Errors

3 declarations

datadata LibError

Constructors

LibError (Maybe LibPositionInfo) LibError'

Instances4Show, Generic, NFData, Rep

Show LibErrorDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
Generic LibErrorDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
NFData LibErrorDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
type Rep LibError = D1 ('MetaData "LibError" "Agda.Interaction.Library.Base" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" '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.7.0.1 · Agda.Interaction.Library.Base

datadata LibError'

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 [AgdaLibFile]
Raised when a library name is defined in several .agda-lib files.
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.7.0.1 · Agda.Interaction.Library.Base
Generic LibError'Defined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
NFData LibError'Defined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
Pretty LibError'Defined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
Pretty-print library management error without position info.
type Rep LibError' = D1 ('MetaData "LibError'" "Agda.Interaction.Library.Base" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" '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 [AgdaLibFile])))) :+: (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.7.0.1 · Agda.Interaction.Library.Base

datadata LibParseError

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.7.0.1 · Agda.Interaction.Library.Base
Generic LibParseErrorDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
NFData LibParseErrorDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
Pretty LibParseErrorDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
Print library file parse error without position info.
type Rep LibParseError = D1 ('MetaData "LibParseError" "Agda.Interaction.Library.Base" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" '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.7.0.1 · Agda.Interaction.Library.Base

Raising warnings and errors

typetype LibErrWarns = [Either LibError LibWarning]

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

8 declarations

typetype LibErrorIO = WriterT LibErrWarns (StateT LibState IO)

Collects LibErrors and LibWarnings.

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

Throws LibErrors exceptions, still collects LibWarnings.

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

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

datadata LibErrors

Collected errors when processing an .agda-lib file.

Constructors

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

Instances4Show, Generic, NFData, Rep

Show LibErrorsDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
Generic LibErrorsDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
NFData LibErrorsDefined in Agda-2.7.0.1 · Agda.Interaction.Library.Base
type Rep LibErrors = D1 ('MetaData "LibErrors" "Agda.Interaction.Library.Base" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" '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.7.0.1 · Agda.Interaction.Library.Base

valuegetCachedProjectConfig

valuestoreCachedProjectConfig

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

valuegetCachedAgdaLibFile

valuestoreCachedAgdaLibFile

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

Prettyprinting errors and warnings

5 declarations

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

Pretty-print LibError.

valueformatLibErrors :: LibErrors -> Doc

Pretty-print LibErrors.

valuehasLineNumber :: LibParseError -> Maybe LineNumber

Does a parse error contain a line number?

valueformatLibPositionInfo :: LibPositionInfo -> LibParseError -> Doc

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.

valueprettyInstalledLibraries :: [AgdaLibFile] -> Doc

Orphan instances

1 instance

NFData IOException