| 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 -> Set TCWarning -> ModuleCheckMode -> Source -> CheckResult
- crModuleInfo :: CheckResult -> ModuleInfo
- crInterface :: CheckResult -> Interface
- crWarnings :: CheckResult -> Set TCWarning
- crMode :: CheckResult -> ModuleCheckMode
- crSource :: CheckResult -> Source
- data Source = Source {}
- scopeCheckFileImport :: TopLevelModuleName -> TCM (ModuleName, Map ModuleName Scope)
- parseSource :: SourceFile -> TCM Source
- typeCheckMain :: Mode -> Source -> TCM CheckResult
- getNonMainInterface :: TopLevelModuleName -> Maybe Source -> TCM Interface
- getNonMainModuleInfo :: TopLevelModuleName -> Maybe Source -> TCM ModuleInfo
- getInterface :: TopLevelModuleName -> MainInterface -> Maybe Source -> TCM ModuleInfo
- importPrimitiveModules :: TCM ()
- raiseNonFatalErrors :: (HasOptions m, MonadTCError m) => CheckResult -> m ()
- data MainInterface
- data TCWorkers
- wantsParallelChecking :: TCM (Maybe TCWorkers)
- chaseModule :: TCWorkers -> TopLevelModuleName -> MainInterface -> Maybe Source -> TCM (TCM ModuleInfo)
- setOptionsFromSourcePragmas :: Bool -> Source -> TCM ()
- readInterface :: InterfaceFile -> TCM (Maybe Interface)
Documentation
Is the aim to type-check the top-level module, or only to scope-check it?
pattern ScopeCheck :: 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 -> Set TCWarning -> ModuleCheckMode -> Source -> CheckResult | Flattened unidirectional pattern for |
crModuleInfo :: CheckResult -> ModuleInfo Source #
crInterface :: CheckResult -> Interface Source #
crWarnings :: CheckResult -> Set TCWarning Source #
crMode :: CheckResult -> ModuleCheckMode Source #
crSource :: CheckResult -> Source Source #
The decorated source code.
Constructors
| Source | |
Fields
| |
scopeCheckFileImport :: TopLevelModuleName -> TCM (ModuleName, Map ModuleName Scope) Source #
Scope checks the given module, generating an interface or retrieving an existing one. Returns the module name and exported scope from the interface.
parseSource :: SourceFile -> TCM Source Source #
Parses a source file and prepares the Source record.
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.
Arguments
| :: TopLevelModuleName | |
| -> Maybe Source | Optional: the source code and some information about the source code. |
| -> 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.
Arguments
| :: TopLevelModuleName | |
| -> Maybe Source | Optional: the source code and some information about the source code. |
| -> TCM ModuleInfo |
Arguments
| :: TopLevelModuleName | |
| -> MainInterface | |
| -> Maybe Source | Optional: the source code and some information about the source code. |
| -> TCM ModuleInfo |
If the module has already been visited (without warnings), then its interface is returned directly.
Otherwise the interface is loaded via getStoredInterface.
If that fails it is created via createInterface or, for non-main modules,
createInterfaceIsolated.
A such created interface is stored for potential later use.
importPrimitiveModules :: TCM () Source #
Import the primitive modules (unless --no-load-primitives).
Arguments
| :: (HasOptions m, MonadTCError m) | |
| => CheckResult | E.g. obtained from |
| -> m () |
If checking produced non-benign warnings, error out.
data MainInterface Source #
Are we loading the interface for the user-loaded file or for an import?
Constructors
| MainInterface Mode | For the main file. In this case state changes inflicted by
|
| NotMainInterface | For an imported file. In this case state changes inflicted by
|
Instances
| Show MainInterface Source # | |
Defined in Agda.Interaction.Imports Methods showsPrec :: Int -> MainInterface -> ShowS # show :: MainInterface -> String # showList :: [MainInterface] -> ShowS # | |
| Eq MainInterface Source # | |
Defined in Agda.Interaction.Imports Methods (==) :: MainInterface -> MainInterface -> Bool # (/=) :: MainInterface -> MainInterface -> Bool # | |
wantsParallelChecking :: TCM (Maybe TCWorkers) Source #
If the user has asked for it, prepare the type checker for loading
in parallel, and return a TCWorkers instance that can be used to
coordinate a number of type-checking tasks.
The given module name, when encountered, will be treated as the
MainInterface.
Arguments
| :: TCWorkers | For synchronization |
| -> TopLevelModuleName | The name of the module to check |
| -> MainInterface | Are we checking the main module? |
| -> Maybe Source | Pre-parsed source |
| -> TCM (TCM ModuleInfo) |
Type-check the given module, using a TCWorkers instance to check
its imports in parallel.
Returns an action which *waits* for completion of type-checking of
the given module. Note that the given action updates the
DecodedModules in the TC state where it is called to the current
results of parallel type-checking. The state after running this
action is guaranteed to contain a DecodedModule for the given
TopLevelModuleName.
If the given MainInterface indicates that we are checking the main
module, its checking will happen in the calling thread, and in the
calling TC state. Otherwise, a thread (with isolated TC state) is
created to check it.
Regardless of whether we spawned a new thread or not, checking of the given module will block until all of its imports have been checked.
setOptionsFromSourcePragmas :: Bool -> Source -> TCM () Source #
Set options from a Source pragma, using the source
ranges of the pragmas for error reporting. Flag to check consistency.
readInterface :: InterfaceFile -> TCM (Maybe Interface) Source #
Read interface file corresponding to a module.