{-# LANGUAGE CPP #-}
module Agda.Interaction.Options.Warnings
(
WarningMode (..)
, warningSet
, warn2Error
, defaultWarningSet
, allWarnings
, usualWarnings
, noWarnings
, unsolvedWarnings
, errorWarnings
, defaultWarningMode
, warningModeUpdate
, warningSets
, WarningName (..)
, warningName2String
, string2WarningName
, usageWarning
)
where
import Control.Arrow ( (&&&) )
import Control.Monad ( guard )
import Data.Traversable ( for )
import Text.Read ( readMaybe )
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Maybe ( fromMaybe, catMaybes )
import Data.List ( stripPrefix, intercalate )
import Agda.Utils.Lens
#include "undefined.h"
import Agda.Utils.Impossible
data WarningMode = WarningMode
{ _warningSet :: Set WarningName
, _warn2Error :: Bool
} deriving (Eq, Show)
warningSet :: Lens' (Set WarningName) WarningMode
warningSet f o = (\ ws -> o { _warningSet = ws }) <$> f (_warningSet o)
warn2Error :: Lens' Bool WarningMode
warn2Error f o = (\ ws -> o { _warn2Error = ws }) <$> f (_warn2Error o)
defaultWarningSet :: String
defaultWarningSet = "warn"
defaultWarningMode :: WarningMode
defaultWarningMode = WarningMode ws False where
ws = fst $ fromMaybe __IMPOSSIBLE__ $ lookup defaultWarningSet warningSets
warningModeUpdate :: String -> Maybe (WarningMode -> WarningMode)
warningModeUpdate str = case str of
"error" -> Just $ set warn2Error True
"noerror" -> Just $ set warn2Error False
_ | Just ws <- fst <$> lookup str warningSets
-> Just $ set warningSet ws
_ -> case stripPrefix "no" str of
Just str' -> (over warningSet . Set.delete) <$> string2WarningName str'
Nothing -> (over warningSet . Set.insert) <$> string2WarningName str
warningSets :: [(String, (Set WarningName, String))]
warningSets = [ ("all" , (allWarnings, "All of the existing warnings"))
, ("warn" , (usualWarnings, "Default warning level"))
, ("ignore", (errorWarnings, "Ignore all the benign warnings"))
]
noWarnings :: Set WarningName
noWarnings = Set.empty
unsolvedWarnings :: Set WarningName
unsolvedWarnings = Set.fromList
[ UnsolvedMetaVariables_
, UnsolvedInteractionMetas_
, UnsolvedConstraints_
]
errorWarnings :: Set WarningName
errorWarnings = Set.fromList
[ CoverageIssue_
, GenericNonFatalError_
, NotStrictlyPositive_
, OverlappingTokensWarning_
, SafeFlagPostulate_
, SafeFlagPragma_
, SafeFlagNonTerminating_
, SafeFlagTerminating_
, SafeFlagPrimTrustMe_
, SafeFlagNoPositivityCheck_
, SafeFlagPolarity_
, TerminationIssue_
, UnsolvedMetaVariables_
, UnsolvedInteractionMetas_
, UnsolvedConstraints_
]
allWarnings :: Set WarningName
allWarnings = Set.fromList [minBound..maxBound]
usualWarnings :: Set WarningName
usualWarnings = allWarnings Set.\\ Set.fromList
[ UnknownFixityInMixfixDecl_
, CoverageNoExactSplit_
]
data WarningName
=
OverlappingTokensWarning_
| UnknownNamesInFixityDecl_
| UnknownFixityInMixfixDecl_
| UnknownNamesInPolarityPragmas_
| PolarityPragmasButNotPostulates_
| UselessPrivate_
| UselessAbstract_
| UselessInstance_
| EmptyMutual_
| EmptyAbstract_
| EmptyPrivate_
| EmptyInstance_
| EmptyMacro_
| EmptyPostulate_
| InvalidTerminationCheckPragma_
| InvalidNoPositivityCheckPragma_
| InvalidCatchallPragma_
| OldBuiltin_
| EmptyRewritePragma_
| UselessPublic_
| UnreachableClauses_
| UselessInline_
| GenericWarning_
| DeprecationWarning_
| InversionDepthReached_
| TerminationIssue_
| CoverageIssue_
| CoverageNoExactSplit_
| NotStrictlyPositive_
| UnsolvedMetaVariables_
| UnsolvedInteractionMetas_
| UnsolvedConstraints_
| GenericNonFatalError_
| SafeFlagPostulate_
| SafeFlagPragma_
| SafeFlagNonTerminating_
| SafeFlagTerminating_
| SafeFlagPrimTrustMe_
| SafeFlagNoPositivityCheck_
| SafeFlagPolarity_
| UserWarning_
deriving (Eq, Ord, Show, Read, Enum, Bounded)
string2WarningName :: String -> Maybe WarningName
string2WarningName = readMaybe . (++ "_")
warningName2String :: WarningName -> String
warningName2String = init . show
usageWarning :: String
usageWarning = intercalate "\n"
[ concat [ "The -W or --warning option can be used to disable or enable "
, "different warnings. The flag -W error (or --warning=error) "
, "can be used to turn all warnings into errors, while -W noerror "
, "turns this off again."
]
, ""
, concat [ "A group of warnings can be enabled by -W group, where group is "
, "one of the following:"
]
, ""
, untable (fmap (fst &&& snd . snd) warningSets)
, concat [ "Individual warnings can be turned on and off by -W Name and "
, "-W noName respectively. The flags available are:"
]
, ""
, untable $ catMaybes $ flip map [minBound..maxBound] $ \ w ->
let wnd = warningNameDescription w in
(warningName2String w, wnd) <$ guard (not $ null wnd)
]
where
untable :: [(String, String)] -> String
untable rows =
let len = maximum (map (length . fst) rows) in
unlines $ flip map rows $ \ (hdr, cnt) ->
concat [ hdr, replicate (1 + len - length hdr) ' ', cnt ]
warningNameDescription :: WarningName -> String
warningNameDescription w = case w of
OverlappingTokensWarning_ -> "Multi-line comments spanning one or more literate text blocks."
UnknownNamesInFixityDecl_ -> "Names not declared in the same scope as their syntax or fixity declaration."
UnknownFixityInMixfixDecl_ -> "Mixfix names without an associated fixity declaration."
UnknownNamesInPolarityPragmas_ -> "Names not declared in the same scope as their polarity pragmas."
PolarityPragmasButNotPostulates_ -> "Polarity pragmas for non-postulates."
UselessPrivate_ -> "`private' blocks where they have no effect."
UselessAbstract_ -> "`abstract' blocks where they have no effect."
UselessInstance_ -> "`instance' blocks where they have no effect."
EmptyMutual_ -> "Empty `mutual' blocks."
EmptyAbstract_ -> "Empty `abstract' blocks."
EmptyPrivate_ -> "Empty `private' blocks."
EmptyInstance_ -> "Empty `instance' blocks."
EmptyMacro_ -> "Empty `macro' blocks."
EmptyPostulate_ -> "Empty `postulate' blocks."
InvalidTerminationCheckPragma_ -> "Termination checking pragmas before non-function or `mutual' blocks."
InvalidNoPositivityCheckPragma_ -> "No positivity checking pragmas before non-`data', `record' or `mutual' blocks."
InvalidCatchallPragma_ -> "`CATCHALL' pragmas before a non-function clause."
OldBuiltin_ -> "Deprecated `BUILTIN' pragmas."
EmptyRewritePragma_ -> "Empty `REWRITE' pragmas."
UselessPublic_ -> "`public' blocks where they have no effect."
UselessInline_ -> "`INLINE' pragmas where they have no effect."
UnreachableClauses_ -> "Unreachable function clauses."
GenericWarning_ -> ""
DeprecationWarning_ -> "Feature deprecation."
InversionDepthReached_ -> "Inversions of pattern-matching failed due to exhausted inversion depth."
TerminationIssue_ -> "Failed termination checks."
CoverageIssue_ -> "Failed coverage checks."
CoverageNoExactSplit_ -> "Failed exact split checks."
NotStrictlyPositive_ -> "Failed strict positivity checks."
UnsolvedMetaVariables_ -> "Unsolved meta variables."
UnsolvedInteractionMetas_ -> "Unsolved interaction meta variables."
UnsolvedConstraints_ -> "Unsolved constraints."
GenericNonFatalError_ -> ""
SafeFlagPostulate_ -> "`postulate' blocks with the safe flag"
SafeFlagPragma_ -> "Unsafe `OPTIONS' pragmas with the safe flag."
SafeFlagNonTerminating_ -> "`NON_TERMINATING' pragmas with the safe flag."
SafeFlagTerminating_ -> "`TERMINATING' pragmas with the safe flag."
SafeFlagPrimTrustMe_ -> "`primTrustMe' usages with the safe flag."
SafeFlagNoPositivityCheck_ -> "`NO_POSITIVITY_CHECK' pragmas with the safe flag."
SafeFlagPolarity_ -> "`POLARITY' pragmas with the safe flag."
UserWarning_ -> "User-defined warning added using the 'WARNING_ON_USAGE' pragma."