| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Interaction.Imports

Description
This module deals with finding imported modules and loading their interface files.
Synopsis

data RelativeTo

= ProjectRoot
| CurrentDir

moduleName :: FilePath -> TCM TopLevelModuleName
moduleName' :: AbsolutePath -> TCM TopLevelModuleName
mergeInterface :: Interface -> TCM ()
addImportedThings :: Signature -> BuiltinThings PrimFun -> Set String -> TCM ()
scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)
alreadyVisited :: TopLevelModuleName -> TCM (Interface, Either Warnings ClockTime) -> TCM (Interface, Either Warnings ClockTime)

data Warnings = Warnings {

terminationProblems :: [([QName], [Range])]
unsolvedMetaVariables :: [Range]
unsolvedConstraints :: Constraints

}

warningsToError :: Warnings -> TypeError
typeCheck :: FilePath -> RelativeTo -> Maybe [AbsolutePath] -> TCM (Interface, Maybe Warnings)
getInterface :: ModuleName -> TCM (Interface, ClockTime)
getInterface' :: TopLevelModuleName -> Bool -> TCM (Interface, Either Warnings ClockTime)
readInterface :: FilePath -> TCM (Maybe Interface)
writeInterface :: FilePath -> Interface -> TCM ClockTime
createInterface :: AbsolutePath -> TopLevelModuleName -> TCM (Interface, Either Warnings ClockTime)
buildInterface :: TopLevelInfo -> HighlightingInfo -> Set String -> TCM Interface
isNewerThan :: FilePath -> FilePath -> IO Bool

Documentation

data RelativeTo | Source

Which directory should form the base of relative include paths?
Constructors

ProjectRoot | The root directory of the "project" containing the current file.
CurrentDir | The current working directory.

moduleName :: FilePath -> TCM TopLevelModuleName | Source

A variant of `moduleName'` which raises an error if the file name does not match the module name. The file name is interpreted relative to the current working directory (unless it is absolute).

moduleName' :: AbsolutePath -> TCM TopLevelModuleName | Source

Computes the module name of the top-level module in the given file.

mergeInterface :: Interface -> TCM () | Source

Merge an interface into the current proof state.

addImportedThings :: Signature -> BuiltinThings PrimFun -> Set String -> TCM () | Source

scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope) | Source

Scope checks the given module. A proper version of the module name (with correct definition sites) is returned.

alreadyVisited :: TopLevelModuleName -> TCM (Interface, Either Warnings ClockTime) -> TCM (Interface, Either Warnings ClockTime) | Source

If the module has already been visited (without warnings), then its interface is returned directly. Otherwise the computation is used to find the interface and the computed interface is stored for potential later use.

data Warnings | Source

Warnings. Invariant: The fields are never empty at the same time.
Constructors

Warnings |

terminationProblems :: [([QName], [Range])] | Termination checking problems are not reported if `optTerminationCheck` is `False`.
unsolvedMetaVariables :: [Range] | Meta-variable problems are reported as type errors unless `optAllowUnsolved` is `True`.
unsolvedConstraints :: Constraints | Same as `unsolvedMetaVariables`.

warningsToError :: Warnings -> TypeError | Source

Turns warnings into an error. Even if several errors are possible only one is raised.

typeCheck | Source

:: FilePath | The file name is interpreted relative to the current working directory (unless it is absolute).
-> RelativeTo |
-> Maybe [AbsolutePath] | If this argument is given, and it does not coincide with the new value of the include directories (after making them absolute), the state is reset (but the command-line options are preserved).
-> TCM (Interface, Maybe Warnings) |
Type checks the given module (if necessary). The function also makes relative directories absolute, based on the `RelativeTo` argument. If this argument is `ProjectRoot`, then the "current file" is taken to be the one given as the first argument.

getInterface :: ModuleName -> TCM (Interface, ClockTime) | Source

Tries to return the interface associated to the given module. The time stamp of the relevant interface file is also returned. May type check the module. An error is raised if a warning is encountered.

getInterface' | Source

:: TopLevelModuleName |
-> Bool | If type checking is necessary, should all state changes inflicted by `createInterface` be preserved?
-> TCM (Interface, Either Warnings ClockTime) |
A more precise variant of `getInterface`. If warnings are encountered then they are returned instead of being turned into errors.

readInterface :: FilePath -> TCM (Maybe Interface) | Source

writeInterface :: FilePath -> Interface -> TCM ClockTime | Source

Writes the given interface to the given file. Returns the file's new modification time stamp, or `Nothing` if the write failed.

createInterface | Source

:: AbsolutePath | The file to type check.
-> TopLevelModuleName | The expected module name.
-> TCM (Interface, Either Warnings ClockTime) |
Tries to type check a module and write out its interface. The function only writes out an interface file if it does not encounter any warnings. If appropriate this function writes out syntax highlighting information.

buildInterface | Source

:: TopLevelInfo | `TopLevelInfo` for the current module.
-> HighlightingInfo | Syntax highlighting info for the module.
-> Set String | Haskell modules imported in imported modules (transitively).
-> TCM Interface |
Builds an interface for the current module, which should already have been successfully type checked.

isNewerThan :: FilePath -> FilePath -> IO Bool | Source

True if the first file is newer than the second file. If a file doesn't exist it is considered to be infinitely old.
Produced by Haddock version 2.4.2