{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Warnings where
import qualified Data.Set as Set
import qualified Data.List as List
import Data.Maybe ( catMaybes )
import Control.Monad ( guard, forM, unless )
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Caching
import {-# SOURCE #-} Agda.TypeChecking.Errors
import {-# SOURCE #-} Agda.TypeChecking.Pretty
import Agda.Syntax.Position
import Agda.Syntax.Parser
import Agda.Syntax.Concrete.Definitions (DeclarationWarning(..))
import Agda.Interaction.Options
import Agda.Interaction.Options.Warnings
import Agda.Utils.Lens
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Except
{-# SPECIALIZE genericWarning :: P.Doc -> TCM () #-}
genericWarning :: MonadTCM tcm => P.Doc -> tcm ()
genericWarning = warning . GenericWarning
{-# SPECIALIZE genericNonFatalError :: P.Doc -> TCM () #-}
genericNonFatalError :: MonadTCM tcm => P.Doc -> tcm ()
genericNonFatalError = warning . GenericNonFatalError
{-# SPECIALIZE warning_ :: Warning -> TCM TCWarning #-}
warning_ :: MonadTCM tcm => Warning -> tcm TCWarning
warning_ w = do
r <- view eRange
c <- view eCall
b <- liftTCM areWeCaching
let r' = case w of { NicifierIssue{} -> NoRange ; _ -> r }
p <- liftTCM $ sayWhen r' c $ prettyWarning w
liftTCM $ return $ TCWarning r w p b
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 :: MonadTCM tcm => [Warning] -> tcm ()
warnings ws = do
wmode <- optWarningMode <$> pragmaOptions
let add w tcwarn tcwarns
| onlyOnce w && elem tcwarn tcwarns = tcwarns
| otherwise = tcwarn : tcwarns
merrs <- forM ws $ \ w' -> do
tcwarn <- warning_ w'
if wmode ^. warn2Error && warningName w' `elem` wmode ^. warningSet
then pure (Just tcwarn)
else Nothing <$ (stTCWarnings %= add w' tcwarn)
let errs = catMaybes merrs
unless (null errs) $ typeError $ NonFatalErrors errs
{-# SPECIALIZE warning :: Warning -> TCM () #-}
warning :: MonadTCM tcm => Warning -> tcm ()
warning = warnings . pure
data WhichWarnings =
ErrorWarnings
| AllWarnings
deriving (Eq, Ord)
isUnsolvedWarning :: Warning -> Bool
isUnsolvedWarning w = warningName w `elem` unsolvedWarnings
classifyWarning :: Warning -> WhichWarnings
classifyWarning w =
if warningName w `elem` errorWarnings
then ErrorWarnings
else AllWarnings
onlyOnce :: Warning -> Bool
onlyOnce InversionDepthReached{} = True
onlyOnce _ = False
onlyShowIfUnsolved :: Warning -> Bool
onlyShowIfUnsolved InversionDepthReached{} = True
onlyShowIfUnsolved _ = False
classifyWarnings :: [TCWarning] -> ([TCWarning], [TCWarning])
classifyWarnings = List.partition $ (< AllWarnings) . classifyWarning . tcWarning
runPM :: PM a -> TCM a
runPM m = do
(res, ws) <- runPMIO m
mapM_ (warning . ParseWarning) ws
case res of
Left e -> throwError (Exception (getRange e) (P.pretty e))
Right a -> return a