Agda.Interaction.Library.Base

Basic data types for library management.

Documentation

type LibName = String

A symbolic library name.

data LibrariesFile

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

Show LibrariesFile

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibrariesFile -> ShowS

show :: LibrariesFile -> String

showList :: [LibrariesFile] -> ShowS

type ExeName = Text

A symbolic executable name.

data ExecutablesFile

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

EmbPrj ExecutablesFile

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ExecutablesFile -> S Int32

icod_ :: ExecutablesFile -> S Int32

value :: Int32 -> R ExecutablesFile

Generic ExecutablesFile

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep ExecutablesFile

Defined in Agda.Interaction.Library.Base

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

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> ExecutablesFile -> ShowS

show :: ExecutablesFile -> String

showList :: [ExecutablesFile] -> ShowS

NFData ExecutablesFile

Defined in Agda.Interaction.Library.Base

Methods

rnf :: ExecutablesFile -> ()

type Rep ExecutablesFile

Defined in Agda.Interaction.Library.Base

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

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

data ProjectConfig

A file can either belong to a project located at a given root containing one or more .agda-lib files, or be part of the default project.

Constructors

ProjectConfig

Fields

• configRoot :: FilePath
• configAgdaLibFiles :: [FilePath]
• configAbove :: !Int

  How many directories above the Agda file is the .agda-lib file located?

DefaultProjectConfig

Instances

Generic ProjectConfig

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep ProjectConfig

Defined in Agda.Interaction.Library.Base

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

NFData ProjectConfig

Defined in Agda.Interaction.Library.Base

Methods

rnf :: ProjectConfig -> ()

type Rep ProjectConfig

Defined in Agda.Interaction.Library.Base

type Rep ProjectConfig = D1 ('MetaData "ProjectConfig" "Agda.Interaction.Library.Base" "Agda-2.6.4.3-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]) :*: S1 ('MetaSel ('Just "configAbove") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))) :+: C1 ('MetaCons "DefaultProjectConfig" 'PrefixI 'False) (U1 :: Type -> Type))

data OptionsPragma

The options from an OPTIONS pragma (or a .agda-lib file).

In the future it might be nice to switch to a more structured representation. Note that, currently, there is not a one-to-one correspondence between list elements and options.

Constructors

OptionsPragma

Fields

• pragmaStrings :: [String]

  The options.

• pragmaRange :: Range

  The range of the options in the pragma (not including things like an OPTIONS keyword).

Instances

EmbPrj OptionsPragma

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: OptionsPragma -> S Int32

icod_ :: OptionsPragma -> S Int32

value :: Int32 -> R OptionsPragma

Monoid OptionsPragma

Defined in Agda.Interaction.Library.Base

Methods

mempty :: OptionsPragma

mappend :: OptionsPragma -> OptionsPragma -> OptionsPragma

mconcat :: [OptionsPragma] -> OptionsPragma

Semigroup OptionsPragma

Defined in Agda.Interaction.Library.Base

Methods

(<>) :: OptionsPragma -> OptionsPragma -> OptionsPragma

sconcat :: NonEmpty OptionsPragma -> OptionsPragma

stimes :: Integral b => b -> OptionsPragma -> OptionsPragma

Show OptionsPragma

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> OptionsPragma -> ShowS

show :: OptionsPragma -> String

showList :: [OptionsPragma] -> ShowS

NFData OptionsPragma

Ranges are not forced.

Defined in Agda.Interaction.Library.Base

Methods

rnf :: OptionsPragma -> ()

data AgdaLibFile

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

Generic AgdaLibFile

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep AgdaLibFile

Defined in Agda.Interaction.Library.Base

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

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> AgdaLibFile -> ShowS

show :: AgdaLibFile -> String

showList :: [AgdaLibFile] -> ShowS

NFData AgdaLibFile

Defined in Agda.Interaction.Library.Base

Methods

rnf :: AgdaLibFile -> ()

type Rep AgdaLibFile

Defined in Agda.Interaction.Library.Base

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

libName :: Lens' AgdaLibFile LibName

Lenses for AgdaLibFile

libFile :: Lens' AgdaLibFile FilePath

libAbove :: Lens' AgdaLibFile Int

libIncludes :: Lens' AgdaLibFile [FilePath]

libDepends :: Lens' AgdaLibFile [LibName]

libPragmas :: Lens' AgdaLibFile OptionsPragma

Library warnings and errors

Position information

type LineNumber = Int

data LibPositionInfo

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

