-- | 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 'AbstractName's in case the name
-- is ambiguous (e.g. an ambiguous constructor or projection).
--
-- We also record for each opened module the set of 'AbstractName's it brought
-- into scope.
--
-- When checking the file is done, we can traverse the each opened module
-- and report all the 'AbstractName's that we not used.

module Agda.Syntax.Scope.UnusedImports
  ( lookedupName
  , registerModuleOpening
  , warnUnusedImports
  ) where

import Prelude hiding (null, (||))

import Data.IntMap.Strict (IntMap)
import Data.IntMap.Strict qualified as IntMap
import Data.List (partition)
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set

import Agda.Interaction.Options (lensOptWarningMode, optQualifiedInstances)
import Agda.Interaction.Options.Warnings (lensSingleWarning, WarningName (UnusedImports_, UnusedImportsAll_), warningSet, unusedImportsWarnings)

import Agda.Syntax.Abstract.Name qualified as A
import Agda.Syntax.Common ( IsInstanceDef(isInstanceDef), IsInstance, KwRange, ImportDirective' (using, impRenaming, publicOpen) )
import Agda.Syntax.Common.Pretty (prettyShow, Pretty (pretty))
import Agda.Syntax.Concrete qualified as C
import Agda.Syntax.Position ( HasRange(getRange), SetRange(setRange), Range )
import Agda.Syntax.Position qualified as P
import Agda.Syntax.Scope.Base as A
import Agda.Syntax.Scope.State ( ScopeM, withCurrentModule )
-- importing Agda.Syntax.Scope.Monad creates import cycles

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Debug ( reportSLn, __IMPOSSIBLE_VERBOSE__ )
import Agda.TypeChecking.Monad.Trace (setCurrentRange)
import Agda.TypeChecking.Warnings (warning)

import Agda.Utils.Boolean  ( (||) )
import Agda.Utils.Function ( applyUnless )
import Agda.Utils.Lens     ( (<&>), Lens' )
import Agda.Utils.List     ( partitionMaybe, hasElem )
import Agda.Utils.List1    ( pattern (:|), List1 )
import Agda.Utils.List1    qualified as List1
import Agda.Utils.List2    ( List2(..) )
import Agda.Utils.List2    qualified as List2
import Agda.Utils.Map      qualified as Map
import Agda.Utils.Maybe    ( fromMaybe, isJust, whenNothing )
import Agda.Utils.Monad    ( forM_, when, unless )
import Agda.Utils.Null     ( Null(null) )

import Agda.Utils.Impossible

-- | Call these whenever a concrete name was translated to an abstract one.
lookedupName ::
     C.QName       -- ^ The concrete name resolved by the scope checker.
  -> ResolvedName  -- ^ The resolution of the name.
  -> ScopeM ()
lookedupName :: QName -> ResolvedName -> ScopeM ()
lookedupName QName
x = \case
    DefinedName Access
_access AbstractName
y Suffix
_suffix -> AbstractName -> ScopeM ()
unamb AbstractName
y
    FieldName List1 AbstractName
ys                  -> List1 AbstractName -> ScopeM ()
add List1 AbstractName
ys
    ConstructorName Set1 Induction
_ind List1 AbstractName
ys       -> List1 AbstractName -> ScopeM ()
add List1 AbstractName
ys
    PatternSynResName List1 AbstractName
ys          -> List1 AbstractName -> ScopeM ()
add List1 AbstractName
ys
    VarName{}                     -> () -> ScopeM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    UnknownName{}                 -> () -> ScopeM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    add :: List1 AbstractName -> ScopeM ()
add = \case
      AbstractName
y  :| []      -> AbstractName -> ScopeM ()
unamb AbstractName
y
      AbstractName
y1 :| AbstractName
y2 : [AbstractName]
ys -> List2 AbstractName -> ScopeM ()
amb (List2 AbstractName -> ScopeM ())
-> List2 AbstractName -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ AbstractName
-> AbstractName -> [AbstractName] -> List2 AbstractName
forall a. a -> a -> [a] -> List2 a
List2 AbstractName
y1 AbstractName
y2 [AbstractName]
ys
    unamb :: AbstractName -> ScopeM ()
unamb = Lens' TCState [AbstractName]
-> ([AbstractName] -> [AbstractName]) -> ScopeM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens ([AbstractName] -> f [AbstractName]) -> TCState -> f TCState
Lens' TCState [AbstractName]
stUnambiguousLookups (([AbstractName] -> [AbstractName]) -> ScopeM ())
-> (AbstractName -> [AbstractName] -> [AbstractName])
-> AbstractName
-> ScopeM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:)
    amb :: List2 AbstractName -> ScopeM ()
amb List2 AbstractName
xs = case QName -> Maybe Int
forall a. HasRange a => a -> Maybe Int
rangeToPosPos QName
x of
      -- Andreas, 2025-11-30
      -- It can happen that a concrete identifier has no range,
      -- e.g. when it comes from an expanded ellipsis.
      -- In this case, we do not record the lookup,
      -- since it should have been looked up already
      -- when processing the pattern from the original lhs
      -- (that was duplicated by ellipsis expansion).
      -- See test/interaction/ExpandEllipsis.
      Maybe Int
Nothing -> () -> ScopeM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      Just Int
i -> Lens' TCState (IntMap (List2 AbstractName))
-> (IntMap (List2 AbstractName) -> IntMap (List2 AbstractName))
-> ScopeM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens (IntMap (List2 AbstractName) -> f (IntMap (List2 AbstractName)))
-> TCState -> f TCState
Lens' TCState (IntMap (List2 AbstractName))
stAmbiguousLookups ((IntMap (List2 AbstractName) -> IntMap (List2 AbstractName))
 -> ScopeM ())
-> (IntMap (List2 AbstractName) -> IntMap (List2 AbstractName))
-> ScopeM ()
forall a b. (a -> b) -> a -> b
$ Int
-> List2 AbstractName
-> IntMap (List2 AbstractName)
-> IntMap (List2 AbstractName)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i List2 AbstractName
xs

rangeToPosPos :: HasRange a => a -> Maybe Int
rangeToPosPos :: forall a. HasRange a => a -> Maybe Int
rangeToPosPos = (Position' () -> Int) -> Maybe (Position' ()) -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> Int) -> (Position' () -> Word32) -> Position' () -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Position' () -> Word32
forall a. Position' a -> Word32
P.posPos) (Maybe (Position' ()) -> Maybe Int)
-> (a -> Maybe (Position' ())) -> a -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Maybe (Position' ())
forall a. Range' a -> Maybe (Position' ())
P.rStart' (Range -> Maybe (Position' ()))
-> (a -> Range) -> a -> Maybe (Position' ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Range
forall a. HasRange a => a -> Range
getRange

-- | 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.
registerModuleOpening ::
     KwRange             -- ^ Range of the @open@ keyword.
  -> A.ModuleName        -- ^ Parent module: module into which we pour the opened module.
  -> C.QName             -- ^ Opened module.
  -> C.ImportDirective   -- ^ Directive restricting the scope of the opened module.
  -> Scope               -- ^ The scope resulting from applying the import directive.
  -> ScopeM ()
registerModuleOpening :: KwRange
-> ModuleName -> QName -> ImportDirective -> Scope -> ScopeM ()
registerModuleOpening KwRange
kwr ModuleName
currentModule QName
x ImportDirective
dir (Scope ModuleName
m0 [ModuleName]
_parents ScopeNameSpaces
ns Map QName ModuleName
imports Maybe DataOrRecordModule
_dataOrRec) = do
  -- @imports@ have been removed by 'restrictPrivate'.
  Bool -> ScopeM () -> ScopeM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Map QName ModuleName -> Bool
forall a. Null a => a -> Bool
null Map QName ModuleName
imports) ScopeM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

  -- When the UnusedImports warning is off, do not collect information about @open@.
  -- E.g. we do not want to see warnings for the automatically inserted
  -- @open import Agda.Primitive using (Set)@.
  -- It is sufficient to check for 'UnusedImports_' since it is implied by 'UnusedImportsAll_'.
  doWarn <- (WarningName
UnusedImports_ WarningName -> Set WarningName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member`) (Set WarningName -> Bool)
-> TCMT IO (Set WarningName) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (Set WarningName) -> TCMT IO (Set WarningName)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Set WarningName -> f (Set WarningName)) -> TCState -> f TCState
Lens' TCState (Set WarningName)
stWarningSet
  reportSLn "warning.unusedImports" 20 $ unlines
    [ "openedModule: " <> prettyShow doWarn
    , "x = " <> prettyShow x
    -- , "currentModule: " <> prettyShow curM
    ]
  when doWarn $ whenNothing (publicOpen dir) do
    let
      m = Range -> ModuleName -> ModuleName
forall a. SetRange a => Range -> a -> a
setRange (QName -> Range
forall a. HasRange a => a -> Range
getRange QName
x) ModuleName
m0
      broughtIntoScope :: NamesInScope -- [Map C.Name (List1 AbstractName)]
      broughtIntoScope = [NamesInScope] -> NamesInScope
forall a. Eq a => [ThingsInScope a] -> ThingsInScope a
mergeNamesMany ([NamesInScope] -> NamesInScope) -> [NamesInScope] -> NamesInScope
forall a b. (a -> b) -> a -> b
$ ((NameSpaceId, NameSpace) -> NamesInScope)
-> ScopeNameSpaces -> [NamesInScope]
forall a b. (a -> b) -> [a] -> [b]
map (NameSpace -> NamesInScope
nsNames (NameSpace -> NamesInScope)
-> ((NameSpaceId, NameSpace) -> NameSpace)
-> (NameSpaceId, NameSpace)
-> NamesInScope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NameSpaceId, NameSpace) -> NameSpace
forall a b. (a, b) -> b
snd) ScopeNameSpaces
ns
      !k = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ QName -> Maybe Int
forall a. HasRange a => a -> Maybe Int
rangeToPosPos QName
x
      hasDir = Bool -> Bool
not (Using' Name Name -> Bool
forall a. Null a => a -> Bool
null (ImportDirective -> Using' Name Name
forall n m. ImportDirective' n m -> Using' n m
using ImportDirective
dir)) Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
|| Bool -> Bool
not (RenamingDirective' Name Name -> Bool
forall a. Null a => a -> Bool
null (ImportDirective -> RenamingDirective' Name Name
forall n m. ImportDirective' n m -> RenamingDirective' n m
impRenaming ImportDirective
dir))
    modifyTCLens stOpenedModules $
      IntMap.insert k (OpenedModule kwr m currentModule hasDir broughtIntoScope)

-- | 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.
warnUnusedImports :: TCM ()
warnUnusedImports :: ScopeM ()
warnUnusedImports = do
    warnAll <- (WarningName
UnusedImportsAll_ WarningName -> Set WarningName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member`) (Set WarningName -> Bool)
-> TCMT IO (Set WarningName) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (Set WarningName) -> TCMT IO (Set WarningName)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Set WarningName -> f (Set WarningName)) -> TCState -> f TCState
Lens' TCState (Set WarningName)
stWarningSet
    st <- useTC stUnusedImportsState
    disambiguatedNames <- useTC stDisambiguatedNames
    -- If instances can be used qualified, they do not need to be imported,
    -- so we should warn about them.
    qualifiedInstances <- optQualifiedInstances <$> pragmaOptions

    reportSLn "warning.unusedImports" 60 $ "unambiguousLookups: " <> prettyShow (unambiguousLookups st)

    let
      -- Disambiguate overloaded lookups.
      addAmbLookup (Int
i :: Int) (List2 AbstractName
ys :: List2 AbstractName) = do
        case Int -> IntMap DisambiguatedName -> Maybe DisambiguatedName
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap DisambiguatedName
disambiguatedNames of
          Just (DisambiguatedName NameKind
_k QName
x) -> ((AbstractName -> Bool) -> [AbstractName] -> [AbstractName]
forall a. (a -> Bool) -> [a] -> [a]
filter ((QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
==) (QName -> Bool) -> (AbstractName -> QName) -> AbstractName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName) (List2 AbstractName -> [Item (List2 AbstractName)]
forall l. IsList l => l -> [Item l]
List2.toList List2 AbstractName
ys) [AbstractName] -> [AbstractName] -> [AbstractName]
forall a. [a] -> [a] -> [a]
++)
          Maybe DisambiguatedName
