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)
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 {
- libFilePos :: Maybe FilePath
- lineNumPos :: LineNumber
- filePos :: FilePath
}
libraryWarningName :: LibWarning -> WarningName
data ProjectConfig
- = ProjectConfig {
  - configRoot :: FilePath
  - configAgdaLibFiles :: [FilePath]
  - configAbove :: !Int
  }
- | DefaultProjectConfig
data VersionView = VersionView {
- vvBase :: LibName
- vvNumbers :: [Integer]
}
versionView :: LibName -> VersionView
unVersionView :: VersionView -> LibName
findLib' :: (a -> LibName) -> LibName -> [a] -> [a]

Documentation

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

Get project root

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).)

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.

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.

type LibName = String Source #

A symbolic library name.

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 pragmaStrings :: [String] The options. pragmaRange :: Range The range of the options in the pragma (not including things like an `OPTIONS` keyword).

Instances

Instances details

EmbPrj OptionsPragma Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OptionsPragma -> S Int32 Source # icod_ :: OptionsPragma -> S Int32 Source # value :: Int32 -> 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

data AgdaLibFile Source #

Content of a .agda-lib file.

Constructors

AgdaLibFile

Fields

_libName :: LibName
The symbolic name of the library.
_libFile :: FilePath
Path to this .agda-lib file (not content of the file).
_libAbove :: !Int
How many directories above the Agda file is the .agda-lib file located?
_libIncludes :: [FilePath]
Roots where to look for the modules of the library.
_libDepends :: [LibName]
Dependencies.
_libPragmas :: OptionsPragma
Default pragma options for all files in the library.

Instances

Instances details

NFData AgdaLibFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: AgdaLibFile -> ()

Generic AgdaLibFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep AgdaLibFile

Instance details

Defined in Agda.Interaction.Library.Base

type Rep AgdaLibFile = D1 ('MetaData "AgdaLibFile" "Agda.Interaction.Library.Base" "Agda-2.6.20240731-inplace" '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 "_libAbove") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))) :*: (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 OptionsPragma)))))

Methods

from :: AgdaLibFile -> Rep AgdaLibFile x

to :: Rep AgdaLibFile x -> AgdaLibFile

Show AgdaLibFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> AgdaLibFile -> ShowS

show :: AgdaLibFile -> String

showList :: [AgdaLibFile] -> ShowS

type Rep AgdaLibFile Source #

Instance details

Defined in Agda.Interaction.Library.Base

type Rep AgdaLibFile = D1 ('MetaData "AgdaLibFile" "Agda.Interaction.Library.Base" "Agda-2.6.20240731-inplace" '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 "_libAbove") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))) :*: (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 OptionsPragma)))))

type ExeName = Text Source #

A symbolic executable name.

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

Instances details

Pretty LibWarning Source #

Instance details

Defined in Agda.Interaction.Library.Base

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 #

NFData LibWarning Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibWarning -> ()

Generic LibWarning Source #

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibWarning

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibWarning = D1 ('MetaData "LibWarning" "Agda.Interaction.Library.Base" "Agda-2.6.20240731-inplace" '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')))

Methods

from :: LibWarning -> Rep LibWarning x

to :: Rep LibWarning x -> LibWarning

Show LibWarning Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibWarning -> ShowS

show :: LibWarning -> String

showList :: [LibWarning] -> ShowS

type Rep LibWarning Source #

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibWarning = D1 ('MetaData "LibWarning" "Agda.Interaction.Library.Base" "Agda-2.6.20240731-inplace" '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 #

Information about which .agda-lib file we are reading and from where in the libraries file it came from.

Constructors

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

Instances

Instances details

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 #

NFData LibPositionInfo Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibPositionInfo -> ()

Generic LibPositionInfo Source #

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibPositionInfo

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibPositionInfo = D1 ('MetaData "LibPositionInfo" "Agda.Interaction.Library.Base" "Agda-2.6.20240731-inplace" '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))))

Methods

from :: LibPositionInfo -> Rep LibPositionInfo x

to :: Rep LibPositionInfo x -> LibPositionInfo

Show LibPositionInfo Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> LibPositionInfo -> ShowS

show :: LibPositionInfo -> String

showList :: [LibPositionInfo] -> ShowS

type Rep LibPositionInfo Source #

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibPositionInfo = D1 ('MetaData "LibPositionInfo" "Agda.Interaction.Library.Base" "Agda-2.6.20240731-inplace" '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))))

libraryWarningName :: LibWarning -> WarningName Source #

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 configRoot :: FilePath configAgdaLibFiles :: [FilePath] configAbove :: !Int How many directories above the Agda file is the `.agda-lib` file located?
DefaultProjectConfig

Instances

Instances details

NFData ProjectConfig Source #

Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: ProjectConfig -> ()

Generic ProjectConfig Source #

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep ProjectConfig

Instance details

Defined in Agda.Interaction.Library.Base

type Rep ProjectConfig = D1 ('MetaData "ProjectConfig" "Agda.Interaction.Library.Base" "Agda-2.6.20240731-inplace" '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))

Methods

from :: ProjectConfig -> Rep ProjectConfig x

to :: Rep ProjectConfig x -> ProjectConfig

type Rep ProjectConfig Source #

Instance details

Defined in Agda.Interaction.Library.Base

type Rep ProjectConfig = D1 ('MetaData "ProjectConfig" "Agda.Interaction.Library.Base" "Agda-2.6.20240731-inplace" '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
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

Show VersionView Source #
Instance details Defined in Agda.Interaction.Library Methods showsPrec :: Int -> VersionView -> ShowS show :: VersionView -> String showList :: [VersionView] -> ShowS
Eq VersionView Source #
Instance details Defined in Agda.Interaction.Library Methods (==) :: VersionView -> VersionView -> Bool (/=) :: VersionView -> VersionView -> Bool

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" ] == []