EmbPrj LibPositionInfo

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibPositionInfo -> S Int32

icod_ :: LibPositionInfo -> S Int32

value :: Int32 -> R LibPositionInfo

Generic LibPositionInfo

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibPositionInfo

Defined in Agda.Interaction.Library.Base

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

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibPositionInfo -> ShowS

show :: LibPositionInfo -> String

showList :: [LibPositionInfo] -> ShowS

NFData LibPositionInfo

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibPositionInfo -> ()

type Rep LibPositionInfo

Defined in Agda.Interaction.Library.Base

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

Constructors

LibWarning (Maybe LibPositionInfo) LibWarning'

Instances

Pretty LibWarning

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibWarning -> Doc

prettyPrec :: Int -> LibWarning -> Doc

prettyList :: [LibWarning] -> Doc

EmbPrj LibWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning -> S Int32

icod_ :: LibWarning -> S Int32

value :: Int32 -> R LibWarning

Generic LibWarning

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibWarning

Defined in Agda.Interaction.Library.Base

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

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibWarning -> ShowS

show :: LibWarning -> String

showList :: [LibWarning] -> ShowS

NFData LibWarning

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibWarning -> ()

type Rep LibWarning

Defined in Agda.Interaction.Library.Base

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

Library Warnings.

Constructors

UnknownField String

Instances

Pretty LibWarning'

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibWarning' -> Doc

prettyPrec :: Int -> LibWarning' -> Doc

prettyList :: [LibWarning'] -> Doc

EmbPrj LibWarning'

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning' -> S Int32

icod_ :: LibWarning' -> S Int32

value :: Int32 -> R LibWarning'

Generic LibWarning'

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibWarning'

Defined in Agda.Interaction.Library.Base

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

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibWarning' -> ShowS

show :: LibWarning' -> String

showList :: [LibWarning'] -> ShowS

NFData LibWarning'

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibWarning' -> ()

type Rep LibWarning'

Defined in Agda.Interaction.Library.Base

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

libraryWarningName :: LibWarning -> WarningName

Errors

data LibError

Constructors

LibError (Maybe LibPositionInfo) LibError'

data LibError'

Collected errors while processing library files.

Constructors

LibrariesFileNotFound FilePath

The user specified replacement for the default libraries file does not exist.

LibNotFound LibrariesFile LibName

Raised when a library name could not successfully be resolved to an .agda-lib file.

AmbiguousLib LibName [AgdaLibFile]

Raised when a library name is defined in several .agda-lib files.

LibParseError LibParseError

The .agda-lib file could not be parsed.

ReadError

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. deriving (Show)

Instances

Pretty LibError'

Pretty-print library management error without position info.

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibError' -> Doc

prettyPrec :: Int -> LibError' -> Doc

prettyList :: [LibError'] -> Doc

data LibParseError

Exceptions thrown by the .agda-lib parser.

Constructors

BadLibraryName String

An invalid library name, e.g., containing spaces.

ReadFailure FilePath IOException

I/O error while reading file.

MissingFields (List1 String)

Missing these mandatory fields.

DuplicateFields (List1 String)

These fields occur each more than once.

MissingFieldName LineNumber

At the given line number, a field name is missing before the :.

BadFieldName LineNumber String

At the given line number, an invalid field name is encountered before the :. (E.g., containing spaces.)

MissingColonForField LineNumber String

At the given line number, the given field is not followed by :.

ContentWithoutField LineNumber

At the given line number, indented text (content) is not preceded by a field.

Instances

Pretty LibParseError

Print library file parse error without position info.

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibParseError -> Doc

prettyPrec :: Int -> LibParseError -> Doc

prettyList :: [LibParseError] -> Doc

Raising warnings and errors

type LibErrWarns = [Either LibError LibWarning]

Collection of LibErrors and LibWarnings.

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 ()

Library Monad

type LibErrorIO = WriterT LibErrWarns (StateT LibState IO)

Collects LibErrors and LibWarnings.

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

Throws Doc exceptions, still collects LibWarnings.

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

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

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 ()

Prettyprinting errors and warnings

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

Pretty-print LibError.

hasLineNumber :: LibParseError -> Maybe LineNumber

Does a parse error contain a line number?

formatLibPositionInfo :: LibPositionInfo -> LibParseError -> Doc

Compute a position position prefix.

Depending on the error to be printed, it will

• either give the name of the libraries file and a line inside it,
• or give the name of the .agda-lib file.

prettyInstalledLibraries :: [AgdaLibFile] -> Doc