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

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

import Control.Monad ( forM, unless )
import Control.Monad.Reader ( ReaderT )
import Control.Monad.State ( StateT )
import Control.Monad.Trans ( lift )

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

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.Lens
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Except

class (MonadPretty m, MonadError TCErr m) => MonadWarning m where
  -- | Render the warning
  addWarning :: TCWarning -> m ()

instance Applicative m => Semigroup (ReaderT s m P.Doc) where
  ReaderT s m Doc
d1 <> :: ReaderT s m Doc -> ReaderT s m Doc -> ReaderT s m Doc
<> ReaderT s m Doc
d2 = Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
(<>) (Doc -> Doc -> Doc) -> ReaderT s m Doc -> ReaderT s m (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT s m Doc
d1 ReaderT s m (Doc -> Doc) -> ReaderT s m Doc -> ReaderT s m Doc
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT s m Doc
d2

instance MonadWarning m => MonadWarning (ReaderT r m) where
  addWarning :: TCWarning -> ReaderT r m ()
addWarning = m () -> ReaderT r m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ())
-> (TCWarning -> m ()) -> TCWarning -> ReaderT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> m ()
forall (m :: * -> *). MonadWarning m => TCWarning -> m ()
addWarning

instance Monad m => Semigroup (StateT s m P.Doc) where
  StateT s m Doc
d1 <> :: StateT s m Doc -> StateT s m Doc -> StateT s m Doc
<> StateT s m Doc
d2 = Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
(<>) (Doc -> Doc -> Doc) -> StateT s m Doc -> StateT s m (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT s m Doc
d1 StateT s m (Doc -> Doc) -> StateT s m Doc -> StateT s m Doc
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT s m Doc
d2

instance MonadWarning m => MonadWarning (StateT s m) where
  addWarning :: TCWarning -> StateT s m ()
addWarning = m () -> StateT s m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT s m ())
-> (TCWarning -> m ()) -> TCWarning -> StateT s m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> m ()
forall (m :: * -> *). MonadWarning m => TCWarning -> m ()
addWarning

-- This instance is more specific than a generic instance
-- @Semigroup a => Semigroup (TCM a)@
instance {-# OVERLAPPING #-} Semigroup (TCM P.Doc) where
  TCM Doc
d1 <> :: TCM Doc -> TCM Doc -> TCM Doc
<> TCM Doc
d2 = Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
(<>) (Doc -> Doc -> Doc) -> TCM Doc -> TCMT IO (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Doc
d1 TCMT IO (Doc -> Doc) -> TCM Doc -> TCM Doc
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TCM Doc
d2

instance MonadWarning TCM where
  addWarning :: TCWarning -> TCM ()
addWarning TCWarning
tcwarn = do
    Lens' [TCWarning] TCState
stTCWarnings Lens' [TCWarning] TCState -> ([TCWarning] -> [TCWarning]) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` Warning -> TCWarning -> [TCWarning] -> [TCWarning]
forall a. Eq a => Warning -> a -> [a] -> [a]
add Warning
w' TCWarning
tcwarn
    TCWarning -> TCM ()
highlightWarning TCWarning
tcwarn
    where
      w' :: Warning
w' = TCWarning -> Warning
tcWarning TCWarning
tcwarn

      add :: Warning -> a -> [a] -> [a]
add Warning
w a
tcwarn [a]
tcwarns
        | Warning -> Bool
onlyOnce Warning
w Bool -> Bool -> Bool
&& a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
tcwarn [a]
tcwarns = [a]
tcwarns -- Eq on TCWarning only checks head constructor
        | Bool
otherwise                         = a
tcwarn a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
tcwarns

{-# SPECIALIZE genericWarning :: P.Doc -> TCM () #-}
genericWarning :: MonadWarning m => P.Doc -> m ()
genericWarning :: Doc -> m ()
genericWarning = Warning -> m ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> m ()) -> (Doc -> Warning) -> Doc -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Warning
GenericWarning

{-# SPECIALIZE genericNonFatalError :: P.Doc -> TCM () #-}
genericNonFatalError :: MonadWarning m => P.Doc -> m ()
genericNonFatalError :: Doc -> m ()
genericNonFatalError = Warning -> m ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> m ()) -> (Doc -> Warning) -> Doc -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Warning
GenericNonFatalError

{-# SPECIALIZE warning_ :: Warning -> TCM TCWarning #-}
warning_ :: MonadWarning m => Warning -> m TCWarning
warning_ :: Warning -> m TCWarning
warning_ Warning
w = do
  Range
r <- Lens' Range TCEnv -> m Range
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Range TCEnv
eRange
  Maybe (Closure Call)
c <- Lens' (Maybe (Closure Call)) TCEnv -> m (Maybe (Closure Call))
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' (Maybe (Closure Call)) TCEnv
eCall
  Bool
b <- m Bool
forall (m :: * -> *). ReadTCState m => m Bool
areWeCaching
  -- NicifierIssues print their own error locations in their list of
  -- issues (but we might need to keep the overall range `r` for
  -- comparing ranges)
  let r' :: Range
r' = case Warning
w of { NicifierIssue{} -> Range
forall a. Range' a
NoRange ; Warning
_ -> Range
r }
  Doc
p <- Range -> Maybe (Closure Call) -> m Doc -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Range -> Maybe (Closure Call) -> m Doc -> m Doc
sayWhen Range
r' Maybe (Closure Call)
c (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Warning -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Warning
w
  TCWarning -> m TCWarning
forall (m :: * -> *) a. Monad m => a -> m a
return (TCWarning -> m TCWarning) -> TCWarning -> m TCWarning
forall a b. (a -> b) -> a -> b
$ Range -> Warning -> Doc -> Bool -> TCWarning
TCWarning Range
r Warning
w Doc
p Bool
b

-- 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 :: [Warning] -> TCM () #-}
warnings :: MonadWarning m => [Warning] -> m ()
warnings :: [Warning] -> m ()
warnings [Warning]
ws = do

  WarningMode
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.
  [Maybe TCWarning]
merrs <- [Warning]
-> (Warning -> m (Maybe TCWarning)) -> m [Maybe TCWarning]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Warning]
ws ((Warning -> m (Maybe TCWarning)) -> m [Maybe TCWarning])
-> (Warning -> m (Maybe TCWarning)) -> m [Maybe TCWarning]
forall a b. (a -> b) -> a -> b
$ \ Warning
w' -> do
    TCWarning
tcwarn <- Warning -> m TCWarning
forall (m :: * -> *). MonadWarning m => Warning -> m TCWarning
warning_ Warning
w'
    if WarningMode
wmode WarningMode -> Lens' Bool WarningMode -> Bool
forall o i. o -> Lens' i o -> i
^. Lens' Bool WarningMode
warn2Error Bool -> Bool -> Bool
&& Warning -> WarningName
warningName Warning
w' WarningName -> Set WarningName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` WarningMode
wmode WarningMode
-> Lens' (Set WarningName) WarningMode -> Set WarningName
forall o i. o -> Lens' i o -> i
^. Lens' (Set WarningName) WarningMode
warningSet
    then Maybe TCWarning -> m (Maybe TCWarning)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TCWarning -> Maybe TCWarning
forall a. a -> Maybe a
Just TCWarning
tcwarn)
    else Maybe TCWarning
forall a. Maybe a
Nothing Maybe TCWarning -> m () -> m (Maybe TCWarning)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ TCWarning -> m ()
forall (m :: * -> *). MonadWarning m => TCWarning -> m ()
addWarning TCWarning
tcwarn

  let errs :: [TCWarning]
errs = [Maybe TCWarning] -> [TCWarning]
forall a. [Maybe a] -> [a]
catMaybes [Maybe TCWarning]
merrs
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TCWarning] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TCWarning]
errs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ TypeError -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ [TCWarning] -> TypeError
NonFatalErrors [TCWarning]
errs

