Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- 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 IO
- data VersionView = VersionView {}
- versionView :: LibName -> VersionView
- unVersionView :: VersionView -> LibName
- findLib' :: (a -> LibName) -> LibName -> [a] -> [a]
Documentation
:: 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 #
:: 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.
:: 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.
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.
Instances
Eq VersionView Source # | |
Defined in Agda.Interaction.Library (==) :: VersionView -> VersionView -> Bool # (/=) :: VersionView -> VersionView -> Bool # | |
Show VersionView Source # | |
Defined in Agda.Interaction.Library 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" ] == []