Safe Haskell	None
Language	Haskell2010

Agda.Interaction.Imports

Description

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

Synopsis

data Mode
pattern ScopeCheck :: Mode
pattern TypeCheck :: Mode
data CheckResult where
- pattern CheckResult :: Interface -> [TCWarning] -> ModuleCheckMode -> Source -> CheckResult
crModuleInfo :: CheckResult -> ModuleInfo
crInterface :: CheckResult -> Interface
crWarnings :: CheckResult -> [TCWarning]
crMode :: CheckResult -> ModuleCheckMode
crSource :: CheckResult -> Source
data Source = Source {
- srcText :: Text
- srcFileType :: FileType
- srcOrigin :: SourceFile
- srcModule :: Module
- srcModuleName :: TopLevelModuleName
- srcProjectLibs :: [AgdaLibFile]
- srcAttributes :: !Attributes
}
scopeCheckImport :: TopLevelModuleName -> ModuleName -> TCM (ModuleName, Map ModuleName Scope)
parseSource :: SourceFile -> TCM Source
typeCheckMain :: Mode -> Source -> TCM CheckResult
readInterface :: InterfaceFile -> TCM (Maybe Interface)

Documentation

data Mode Source #

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

Instances

Instances details

Show Mode Source #
Instance details Defined in Agda.Interaction.Imports Methods showsPrec :: Int -> Mode -> ShowS show :: Mode -> String showList :: [Mode] -> ShowS
Eq Mode Source #
Instance details Defined in Agda.Interaction.Imports Methods (==) :: Mode -> Mode -> Bool (/=) :: Mode -> Mode -> Bool

pattern ScopeCheck :: Mode Source #

pattern TypeCheck :: Mode Source #

data CheckResult where Source #

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.

Bundled Patterns

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

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

crModuleInfo :: CheckResult -> ModuleInfo Source #

crInterface :: CheckResult -> Interface Source #

crWarnings :: CheckResult -> [TCWarning] Source #

crMode :: CheckResult -> ModuleCheckMode Source #

crSource :: CheckResult -> Source Source #

data Source Source #

The decorated source code.

Constructors

Source
Fields 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.

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

parseSource :: SourceFile -> TCM Source Source #

Parses a source file and prepares the Source record.

typeCheckMain Source #

Arguments

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

readInterface :: InterfaceFile -> TCM (Maybe Interface) Source #

Read interface file corresponding to a module.