ModuleAgda-2.7.0.1Haskell2010

Agda.Interaction.Imports

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

3 types
9 values

PackageAgda-2.7.0.1
Exports15
LanguageHaskell2010
LicenceMIT
SourceImports.hs

datadata Mode

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

Instances2Eq, Show

Eq ModeDefined in Agda-2.7.0.1 · Agda.Interaction.Imports
Show ModeDefined in Agda-2.7.0.1 · Agda.Interaction.Imports

constructorScopeCheck

constructorTypeCheck

datadata CheckResult

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.

patternpattern CheckResult :: Interface -> [TCWarning] -> ModuleCheckMode -> Source -> CheckResult

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

valuecrModuleInfo :: CheckResult -> ModuleInfo

valuecrInterface :: CheckResult -> Interface

valuecrWarnings :: CheckResult -> [TCWarning]

valuecrMode :: CheckResult -> ModuleCheckMode

valuecrSource :: CheckResult -> Source

datadata Source

The decorated source code.

Constructors

Source
- srcText :: Text
  Source code.
- srcFileType :: FileType
  Source file type
- srcOrigin :: SourceFile
  Source location at the time of its parsing
- srcModule :: Module
  The parsed module.
- srcModuleName :: TopLevelModuleName
  The top-level module name.
- srcProjectLibs :: [AgdaLibFile]
  The .agda-lib file(s) of the project this file belongs to.
- srcAttributes :: !Attributes
  Every encountered attribute.

valuescopeCheckImport

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

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

valueparseSource :: SourceFile -> TCM Source

Parses a source file and prepares the Source record.

valuetypeCheckMain

:: Mode
Should the file be type-checked, or only scope-checked?
-> Source
The decorated source code.
-> TCM CheckResult

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.

valuereadInterface :: InterfaceFile -> TCM (Maybe Interface)

Read interface file corresponding to a module.