| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.Library
Contents
Description
Library management.
Sample use:
-- Get libraries as listed in.agda/librariesfile. libs <- getInstalledLibraries Nothing -- Get the libraries (and immediate paths) relevant forprojectRoot. -- This involves locating and processing the.agda-libfile 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)
- getAgdaAppDir :: IO 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 OptionsPragma = OptionsPragma {
- pragmaStrings :: [String]
- pragmaRange :: Range
- data AgdaLibFile = AgdaLibFile {
- _libName :: LibName
- _libFile :: FilePath
- _libAbove :: !Int
- _libIncludes :: [FilePath]
- _libDepends :: [LibName]
- _libPragmas :: OptionsPragma
- type ExeName = Text
- type LibM = ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO))
- mkLibM :: [AgdaLibFile] -> LibErrorIO a -> LibM a
- data LibWarning = LibWarning (Maybe LibPositionInfo) LibWarning'
- data LibPositionInfo = LibPositionInfo {}
- libraryWarningName :: LibWarning -> WarningName
- data ProjectConfig
- = ProjectConfig {
- configRoot :: FilePath
- configAgdaLibFiles :: [FilePath]
- configAbove :: !Int
- | DefaultProjectConfig
- = ProjectConfig {
- data VersionView = VersionView {}
- versionView :: LibName -> VersionView
- unVersionView :: VersionView -> LibName
- findLib' :: (a -> LibName) -> LibName -> [a] -> [a]
Documentation
getAgdaAppDir :: IO FilePath Source #
Get the path to ~/.agda (system-specific).
Can be overwritten by the AGDA_DIR environment variable.
(This is not to be confused with the directory for the data files that Agda needs (e.g. the primitive modules).)
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 OptionsPragma Source #
The options from an OPTIONS pragma (or a .agda-lib file).
In the future it might be nice to switch to a more structured representation. Note that, currently, there is not a one-to-one correspondence between list elements and options.
Constructors
| OptionsPragma | |
Fields
| |
Instances
| EmbPrj OptionsPragma Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common | |
| Monoid OptionsPragma Source # | |
Defined in Agda.Interaction.Library.Base Methods mempty :: OptionsPragma # mappend :: OptionsPragma -> OptionsPragma -> OptionsPragma # mconcat :: [OptionsPragma] -> OptionsPragma # | |
| Semigroup OptionsPragma Source # | |
Defined in Agda.Interaction.Library.Base Methods (<>) :: OptionsPragma -> OptionsPragma -> OptionsPragma # sconcat :: NonEmpty OptionsPragma -> OptionsPragma # stimes :: Integral b => b -> OptionsPragma -> OptionsPragma # | |
| Show OptionsPragma Source # | |
Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> OptionsPragma -> ShowS # show :: OptionsPragma -> String # showList :: [OptionsPragma] -> ShowS # | |
| NFData OptionsPragma Source # | Ranges are not forced. |
Defined in Agda.Interaction.Library.Base Methods rnf :: OptionsPragma -> () # | |
data AgdaLibFile Source #
Content of a .agda-lib file.
Constructors
| AgdaLibFile | |
Fields
| |
Instances
type LibM = ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) Source #
Throws LibErrors exceptions, still collects LibWarnings.
mkLibM :: [AgdaLibFile] -> LibErrorIO a -> LibM a Source #
Raise collected LibErrors as exception.
data LibWarning Source #
Constructors
| LibWarning (Maybe LibPositionInfo) LibWarning' |
Instances
data LibPositionInfo Source #
Information about which .agda-lib file we are reading
and from where in the libraries file it came from.
Constructors
| LibPositionInfo | |
Fields
| |
Instances
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.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "ProjectConfig" 'PrefixI 'True) (S1 ('MetaSel ('Just "configRoot") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: (S1 ('MetaSel ('Just "configAgdaLibFiles") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]) :*: S1 ('MetaSel ('Just "configAbove") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))) :+: 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
| Show VersionView Source # | |
Defined in Agda.Interaction.Library Methods showsPrec :: Int -> VersionView -> ShowS # show :: VersionView -> String # showList :: [VersionView] -> ShowS # | |
| Eq VersionView Source # | |
Defined in Agda.Interaction.Library | |
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" ] == []