Nothing -> (List2 AbstractName -> [Item (List2 AbstractName)]
forall l. IsList l => l -> [Item l]
List2.toList List2 AbstractName
ys [AbstractName] -> [AbstractName] -> [AbstractName]
forall a. [a] -> [a] -> [a]
++) -- __IMPOSSIBLE__
      allLookups :: [AbstractName]
      allLookups = (Int -> List2 AbstractName -> [AbstractName] -> [AbstractName])
-> [AbstractName] -> IntMap (List2 AbstractName) -> [AbstractName]
forall a b. (Int -> a -> b -> b) -> b -> IntMap a -> b
IntMap.foldrWithKey Int -> List2 AbstractName -> [AbstractName] -> [AbstractName]
addAmbLookup (UnusedImportsState -> [AbstractName]
unambiguousLookups UnusedImportsState
st) (UnusedImportsState -> IntMap (List2 AbstractName)
ambiguousLookups UnusedImportsState
st)

      -- To make a set of the list of looked-up 'AbstractName's,
      -- we need to convert them to 'ImportedName's lest we
      -- conflate names from different openings.
      lookups :: [ImportedName]
      (unknowns, lookups) = partitionMaybe toImportedName allLookups
      isLookedUp, isInst, isUsed  :: ImportedName -> Bool
      isLookedUp = [ImportedName] -> ImportedName -> Bool
