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

Safe Haskell | None

Agda.Interaction.Imports

Description

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

Synopsis

- mergeInterface :: Interface -> TCM ()
- addImportedThings :: Signature -> BuiltinThings PrimFun -> Set String -> PatternSynDefns -> TCM ()
- scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)
- alreadyVisited :: TopLevelModuleName -> TCM (Interface, Either Warnings ClockTime) -> TCM (Interface, Either Warnings ClockTime)
- typeCheck :: AbsolutePath -> TCM (Interface, Maybe Warnings)
- getInterface :: ModuleName -> TCM (Interface, ClockTime)
- getInterface' :: TopLevelModuleName -> Bool -> TCM (Interface, Either Warnings ClockTime)
- highlightFromInterface :: Interface -> AbsolutePath -> TCM ()
- readInterface :: FilePath -> TCM (Maybe Interface)
- writeInterface :: FilePath -> Interface -> TCM ClockTime
- createInterface :: AbsolutePath -> TopLevelModuleName -> TCM (Interface, Either Warnings ClockTime)
- buildInterface :: TopLevelInfo -> HighlightingInfo -> Set String -> [OptionsPragma] -> TCM Interface
- isNewerThan :: FilePath -> FilePath -> IO Bool

# Documentation

mergeInterface :: Interface -> TCM ()

Merge an interface into the current proof state.

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

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

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)

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.

typeCheck :: AbsolutePath -> TCM (Interface, Maybe Warnings)

Type checks the given module (if necessary).

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

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'

Arguments

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

highlightFromInterface

Arguments

:: Interface |
-> AbsolutePath | The corresponding file.
-> TCM () |

Print the highlighting information contained in the given interface.

readInterface :: FilePath -> TCM (Maybe Interface)

writeInterface :: FilePath -> Interface -> TCM ClockTime

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

createInterface

Arguments

:: 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

Arguments

:: TopLevelInfo | `TopLevelInfo` for the current module.
-> HighlightingInfo | Syntax highlighting info for the module.
-> Set String | Haskell modules imported in imported modules (transitively).
-> [OptionsPragma] | Options set in `OPTIONS` pragmas.
-> TCM Interface |

Builds an interface for the current module, which should already have been successfully type checked.

isNewerThan :: FilePath -> FilePath -> IO Bool

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