Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 -> 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 :: 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 -> [OptionsPragma] -> TCM Interface
isNewerThan :: FilePath -> FilePath -> IO Bool
Documentation
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 :: ConstraintsSame as unsolvedMetaVariables.
warningsToError :: Warnings -> TypeErrorSource
Turns warnings into an error. Even if several errors are possible only one is raised.
typeCheck :: AbsolutePath -> TCM (Interface, Maybe Warnings)Source
Type checks the given module (if necessary).
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
-> BoolIf 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 ClockTimeSource
Writes the given interface to the given file. Returns the file's new modification time stamp, or Nothing if the write failed.
createInterfaceSource
:: AbsolutePathThe file to type check.
-> TopLevelModuleNameThe 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.

buildInterfaceSource
:: TopLevelInfoTopLevelInfo for the current module.
-> HighlightingInfoSyntax highlighting info for the module.
-> Set StringHaskell 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 BoolSource
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.6.1