forall a. Ord a => [a] -> a -> Bool
hasElem [ImportedName]
lookups
      isInst = Maybe KwRange -> Bool
forall a. Maybe a -> Bool
isJust (Maybe KwRange -> Bool)
-> (ImportedName -> Maybe KwRange) -> ImportedName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ImportedName -> Maybe KwRange
forall a. IsInstanceDef a => a -> Maybe KwRange
isInstanceDef
      isUsed = Bool
-> ((ImportedName -> Bool) -> ImportedName -> Bool)
-> (ImportedName -> Bool)
-> ImportedName
-> Bool
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless Bool
qualifiedInstances (ImportedName -> Bool
isInst (ImportedName -> Bool)
-> (ImportedName -> Bool) -> ImportedName -> Bool
forall a. Boolean a => a -> a -> a
||) ImportedName -> Bool
isLookedUp

    reportSLn "warning.unusedImports" 60 $ "allLookups: " <> prettyShow allLookups
    reportSLn "warning.unusedImports" 60 $ "lookups: " <> prettyShow lookups
    reportSLn "warning.unusedImports" 60 $ "unknowns: " <> prettyShow unknowns

    -- Iterate through the @open@ statements and issue warnings.
    forM_ (openedModules st) \ (OpenedModule (KwRange
kwr :: KwRange) (ModuleName
m :: A.ModuleName) (ModuleName
parent :: A.ModuleName) (Bool
hasDir :: Bool) (NamesInScope
sc :: NamesInScope)) -> do
      let
        -- Partition the names brought into scope by the open statement
        -- into used and unused ones.
        f :: (C.Name, List1 AbstractName) -> Maybe (C.Name, List1 ImportedName)
        f :: (Name, List1 AbstractName) -> Maybe (Name, List1 ImportedName)
