Agda.Interaction.Imports

Is the aim to type-check the top-level module, or only to scope-check it?

The result and associated parameters of a type-checked file, when invoked directly via interaction or a backend. Note that the constructor is not exported.

Flattened unidirectional pattern for CheckResult for destructuring inside the ModuleInfo field.

The decorated source code.

Scope checks the given module, generating an interface or retrieving an existing one. Returns the module name and exported scope from the interface.

Parses a source file and prepares the Source record.

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.

If the Mode is ScopeCheck, then type-checking is not performed, only scope-checking. (This may include type-checking of imported modules.) In this case the generated, partial interface is not stored in the state (stDecodedModules). Note, however, that if the file has already been type-checked, then a complete interface is returned.

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.

A more precise variant of getNonMainInterface. If warnings are encountered then they are returned instead of being turned into errors.

Import the primitive modules (unless --no-load-primitives).

If checking produced non-benign warnings, error out.

Read interface file corresponding to a module.