{-# SPECIALIZE warning :: Warning -> TCM () #-}
warning :: MonadWarning m => Warning -> m ()
warning :: Warning -> m ()
warning = [Warning] -> m ()
forall (m :: * -> *). MonadWarning m => [Warning] -> m ()
warnings ([Warning] -> m ()) -> (Warning -> [Warning]) -> Warning -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> [Warning]
forall (f :: * -> *) a. Applicative f => a -> f a
pure

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 Warning
w = case Warning
w of
   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

-- | Should we only emit a single warning with this constructor.
onlyOnce :: Warning -> Bool
onlyOnce :: Warning -> Bool
onlyOnce InversionDepthReached{} = Bool
True
onlyOnce Warning
_ = Bool
False

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
/= :: WhichWarnings -> WhichWarnings -> Bool
$c/= :: WhichWarnings -> WhichWarnings -> Bool
== :: WhichWarnings -> WhichWarnings -> Bool
$c== :: 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
min :: WhichWarnings -> WhichWarnings -> WhichWarnings
$cmin :: WhichWarnings -> WhichWarnings -> WhichWarnings
max :: WhichWarnings -> WhichWarnings -> WhichWarnings
$cmax :: WhichWarnings -> WhichWarnings -> WhichWarnings
>= :: WhichWarnings -> WhichWarnings -> Bool
$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
compare :: WhichWarnings -> WhichWarnings -> Ordering
$ccompare :: WhichWarnings -> WhichWarnings -> Ordering
$cp1Ord :: Eq 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

-- | Assorted warnings and errors to be displayed to the user
data WarningsAndNonFatalErrors = WarningsAndNonFatalErrors
  { WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings     :: [TCWarning]
  , WarningsAndNonFatalErrors -> [TCWarning]
nonFatalErrors :: [TCWarning]
  }

-- | The only way to construct a empty WarningsAndNonFatalErrors

emptyWarningsAndNonFatalErrors :: WarningsAndNonFatalErrors
emptyWarningsAndNonFatalErrors :: WarningsAndNonFatalErrors
emptyWarningsAndNonFatalErrors = [TCWarning] -> [TCWarning] -> WarningsAndNonFatalErrors
WarningsAndNonFatalErrors [] []

classifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings [TCWarning]
ws = [TCWarning] -> [TCWarning] -> WarningsAndNonFatalErrors
WarningsAndNonFatalErrors [TCWarning]
warnings [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


-- | running the Parse monad

runPM :: PM a -> TCM a
runPM :: PM a -> TCM a
runPM PM a
m = do
  (Either ParseError a
res, [ParseWarning]
ws) <- PM a -> TCMT IO (Either ParseError a, [ParseWarning])
forall (m :: * -> *) a.
MonadIO m =>
PM a -> m (Either ParseError a, [ParseWarning])
runPMIO PM a
m
  (ParseWarning -> TCM ()) -> [ParseWarning] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Warning -> TCM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> TCM ())
-> (ParseWarning -> Warning) -> ParseWarning -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseWarning -> Warning
ParseWarning) [ParseWarning]
ws
  case Either ParseError a
res of
    Left  ParseError
e -> TCErr -> TCM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Range -> Doc -> TCErr
Exception (ParseError -> Range
forall t. HasRange t => t -> Range
getRange ParseError
e) (ParseError -> Doc
forall a. Pretty a => a -> Doc
P.pretty ParseError
e))
    Right a
a -> a -> TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a