Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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
Show LibrariesFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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

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 #

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

toConstr :: ExecutablesFile -> Constr #

dataTypeOf :: ExecutablesFile -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic ExecutablesFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep ExecutablesFile :: Type -> Type #

Show ExecutablesFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

NFData ExecutablesFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: ExecutablesFile -> () #

type Rep ExecutablesFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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

Instances

Instances details
Generic ProjectConfig Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep ProjectConfig :: Type -> Type #

NFData ProjectConfig Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: ProjectConfig -> () #

type Rep ProjectConfig Source # 
Instance details

Defined in Agda.Interaction.Library.Base

type Rep ProjectConfig = D1 ('MetaData "ProjectConfig" "Agda.Interaction.Library.Base" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "ProjectConfig" 'PrefixI 'True) (S1 ('MetaSel ('Just "configRoot") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "configAgdaLibFiles") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath])) :+: C1 ('MetaCons "DefaultProjectConfig" 'PrefixI 'False) (U1 :: Type -> Type))

data AgdaLibFile Source #

Content of a .agda-lib file.

Constructors

AgdaLibFile 

Fields

Instances

Instances details
Generic AgdaLibFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep AgdaLibFile :: Type -> Type #

Show AgdaLibFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

NFData AgdaLibFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: AgdaLibFile -> () #

type Rep AgdaLibFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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

libName :: Lens' LibName AgdaLibFile Source #

Lenses for AgdaLibFile

Library warnings and errors

data LibPositionInfo Source #

Constructors

LibPositionInfo 

Fields

Instances

Instances details
EmbPrj LibPositionInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

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 #

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

toConstr :: LibPositionInfo -> Constr #

dataTypeOf :: LibPositionInfo -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic LibPositionInfo Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibPositionInfo :: Type -> Type #

Show LibPositionInfo Source # 
Instance details

Defined in Agda.Interaction.Library.Base

NFData LibPositionInfo Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibPositionInfo -> () #

type Rep LibPositionInfo Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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

data LibWarning Source #

Instances

Instances details
EmbPrj LibWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Pretty LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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 #

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

toConstr :: LibWarning -> Constr #

dataTypeOf :: LibWarning -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibWarning :: Type -> Type #

Show LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

NFData LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibWarning -> () #

type Rep LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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

data LibWarning' Source #

Library Warnings.

Constructors

UnknownField String 

Instances

Instances details
EmbPrj LibWarning' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Pretty LibWarning' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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' #

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

toConstr :: LibWarning' -> Constr #

dataTypeOf :: LibWarning' -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic LibWarning' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibWarning' :: Type -> Type #

Show LibWarning' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

NFData LibWarning' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibWarning' -> () #

type Rep LibWarning' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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

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

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 LibErrors and LibWarnings.

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

Throws Doc exceptions, still collects LibWarnings.

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 #

Prettyprinting errors and warnings