Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Agda.Interaction.Library.Base
Description
Basic data types for library management.
Synopsis
- type LibName = String
- data LibrariesFile = LibrariesFile {}
- type ExeName = Text
- data ExecutablesFile = ExecutablesFile {}
- libNameForCurrentDir :: LibName
- data ProjectConfig
- = ProjectConfig {
- configRoot :: FilePath
- configAgdaLibFiles :: [FilePath]
- | DefaultProjectConfig
- = ProjectConfig {
- 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
data LibrariesFile Source #
Constructors
LibrariesFile | |
Instances
Show LibrariesFile Source # | |
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibrariesFile -> ShowS show :: LibrariesFile -> String showList :: [LibrariesFile] -> ShowS |
data ExecutablesFile Source #
Constructors
ExecutablesFile | |
Instances
EmbPrj ExecutablesFile Source # | |
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 # | |
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 # | |
Defined in Agda.Interaction.Library.Base Associated Types type Rep ExecutablesFile :: Type -> Type Methods from :: ExecutablesFile -> Rep ExecutablesFile x to :: Rep ExecutablesFile x -> ExecutablesFile | |
Show ExecutablesFile Source # | |
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> ExecutablesFile -> ShowS show :: ExecutablesFile -> String showList :: [ExecutablesFile] -> ShowS | |
NFData ExecutablesFile Source # | |
Defined in Agda.Interaction.Library.Base Methods rnf :: ExecutablesFile -> () | |
type Rep ExecutablesFile Source # | |
Defined in Agda.Interaction.Library.Base type Rep ExecutablesFile = D1 ('MetaData "ExecutablesFile" "Agda.Interaction.Library.Base" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" '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
Generic ProjectConfig Source # | |
Defined in Agda.Interaction.Library.Base Associated Types type Rep ProjectConfig :: Type -> Type | |
NFData ProjectConfig Source # | |
Defined in Agda.Interaction.Library.Base Methods rnf :: ProjectConfig -> () | |
type Rep ProjectConfig Source # | |
Defined in Agda.Interaction.Library.Base type Rep ProjectConfig = D1 ('MetaData "ProjectConfig" "Agda.Interaction.Library.Base" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" '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
Generic AgdaLibFile Source # | |
Defined in Agda.Interaction.Library.Base Associated Types type Rep AgdaLibFile :: Type -> Type | |
Show AgdaLibFile Source # | |
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> AgdaLibFile -> ShowS show :: AgdaLibFile -> String showList :: [AgdaLibFile] -> ShowS | |
NFData AgdaLibFile Source # | |
Defined in Agda.Interaction.Library.Base Methods rnf :: AgdaLibFile -> () | |
type Rep AgdaLibFile Source # | |
Defined in Agda.Interaction.Library.Base type Rep AgdaLibFile = D1 ('MetaData "AgdaLibFile" "Agda.Interaction.Library.Base" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" '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]))))) |
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
|
Instances
EmbPrj LibPositionInfo Source # | |
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 # | |
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 # | |
Defined in Agda.Interaction.Library.Base Associated Types type Rep LibPositionInfo :: Type -> Type Methods from :: LibPositionInfo -> Rep LibPositionInfo x to :: Rep LibPositionInfo x -> LibPositionInfo | |
Show LibPositionInfo Source # | |
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibPositionInfo -> ShowS show :: LibPositionInfo -> String showList :: [LibPositionInfo] -> ShowS | |
NFData LibPositionInfo Source # | |
Defined in Agda.Interaction.Library.Base Methods rnf :: LibPositionInfo -> () | |
type Rep LibPositionInfo Source # | |
Defined in Agda.Interaction.Library.Base type Rep LibPositionInfo = D1 ('MetaData "LibPositionInfo" "Agda.Interaction.Library.Base" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" '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
EmbPrj LibWarning Source # | |
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 # | |
Defined in Agda.Interaction.Library.Base Methods pretty :: LibWarning -> Doc Source # prettyPrec :: Int -> LibWarning -> Doc Source # prettyList :: [LibWarning] -> Doc Source # | |
Data LibWarning Source # | |
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 # | |
Defined in Agda.Interaction.Library.Base Associated Types type Rep LibWarning :: Type -> Type | |
Show LibWarning Source # | |
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibWarning -> ShowS show :: LibWarning -> String showList :: [LibWarning] -> ShowS | |
NFData LibWarning Source # | |
Defined in Agda.Interaction.Library.Base Methods rnf :: LibWarning -> () | |
type Rep LibWarning Source # | |
Defined in Agda.Interaction.Library.Base type Rep LibWarning = D1 ('MetaData "LibWarning" "Agda.Interaction.Library.Base" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" '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
EmbPrj LibWarning' Source # | |
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 # | |
Defined in Agda.Interaction.Library.Base Methods pretty :: LibWarning' -> Doc Source # prettyPrec :: Int -> LibWarning' -> Doc Source # prettyList :: [LibWarning'] -> Doc Source # | |
Data LibWarning' Source # | |
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 # | |
Defined in Agda.Interaction.Library.Base Associated Types type Rep LibWarning' :: Type -> Type | |
Show LibWarning' Source # | |
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibWarning' -> ShowS show :: LibWarning' -> String showList :: [LibWarning'] -> ShowS | |
NFData LibWarning' Source # | |
Defined in Agda.Interaction.Library.Base Methods rnf :: LibWarning' -> () | |
type Rep LibWarning' Source # | |
Defined in Agda.Interaction.Library.Base type Rep LibWarning' = D1 ('MetaData "LibWarning'" "Agda.Interaction.Library.Base" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "UnknownField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) |
Collected errors while processing library files.
Constructors
LibNotFound LibrariesFile LibName | Raised when a library name could not successfully be resolved
to an |
AmbiguousLib LibName [AgdaLibFile] | Raised when a library name is defined in several |
OtherError String | Generic error. |
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
.