Agda
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Scope.UnusedImports

Description

Warn about unused imports.

For each open statement, we want to issue a warning about concrete names brought into scope by this statement which are not referenced subsequently.

To this end, whenever we lookup a concrete name during scope checking, we mark it as used by calling lookedupName with the results of the lookup, which is an AbstractName or several AbstractNames in case the name is ambiguous (e.g. an ambiguous constructor or projection).

We also record for each opened module the set of AbstractNames it brought into scope.

When checking the file is done, we can traverse the each opened module and report all the AbstractNames that we not used.

Synopsis

Documentation

lookedupName Source #

Arguments

:: QName

The concrete name resolved by the scope checker.

-> ResolvedName

The resolution of the name.

-> ScopeM () 

Call these whenever a concrete name was translated to an abstract one.

registerModuleOpening Source #

Arguments

:: KwRange

Range of the open keyword.

-> ModuleName

Parent module: module into which we pour the opened module.

-> QName

Opened module.

-> ImportDirective

Directive restricting the scope of the opened module.

-> Scope

The scope resulting from applying the import directive.

-> ScopeM () 

Call this when opening a module with all the names it brings into scope. When the UnusedImports warning is enabled, we will store this information to later issue a warning connected to this open statement for the names that were not used.

warnUnusedImports :: TCM () Source #

Call this when a file has been checked to generate the unused-imports warnings for each opened module. Assumes that all names have been looked up via lookedupName. Needs the disambiguation information from the type checker to correctly report ununsed overloaded names.