{-# 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 )
import Data.List ( stripPrefix, intercalate )
import Agda.Utils.Lens
import Agda.Utils.Maybe
#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_
, MissingDefinitions_
, NotAllowedInMutual_
, NotStrictlyPositive_
, OverlappingTokensWarning_
, PragmaCompiled_
, SafeFlagPostulate_
, SafeFlagPragma_
, SafeFlagNonTerminating_
, SafeFlagTerminating_
, SafeFlagWithoutKFlagPrimEraseEquality_
, SafeFlagNoPositivityCheck_
, SafeFlagPolarity_
, SafeFlagNoUniverseCheck_
, TerminationIssue_
, UnsolvedMetaVariables_
, UnsolvedInteractionMetas_
, UnsolvedConstraints_
, InfectiveImport_
, CoInfectiveImport_
]
allWarnings :: Set WarningName
allWarnings = Set.fromList [minBound..maxBound]
usualWarnings :: Set WarningName
usualWarnings = allWarnings Set.\\ Set.fromList
[ UnknownFixityInMixfixDecl_
, CoverageNoExactSplit_
]
data WarningName
=
OverlappingTokensWarning_
| LibUnknownField_
| EmptyAbstract_
| EmptyInstance_
| EmptyMacro_
| EmptyMutual_
| EmptyPostulate_
| EmptyPrivate_
| EmptyGeneralize_
| EmptyPrimitive_
| InvalidCatchallPragma_
| InvalidNoUniverseCheckPragma_
| InvalidTerminationCheckPragma_
| InvalidNoPositivityCheckPragma_
| MissingDefinitions_
| NotAllowedInMutual_
| PolarityPragmasButNotPostulates_
| PragmaNoTerminationCheck_
| PragmaCompiled_
| UnknownFixityInMixfixDecl_
| UnknownNamesInFixityDecl_
| UnknownNamesInPolarityPragmas_
| UselessAbstract_
| UselessInstance_
| UselessPrivate_
| OldBuiltin_
| EmptyRewritePragma_
| IllformedAsClause_
| UselessPublic_
| UnreachableClauses_
| UselessInline_
| WrongInstanceDeclaration_
| InstanceWithExplicitArg_
| InstanceNoOutputTypeName_
| InstanceArgWithExplicitArg_
| GenericWarning_
| DeprecationWarning_
| InversionDepthReached_
| TerminationIssue_
| CoverageIssue_
| CoverageNoExactSplit_
| ModuleDoesntExport_
| NotStrictlyPositive_
| UnsolvedMetaVariables_
| UnsolvedInteractionMetas_
| UnsolvedConstraints_
| GenericNonFatalError_
| SafeFlagPostulate_
| SafeFlagPragma_
| SafeFlagNonTerminating_
| SafeFlagTerminating_
| SafeFlagWithoutKFlagPrimEraseEquality_
| SafeFlagNoPositivityCheck_
| SafeFlagPolarity_
| SafeFlagNoUniverseCheck_
| UserWarning_
| WithoutKFlagPrimEraseEquality_
| CantGeneralizeOverSorts_
| AbsurdPatternRequiresNoRHS_
| InfectiveImport_
| CoInfectiveImport_
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 $ forMaybe [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."
LibUnknownField_ -> "Unknown field in library file"
EmptyAbstract_ -> "Empty `abstract' blocks."
EmptyInstance_ -> "Empty `instance' blocks."
EmptyMacro_ -> "Empty `macro' blocks."
EmptyMutual_ -> "Empty `mutual' blocks."
EmptyPostulate_ -> "Empty `postulate' blocks."
EmptyPrivate_ -> "Empty `private' blocks."
EmptyGeneralize_ -> "Empty `variable' blocks."
EmptyPrimitive_ -> "Empty `primitive' blocks."
InvalidCatchallPragma_ -> "`CATCHALL' pragmas before a non-function clause."
InvalidNoPositivityCheckPragma_ -> "No positivity checking pragmas before non-`data', `record' or `mutual' blocks."
InvalidNoUniverseCheckPragma_ -> "No universe checking pragmas before non-`data' or `record' declaration."
InvalidTerminationCheckPragma_ -> "Termination checking pragmas before non-function or `mutual' blocks."
MissingDefinitions_ -> "Declarations not associated to a definition."
NotAllowedInMutual_ -> "Declarations not allowed in a mutual block."
PolarityPragmasButNotPostulates_ -> "Polarity pragmas for non-postulates."
PragmaNoTerminationCheck_ -> "`NO_TERMINATION_CHECK' pragmas are deprecated"
PragmaCompiled_ -> "'COMPILE' pragmas not allowed in safe mode."
UnknownFixityInMixfixDecl_ -> "Mixfix names without an associated fixity declaration."
UnknownNamesInFixityDecl_ -> "Names not declared in the same scope as their syntax or fixity declaration."
UnknownNamesInPolarityPragmas_ -> "Names not declared in the same scope as their polarity pragmas."
UselessAbstract_ -> "`abstract' blocks where they have no effect."
UselessInstance_ -> "`instance' blocks where they have no effect."
UselessPrivate_ -> "`private' blocks where they have no effect."
OldBuiltin_ -> "Deprecated `BUILTIN' pragmas."
EmptyRewritePragma_ -> "Empty `REWRITE' pragmas."
IllformedAsClause_ -> "Illformed `as'-clauses in `import' statements."
UselessPublic_ -> "`public' blocks where they have no effect."
UselessInline_ -> "`INLINE' pragmas where they have no effect."
WrongInstanceDeclaration_ -> "Terms marked as eligible for instance search should end with a name."
InstanceWithExplicitArg_ -> "`instance` declarations with explicit arguments are never considered by instance search."
InstanceNoOutputTypeName_ -> "instance arguments whose type does not end in a named or variable type are never considered by instance search."
InstanceArgWithExplicitArg_ -> "instance arguments with explicit arguments are never considered by instance search."
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."
ModuleDoesntExport_ -> "Imported name is not actually exported."
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."
SafeFlagWithoutKFlagPrimEraseEquality_ -> "`primEraseEquality' usages with the safe and without-K flags."
SafeFlagNoPositivityCheck_ -> "`NO_POSITIVITY_CHECK' pragmas with the safe flag."
SafeFlagPolarity_ -> "`POLARITY' pragmas with the safe flag."
SafeFlagNoUniverseCheck_ -> "`NO_UNIVERSE_CHECK' pragmas with the safe flag."
UserWarning_ -> "User-defined warning added using the 'WARNING_ON_USAGE' pragma."
AbsurdPatternRequiresNoRHS_ -> "A clause with an absurd pattern does not need a Right Hand Side."
CantGeneralizeOverSorts_ -> "Attempt to generalize over sort metas in 'variable' declaration."
WithoutKFlagPrimEraseEquality_ -> "`primEraseEquality' usages with the without-K flags."
InfectiveImport_ -> "Importing a file using e.g. `--cubical' into one which doesn't"
CoInfectiveImport_ -> "Importing a file not using e.g. `--safe' from one which does"