f = (List1 AbstractName -> Maybe (List1 ImportedName))
-> (Name, List1 AbstractName) -> Maybe (Name, List1 ImportedName)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (Name, a) -> f (Name, b)
traverse ((List1 AbstractName -> Maybe (List1 ImportedName))
 -> (Name, List1 AbstractName) -> Maybe (Name, List1 ImportedName))
-> (List1 AbstractName -> Maybe (List1 ImportedName))
-> (Name, List1 AbstractName)
-> Maybe (Name, List1 ImportedName)
forall a b. (a -> b) -> a -> b
$ (AbstractName -> Maybe ImportedName)
-> List1 AbstractName -> Maybe (List1 ImportedName)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse AbstractName -> Maybe ImportedName
toImportedName
        -- f (x, ys) = (x ,) <$> traverse toImportedName ys
        imps, imps', used, unused :: [(C.Name, List1 ImportedName)]
        ([(Name, List1 AbstractName)]
other, [(Name, List1 ImportedName)]
imps) = ((Name, List1 AbstractName) -> Maybe (Name, List1 ImportedName))
-> [(Name, List1 AbstractName)]
-> ([(Name, List1 AbstractName)], [(Name, List1 ImportedName)])
forall a b. (a -> Maybe b) -> [a] -> ([a], [b])
partitionMaybe (Name, List1 AbstractName) -> Maybe (Name, List1 ImportedName)
f ([(Name, List1 AbstractName)]
 -> ([(Name, List1 AbstractName)], [(Name, List1 ImportedName)]))
