Agda.Interaction.Imports

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

Documentation

data MainInterface

Are we loading the interface for the user-loaded file or for an import?

Constructors

MainInterface

Interface for main file.

NotMainInterface

Interface for imported file.

Instances

Eq MainInterface

Show MainInterface

mergeInterface :: Interface -> TCM ()

Merge an interface into the current proof state.

addImportedThings :: Signature -> BuiltinThings PrimFun -> Set String -> Set String -> PatternSynDefns -> DisplayForms -> 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.

data MaybeWarnings

Constructors

NoWarnings

SomeWarnings Warnings

hasWarnings :: MaybeWarnings -> Bool

alreadyVisited :: TopLevelModuleName -> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)

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.

typeCheckMain :: AbsolutePath -> TCM (Interface, MaybeWarnings)

Type checks the main file of the interaction. This could be the file loaded in the interacting editor (emacs), or the file passed on the command line.

First, the primitive modules are imported. Then, getInterface' is called to do the main work.

getInterface :: ModuleName -> TCM Interface

Tries to return the interface associated to the given (imported) module. The time stamp of the relevant interface file is also returned. Calls itself recursively for the imports of the given module. May type check the module. An error is raised if a warning is encountered.

Do not use this for the main file, use typeCheckMain instead.

getInterface_ :: TopLevelModuleName -> TCM Interface

See getInterface.

getInterface'

Arguments

:: TopLevelModuleName

-> MainInterface

If type checking is necessary, should all state changes inflicted by createInterface be preserved?

-> TCM (Interface, MaybeWarnings)

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

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

removePrivates :: ScopeInfo -> ScopeInfo

createInterface

Arguments

:: AbsolutePath

The file to type check.

-> TopLevelModuleName

The expected module name.

-> TCM (Interface, MaybeWarnings)

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.

constructIScope :: Interface -> Interface

buildInterface

Arguments

:: AbsolutePath

-> TopLevelInfo

TopLevelInfo for the current module.

-> HighlightingInfo

Syntax highlighting info for the module.

-> Set String

MAlonzo: Haskell modules imported in imported modules (transitively).

-> Set String

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

getInterfaceFileHashes :: FilePath -> TCM (Maybe (Hash, Hash))

Returns (iSourceHash, iFullHash)

moduleHash :: ModuleName -> TCM Hash

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.