module Agda.TypeChecking.Warnings
  ( MonadWarning(..)
  , warning'_, warning_, warning', warning, warnings
  , raiseWarningsOnUsage
  , isUnsolvedWarning
  , isMetaWarning
  , isMetaTCWarning
  , onlyShowIfUnsolved
  , WhichWarnings(..), classifyWarning
  -- not exporting constructor of WarningsAndNonFatalErrors
  , WarningsAndNonFatalErrors, tcWarnings, nonFatalErrors
  , classifyWarnings
  ) where

import Control.Monad ( forM, unless )
import Control.Monad.Except ( MonadError(..) )
import Control.Monad.Reader ( ReaderT )
import Control.Monad.State  ( StateT )
import Control.Monad.Trans  ( MonadTrans, lift )
import Control.Monad.Trans.Maybe
import Control.Monad.Writer ( WriterT )

import Data.Foldable
import qualified Data.List as List
import qualified Data.Map  as Map
import qualified Data.Set  as Set
import Data.Maybe     ( catMaybes )
import Data.Semigroup ( Semigroup, (<>) )

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Caching
import {-# SOURCE #-} Agda.TypeChecking.Pretty ( MonadPretty, prettyTCM, vcat, ($$) )
import {-# SOURCE #-} Agda.TypeChecking.Pretty.Call
import {-# SOURCE #-} Agda.TypeChecking.Pretty.Warning ( prettyWarning )

import Agda.Syntax.Abstract.Name ( QName )
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Syntax.Position
import Agda.Syntax.Parser

import Agda.Interaction.Options
import Agda.Interaction.Options.Warnings
import {-# SOURCE #-} Agda.Interaction.Highlighting.Generate (highlightWarning)

import Agda.Utils.CallStack ( CallStack, HasCallStack, withCallerCallStack )
import Agda.Utils.Function  ( applyUnless )
import Agda.Utils.Lens
import Agda.Utils.List1 (List1)
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import qualified Agda.Utils.Set1 as Set1
import Agda.Utils.Singleton

import Agda.Utils.Impossible


-- * The warning monad
---------------------------------------------------------------------------

class (MonadPretty m, MonadError TCErr m) => MonadWarning m where
  -- | Store a warning and generate highlighting from it.
  addWarning :: TCWarning -> m ()

  default addWarning
    :: (MonadWarning n, MonadTrans t, t n ~ m)
    => TCWarning -> m ()
  addWarning = n () -> m ()
n () -> t n ()
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (n () -> m ()) -> (TCWarning -> n ()) -> TCWarning -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> n ()
forall (m :: * -> *). MonadWarning m => TCWarning -> m ()
addWarning

instance MonadWarning m => MonadWarning (MaybeT m)
instance MonadWarning m => MonadWarning (ReaderT r m)
instance MonadWarning m => MonadWarning (StateT s m)
instance (MonadWarning m, Monoid w) => MonadWarning (WriterT w m)

instance MonadWarning TCM where
  addWarning :: TCWarning -> TCM ()
addWarning TCWarning
tcwarn = do
    (Set TCWarning -> f (Set TCWarning)) -> TCState -> f TCState
Lens' TCState (Set TCWarning)
stTCWarnings Lens' TCState (Set TCWarning)
-> (Set TCWarning -> Set TCWarning) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` TCWarning -> Set TCWarning -> Set TCWarning
forall a. Ord a => a -> Set a -> Set a
Set.insert TCWarning
tcwarn
    TCWarning -> TCM ()
highlightWarning TCWarning
tcwarn

-- * Raising warnings
---------------------------------------------------------------------------

{-# SPECIALIZE warning'_ :: CallStack -> Warning -> TCM TCWarning #-}
warning'_ :: (MonadWarning m) => CallStack -> Warning -> m TCWarning
warning'_ :: forall (m :: * -> *).
MonadWarning m =>
CallStack -> Warning -> m TCWarning
warning'_ CallStack
loc Warning
w = do
  r <- Lens' TCEnv Range -> m Range
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Range -> f Range) -> TCEnv -> f TCEnv
Lens' TCEnv Range
eRange
  c <- viewTC eCall
  b <- areWeCaching
  let r' = case Warning
w of
        -- Some warnings come with their own error locations.
        NicifierIssue             DeclarationWarning
w0 -> DeclarationWarning -> Range
forall a. HasRange a => a -> Range
getRange DeclarationWarning
w0
        UnsolvedInteractionMetas  Set1 Range
rs -> Set1 Range -> Range
forall a. HasRange a => a -> Range
getRange Set1 Range
rs
        UnsolvedMetaVariables     Set1 Range
rs -> Set1 Range -> Range
forall a. HasRange a => a -> Range
getRange Set1 Range
rs
        UnsolvedConstraints       List1 ProblemConstraint
cs -> List1 ProblemConstraint -> Range
forall a. HasRange a => a -> Range
getRange List1 ProblemConstraint
cs
        InteractionMetaBoundaries Set1 Range
rs -> Set1 Range -> Range
forall a. HasRange a => a -> Range
getRange Set1 Range
rs
        Warning
_ -> Range
r
  let wn = Warning -> WarningName
warningName Warning
w
  let ws = WarningName -> [Char]
warningName2String WarningName
wn
  p <- vcat
    [ pure $ P.hsep
      [ if null r' then mempty else P.pretty r' P.<> P.colon
      , if wn `elem` errorWarnings then "error:" P.<+> P.brackets (P.text ws)
        else P.text $ "warning: -W[no]" ++ ws
        -- Only benign warnings can be deactivated with -WnoXXX.
      ]
    , prettyWarning w
    , prettyTCM c
    ]
  return $ TCWarning loc r' w p (P.render p) b

{-# SPECIALIZE warning_ :: Warning -> TCM TCWarning #-}
warning_ :: (HasCallStack, MonadWarning m) => Warning -> m TCWarning
warning_ :: forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m TCWarning
warning_ = (CallStack -> m TCWarning) -> m TCWarning
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> m TCWarning) -> m TCWarning)
-> (Warning -> CallStack -> m TCWarning) -> Warning -> m TCWarning
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CallStack -> Warning -> m TCWarning)
-> Warning -> CallStack -> m TCWarning
forall a b c. (a -> b -> c) -> b -> a -> c
flip CallStack -> Warning -> m TCWarning
forall (m :: * -> *).
MonadWarning m =>
CallStack -> Warning -> m TCWarning
warning'_

-- UNUSED Liang-Ting Chen 2019-07-16
---- | @applyWarningMode@ filters out the warnings the user has not requested
---- Users are not allowed to ignore non-fatal errors.
--
--applyWarningMode :: WarningMode -> Warning -> Maybe Warning
--applyWarningMode wm w = case classifyWarning w of
--  ErrorWarnings -> Just w
--  AllWarnings   -> w <$ guard (Set.member (warningName w) $ wm ^. warningSet)

{-# SPECIALIZE warnings' :: CallStack -> List1 Warning -> TCM () #-}
warnings' :: MonadWarning m => CallStack -> List1 Warning -> m ()
warnings' :: forall (m :: * -> *).
MonadWarning m =>
CallStack -> List1 Warning -> m ()
warnings' CallStack
loc List1 Warning
ws = do

  wmode <- PragmaOptions -> WarningMode
optWarningMode (PragmaOptions -> WarningMode) -> m PragmaOptions -> m WarningMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

  -- We collect *all* of the warnings no matter whether they are in the @warningSet@
  -- or not. If we find one which should be turned into an error, we keep processing
  -- the rest of the warnings and *then* report all of the errors at once.
  merrs <- forM ws $ \ Warning
w' -> do
    tcwarn <- CallStack -> Warning -> m TCWarning
forall (m :: * -> *).
MonadWarning m =>
CallStack -> Warning -> m TCWarning
warning'_ CallStack
loc Warning
w'
    if wmode ^. warn2Error && warningName w' `elem` wmode ^. warningSet
    then pure (Just tcwarn)
    else Nothing <$ addWarning tcwarn

  List1.unlessNull (List1.catMaybes merrs) \ List1 TCWarning
errs ->
    CallStack -> TypeError -> m ()
forall (m :: * -> *) a.
MonadTCError m =>
CallStack -> TypeError -> m a
typeError' CallStack
loc (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Set1 TCWarning -> TypeError
NonFatalErrors (Set1 TCWarning -> TypeError) -> Set1 TCWarning -> TypeError
forall a b. (a -> b) -> a -> b
$ List1 TCWarning -> Set1 TCWarning
forall a. Ord a => NonEmpty a -> NESet a
Set1.fromList List1 TCWarning
errs

{-# SPECIALIZE warnings :: HasCallStack => List1 Warning -> TCM () #-}
warnings :: (HasCallStack, MonadWarning m) => List1 Warning -> m ()
warnings :: forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
List1 Warning -> m ()
warnings = (CallStack -> m ()) -> m ()
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> m ()) -> m ())
-> (List1 Warning -> CallStack -> m ()) -> List1 Warning -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CallStack -> List1 Warning -> m ())
-> List1 Warning -> CallStack -> m ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip CallStack -> List1 Warning -> m ()
forall (m :: * -> *).
MonadWarning m =>
CallStack -> List1 Warning -> m ()
warnings'

{-# SPECIALIZE warning' :: CallStack -> Warning -> TCM () #-}
warning' :: MonadWarning m => CallStack -> Warning -> m ()
warning' :: forall (m :: * -> *).
MonadWarning m =>
CallStack -> Warning -> m ()
warning' CallStack
loc = CallStack -> List1 Warning -> m ()
forall (m :: * -> *).
MonadWarning m =>
CallStack -> List1 Warning -> m ()
warnings' CallStack
loc (List1 Warning -> m ())
-> (Warning -> List1 Warning) -> Warning -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> List1 Warning
forall el coll. Singleton el coll => el -> coll
singleton

{-# SPECIALIZE warning :: HasCallStack => Warning -> TCM () #-}
warning :: (HasCallStack, MonadWarning m) => Warning -> m ()
warning :: forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning = (CallStack -> m ()) -> m ()
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> m ()) -> m ())
-> (Warning -> CallStack -> m ()) -> Warning -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CallStack -> Warning -> m ()) -> Warning -> CallStack -> m ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip CallStack -> Warning -> m ()
forall (m :: * -> *).
MonadWarning m =>
CallStack -> Warning -> m ()
warning'

-- | Raise every 'WARNING_ON_USAGE' connected to a name.
{-# SPECIALIZE raiseWarningsOnUsage :: QName -> TCM () #-}
raiseWarningsOnUsage :: (MonadWarning m, ReadTCState m) => QName -> m ()
raiseWarningsOnUsage :: forall (m :: * -> *).
(MonadWarning m, ReadTCState m) =>
QName -> m ()
raiseWarningsOnUsage QName
d = do
  -- In case we find a defined name, we start by checking whether there's
  -- a warning attached to it
  [Char] -> VerboseLevel -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"scope.warning.usage" VerboseLevel
50 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Checking usage of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
P.prettyShow QName
d
  (Text -> m ()) -> Maybe Text -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Warning -> m ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> m ()) -> (Text -> Warning) -> Text -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Warning
UserWarning) (Maybe Text -> m ()) -> m (Maybe Text) -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> Map QName Text -> Maybe Text
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
d (Map QName Text -> Maybe Text)
-> m (Map QName Text) -> m (Maybe Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Map QName Text)
forall (m :: * -> *). ReadTCState m => m (Map QName Text)
getUserWarnings


-- * Classifying warnings
---------------------------------------------------------------------------

isUnsolvedWarning :: Warning -> Bool
isUnsolvedWarning :: Warning -> Bool
isUnsolvedWarning Warning
w = Warning -> WarningName
warningName Warning
w WarningName -> Set WarningName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set WarningName
unsolvedWarnings

isMetaWarning :: Warning -> Bool
isMetaWarning :: Warning -> Bool
isMetaWarning = \case
   UnsolvedInteractionMetas{} -> Bool
True
   UnsolvedMetaVariables{}    -> Bool
True
   Warning
_                          -> Bool
False

isMetaTCWarning :: TCWarning -> Bool
isMetaTCWarning :: TCWarning -> Bool
isMetaTCWarning = Warning -> Bool
isMetaWarning (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning

onlyShowIfUnsolved :: Warning -> Bool
onlyShowIfUnsolved :: Warning -> Bool
onlyShowIfUnsolved InversionDepthReached{} = Bool
True
onlyShowIfUnsolved Warning
_ = Bool
False

-- | Classifying warnings: some are benign, others are (non-fatal) errors

data WhichWarnings =
    ErrorWarnings -- ^ warnings that will be turned into errors
  | AllWarnings   -- ^ all warnings, including errors and benign ones
  -- Note: order of constructors is important for the derived Ord instance
  deriving (WhichWarnings -> WhichWarnings -> Bool
(WhichWarnings -> WhichWarnings -> Bool)
-> (WhichWarnings -> WhichWarnings -> Bool) -> Eq WhichWarnings
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: WhichWarnings -> WhichWarnings -> Bool
== :: WhichWarnings -> WhichWarnings -> Bool
$c/= :: WhichWarnings -> WhichWarnings -> Bool
/= :: WhichWarnings -> WhichWarnings -> Bool
Eq, Eq WhichWarnings
Eq WhichWarnings =>
(WhichWarnings -> WhichWarnings -> Ordering)
-> (WhichWarnings -> WhichWarnings -> Bool)
-> (WhichWarnings -> WhichWarnings -> Bool)
-> (WhichWarnings -> WhichWarnings -> Bool)
-> (WhichWarnings -> WhichWarnings -> Bool)
-> (WhichWarnings -> WhichWarnings -> WhichWarnings)
-> (WhichWarnings -> WhichWarnings -> WhichWarnings)
-> Ord WhichWarnings
WhichWarnings -> WhichWarnings -> Bool
WhichWarnings -> WhichWarnings -> Ordering
WhichWarnings -> WhichWarnings -> WhichWarnings
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 :: WhichWarnings -> WhichWarnings -> Ordering
compare :: WhichWarnings -> WhichWarnings -> Ordering
$c< :: WhichWarnings -> WhichWarnings -> Bool
< :: WhichWarnings -> WhichWarnings -> Bool
$c<= :: WhichWarnings -> WhichWarnings -> Bool
<= :: WhichWarnings -> WhichWarnings -> Bool
$c> :: WhichWarnings -> WhichWarnings -> Bool
> :: WhichWarnings -> WhichWarnings -> Bool
$c>= :: WhichWarnings -> WhichWarnings -> Bool
>= :: WhichWarnings -> WhichWarnings -> Bool
$cmax :: WhichWarnings -> WhichWarnings -> WhichWarnings
max :: WhichWarnings -> WhichWarnings -> WhichWarnings
$cmin :: WhichWarnings -> WhichWarnings -> WhichWarnings
min :: WhichWarnings -> WhichWarnings -> WhichWarnings
Ord)

classifyWarning :: Warning -> WhichWarnings
classifyWarning :: Warning -> WhichWarnings
classifyWarning Warning
w =
  if Warning -> WarningName
warningName Warning
w WarningName -> Set WarningName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set WarningName
errorWarnings
  then WhichWarnings
ErrorWarnings
  else WhichWarnings
AllWarnings

classifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings [TCWarning]
ws =
    Set TCWarning -> Set TCWarning -> WarningsAndNonFatalErrors
WarningsAndNonFatalErrors ([TCWarning] -> Set TCWarning
forall a. Ord a => [a] -> Set a
Set.fromList [TCWarning]
warnings) ([TCWarning] -> Set TCWarning
forall a. Ord a => [a] -> Set a
Set.fromList [TCWarning]
errors)
  where
    partite :: TCWarning -> Bool
partite = (WhichWarnings -> WhichWarnings -> Bool
forall a. Ord a => a -> a -> Bool
< WhichWarnings
AllWarnings) (WhichWarnings -> Bool)
-> (TCWarning -> WhichWarnings) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> WhichWarnings
classifyWarning (Warning -> WhichWarnings)
-> (TCWarning -> Warning) -> TCWarning -> WhichWarnings
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning
    ([TCWarning]
errors, [TCWarning]
warnings) = (TCWarning -> Bool) -> [TCWarning] -> ([TCWarning], [TCWarning])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition TCWarning -> Bool
partite [TCWarning]
ws