-> [(Name, List1 AbstractName)]
-> ([(Name, List1 AbstractName)], [(Name, List1 ImportedName)])
forall a b. (a -> b) -> a -> b
$ NamesInScope -> [(Name, List1 AbstractName)]
forall k a. Map k a -> [(k, a)]
Map.toList NamesInScope
sc
        imps' :: [(Name, List1 ImportedName)]
imps' = ((Name, List1 ImportedName) -> (Name, List1 ImportedName))
-> [(Name, List1 ImportedName)] -> [(Name, List1 ImportedName)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
x, List1 ImportedName
ys) -> (Name
x, Range -> ImportedName -> ImportedName
forall a. SetRange a => Range -> a -> a
setRange (Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x) (ImportedName -> ImportedName)
-> List1 ImportedName -> List1 ImportedName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 ImportedName
ys)) [(Name, List1 ImportedName)]
imps
        ([(Name, List1 ImportedName)]
used, [(Name, List1 ImportedName)]
unused) = ((Name, List1 ImportedName) -> Bool)
-> [(Name, List1 ImportedName)]
-> ([(Name, List1 ImportedName)], [(Name, List1 ImportedName)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((ImportedName -> Bool) -> List1 ImportedName -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ImportedName -> Bool
isUsed (List1 ImportedName -> Bool)
-> ((Name, List1 ImportedName) -> List1 ImportedName)
-> (Name, List1 ImportedName)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, List1 ImportedName) -> List1 ImportedName
forall a b. (a, b) -> b
snd) [(Name, List1 ImportedName)]
imps'

      String -> Int -> String -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"warning.unusedImports" Int
60 (String -> ScopeM ()) -> String -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ String
"used: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [(Name, List1 ImportedName)] -> String
forall a. Pretty a => a -> String
prettyShow [(Name, List1 ImportedName)]
used
      String -> Int -> String -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"warning.unusedImports" Int
60 (String -> ScopeM ()) -> String -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ String
"unused: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [(Name, List1 ImportedName)] -> String
forall a. Pretty a => a -> String
prettyShow [(Name, List1 ImportedName)]
unused
      Bool -> ScopeM () -> ScopeM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ([(Name, List1 AbstractName)] -> Bool
forall a. Null a => a -> Bool
null [(Name, List1 AbstractName)]
other) (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ String -> ScopeM ()
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ ([(Name, List1 AbstractName)] -> String
forall a. Show a => a -> String
show [(Name, List1 AbstractName)]
other)

      let
        -- Commands to issue the warnings:
        warn :: Maybe (List1 AbstractName) -> ScopeM ()
warn = Range -> ScopeM () -> ScopeM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange ((KwRange, ModuleName) -> Range
forall a. HasRange a => a -> Range
getRange (KwRange
kwr, ModuleName
m)) (ScopeM () -> ScopeM ())
-> (Maybe (List1 AbstractName) -> ScopeM ())
-> Maybe (List1 AbstractName)
-> ScopeM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> ScopeM () -> ScopeM ()
forall (m :: * -> *) a.
(ReadTCState m, MonadTCState m) =>
ModuleName -> m a -> m a
withCurrentModule ModuleName
parent (ScopeM () -> ScopeM ())
-> (Maybe (List1 AbstractName) -> ScopeM ())
-> Maybe (List1 AbstractName)
-> ScopeM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> ScopeM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> ScopeM ())
-> (Maybe (List1 AbstractName) -> Warning)
-> Maybe (List1 AbstractName)
-> ScopeM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> Maybe (List1 AbstractName) -> Warning
UnusedImports ModuleName
m
        warnModule :: ScopeM ()
warnModule = Maybe (List1 AbstractName) -> ScopeM ()
warn Maybe (List1 AbstractName)
forall a. Maybe a
Nothing
        warnEach :: ScopeM ()
warnEach = do
          [List1 ImportedName]
-> (List1 (List1 ImportedName) -> ScopeM ()) -> ScopeM ()
forall (m :: * -> *) a.
Applicative m =>
[a] -> (List1 a -> m ()) -> m ()
List1.unlessNull (((Name, List1 ImportedName) -> List1 ImportedName)
-> [(Name, List1 ImportedName)] -> [List1 ImportedName]
forall a b. (a -> b) -> [a] -> [b]
map (Name, List1 ImportedName) -> List1 ImportedName
forall a b. (a, b) -> b
snd [(Name, List1 ImportedName)]
unused) \ List1 (List1 ImportedName)
unused1 -> do
            Maybe (List1 AbstractName) -> ScopeM ()
warn (Maybe (List1 AbstractName) -> ScopeM ())
-> Maybe (List1 AbstractName) -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ List1 AbstractName -> Maybe (List1 AbstractName)
forall a. a -> Maybe a
Just (List1 AbstractName -> Maybe (List1 AbstractName))
-> List1 AbstractName -> Maybe (List1 AbstractName)
forall a b. (a -> b) -> a -> b
$ (List1 ImportedName -> AbstractName)
-> List1 (List1 ImportedName) -> List1 AbstractName
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ImportedName -> AbstractName
iName (ImportedName -> AbstractName)
-> (List1 ImportedName -> ImportedName)
-> List1 ImportedName
-> AbstractName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 ImportedName -> ImportedName
forall a. NonEmpty a -> a
List1.head) List1 (List1 ImportedName)
unused1

      -- Issue warning.
      -- If nothing was used, we warn about the whole import.
      -- If the open statement has a 'using' or 'renaming' directive,
      -- or if the 'UnusedImportsAll_' warning is enabled,
      -- we warn about each unused name individually.
      -- Otherwise, we just warn once about the whole import.
      if  | Bool
