module Agda.TypeChecking.Warnings where
import qualified Data.List as List
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Pretty
import Agda.Syntax.Position
import Agda.Syntax.Parser
import Agda.Interaction.Options
import Agda.Utils.Lens
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Except
#if __GLASGOW_HASKELL__ <= 708
import Control.Applicative ((<$>))
#endif
genericWarning :: MonadTCM tcm => P.Doc -> tcm ()
genericWarning = warning . GenericWarning
genericNonFatalError :: MonadTCM tcm => P.Doc -> tcm ()
genericNonFatalError = warning . GenericNonFatalError
warning_ :: MonadTCM tcm => Warning -> tcm TCWarning
warning_ w = do
r <- view eRange
c <- view eCall
let r' = case w of { NicifierIssue{} -> NoRange ; _ -> r }
p <- liftTCM $ sayWhen r' c $ prettyWarning w
liftTCM $ return $ TCWarning r w p
warning :: MonadTCM tcm => Warning -> tcm ()
warning w = do
tcwarn <- warning_ w
wmode <- optWarningMode <$> pragmaOptions
case wmode of
IgnoreAllWarnings -> case classifyWarning w of
ErrorWarnings -> raiseWarning tcwarn
AllWarnings -> return ()
TurnIntoErrors -> typeError $ NonFatalErrors [tcwarn]
LeaveAlone -> raiseWarning tcwarn
where raiseWarning tcw = stTCWarnings %= (tcw :)
data WhichWarnings =
ErrorWarnings
| AllWarnings
deriving (Eq, Ord)
isUnsolvedWarning :: Warning -> Bool
isUnsolvedWarning w = case w of
UnsolvedMetaVariables{} -> True
UnsolvedInteractionMetas{} -> True
UnsolvedConstraints{} -> True
_ -> False
classifyWarning :: Warning -> WhichWarnings
classifyWarning w = case w of
OldBuiltin{} -> AllWarnings
EmptyRewritePragma -> AllWarnings
UselessPublic -> AllWarnings
UnreachableClauses{} -> AllWarnings
UselessInline{} -> AllWarnings
GenericWarning{} -> AllWarnings
DeprecationWarning{} -> AllWarnings
NicifierIssue{} -> AllWarnings
TerminationIssue{} -> ErrorWarnings
CoverageIssue{} -> ErrorWarnings
CoverageNoExactSplit{} -> ErrorWarnings
NotStrictlyPositive{} -> ErrorWarnings
UnsolvedMetaVariables{} -> ErrorWarnings
UnsolvedInteractionMetas{} -> ErrorWarnings
UnsolvedConstraints{} -> ErrorWarnings
GenericNonFatalError{} -> ErrorWarnings
SafeFlagPostulate{} -> ErrorWarnings
SafeFlagPragma{} -> ErrorWarnings
SafeFlagNonTerminating -> ErrorWarnings
SafeFlagTerminating -> ErrorWarnings
SafeFlagPrimTrustMe -> ErrorWarnings
SafeFlagNoPositivityCheck -> ErrorWarnings
SafeFlagPolarity -> ErrorWarnings
ParseWarning{} -> ErrorWarnings
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