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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Interaction.Library.Base

Contents

- Library warnings and errors
- 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
- data LibError = LibError (Maybe LibPositionInfo) LibError'
- libraryWarningName :: LibWarning -> WarningName
- data LibError'
  - = LibNotFound LibrariesFile LibName
  - | AmbiguousLib LibName [AgdaLibFile]
  - | OtherError String
- type LibState = (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
- type LibErrorIO = WriterT [Either LibError LibWarning] (StateT LibState IO)
- type LibM = ExceptT Doc (WriterT [LibWarning] (StateT LibState IO))
- warnings :: MonadWriter [Either LibError LibWarning] m => [LibWarning] -> m ()
- warnings' :: MonadWriter [Either LibError LibWarning] m => [LibWarning'] -> m ()
- raiseErrors' :: MonadWriter [Either LibError LibWarning] m => [LibError'] -> m ()
- raiseErrors :: MonadWriter [Either LibError LibWarning] m => [LibError] -> m ()
- 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 ()
- formatLibPositionInfo :: LibPositionInfo -> String -> Doc
- formatLibError :: [AgdaLibFile] -> LibError -> 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 Source # show :: LibrariesFile -> String Source # showList :: [LibrariesFile] -> ShowS Source #

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 #
Data ExecutablesFile Source # |

Instance details

Defined in Agda.Interaction.Library.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExecutablesFile -> c ExecutablesFile Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExecutablesFile Source #

toConstr :: ExecutablesFile -> Constr Source #

dataTypeOf :: ExecutablesFile -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExecutablesFile) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExecutablesFile) Source #

gmapT :: (forall b. Data b => b -> b) -> ExecutablesFile -> ExecutablesFile Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExecutablesFile -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExecutablesFile -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ExecutablesFile -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ExecutablesFile -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExecutablesFile -> m ExecutablesFile Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExecutablesFile -> m ExecutablesFile Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExecutablesFile -> m ExecutablesFile Source #

Generic ExecutablesFile Source # |
Instance details Defined in Agda.Interaction.Library.Base Associated Types type Rep ExecutablesFile :: Type -> Type Source # 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 #
NFData ExecutablesFile Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: ExecutablesFile -> () 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.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 Source # Methods from :: ProjectConfig -> Rep ProjectConfig x Source # to :: Rep ProjectConfig x -> ProjectConfig Source #
NFData ProjectConfig Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: 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.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 Source # 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 #
NFData AgdaLibFile Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: AgdaLibFile -> () 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.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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

type LineNumber = Int Source #

data LibPositionInfo Source #

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 #
Data LibPositionInfo Source # |

Instance details

Defined in Agda.Interaction.Library.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LibPositionInfo -> c LibPositionInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LibPositionInfo Source #

toConstr :: LibPositionInfo -> Constr Source #

dataTypeOf :: LibPositionInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LibPositionInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LibPositionInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> LibPositionInfo -> LibPositionInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LibPositionInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LibPositionInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LibPositionInfo -> m LibPositionInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LibPositionInfo -> m LibPositionInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LibPositionInfo -> m LibPositionInfo Source #

Generic LibPositionInfo Source # |
Instance details Defined in Agda.Interaction.Library.Base Associated Types type Rep LibPositionInfo :: Type -> Type Source # 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 #
NFData LibPositionInfo Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: LibPositionInfo -> () 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.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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))))

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 #
Data LibWarning Source # |

Instance details

Defined in Agda.Interaction.Library.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LibWarning -> c LibWarning Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LibWarning Source #

toConstr :: LibWarning -> Constr Source #

dataTypeOf :: LibWarning -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LibWarning) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LibWarning) Source #

gmapT :: (forall b. Data b => b -> b) -> LibWarning -> LibWarning Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LibWarning -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LibWarning -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LibWarning -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LibWarning -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning Source #

Generic LibWarning Source # |
Instance details Defined in Agda.Interaction.Library.Base Associated Types type Rep LibWarning :: Type -> Type Source # 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 #
NFData LibWarning Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: LibWarning -> () 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.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 #
Data LibWarning' Source # |

Instance details

Defined in Agda.Interaction.Library.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LibWarning' -> c LibWarning' Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LibWarning' Source #

toConstr :: LibWarning' -> Constr Source #

dataTypeOf :: LibWarning' -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LibWarning') Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LibWarning') Source #

gmapT :: (forall b. Data b => b -> b) -> LibWarning' -> LibWarning' Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LibWarning' -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LibWarning' -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning' Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning' Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning' Source #

Generic LibWarning' Source # |
Instance details Defined in Agda.Interaction.Library.Base Associated Types type Rep LibWarning' :: Type -> Type Source # 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 #
NFData LibWarning' Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: LibWarning' -> () 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.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "UnknownField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

data LibError Source #

Constructors

LibError (Maybe LibPositionInfo) LibError' |

libraryWarningName :: LibWarning -> WarningName Source #

data LibError' Source #

Collected errors while processing library files.

Constructors

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`.
OtherError String | Generic error.

#### Instances

Instances details

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 LibState = (Map FilePath ProjectConfig, Map FilePath AgdaLibFile) Source #

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

type LibErrorIO = WriterT [Either LibError LibWarning] (StateT LibState IO) Source #

Collects `LibError`s and `LibWarning`s.

type LibM = ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) Source #

Throws `Doc` exceptions, still collects `LibWarning`s.

warnings :: MonadWriter [Either LibError LibWarning] m => [LibWarning] -> m () Source #

warnings' :: MonadWriter [Either LibError LibWarning] m => [LibWarning'] -> m () Source #

raiseErrors' :: MonadWriter [Either LibError LibWarning] m => [LibError'] -> m () Source #

raiseErrors :: MonadWriter [Either LibError LibWarning] m => [LibError] -> m () 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

formatLibPositionInfo :: LibPositionInfo -> String -> Doc Source #

formatLibError :: [AgdaLibFile] -> LibError -> Doc Source #

Pretty-print `LibError`.