Safe Haskell	None
Language	Haskell2010

Agda.Interaction.Library.Base

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
Orphan instances

Description

Basic data types for library management.

Synopsis

data LibName = LibName {
- libNameBase :: Text
- libNameVersion :: [Integer]
}
parseLibName :: String -> LibName
data LibrariesFile = LibrariesFile {
- lfPath :: FilePath
- lfExists :: Bool
}
type ExeName = Text
type ExeMap = Map ExeName FilePath
data ExecutablesFile = ExecutablesFile {
- efPath :: FilePath
- efExists :: Bool
}
libNameForCurrentDir :: LibName
data ProjectConfig
- = ProjectConfig {
  - configRoot :: FilePath
  - configAgdaLibFile :: FilePath
  - configAbove :: !Int
  }
- | DefaultProjectConfig
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 {
- libFilePos :: Maybe FilePath
- lineNumPos :: LineNumber
- filePos :: FilePath
}
data LibWarning = LibWarning (Maybe LibPositionInfo) LibWarning'
data LibWarning' = UnknownField String
libraryWarningName :: LibWarning -> WarningName
data LibError = LibError (Maybe LibPositionInfo) LibError'
data LibError'
- = LibrariesFileNotFound FilePath
- | LibNotFound LibrariesFile LibName
- | AmbiguousLib LibName (List2 AgdaLibFile)
- | SeveralAgdaLibFiles FilePath (List2 FilePath)
- | LibParseError LibParseError
- | ReadError IOException String
- | DuplicateExecutable FilePath Text (List2 (LineNumber, FilePath))
data LibParseError
- = BadLibraryName String
- | ReadFailure FilePath IOException
- | MissingFields (List1 String)
- | DuplicateFields (List1 String)
- | MissingFieldName LineNumber
- | BadFieldName LineNumber String
- | MissingColonForField LineNumber String
- | ContentWithoutField LineNumber
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 {
- libErrorsInstalledLibraries :: [AgdaLibFile]
- libErrors :: List1 LibError
}
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

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

Instances

Instances details

Pretty LibName Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibName -> Doc Source #

prettyPrec :: Int -> LibName -> Doc Source #

prettyList :: [LibName] -> Doc Source #

Null LibName Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

empty :: LibName Source #

null :: LibName -> Bool Source #

NFData LibName Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibName -> () #

