Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Interaction.Library.Base

Contents

Library warnings and errors
- Position information
- Warnings
Errors
- Raising warnings and errors
Library Monad
Prettyprinting errors and warnings

Description

Basic data types for library management.

Synopsis

type LibName = String
data LibrariesFile = LibrariesFile {
- lfPath :: FilePath
- lfExists :: Bool
}
type ExeName = Text
data ExecutablesFile = ExecutablesFile {
- efPath :: FilePath
- efExists :: Bool
}
libNameForCurrentDir :: LibName
data ProjectConfig
- = ProjectConfig {
  - configRoot :: FilePath
  - configAgdaLibFiles :: [FilePath]
  }
- | DefaultProjectConfig
data AgdaLibFile = AgdaLibFile {
- _libName :: LibName
- _libFile :: FilePath
- _libIncludes :: [FilePath]
- _libDepends :: [LibName]
- _libPragmas :: [String]
}
emptyLibFile :: AgdaLibFile
libName :: Lens' LibName AgdaLibFile
libFile :: Lens' FilePath AgdaLibFile
libIncludes :: Lens' [FilePath] AgdaLibFile
libDepends :: Lens' [LibName] AgdaLibFile
libPragmas :: Lens' [String] AgdaLibFile
type LineNumber = Int
data LibPositionInfo = LibPositionInfo {
- 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 [AgdaLibFile]
- | LibParseError LibParseError
- | ReadError IOException String
- | DuplicateExecutable FilePath Text (List2 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 Doc (WriterT [LibWarning] (StateT LibState IO))
type LibState = (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
getCachedProjectConfig :: (MonadState LibState m, MonadIO m) => FilePath -> m (Maybe ProjectConfig)
storeCachedProjectConfig :: (MonadState LibState m, MonadIO m) => FilePath -> ProjectConfig -> m ()
getCachedAgdaLibFile :: (MonadState LibState m, MonadIO m) => FilePath -> m (Maybe AgdaLibFile)
storeCachedAgdaLibFile :: (MonadState LibState m, MonadIO m) => FilePath -> AgdaLibFile -> m ()
formatLibError :: [AgdaLibFile] -> LibError -> Doc
hasLineNumber :: LibParseError -> Maybe LineNumber
formatLibPositionInfo :: LibPositionInfo -> LibParseError -> Doc
prettyInstalledLibraries :: [AgdaLibFile] -> Doc

Documentation

type LibName = String Source #

A symbolic library name.

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

Show LibrariesFile Source #
Instance details Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibrariesFile -> ShowS # show :: LibrariesFile -> String # showList :: [LibrariesFile] -> ShowS #

type ExeName = Text Source #

A symbolic executable name.

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 Int32 Source # icod_ :: ExecutablesFile -> S Int32 Source # value :: Int32 -> R ExecutablesFile Source #
Generic ExecutablesFile Source #
Instance details Defined in Agda.Interaction.Library.Base Associated Types type Rep ExecutablesFile :: Type -> Type # 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 #
NFData ExecutablesFile Source #
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: ExecutablesFile -> () #
type Rep ExecutablesFile Source #
Instance details Defined in Agda.Interaction.Library.Base type Rep ExecutablesFile = D1 ('MetaData "ExecutablesFile" "Agda.Interaction.Library.Base" "Agda-2.6.2.2.20221128-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 one or more .agda-lib files, or be part of the default project.

Constructors

ProjectConfig
Fields configRoot :: FilePath configAgdaLibFiles :: [FilePath]
DefaultProjectConfig

Instances

Instances details

Generic ProjectConfig Source #
Instance details Defined in Agda.Interaction.Library.Base Associated Types type Rep ProjectConfig :: Type -> Type # Methods from :: ProjectConfig -> Rep ProjectConfig x # to :: Rep ProjectConfig x -> ProjectConfig #
NFData ProjectConfig Source #
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: 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.6.2.2.20221128-inplace" 'False) (C1 ('MetaCons "ProjectConfig" 'PrefixI 'True) (S1 ('MetaSel ('Just "configRoot") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "configAgdaLibFiles") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath])) :+: C1 ('MetaCons "DefaultProjectConfig" 'PrefixI 'False) (U1 :: Type -> Type))

data AgdaLibFile Source #

Content of a .agda-lib file.

Constructors

AgdaLibFile
Fields _libName :: LibName The symbolic name of the library. _libFile :: FilePath Path to this `.agda-lib` file (not content of the file). _libIncludes :: [FilePath] Roots where to look for the modules of the library. _libDepends :: [LibName] Dependencies. _libPragmas :: [String] Default pragma options for all files in the library.

Instances

Instances details

Generic AgdaLibFile Source #
Instance details Defined in Agda.Interaction.Library.Base Associated Types type Rep AgdaLibFile :: Type -> Type # 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 #
NFData AgdaLibFile Source #
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: AgdaLibFile -> () #
type Rep AgdaLibFile Source #
Instance details Defined in Agda.Interaction.Library.Base type Rep AgdaLibFile = D1 ('MetaData "AgdaLibFile" "Agda.Interaction.Library.Base" "Agda-2.6.2.2.20221128-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 "_libIncludes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]) :: (S1 ('MetaSel ('Just "_libDepends") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LibName]) :: S1 ('MetaSel ('Just "_libPragmas") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])))))

emptyLibFile :: AgdaLibFile Source #

libName :: Lens' LibName AgdaLibFile Source #

Lenses for AgdaLibFile

libFile :: Lens' FilePath AgdaLibFile Source #

libIncludes :: Lens' [FilePath] AgdaLibFile Source #

libDepends :: Lens' [LibName] AgdaLibFile Source #

libPragmas :: Lens' [String] AgdaLibFile Source #

Library warnings and errors

Position information

type LineNumber = Int Source #

data LibPositionInfo Source #

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

Constructors

LibPositionInfo
Fields 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 Int32 Source # icod_ :: LibPositionInfo -> S Int32 Source # value :: Int32 -> R LibPositionInfo Source #
Generic LibPositionInfo Source #
Instance details Defined in Agda.Interaction.Library.Base Associated Types type Rep LibPositionInfo :: Type -> Type # 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 #
NFData LibPositionInfo Source #
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: LibPositionInfo -> () #
type Rep LibPositionInfo Source #
Instance details Defined in Agda.Interaction.Library.Base type Rep LibPositionInfo = D1 ('MetaData "LibPositionInfo" "Agda.Interaction.Library.Base" "Agda-2.6.2.2.20221128-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

EmbPrj LibWarning Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: LibWarning -> S Int32 Source # icod_ :: LibWarning -> S Int32 Source # value :: Int32 -> R LibWarning Source #
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 #
Generic LibWarning Source #
Instance details Defined in Agda.Interaction.Library.Base Associated Types type Rep LibWarning :: Type -> Type # 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 #
NFData LibWarning Source #
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: LibWarning -> () #
type Rep LibWarning Source #
Instance details Defined in Agda.Interaction.Library.Base type Rep LibWarning = D1 ('MetaData "LibWarning" "Agda.Interaction.Library.Base" "Agda-2.6.2.2.20221128-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

EmbPrj LibWarning' Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: LibWarning' -> S Int32 Source # icod_ :: LibWarning' -> S Int32 Source # value :: Int32 -> R LibWarning' Source #
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 #
Generic LibWarning' Source #
Instance details Defined in Agda.Interaction.Library.Base Associated Types type Rep LibWarning' :: Type -> Type # 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 #
NFData LibWarning' Source #
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: LibWarning' -> () #
type Rep LibWarning' Source #
Instance details Defined in Agda.Interaction.Library.Base type Rep LibWarning' = D1 ('MetaData "LibWarning'" "Agda.Interaction.Library.Base" "Agda-2.6.2.2.20221128-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'

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 [AgdaLibFile]	Raised when a library name is defined in several `.agda-lib files`.
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 FilePath) The resolutions of the executable. deriving (Show)

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 #

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 #