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

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 Defined in Agda.Interaction.Library.Base Methods pretty :: LibName -> Doc Source # prettyPrec :: Int -> LibName -> Doc Source # prettyList :: [LibName] -> Doc Source #
Null LibName Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods empty :: LibName Source # null :: LibName -> Bool Source #
NFData LibName Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: LibName -> () Source #
Generic LibName Source # |

Instance details

Defined in Agda.Interaction.Library.Base

Associated Types

type Rep LibName |

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibName = D1 ('MetaData "LibName" "Agda.Interaction.Library.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "LibName" 'PrefixI 'True) (S1 ('MetaSel ('Just "libNameBase") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :*: S1 ('MetaSel ('Just "libNameVersion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Integer])))

Methods

from :: LibName -> Rep LibName x Source #

to :: Rep LibName x -> LibName Source #

Show LibName Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> LibName -> ShowS Source # show :: LibName -> String Source # showList :: [LibName] -> ShowS Source #
Eq LibName Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods (==) :: LibName -> LibName -> Bool Source # (/=) :: LibName -> LibName -> Bool Source #
Ord LibName Source # | In comparisons, a missing version number is assumed to be infinity. E.g. `foo > foo-2.2 > foo-2.0.1 > foo-2 > foo-1.0`.
Instance details Defined in Agda.Interaction.Library.Base Methods compare :: LibName -> LibName -> Ordering Source # (<) :: LibName -> LibName -> Bool Source # (<=) :: LibName -> LibName -> Bool Source # (>) :: LibName -> LibName -> Bool Source # (>=) :: LibName -> LibName -> Bool Source # max :: LibName -> LibName -> LibName Source # min :: LibName -> LibName -> LibName Source #
Hashable LibName Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods hashWithSalt :: Int -> LibName -> Int Source # hash :: LibName -> Int Source #
type Rep LibName Source # |

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibName = D1 ('MetaData "LibName" "Agda.Interaction.Library.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "LibName" 'PrefixI 'True) (S1 ('MetaSel ('Just "libNameBase") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :*: S1 ('MetaSel ('Just "libNameVersion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Integer])))

parseLibName :: String -> LibName Source #

Split a library name into basename and a list of version numbers.

    parseLibName "foo-1.2.3"    == LibName "foo" [1, 2, 3]
    parseLibName "foo-01.002.3" == LibName "foo" [1, 2, 3]

Note that because of leading zeros, `parseLibName` is not injective. (`prettyShow . parseLibName` would produce a normal form.)

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 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 -> () Source #
Monoid OptionsPragma Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods mempty :: OptionsPragma Source # mappend :: OptionsPragma -> OptionsPragma -> OptionsPragma Source # mconcat :: [OptionsPragma] -> OptionsPragma Source #
Semigroup OptionsPragma Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods (<>) :: OptionsPragma -> OptionsPragma -> OptionsPragma Source # sconcat :: NonEmpty OptionsPragma -> OptionsPragma Source # stimes :: Integral b => b -> OptionsPragma -> OptionsPragma Source #
Show OptionsPragma Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> OptionsPragma -> ShowS Source # show :: OptionsPragma -> String Source # showList :: [OptionsPragma] -> ShowS Source #

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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 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 #
type Rep AgdaLibFile Source # |

Instance details

Defined in Agda.Interaction.Library.Base

type Rep AgdaLibFile = D1 ('MetaData "AgdaLibFile" "Agda.Interaction.Library.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 `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

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 Word32 Source # icod_ :: LibWarning -> S Word32 Source # value :: Word32 -> R LibWarning Source #
NFData LibWarning Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: LibWarning -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 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 #
type Rep LibWarning Source # |

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibWarning = D1 ('MetaData "LibWarning" "Agda.Interaction.Library.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Word32 Source # icod_ :: LibPositionInfo -> S Word32 Source # value :: Word32 -> R LibPositionInfo Source #
NFData LibPositionInfo Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: LibPositionInfo -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 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 #
type Rep LibPositionInfo Source # |

Instance details

Defined in Agda.Interaction.Library.Base

type Rep LibPositionInfo = D1 ('MetaData "LibPositionInfo" "Agda.Interaction.Library.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 an .agda-lib file, or be part of the default project.

Constructors

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 |

#### Instances

Instances details

NFData ProjectConfig Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods rnf :: ProjectConfig -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ProjectConfig" 'PrefixI 'True) (S1 ('MetaSel ('Just "configRoot") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: (S1 ('MetaSel ('Just "configAgdaLibFile") '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 Source #

to :: Rep ProjectConfig x -> 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.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ProjectConfig" 'PrefixI 'True) (S1 ('MetaSel ('Just "configRoot") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: (S1 ('MetaSel ('Just "configAgdaLibFile") '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

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