Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Interaction.Library
Contents
Description
Library management.
Sample use:
-- Get libraries as listed in.agda/libraries
file. libs <- getInstalledLibraries Nothing -- Get the libraries (and immediate paths) relevant forprojectRoot
. -- This involves locating and processing the.agda-lib
file for the project. (libNames, includePaths) <- getDefaultLibraries projectRoot True -- Get include paths of depended-on libraries. resolvedPaths <- libraryIncludePaths Nothing libs libNames let allPaths = includePaths ++ resolvedPaths
Synopsis
- findProjectRoot :: FilePath -> LibM (Maybe FilePath)
- getDefaultLibraries :: FilePath -> Bool -> LibM ([LibName], [FilePath])
- getInstalledLibraries :: Maybe FilePath -> LibM [AgdaLibFile]
- getTrustedExecutables :: LibM (Map ExeName FilePath)
- libraryIncludePaths :: Maybe FilePath -> [AgdaLibFile] -> [LibName] -> LibM [FilePath]
- getAgdaLibFiles' :: FilePath -> LibErrorIO [AgdaLibFile]
- getPrimitiveLibDir :: IO FilePath
- type LibName = String
- data AgdaLibFile = AgdaLibFile {
- _libName :: LibName
- _libFile :: FilePath
- _libIncludes :: [FilePath]
- _libDepends :: [LibName]
- _libPragmas :: [String]
- type ExeName = Text
- type LibM = ExceptT Doc (WriterT [LibWarning] (StateT LibState IO))
- mkLibM :: [AgdaLibFile] -> LibErrorIO a -> LibM a
- data LibWarning = LibWarning (Maybe LibPositionInfo) LibWarning'
- data LibPositionInfo = LibPositionInfo {
- libFilePos :: Maybe FilePath
- lineNumPos :: LineNumber
- filePos :: FilePath
- libraryWarningName :: LibWarning -> WarningName
- data ProjectConfig
- = ProjectConfig {
- configRoot :: FilePath
- configAgdaLibFiles :: [FilePath]
- | DefaultProjectConfig
- = ProjectConfig {
- data VersionView = VersionView {}
- versionView :: LibName -> VersionView
- unVersionView :: VersionView -> LibName
- findLib' :: (a -> LibName) -> LibName -> [a] -> [a]
Documentation
findProjectRoot :: FilePath -> LibM (Maybe FilePath) Source #
Get project root
Arguments
:: FilePath | Project root. |
-> Bool | Use |
-> LibM ([LibName], [FilePath]) | The returned |
Get dependencies and include paths for given project root:
Look for .agda-lib
files according to findAgdaLibFiles
.
If none are found, use default dependencies (according to defaults
file)
and current directory (project root).
getInstalledLibraries Source #
Arguments
:: Maybe FilePath | Override the default |
-> LibM [AgdaLibFile] | Content of library files. (Might have empty |
Parse the descriptions of the libraries Agda knows about.
Returns none if there is no libraries
file.
getTrustedExecutables Source #
Return the trusted executables Agda knows about.
Returns none if there is no executables
file.
Arguments
:: Maybe FilePath |
|
-> [AgdaLibFile] | Libraries Agda knows about. |
-> [LibName] | (Non-empty) library names to be resolved to (lists of) pathes. |
-> LibM [FilePath] | Resolved pathes (no duplicates). Contains "." if |
Get all include pathes for a list of libraries to use.
getAgdaLibFiles' :: FilePath -> LibErrorIO [AgdaLibFile] Source #
Get the contents of .agda-lib
files in the given project root.
getPrimitiveLibDir :: IO FilePath Source #
Returns the absolute default lib dir. This directory is used to store the Primitive.agda file.
data AgdaLibFile Source #
Content of a .agda-lib
file.
Constructors
AgdaLibFile | |
Fields
|
Instances
Show AgdaLibFile Source # | |
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> AgdaLibFile -> ShowS show :: AgdaLibFile -> String showList :: [AgdaLibFile] -> ShowS | |
Generic AgdaLibFile Source # | |
Defined in Agda.Interaction.Library.Base Associated Types type Rep AgdaLibFile :: Type -> Type | |
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.1-LvHTW8pd3Vr2rIoKv0Upjq" '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]))))) |
type LibM = ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) Source #
Throws Doc
exceptions, still collects LibWarning
s.
mkLibM :: [AgdaLibFile] -> LibErrorIO a -> LibM a Source #
Raise collected LibErrors
as exception.
data LibWarning Source #
Constructors
LibWarning (Maybe LibPositionInfo) LibWarning' |
Instances
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 | |
Show LibWarning Source # | |
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibWarning -> ShowS show :: LibWarning -> String showList :: [LibWarning] -> ShowS | |
Generic LibWarning Source # | |
Defined in Agda.Interaction.Library.Base Associated Types type Rep LibWarning :: Type -> Type | |
NFData LibWarning Source # | |
Defined in Agda.Interaction.Library.Base Methods rnf :: LibWarning -> () | |
Pretty LibWarning Source # | |
Defined in Agda.Interaction.Library.Base Methods pretty :: LibWarning -> Doc Source # prettyPrec :: Int -> LibWarning -> Doc Source # prettyList :: [LibWarning] -> Doc Source # | |
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 # | |
type Rep LibWarning Source # | |
Defined in Agda.Interaction.Library.Base type Rep LibWarning = D1 ('MetaData "LibWarning" "Agda.Interaction.Library.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 LibPositionInfo Source #
Constructors
LibPositionInfo | |
Fields
|
Instances
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 | |
Show LibPositionInfo Source # | |
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibPositionInfo -> ShowS show :: LibPositionInfo -> String showList :: [LibPositionInfo] -> ShowS | |
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 | |
NFData LibPositionInfo Source # | |
Defined in Agda.Interaction.Library.Base Methods rnf :: LibPositionInfo -> () | |
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 # | |
type Rep LibPositionInfo Source # | |
Defined in Agda.Interaction.Library.Base type Rep LibPositionInfo = D1 ('MetaData "LibPositionInfo" "Agda.Interaction.Library.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 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.1-LvHTW8pd3Vr2rIoKv0Upjq" '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)) |
Exported for testing
data VersionView Source #
Library names are structured into the base name and a suffix of version
numbers, e.g. mylib-1.2.3
. The version suffix is optional.
Constructors
VersionView | |
Instances
Eq VersionView Source # | |
Defined in Agda.Interaction.Library | |
Show VersionView Source # | |
Defined in Agda.Interaction.Library Methods showsPrec :: Int -> VersionView -> ShowS show :: VersionView -> String showList :: [VersionView] -> ShowS |
versionView :: LibName -> VersionView Source #
Split a library name into basename and a list of version numbers.
versionView "foo-1.2.3" == VersionView "foo" [1, 2, 3] versionView "foo-01.002.3" == VersionView "foo" [1, 2, 3]
Note that because of leading zeros, versionView
is not injective.
(unVersionView . versionView
would produce a normal form.)
unVersionView :: VersionView -> LibName Source #
Print a VersionView
, inverse of versionView
(modulo leading zeros).
findLib' :: (a -> LibName) -> LibName -> [a] -> [a] Source #
Generalized version of findLib
for testing.
findLib' id "a" [ "a-1", "a-02", "a-2", "b" ] == [ "a-02", "a-2" ]
findLib' id "a" [ "a", "a-1", "a-01", "a-2", "b" ] == [ "a" ] findLib' id "a-1" [ "a", "a-1", "a-01", "a-2", "b" ] == [ "a-1", "a-01" ] findLib' id "a-2" [ "a", "a-1", "a-01", "a-2", "b" ] == [ "a-2" ] findLib' id "c" [ "a", "a-1", "a-01", "a-2", "b" ] == []