Agda-2.8.0: A dependently typed functional programming language and proof assistant

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 {
  - srcText :: Text
  - srcFileType :: FileType
  - srcOrigin :: SourceFile
  - srcModule :: Module
  - srcModuleName :: TopLevelModuleName
  - srcProjectLibs :: [AgdaLibFile]
  - srcAttributes :: !Attributes
  }
- scopeCheckImport :: 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 ()
- 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 Source # show :: Mode -> String Source # showList :: [Mode] -> ShowS Source #
Eq Mode Source # |
Instance details Defined in Agda.Interaction.Imports Methods (==) :: Mode -> Mode -> Bool Source # (/=) :: Mode -> Mode -> Bool Source #

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

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.

getNonMainInterface Source #

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.

getNonMainModuleInfo Source #

Arguments

:: TopLevelModuleName |
-> Maybe Source | Optional: the source code and some information about the source code.
-> TCM ModuleInfo |

getInterface Source #

Arguments

:: TopLevelModuleName |
-> MainInterface |
-> Maybe Source | Optional: the source code and some information about the source code.
-> TCM ModuleInfo |

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

importPrimitiveModules :: TCM () Source #

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

raiseNonFatalErrors Source #

Arguments

:: (HasOptions m, MonadTCError m) |
=> CheckResult | E.g. obtained from `typeCheckMain`.
-> m () |

If checking produced non-benign warnings, error out.

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

Read interface file corresponding to a module.