Generic LibName Source #

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibName

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibName = D1 ('MetaData "LibName" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-inplace" 'False) (C1 ('MetaCons "LibName" 'PrefixI 'True) (S1 ('MetaSel ('Just "libNameBase") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :*: S1 ('MetaSel ('Just "libNameVersion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Integer])))

Methods

from :: LibName -> Rep LibName x #

to :: Rep LibName x -> LibName #

Show LibName Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibName -> ShowS #

show :: LibName -> String #

showList :: [LibName] -> ShowS #

Eq LibName Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

(==) :: LibName -> LibName -> Bool #

(/=) :: LibName -> LibName -> Bool #

Ord LibName Source #

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.

Instance details

Defined in Agda.Interaction.Library.Base

Methods

compare :: LibName -> LibName -> Ordering #

(<) :: LibName -> LibName -> Bool #

(<=) :: LibName -> LibName -> Bool #

(>) :: LibName -> LibName -> Bool #

(>=) :: LibName -> LibName -> Bool #

max :: LibName -> LibName -> LibName #

min :: LibName -> LibName -> LibName #

Hashable LibName Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

hashWithSalt :: Int -> LibName -> Int

hash :: LibName -> Int

type Rep LibName Source #

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibName = D1 ('MetaData "LibName" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-inplace" 'False) (C1 ('MetaCons "LibName" 'PrefixI 'True) (S1 ('MetaSel ('Just "libNameBase") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :*: S1 ('MetaSel ('Just "libNameVersion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Integer])))

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
Fields lfPath :: FilePath E.g. `~.agdalibraries`. lfExists :: Bool The libraries file might not exist, but we may print its assumed location in error messages.

Instances

Instances details

NFData LibrariesFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibrariesFile -> () #

Generic LibrariesFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibrariesFile

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibrariesFile = D1 ('MetaData "LibrariesFile" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-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)))

Methods

from :: LibrariesFile -> Rep LibrariesFile x #

to :: Rep LibrariesFile x -> LibrariesFile #

Show LibrariesFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibrariesFile -> ShowS #

show :: LibrariesFile -> String #

showList :: [LibrariesFile] -> ShowS #

type Rep LibrariesFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibrariesFile = D1 ('MetaData "LibrariesFile" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-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)))

type ExeName = Text Source #

A symbolic executable name.

type ExeMap = Map ExeName FilePath Source #

data ExecutablesFile Source #

Constructors

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

Instances

Instances details

EmbPrj ExecutablesFile Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ExecutablesFile -> S Word32 Source #

icod_ :: ExecutablesFile -> S Word32 Source #

value :: Word32 -> R ExecutablesFile Source #

NFData ExecutablesFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: ExecutablesFile -> () #

Generic ExecutablesFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep ExecutablesFile

Instance details

Defined in Agda.Interaction.Library.Base

type Rep ExecutablesFile = D1 ('MetaData "ExecutablesFile" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-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)))

Methods

from :: ExecutablesFile -> Rep ExecutablesFile x #

to :: Rep ExecutablesFile x -> ExecutablesFile #

Show ExecutablesFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> ExecutablesFile -> ShowS #

show :: ExecutablesFile -> String #

showList :: [ExecutablesFile] -> ShowS #

type Rep ExecutablesFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

type Rep ExecutablesFile = D1 ('MetaData "ExecutablesFile" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-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 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

Instances

Instances details

NFData ProjectConfig Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: ProjectConfig -> () #

Generic ProjectConfig Source #

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep ProjectConfig

Instance details

Defined in Agda.Interaction.Library.Base

type Rep ProjectConfig = D1 ('MetaData "ProjectConfig" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-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))

Methods

from :: ProjectConfig -> Rep ProjectConfig x #

to :: Rep ProjectConfig x -> ProjectConfig #

type Rep ProjectConfig Source #

Instance details

Defined in Agda.Interaction.Library.Base

type Rep ProjectConfig = D1 ('MetaData "ProjectConfig" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-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 pragmaStrings :: [String] The options. pragmaRange :: Range The range of the options in the pragma (not including things like an `OPTIONS` keyword).

Instances

Instances details

EmbPrj OptionsPragma Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OptionsPragma -> S Word32 Source # icod_ :: OptionsPragma -> S Word32 Source # value :: Word32 -> R OptionsPragma Source #
NFData OptionsPragma Source #	Ranges are not forced.
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: OptionsPragma -> () #
Monoid OptionsPragma Source #
Instance details Defined in Agda.Interaction.Library.Base Methods mempty :: OptionsPragma # mappend :: OptionsPragma -> OptionsPragma -> OptionsPragma # mconcat :: [OptionsPragma] -> OptionsPragma #
Semigroup OptionsPragma Source #
Instance details Defined in Agda.Interaction.Library.Base Methods (<>) :: OptionsPragma -> OptionsPragma -> OptionsPragma # sconcat :: NonEmpty OptionsPragma -> OptionsPragma # stimes :: Integral b => b -> OptionsPragma -> OptionsPragma #
Show OptionsPragma Source #
Instance details 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

_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.

Instances

Instances details

NFData AgdaLibFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: AgdaLibFile -> () #

Generic AgdaLibFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep AgdaLibFile

Instance details

Defined in Agda.Interaction.Library.Base

type Rep AgdaLibFile = D1 ('MetaData "AgdaLibFile" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-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)))))

Methods

from :: AgdaLibFile -> Rep AgdaLibFile x #

to :: Rep AgdaLibFile x -> AgdaLibFile #

Show AgdaLibFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> AgdaLibFile -> ShowS #

show :: AgdaLibFile -> String #

showList :: [AgdaLibFile] -> ShowS #

type Rep AgdaLibFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

type Rep AgdaLibFile = D1 ('MetaData "AgdaLibFile" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-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)))))

emptyLibFile :: AgdaLibFile Source #

Lenses

Lenses for `ProjectConfig`

lensConfigAbove :: Lens' ProjectConfig Int Source #

Lenses for `AgdaLibFile`

libName :: Lens' AgdaLibFile LibName Source #

libFile :: Lens' AgdaLibFile FilePath Source #

libAbove :: Lens' AgdaLibFile Int Source #

libIncludes :: Lens' AgdaLibFile [FilePath] Source #

libDepends :: Lens' AgdaLibFile [LibName] Source #

libPragmas :: Lens' AgdaLibFile OptionsPragma 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 libFilePos :: Maybe FilePath Name of `libraries` file. lineNumPos :: LineNumber Line number in `libraries` file. filePos :: FilePath Library file.

Instances

Instances details

EmbPrj LibPositionInfo Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibPositionInfo -> S Word32 Source #

icod_ :: LibPositionInfo -> S Word32 Source #

value :: Word32 -> R LibPositionInfo Source #

NFData LibPositionInfo Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibPositionInfo -> () #

Generic LibPositionInfo Source #

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibPositionInfo

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibPositionInfo = D1 ('MetaData "LibPositionInfo" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-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))))

Methods

from :: LibPositionInfo -> Rep LibPositionInfo x #

to :: Rep LibPositionInfo x -> LibPositionInfo #

Show LibPositionInfo Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibPositionInfo -> ShowS #

show :: LibPositionInfo -> String #

showList :: [LibPositionInfo] -> ShowS #

type Rep LibPositionInfo Source #

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibPositionInfo = D1 ('MetaData "LibPositionInfo" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-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

Instances details

Pretty LibWarning Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibWarning -> Doc Source #

prettyPrec :: Int -> LibWarning -> Doc Source #

prettyList :: [LibWarning] -> Doc Source #

EmbPrj LibWarning Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning -> S Word32 Source #

icod_ :: LibWarning -> S Word32 Source #

value :: Word32 -> R LibWarning Source #

NFData LibWarning Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibWarning -> () #

Generic LibWarning Source #

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibWarning

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibWarning = D1 ('MetaData "LibWarning" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-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')))

Methods

from :: LibWarning -> Rep LibWarning x #

to :: Rep LibWarning x -> LibWarning #

Show LibWarning Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibWarning -> ShowS #

show :: LibWarning -> String #

showList :: [LibWarning] -> ShowS #

type Rep LibWarning Source #

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibWarning = D1 ('MetaData "LibWarning" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-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

Instances details

Pretty LibWarning' Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibWarning' -> Doc Source #

prettyPrec :: Int -> LibWarning' -> Doc Source #

prettyList :: [LibWarning'] -> Doc Source #

EmbPrj LibWarning' Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning' -> S Word32 Source #

icod_ :: LibWarning' -> S Word32 Source #

value :: Word32 -> R LibWarning' Source #

NFData LibWarning' Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibWarning' -> () #

Generic LibWarning' Source #

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibWarning'
Instance details Defined in Agda.Interaction.Library.Base type Rep LibWarning' = D1 ('MetaData "LibWarning'" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-inplace" 'False) (C1 ('MetaCons "UnknownField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

Methods

from :: LibWarning' -> Rep LibWarning' x #

to :: Rep LibWarning' x -> LibWarning' #

Show LibWarning' Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibWarning' -> ShowS #

show :: LibWarning' -> String #

showList :: [LibWarning'] -> ShowS #

type Rep LibWarning' Source #

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibWarning' = D1 ('MetaData "LibWarning'" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-inplace" 'False) (C1 ('MetaCons "UnknownField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

libraryWarningName :: LibWarning -> WarningName Source #

Errors

data LibError Source #

Constructors

LibError (Maybe LibPositionInfo) LibError'

Instances

Instances details

NFData LibError Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibError -> () #

Generic LibError Source #

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibError

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibError = D1 ('MetaData "LibError" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-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')))

Methods

from :: LibError -> Rep LibError x #

to :: Rep LibError x -> LibError #

Show LibError Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibError -> ShowS #

show :: LibError -> String #

showList :: [LibError] -> ShowS #

type Rep LibError Source #

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibError = D1 ('MetaData "LibError" "Agda.Interaction.Library.Base" "Agda-2.7.20250510-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')))

data 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	An I/O Error occurred when reading a file.
Fields IOException The caught exception String Explanation when this error occurred.
DuplicateExecutable	The `executables` file contains duplicate entries.
Fields FilePath Name of the `executables` file. Text Name of the executable that is defined twice. (List2 (LineNumber, FilePath)) The resolutions of the executable.

Instances

Instances details

Pretty LibError' Source #

Pretty-print library management error without position info.

Instance details

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibError' -> Doc Source #

prettyPrec :: Int -> LibError' -> Doc Source #

prettyList :: [LibError'] -> Doc Source #

NFData LibError' Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibError' -> () #

Generic LibError' Source #

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibError'

Instance details

Defined in Agda.Interaction.Library.Base

Methods

from :: LibError' -> Rep LibError' x #

to :: Rep LibError' x -> LibError' #

Show LibError' Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibError' -> ShowS #

show :: LibError' -> String #

showList :: [LibError'] -> ShowS #

type Rep LibError' Source #

Instance details

Defined in Agda.Interaction.Library.Base

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 `:`. (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.

Instances

Instances details

Pretty LibParseError Source #

Print library file parse error without position info.

Instance details

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibParseError -> Doc Source #

prettyPrec :: Int -> LibParseError -> Doc Source #

prettyList :: [LibParseError] -> Doc Source #

NFData LibParseError Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibParseError -> () #

Generic LibParseError Source #

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibParseError

Instance details

Defined in Agda.Interaction.Library.Base

Methods

from :: LibParseError -> Rep LibParseError x #

to :: Rep LibParseError x -> LibParseError #

Show LibParseError Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibParseError -> ShowS #

show :: LibParseError -> String #

showList :: [LibParseError] -> ShowS #

type Rep LibParseError Source #

Instance details

Defined in Agda.Interaction.Library.Base

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 LibErrors (WriterT [LibWarning] (StateT LibState IO)) Source #

Throws LibErrors exceptions, still collects LibWarnings.

type LibState = LibCache Source #

data LibCache Source #

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

Constructors

LibCache
Fields 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.