Agda-2.8.0: A dependently typed functional programming language and proof assistant

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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep LibName x -> LibName Source #

Show LibName Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibName -> ShowS Source # show :: LibName -> String Source # showList :: [LibName] -> ShowS Source #
Eq LibName Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods (==) :: LibName -> LibName -> Bool Source # (/=) :: LibName -> LibName -> Bool Source #
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 Source # (<) :: LibName -> LibName -> Bool Source # (<=) :: LibName -> LibName -> Bool Source # (>) :: LibName -> LibName -> Bool Source # (>=) :: LibName -> LibName -> Bool Source # max :: LibName -> LibName -> LibName Source # min :: LibName -> LibName -> LibName Source #
Hashable LibName Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods hashWithSalt :: Int -> LibName -> Int Source # hash :: LibName -> Int Source #
type Rep LibName Source # |

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibName = D1 ('MetaData "LibName" "Agda.Interaction.Library.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep LibrariesFile x -> LibrariesFile Source #

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

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibrariesFile = D1 ('MetaData "LibrariesFile" "Agda.Interaction.Library.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep ExecutablesFile x -> ExecutablesFile Source #

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

Instance details

Defined in Agda.Interaction.Library.Base

type Rep ExecutablesFile = D1 ('MetaData "ExecutablesFile" "Agda.Interaction.Library.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep ProjectConfig x -> ProjectConfig Source #

type Rep ProjectConfig Source # |

Instance details

Defined in Agda.Interaction.Library.Base

type Rep ProjectConfig = D1 ('MetaData "ProjectConfig" "Agda.Interaction.Library.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 -> () Source #
Monoid OptionsPragma Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods mempty :: OptionsPragma Source # mappend :: OptionsPragma -> OptionsPragma -> OptionsPragma Source # mconcat :: [OptionsPragma] -> OptionsPragma Source #
Semigroup OptionsPragma Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods (<>) :: OptionsPragma -> OptionsPragma -> OptionsPragma Source # sconcat :: NonEmpty OptionsPragma -> OptionsPragma Source # stimes :: Integral b => b -> OptionsPragma -> OptionsPragma Source #
Show OptionsPragma Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> OptionsPragma -> ShowS Source # show :: OptionsPragma -> String Source # showList :: [OptionsPragma] -> ShowS Source #

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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep AgdaLibFile x -> AgdaLibFile Source #

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

Instance details

Defined in Agda.Interaction.Library.Base

type Rep AgdaLibFile = D1 ('MetaData "AgdaLibFile" "Agda.Interaction.Library.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep LibPositionInfo x -> LibPositionInfo Source #

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

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibPositionInfo = D1 ('MetaData "LibPositionInfo" "Agda.Interaction.Library.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep LibWarning x -> LibWarning Source #

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

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibWarning = D1 ('MetaData "LibWarning" "Agda.Interaction.Library.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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' -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "UnknownField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

Methods

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

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

Show LibWarning' Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibWarning' -> ShowS Source # show :: LibWarning' -> String Source # showList :: [LibWarning'] -> ShowS Source #
type Rep LibWarning' Source # |
Instance details Defined in Agda.Interaction.Library.Base type Rep LibWarning' = D1 ('MetaData "LibWarning'" "Agda.Interaction.Library.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep LibError x -> LibError Source #

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

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibError = D1 ('MetaData "LibError" "Agda.Interaction.Library.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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' -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))))))

Methods

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

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

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

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibError' = D1 ('MetaData "LibError'" "Agda.Interaction.Library.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 `:`. (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 -> () Source #
Generic LibParseError Source # |

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibParseError |

Instance details

Defined in Agda.Interaction.Library.Base

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

Methods

from :: LibParseError -> Rep LibParseError x Source #

to :: Rep LibParseError x -> LibParseError Source #

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

Instance details

Defined in Agda.Interaction.Library.Base

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

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.

#### Instances

Instances details

Null LibCache Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods empty :: LibCache Source # null :: LibCache -> Bool Source #
NFData LibCache Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: LibCache -> () Source #
Generic LibCache Source # |

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibCache |

Instance details

Defined in Agda.Interaction.Library.Base

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

Methods

from :: LibCache -> Rep LibCache x Source #

to :: Rep LibCache x -> LibCache Source #

type Rep LibCache Source # |

Instance details

Defined in Agda.Interaction.Library.Base

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

data LibErrors Source #

Collected errors when processing an `.agda-lib` file.

Constructors

LibErrors |

Fields

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

#### Instances

Instances details

NFData LibErrors Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: LibErrors -> () Source #
Generic LibErrors Source # |

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibErrors |

Instance details

Defined in Agda.Interaction.Library.Base

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

Methods

from :: LibErrors -> Rep LibErrors x Source #

to :: Rep LibErrors x -> LibErrors Source #

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

Instance details

Defined in Agda.Interaction.Library.Base

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

runLibM :: LibM a -> LibState -> IO ((Either LibErrors a, [LibWarning]), LibState) Source #

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

formatLibErrors :: LibErrors -> Doc Source #

Pretty-print `LibErrors`.

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 # |
Instance details Methods rnf :: IOException -> () Source #