hasDir      -> ScopeM ()
warnEach
          | [(Name, List1 ImportedName)] -> Bool
forall a. Null a => a -> Bool
null [(Name, List1 ImportedName)]
used   -> ScopeM ()
warnModule
          | Bool
warnAll     -> ScopeM ()
warnEach
          | Bool
otherwise   -> () -> ScopeM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

------------------------------------------------------------------------------
-- * Auxiliary definitions

-- | A wrapper around 'AbstractName' to make the position of the 'Opened' in the lineage available.
--   This wrapper is needed when 'AbstractName's are stored in sets
--   so that we do not conflate different 'AbstractName's with the same underlying 'A.QName'
--   that were brought into scope by different 'open' statements.
data ImportedName = ImportedName
  { ImportedName -> Int
iWhere :: Int -- Position of 'Opened' extracted from the 'AbstractName'.
  , ImportedName -> AbstractName
iName  :: AbstractName
  } deriving (ImportedName -> ImportedName -> Bool
(ImportedName -> ImportedName -> Bool)
-> (ImportedName -> ImportedName -> Bool) -> Eq ImportedName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ImportedName -> ImportedName -> Bool
== :: ImportedName -> ImportedName -> Bool
$c/= :: ImportedName -> ImportedName -> Bool
/= :: ImportedName -> ImportedName -> Bool
Eq, Eq ImportedName
Eq ImportedName =>
(ImportedName -> ImportedName -> Ordering)
-> (ImportedName -> ImportedName -> Bool)
-> (ImportedName -> ImportedName -> Bool)
-> (ImportedName -> ImportedName -> Bool)
-> (ImportedName -> ImportedName -> Bool)
-> (ImportedName -> ImportedName -> ImportedName)
-> (ImportedName -> ImportedName -> ImportedName)
-> Ord ImportedName
ImportedName -> ImportedName -> Bool
ImportedName -> ImportedName -> Ordering
ImportedName -> ImportedName -> ImportedName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ImportedName -> ImportedName -> Ordering
compare :: ImportedName -> ImportedName -> Ordering
$c< :: ImportedName -> ImportedName -> Bool
< :: ImportedName -> ImportedName -> Bool
$c<= :: ImportedName -> ImportedName -> Bool
<= :: ImportedName -> ImportedName -> Bool
$c> :: ImportedName -> ImportedName -> Bool
> :: ImportedName -> ImportedName -> Bool
$c>= :: ImportedName -> ImportedName -> Bool
>= :: ImportedName -> ImportedName -> Bool
$cmax :: ImportedName -> ImportedName -> ImportedName
max :: ImportedName -> ImportedName -> ImportedName
$cmin :: ImportedName -> ImportedName -> ImportedName
min :: ImportedName -> ImportedName -> ImportedName
Ord, Int -> ImportedName -> String -> String
[ImportedName] -> String -> String
ImportedName -> String
(Int -> ImportedName -> String -> String)
-> (ImportedName -> String)
-> ([ImportedName] -> String -> String)
-> Show ImportedName
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> ImportedName -> String -> String
showsPrec :: Int -> ImportedName -> String -> String
$cshow :: ImportedName -> String
show :: ImportedName -> String
$cshowList :: [ImportedName] -> String -> String
showList :: [ImportedName] -> String -> String
Show)

