Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.Library.Base

Description

Basic data types for library management.

Synopsis

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
NFData LibrariesFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibrariesFile -> ()

Generic LibrariesFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibrariesFile 
Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibrariesFile = D1 ('MetaData "LibrariesFile" "Agda.Interaction.Library.Base" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "LibrariesFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "lfPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "lfExists") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))
Show LibrariesFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibrariesFile -> ShowS

show :: LibrariesFile -> String

showList :: [LibrariesFile] -> ShowS

type Rep LibrariesFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibrariesFile = D1 ('MetaData "LibrariesFile" "Agda.Interaction.Library.Base" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "LibrariesFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "lfPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "lfExists") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

type ExeName = Text Source #

A symbolic executable name.

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

NFData ExecutablesFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: ExecutablesFile -> ()

Generic ExecutablesFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep ExecutablesFile 
Instance details

Defined in Agda.Interaction.Library.Base

type Rep ExecutablesFile = D1 ('MetaData "ExecutablesFile" "Agda.Interaction.Library.Base" "Agda-2.6.20240714-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)))
Show ExecutablesFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> ExecutablesFile -> ShowS

show :: ExecutablesFile -> String

showList :: [ExecutablesFile] -> ShowS

type Rep ExecutablesFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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

DefaultProjectConfig 

Instances

Instances details
NFData ProjectConfig Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: ProjectConfig -> ()

Generic ProjectConfig Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep ProjectConfig 
Instance details

Defined in Agda.Interaction.Library.Base

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

Instances

Instances details
EmbPrj OptionsPragma Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: OptionsPragma -> S Int32 Source #

icod_ :: OptionsPragma -> S Int32 Source #

value :: Int32 -> R OptionsPragma Source #

NFData OptionsPragma Source #

Ranges are not forced.

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: OptionsPragma -> ()

Monoid OptionsPragma Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Semigroup OptionsPragma Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Show OptionsPragma Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> OptionsPragma -> ShowS

show :: OptionsPragma -> String

showList :: [OptionsPragma] -> ShowS

data AgdaLibFile Source #

Content of a .agda-lib file.

Constructors

AgdaLibFile 

Fields

Instances

Instances details
NFData AgdaLibFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: AgdaLibFile -> ()

Generic AgdaLibFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep AgdaLibFile 
Instance details

Defined in Agda.Interaction.Library.Base

type Rep AgdaLibFile = D1 ('MetaData "AgdaLibFile" "Agda.Interaction.Library.Base" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "AgdaLibFile" 'PrefixI 'True) ((S1 ('MetaSel ('Just "_libName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibName) :*: (S1 ('MetaSel ('Just "_libFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "_libAbove") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))) :*: (S1 ('MetaSel ('Just "_libIncludes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]) :*: (S1 ('MetaSel ('Just "_libDepends") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LibName]) :*: S1 ('MetaSel ('Just "_libPragmas") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OptionsPragma)))))

Methods

from :: AgdaLibFile -> Rep AgdaLibFile x

to :: Rep AgdaLibFile x -> AgdaLibFile

Show AgdaLibFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> AgdaLibFile -> ShowS

show :: AgdaLibFile -> String

showList :: [AgdaLibFile] -> ShowS

type Rep AgdaLibFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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

libName :: Lens' AgdaLibFile LibName Source #

Lenses for AgdaLibFile

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

Instances

Instances details
EmbPrj LibPositionInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

NFData LibPositionInfo Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibPositionInfo -> ()

Generic LibPositionInfo Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibPositionInfo 
Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibPositionInfo = D1 ('MetaData "LibPositionInfo" "Agda.Interaction.Library.Base" "Agda-2.6.20240714-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))))
Show LibPositionInfo Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibPositionInfo -> ShowS

show :: LibPositionInfo -> String

showList :: [LibPositionInfo] -> ShowS

type Rep LibPositionInfo Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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

Instances

Instances details
Pretty LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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 #

NFData LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibWarning -> ()

Generic LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibWarning 
Instance details

Defined in Agda.Interaction.Library.Base

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

Methods

from :: LibWarning -> Rep LibWarning x

to :: Rep LibWarning x -> LibWarning

Show LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibWarning -> ShowS

show :: LibWarning -> String

showList :: [LibWarning] -> ShowS

type Rep LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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

data LibWarning' Source #

Library Warnings.

Constructors

UnknownField String 

Instances

Instances details
Pretty LibWarning' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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 #

NFData LibWarning' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibWarning' -> ()

Generic LibWarning' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibWarning' 
Instance details

Defined in Agda.Interaction.Library.Base

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

Methods

from :: LibWarning' -> Rep LibWarning' x

to :: Rep LibWarning' x -> LibWarning'

Show LibWarning' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibWarning' -> ShowS

show :: LibWarning' -> String

showList :: [LibWarning'] -> ShowS

type Rep LibWarning' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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

Errors

data LibError Source #

Instances

Instances details
NFData LibError Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibError -> ()

Generic LibError Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibError 
Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibError = D1 ('MetaData "LibError" "Agda.Interaction.Library.Base" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "LibError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe LibPositionInfo)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibError')))

Methods

from :: LibError -> Rep LibError x

to :: Rep LibError x -> LibError

Show LibError Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibError -> ShowS

show :: LibError -> String

showList :: [LibError] -> ShowS

type Rep LibError Source # 
Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibError = D1 ('MetaData "LibError" "Agda.Interaction.Library.Base" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "LibError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe LibPositionInfo)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibError')))

data LibError' Source #

Collected errors while processing library files.

Constructors

LibrariesFileNotFound FilePath

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

LibNotFound LibrariesFile LibName

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

AmbiguousLib LibName [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.

Instances

Instances details
Pretty LibError' Source #

Pretty-print library management error without position info.

Instance details

Defined in Agda.Interaction.Library.Base

NFData LibError' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibError' -> ()

Generic LibError' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibError' 
Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibError' = D1 ('MetaData "LibError'" "Agda.Interaction.Library.Base" "Agda-2.6.20240714-inplace" '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 [AgdaLibFile])))) :+: (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

to :: Rep LibError' x -> LibError'

Show LibError' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibError' -> ShowS

show :: LibError' -> String

showList :: [LibError'] -> ShowS

type Rep LibError' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibError' = D1 ('MetaData "LibError'" "Agda.Interaction.Library.Base" "Agda-2.6.20240714-inplace" '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 [AgdaLibFile])))) :+: (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

NFData LibParseError Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibParseError -> ()

Generic LibParseError Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibParseError 
Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibParseError = D1 ('MetaData "LibParseError" "Agda.Interaction.Library.Base" "Agda-2.6.20240714-inplace" '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)))))
Show LibParseError Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibParseError -> ShowS

show :: LibParseError -> String

showList :: [LibParseError] -> ShowS

type Rep LibParseError Source # 
Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibParseError = D1 ('MetaData "LibParseError" "Agda.Interaction.Library.Base" "Agda-2.6.20240714-inplace" '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 LibErrors and LibWarnings.

warnings :: MonadWriter LibErrWarns m => List1 LibWarning -> m () Source #

warnings' :: MonadWriter LibErrWarns m => List1 LibWarning' -> m () Source #

raiseErrors' :: MonadWriter LibErrWarns m => List1 LibError' -> m () Source #

raiseErrors :: MonadWriter LibErrWarns m => List1 LibError -> m () Source #

Library Monad

type LibErrorIO = WriterT LibErrWarns (StateT LibState IO) Source #

Collects LibErrors and LibWarnings.

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

Throws LibErrors exceptions, still collects LibWarnings.

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

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

data LibErrors Source #

Collected errors when processing an .agda-lib file.

Instances

Instances details
NFData LibErrors Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibErrors -> ()

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.6.20240714-inplace" '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

to :: Rep LibErrors x -> LibErrors

Show LibErrors Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibErrors -> ShowS

show :: LibErrors -> String

showList :: [LibErrors] -> ShowS

type Rep LibErrors Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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

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

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.

Orphan instances

NFData IOException Source # 
Instance details

Methods

rnf :: IOException -> ()