Agda-2.6.2.1.20220327: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Interaction.Library

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

Documentation

getDefaultLibraries Source #

Arguments

:: FilePath

Project root.

-> Bool

Use defaults if no .agda-lib file exists for this project?

-> LibM ([LibName], [FilePath])

The returned LibNames 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 LibNames.)

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 AgdaLibFile Source #

Content of a .agda-lib file.

Constructors

AgdaLibFile 

Fields

Instances

Instances details
Generic AgdaLibFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep AgdaLibFile :: Type -> Type #

Show AgdaLibFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

NFData AgdaLibFile Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: AgdaLibFile -> () #

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.2.1.20220327-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 "_libIncludes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]) :*: (S1 ('MetaSel ('Just "_libDepends") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LibName]) :*: S1 ('MetaSel ('Just "_libPragmas") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])))))

type ExeName = Text Source #

A symbolic executable name.

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

Throws Doc exceptions, still collects LibWarnings.

mkLibM :: [AgdaLibFile] -> LibErrorIO a -> LibM a Source #

Raise collected LibErrors as exception.

data LibWarning Source #

Instances

Instances details
EmbPrj LibWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Pretty LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Data LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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 #

Generic LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibWarning :: Type -> Type #

Show LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

NFData LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibWarning -> () #

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.2.1.20220327-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 #

Constructors

LibPositionInfo 

Fields

Instances

Instances details
EmbPrj LibPositionInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Data LibPositionInfo Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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 #

Generic LibPositionInfo Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibPositionInfo :: Type -> Type #

Show LibPositionInfo Source # 
Instance details

Defined in Agda.Interaction.Library.Base

NFData LibPositionInfo Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: LibPositionInfo -> () #

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

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.

Instances

Instances details
Generic ProjectConfig Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep ProjectConfig :: Type -> Type #

NFData ProjectConfig Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

rnf :: 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.2.1.20220327-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])) :+: 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 Ints.

Instances

Instances details
Show VersionView Source # 
Instance details

Defined in Agda.Interaction.Library

Eq VersionView Source # 
Instance details

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