instance HasRange ImportedName where
  getRange :: ImportedName -> Range
getRange = AbstractName -> Range
forall a. HasRange a => a -> Range
getRange (AbstractName -> Range)
-> (ImportedName -> AbstractName) -> ImportedName -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ImportedName -> AbstractName
iName

instance SetRange ImportedName where
  setRange :: Range -> ImportedName -> ImportedName
setRange Range
r (ImportedName Int
i AbstractName
n) = Int -> AbstractName -> ImportedName
ImportedName Int
i (Range -> AbstractName -> AbstractName
forall a. SetRange a => Range -> a -> a
setRange Range
r AbstractName
n)

instance Pretty ImportedName where
  pretty :: ImportedName -> Doc
pretty (ImportedName Int
i AbstractName
n) = AbstractName -> Doc
forall a. Pretty a => a -> Doc
pretty AbstractName
n Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
" (at position " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
i Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
")"

instance IsInstanceDef ImportedName where
  isInstanceDef :: ImportedName -> Maybe KwRange
isInstanceDef = AbstractName -> Maybe KwRange
forall a. IsInstanceDef a => a -> Maybe KwRange
isInstanceDef (AbstractName -> Maybe KwRange)
-> (ImportedName -> AbstractName) -> ImportedName -> Maybe KwRange
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ImportedName -> AbstractName
iName

