Safe Haskell	None
Language	Haskell2010

Agda.Interaction.Library

Contents

Exported for testing
Orphan instances

Description

Library management.

Sample use:

    -- Get libraries as listed in .agda/libraries file.
    libs <- getInstalledLibraries Nothing

    -- Get the libraries (and immediate paths) relevant for projectRoot.
    -- 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 -> IO (Maybe FilePath)
getDefaultLibraries :: FilePath -> Bool -> LibM ([LibName], [FilePath])
getInstalledLibraries :: Maybe FilePath -> LibM [AgdaLibFile]
libraryIncludePaths :: Maybe FilePath -> [AgdaLibFile] -> [LibName] -> LibM [FilePath]
type LibName = String
type LibM = ExceptT Doc (WriterT [LibWarning] IO)
data LibWarning = LibWarning LibPositionInfo LibWarning'
data LibPositionInfo = LibPositionInfo {
- libFilePos :: Maybe FilePath
- lineNumPos :: LineNumber
- filePos :: FilePath
}
libraryWarningName :: LibWarning -> WarningName
data VersionView = VersionView {
- vvBase :: LibName
- vvNumbers :: [Integer]
}
versionView :: LibName -> VersionView
unVersionView :: VersionView -> LibName
findLib' :: (a -> LibName) -> LibName -> [a] -> [a]

Documentation

findProjectRoot :: FilePath -> IO (Maybe FilePath) Source #

Get project root

getDefaultLibraries Source #

Arguments

:: FilePath	Project root.
-> Bool	Use `defaults` if no `.agda-lib` file exists for this project?
-> LibM ([LibName], [FilePath])	The returned `LibName`s are all non-empty strings.

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 `libraries` file?
-> LibM [AgdaLibFile]	Content of library files. (Might have empty `LibName`s.)

Parse the descriptions of the libraries Agda knows about.

Returns none if there is no libraries file.

libraryIncludePaths Source #

Arguments

:: Maybe FilePath	`libraries` file (error reporting only).
-> [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 `[LibName]` does.

Get all include pathes for a list of libraries to use.

type LibName = String Source #

A symbolic library name.

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

Throws Doc exceptions, still collects LibWarnings.

data LibWarning Source #

Constructors

LibWarning LibPositionInfo LibWarning'

Instances

Instances details

Data LibWarning Source #
Instance details Defined in Agda.Interaction.Library 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 #
Instance details Defined in Agda.Interaction.Library Methods showsPrec :: Int -> LibWarning -> ShowS # show :: LibWarning -> String # showList :: [LibWarning] -> ShowS #
Pretty LibWarning Source #
Instance details Defined in Agda.Interaction.Library Methods pretty :: LibWarning -> Doc Source # prettyPrec :: Int -> LibWarning -> Doc Source # prettyList :: [LibWarning] -> Doc Source #
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 #

data LibPositionInfo Source #

Constructors

LibPositionInfo
Fields libFilePos :: Maybe FilePath Name of `libraries` file lineNumPos :: LineNumber Line number in `libraries` file. filePos :: FilePath Library file

Instances

Instances details

Data LibPositionInfo Source #
Instance details Defined in Agda.Interaction.Library 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 #
Instance details Defined in Agda.Interaction.Library Methods showsPrec :: Int -> LibPositionInfo -> ShowS # show :: LibPositionInfo -> String # showList :: [LibPositionInfo] -> ShowS #
EmbPrj LibPositionInfo Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: LibPositionInfo -> S Int32 Source # icod_ :: LibPositionInfo -> S Int32 Source # value :: Int32 -> R LibPositionInfo Source #

libraryWarningName :: LibWarning -> WarningName Source #

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
Fields vvBase :: LibName Actual library name. vvNumbers :: [Integer] Major version, minor version, subminor version, etc., all non-negative. Note: a priori, there is no reason why the version numbers should be `Int`s.

Instances

Instances details

Eq VersionView Source #
Instance details Defined in Agda.Interaction.Library Methods (==) :: VersionView -> VersionView -> Bool # (/=) :: VersionView -> VersionView -> Bool #
Show VersionView Source #
Instance details 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" ] == []

Orphan instances

Pretty LibWarning' Source #
Instance details Methods pretty :: LibWarning' -> Doc Source # prettyPrec :: Int -> LibWarning' -> Doc Source # prettyList :: [LibWarning'] -> Doc Source #