Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
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]
- getAgdaLibFiles' :: FilePath -> LibErrorIO [AgdaLibFile]
- getPrimitiveLibDir :: IO FilePath
- type LibName = String
- data AgdaLibFile = AgdaLibFile {
  - _libName :: LibName
  - _libFile :: FilePath
  - _libIncludes :: [FilePath]
  - _libDepends :: [LibName]
  - _libPragmas :: [String]
  }
- type ExeName = Text
- type LibM = ExceptT Doc (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]
    }
  - | 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

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

- _libIncludes :: [FilePath]

  Roots where to look for the modules of the library.

- _libDepends :: [LibName]

  Dependencies.

- _libPragmas :: [String]

  Default pragma options for all files in the library.

#### Instances

Instances details

Generic AgdaLibFile Source # |
Instance details Defined in Agda.Interaction.Library.Base Associated Types type Rep AgdaLibFile :: Type -> Type Source # Methods from :: AgdaLibFile -> Rep AgdaLibFile x Source # to :: Rep AgdaLibFile x -> AgdaLibFile Source #
Show AgdaLibFile Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> AgdaLibFile -> ShowS Source # show :: AgdaLibFile -> String Source # showList :: [AgdaLibFile] -> ShowS Source #
NFData AgdaLibFile Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: AgdaLibFile -> () Source #
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.2-7KnEKyKhaJHFPwDzdI3vIK" '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 `LibWarning`s.

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

Raise collected `LibErrors` as exception.

data LibWarning Source #

Constructors

LibWarning (Maybe LibPositionInfo) LibWarning' |

#### Instances

Instances details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LibWarning Source #

toConstr :: LibWarning -> Constr Source #

dataTypeOf :: LibWarning -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LibWarning) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LibWarning) Source #

gmapT :: (forall b. Data b => b -> b) -> LibWarning -> LibWarning Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LibWarning -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LibWarning -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LibWarning -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LibWarning -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning Source #

Generic LibWarning Source # |
Instance details Defined in Agda.Interaction.Library.Base Associated Types type Rep LibWarning :: Type -> Type Source # Methods from :: LibWarning -> Rep LibWarning x Source # to :: Rep LibWarning x -> LibWarning Source #
Show LibWarning Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibWarning -> ShowS Source # show :: LibWarning -> String Source # showList :: [LibWarning] -> ShowS Source #
NFData LibWarning Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: LibWarning -> () Source #
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.2-7KnEKyKhaJHFPwDzdI3vIK" '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

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LibPositionInfo Source #

toConstr :: LibPositionInfo -> Constr Source #

dataTypeOf :: LibPositionInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LibPositionInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LibPositionInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> LibPositionInfo -> LibPositionInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LibPositionInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LibPositionInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LibPositionInfo -> m LibPositionInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LibPositionInfo -> m LibPositionInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LibPositionInfo -> m LibPositionInfo Source #

Generic LibPositionInfo Source # |
Instance details Defined in Agda.Interaction.Library.Base Associated Types type Rep LibPositionInfo :: Type -> Type Source # Methods from :: LibPositionInfo -> Rep LibPositionInfo x Source # to :: Rep LibPositionInfo x -> LibPositionInfo Source #
Show LibPositionInfo Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibPositionInfo -> ShowS Source # show :: LibPositionInfo -> String Source # showList :: [LibPositionInfo] -> ShowS Source #
NFData LibPositionInfo Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: LibPositionInfo -> () Source #
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.2-7KnEKyKhaJHFPwDzdI3vIK" '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]

DefaultProjectConfig |

#### Instances

Instances details

Generic ProjectConfig Source # |
Instance details Defined in Agda.Interaction.Library.Base Associated Types type Rep ProjectConfig :: Type -> Type Source # Methods from :: ProjectConfig -> Rep ProjectConfig x Source # to :: Rep ProjectConfig x -> ProjectConfig Source #
NFData ProjectConfig Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: ProjectConfig -> () Source #
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.2-7KnEKyKhaJHFPwDzdI3vIK" '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 `Int`s.

#### Instances

Instances details

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

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