-- | Convert an 'AbstractName' to an 'ImportedName' if it was brought into scope by an 'open' statement.
toImportedName :: AbstractName -> Maybe ImportedName
toImportedName :: AbstractName -> Maybe ImportedName
toImportedName AbstractName
x = case AbstractName -> WhyInScope
anameLineage AbstractName
x of
  Opened QName
m WhyInScope
_ -> QName -> Maybe Int
forall a. HasRange a => a -> Maybe Int
rangeToPosPos QName
m Maybe Int -> (Int -> ImportedName) -> Maybe ImportedName
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Int -> AbstractName -> ImportedName
`ImportedName` AbstractName
x)
  Applied{} -> Maybe ImportedName
forall a. Maybe a
Nothing
  Defined{} -> Maybe ImportedName
forall a. Maybe a
Nothing

-- Lenses for the components of the UnusedImportsState in the TCState.

stUnambiguousLookups :: Lens' TCState [AbstractName]
stUnambiguousLookups :: Lens' TCState [AbstractName]
stUnambiguousLookups = (UnusedImportsState -> f UnusedImportsState)
-> TCState -> f TCState
Lens' TCState UnusedImportsState
stUnusedImportsState ((UnusedImportsState -> f UnusedImportsState)
 -> TCState -> f TCState)
-> (([AbstractName] -> f [AbstractName])
    -> UnusedImportsState -> f UnusedImportsState)
-> ([AbstractName] -> f [AbstractName])
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([AbstractName] -> f [AbstractName])
-> UnusedImportsState -> f UnusedImportsState
Lens' UnusedImportsState [AbstractName]
lensUnambiguousLookups

stAmbiguousLookups :: Lens' TCState (IntMap (List2 AbstractName))
stAmbiguousLookups :: Lens' TCState (IntMap (List2 AbstractName))
stAmbiguousLookups = (UnusedImportsState -> f UnusedImportsState)
-> TCState -> f TCState
Lens' TCState UnusedImportsState
stUnusedImportsState ((UnusedImportsState -> f UnusedImportsState)
 -> TCState -> f TCState)
-> ((IntMap (List2 AbstractName)
     -> f (IntMap (List2 AbstractName)))
    -> UnusedImportsState -> f UnusedImportsState)
-> (IntMap (List2 AbstractName) -> f (IntMap (List2 AbstractName)))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IntMap (List2 AbstractName) -> f (IntMap (List2 AbstractName)))
-> UnusedImportsState -> f UnusedImportsState
Lens' UnusedImportsState (IntMap (List2 AbstractName))
lensAmbiguousLookups

stOpenedModules :: Lens' TCState (IntMap OpenedModule)
stOpenedModules :: Lens' TCState (IntMap OpenedModule)
stOpenedModules = (UnusedImportsState -> f UnusedImportsState)
-> TCState -> f TCState
Lens' TCState UnusedImportsState
stUnusedImportsState ((UnusedImportsState -> f UnusedImportsState)
 -> TCState -> f TCState)
-> ((IntMap OpenedModule -> f (IntMap OpenedModule))
    -> UnusedImportsState -> f UnusedImportsState)
-> (IntMap OpenedModule -> f (IntMap OpenedModule))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IntMap OpenedModule -> f (IntMap OpenedModule))
-> UnusedImportsState -> f UnusedImportsState
Lens' UnusedImportsState (IntMap OpenedModule)
lensOpenedModules