Safe Haskell	None
Language	Haskell2010

Agda.Interaction.Library

Contents

Exported for testing

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 -> 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]
getAgdaLibFile :: FilePath -> LibM [AgdaLibFile]
getPrimitiveLibDir :: IO AbsolutePath
classifyBuiltinModule_ :: AbsolutePath -> AbsolutePath -> Maybe IsBuiltinModule
builtinModules :: Set FilePath
builtinModulesWithSafePostulates :: Set FilePath
builtinModulesWithUnsafePostulates :: Set FilePath
primitiveModules :: Set FilePath
data LibName
parseLibName :: String -> LibName
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 {
- libFilePos :: Maybe FilePath
- lineNumPos :: LineNumber
- filePos :: FilePath
}
libraryWarningName :: LibWarning -> WarningName
data ProjectConfig
- = ProjectConfig {
  - configRoot :: FilePath
  - configAgdaLibFile :: FilePath
  - configAbove :: !Int
  }
- | DefaultProjectConfig
findLib' :: (a -> LibName) -> LibName -> [a] -> [a]

Documentation

findProjectRoot :: FilePath -> LibM (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.

getTrustedExecutables Source #

Arguments

:: LibM (Map ExeName FilePath)

Content of executables files.

Return the trusted executables Agda knows about.

Returns none if there is no executables 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.

getAgdaLibFile :: FilePath -> LibM [AgdaLibFile] Source #

Get the content of the .agda-lib file in the given project root.

getPrimitiveLibDir :: IO AbsolutePath Source #

Returns the absolute default lib dir. This directory is used to store the Primitive.agda file.

classifyBuiltinModule_ :: AbsolutePath -> AbsolutePath -> Maybe IsBuiltinModule Source #

Determine whether the second absolute path refers to one of Agda's primitive modules. The first argument should be the result of getPrimitiveLibDir.

builtinModules :: Set FilePath Source #

All builtin modules.

builtinModulesWithSafePostulates :: Set FilePath Source #

These builtins may use postulates, and are still considered --safe.

builtinModulesWithUnsafePostulates :: Set FilePath Source #

These builtins may not use postulates under --safe. They are not automatically unsafe, but will be if they use an unsafe feature.

primitiveModules :: Set FilePath Source #

The very magical, auto-imported modules.

data LibName Source #

A symbolic library name.

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

Instances details

Pretty LibName Source #

Instance details

OptionsPragma
Fields pragmaStrings :: [String] The options. pragmaRange :: Range The range of the options in the pragma (not including things like an `OPTIONS` keyword).

EmbPrj OptionsPragma Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OptionsPragma -> S Word32 Source # icod_ :: OptionsPragma -> S Word32 Source # value :: Word32 -> R OptionsPragma Source #
NFData OptionsPragma Source #	Ranges are not forced.
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: OptionsPragma -> () #
Monoid OptionsPragma Source #
Instance details Defined in Agda.Interaction.Library.Base Methods mempty :: OptionsPragma # mappend :: OptionsPragma -> OptionsPragma -> OptionsPragma # mconcat :: [OptionsPragma] -> OptionsPragma #
Semigroup OptionsPragma Source #
Instance details Defined in Agda.Interaction.Library.Base Methods (<>) :: OptionsPragma -> OptionsPragma -> OptionsPragma # sconcat :: NonEmpty OptionsPragma -> OptionsPragma # stimes :: Integral b => b -> OptionsPragma -> OptionsPragma #
Show OptionsPragma Source #
Instance details Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> OptionsPragma -> ShowS # show :: OptionsPragma -> String # showList :: [OptionsPragma] -> ShowS #

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

ProjectConfig
Fields configRoot :: FilePath Directory which contains the `.agda-lib` file for the current project. configAgdaLibFile :: FilePath `.agda-lib` file relative to `configRoot` (filename only, no directory). configAbove :: !Int How many directories above the Agda file is the `.agda-lib` file located?
DefaultProjectConfig

Documentation

Instances

Instances

Instances

Instances

Instances

Instances

Exported for testing