1 2module Agda.Interaction.Options.Warnings 3 ( 4 WarningMode (..) 5 , warningSet 6 , warn2Error 7 , defaultWarningSet 8 , allWarnings 9 , usualWarnings 10 , noWarnings 11 , unsolvedWarnings 12 , incompleteMatchWarnings 13 , errorWarnings 14 , defaultWarningMode 15 , WarningModeError(..) 16 , prettyWarningModeError 17 , warningModeUpdate 18 , warningSets 19 , WarningName (..) 20 , warningName2String 21 , string2WarningName 22 , usageWarning 23 ) 24where 25 26import Control.Arrow ( (&&&) ) 27import Control.DeepSeq 28import Control.Monad ( guard, when ) 29 30import Text.Read ( readMaybe ) 31import Data.Set (Set) 32import qualified Data.Set as Set 33import Data.List ( stripPrefix, intercalate ) 34 35import GHC.Generics (Generic) 36 37import Agda.Utils.Lens 38import Agda.Utils.List 39import Agda.Utils.Maybe 40 41import Agda.Utils.Impossible 42 43 44-- | A @WarningMode@ has two components: a set of warnings to be displayed 45-- and a flag stating whether warnings should be turned into fatal errors. 46data WarningMode = WarningMode 47 { _warningSet :: Set WarningName 48 , _warn2Error :: Bool 49 } deriving (Eq, Show, Generic) 50 51instance NFData WarningMode 52 53warningSet :: Lens' (Set WarningName) WarningMode 54warningSet f o = (\ ws -> o { _warningSet = ws }) <$> f (_warningSet o) 55 56warn2Error :: Lens' Bool WarningMode 57warn2Error f o = (\ ws -> o { _warn2Error = ws }) <$> f (_warn2Error o) 58 59-- | The @defaultWarningMode@ is a curated set of warnings covering non-fatal 60-- errors and disabling style-related ones 61 62defaultWarningSet :: String 63defaultWarningSet = "warn" 64 65defaultWarningMode :: WarningMode 66defaultWarningMode = WarningMode ws False where 67 ws = fst $ fromMaybe __IMPOSSIBLE__ $ lookup defaultWarningSet warningSets 68 69-- | Some warnings are errors and cannot be turned off. 70data WarningModeError = Unknown String | NoNoError String 71 72prettyWarningModeError :: WarningModeError -> String 73prettyWarningModeError = \case 74 Unknown str -> concat [ "Unknown warning flag: ", str, "." ] 75 NoNoError str -> concat [ "You may only turn off benign warnings. The warning " 76 , str 77 ," is a non-fatal error and thus cannot be ignored." ] 78 79-- | From user-given directives we compute WarningMode updates 80type WarningModeUpdate = WarningMode -> WarningMode 81 82-- | @warningModeUpdate str@ computes the action of @str@ over the current 83-- @WarningMode@: it may reset the set of warnings, add or remove a specific 84-- flag or demand that any warning be turned into an error 85 86warningModeUpdate :: String -> Either WarningModeError WarningModeUpdate 87warningModeUpdate str = case str of 88 "error" -> pure $ set warn2Error True 89 "noerror" -> pure $ set warn2Error False 90 _ | Just ws <- fst <$> lookup str warningSets 91 -> pure $ set warningSet ws 92 _ -> case stripPrefix "no" str of 93 Nothing -> do 94 wname <- maybe (Left (Unknown str)) Right (string2WarningName str) 95 pure (over warningSet $ Set.insert wname) 96 Just str' -> do 97 wname <- maybe (Left (Unknown str')) Right (string2WarningName str') 98 when (wname `elem` errorWarnings) (Left (NoNoError str')) 99 pure (over warningSet $ Set.delete wname) 100 101-- | Common sets of warnings 102 103warningSets :: [(String, (Set WarningName, String))] 104warningSets = [ ("all" , (allWarnings, "All of the existing warnings")) 105 , ("warn" , (usualWarnings, "Default warning level")) 106 , ("ignore", (errorWarnings, "Ignore all the benign warnings")) 107 ] 108 109noWarnings :: Set WarningName 110noWarnings = Set.empty 111 112unsolvedWarnings :: Set WarningName 113unsolvedWarnings = Set.fromList 114 [ UnsolvedMetaVariables_ 115 , UnsolvedInteractionMetas_ 116 , UnsolvedConstraints_ 117 ] 118 119incompleteMatchWarnings :: Set WarningName 120incompleteMatchWarnings = Set.fromList [ CoverageIssue_ ] 121 122errorWarnings :: Set WarningName 123errorWarnings = Set.fromList 124 [ CoverageIssue_ 125 , GenericNonFatalError_ 126 , MissingDefinitions_ 127 , NotAllowedInMutual_ 128 , NotStrictlyPositive_ 129 , OverlappingTokensWarning_ 130 , PragmaCompiled_ 131 , SafeFlagPostulate_ 132 , SafeFlagPragma_ 133 , SafeFlagNonTerminating_ 134 , SafeFlagTerminating_ 135 , SafeFlagWithoutKFlagPrimEraseEquality_ 136 , SafeFlagNoPositivityCheck_ 137 , SafeFlagPolarity_ 138 , SafeFlagNoUniverseCheck_ 139 , SafeFlagEta_ 140 , SafeFlagInjective_ 141 , SafeFlagNoCoverageCheck_ 142 , TerminationIssue_ 143 , UnsolvedMetaVariables_ 144 , UnsolvedInteractionMetas_ 145 , UnsolvedConstraints_ 146 , InfectiveImport_ 147 , CoInfectiveImport_ 148 , RewriteNonConfluent_ 149 , RewriteMaybeNonConfluent_ 150 , RewriteAmbiguousRules_ 151 , RewriteMissingRule_ 152 , ExeNotFoundWarning_ 153 , ExeNotExecutableWarning_ 154 ] 155 156allWarnings :: Set WarningName 157allWarnings = Set.fromList [minBound..maxBound] 158 159usualWarnings :: Set WarningName 160usualWarnings = allWarnings Set.\\ Set.fromList 161 [ UnknownFixityInMixfixDecl_ 162 , CoverageNoExactSplit_ 163 , ShadowingInTelescope_ 164 ] 165 166-- | The @WarningName@ data enumeration is meant to have a one-to-one correspondance 167-- to existing warnings in the codebase. 168 169data WarningName 170 = 171 -- Parser Warnings 172 OverlappingTokensWarning_ 173 | UnsupportedAttribute_ 174 | MultipleAttributes_ 175 -- Library Warnings 176 | LibUnknownField_ 177 -- Nicifer Warnings 178 | EmptyAbstract_ 179 | EmptyConstructor_ 180 | EmptyField_ 181 | EmptyGeneralize_ 182 | EmptyInstance_ 183 | EmptyMacro_ 184 | EmptyMutual_ 185 | EmptyPostulate_ 186 | EmptyPrimitive_ 187 | EmptyPrivate_ 188 | EmptyRewritePragma_ 189 | EmptyWhere_ 190 | InvalidCatchallPragma_ 191 | InvalidConstructor_ 192 | InvalidConstructorBlock_ 193 | InvalidCoverageCheckPragma_ 194 | InvalidNoPositivityCheckPragma_ 195 | InvalidNoUniverseCheckPragma_ 196 | InvalidRecordDirective_ 197 | InvalidTerminationCheckPragma_ 198 | MissingDefinitions_ 199 | NotAllowedInMutual_ 200 | OpenPublicAbstract_ 201 | OpenPublicPrivate_ 202 | PolarityPragmasButNotPostulates_ 203 | PragmaCompiled_ 204 | PragmaNoTerminationCheck_ 205 | ShadowingInTelescope_ 206 | UnknownFixityInMixfixDecl_ 207 | UnknownNamesInFixityDecl_ 208 | UnknownNamesInPolarityPragmas_ 209 | UselessAbstract_ 210 | UselessInstance_ 211 | UselessPrivate_ 212 -- Scope and Type Checking Warnings 213 | AbsurdPatternRequiresNoRHS_ 214 | AsPatternShadowsConstructorOrPatternSynonym_ 215 | CantGeneralizeOverSorts_ 216 | ClashesViaRenaming_ -- issue #4154 217 | CoverageIssue_ 218 | CoverageNoExactSplit_ 219 | DeprecationWarning_ 220 | DuplicateUsing_ 221 | FixityInRenamingModule_ 222 | GenericNonFatalError_ 223 | GenericUseless_ 224 | GenericWarning_ 225 | IllformedAsClause_ 226 | InstanceArgWithExplicitArg_ 227 | InstanceWithExplicitArg_ 228 | InstanceNoOutputTypeName_ 229 | InversionDepthReached_ 230 | ModuleDoesntExport_ 231 | NoGuardednessFlag_ 232 | NotInScope_ 233 | NotStrictlyPositive_ 234 | OldBuiltin_ 235 | PragmaCompileErased_ 236 | RewriteMaybeNonConfluent_ 237 | RewriteNonConfluent_ 238 | RewriteAmbiguousRules_ 239 | RewriteMissingRule_ 240 | SafeFlagEta_ 241 | SafeFlagInjective_ 242 | SafeFlagNoCoverageCheck_ 243 | SafeFlagNonTerminating_ 244 | SafeFlagNoPositivityCheck_ 245 | SafeFlagNoUniverseCheck_ 246 | SafeFlagPolarity_ 247 | SafeFlagPostulate_ 248 | SafeFlagPragma_ 249 | SafeFlagTerminating_ 250 | SafeFlagWithoutKFlagPrimEraseEquality_ 251 | TerminationIssue_ 252 | UnreachableClauses_ 253 | UnsolvedConstraints_ 254 | UnsolvedInteractionMetas_ 255 | UnsolvedMetaVariables_ 256 | UselessHiding_ 257 | UselessInline_ 258 | UselessPatternDeclarationForRecord_ 259 | UselessPublic_ 260 | UserWarning_ 261 | WithoutKFlagPrimEraseEquality_ 262 | WrongInstanceDeclaration_ 263 -- Checking consistency of options 264 | CoInfectiveImport_ 265 | InfectiveImport_ 266 -- Record field warnings 267 | DuplicateFieldsWarning_ 268 | TooManyFieldsWarning_ 269 -- System call warnings 270 | ExeNotFoundWarning_ 271 | ExeNotExecutableWarning_ 272 deriving (Eq, Ord, Show, Read, Enum, Bounded, Generic) 273 274instance NFData WarningName 275 276-- | The flag corresponding to a warning is precisely the name of the constructor 277-- minus the trailing underscore. 278 279-- sorry 280string2WarningName :: String -> Maybe WarningName 281string2WarningName = readMaybe . (++ "_") 282 283warningName2String :: WarningName -> String 284warningName2String = initWithDefault __IMPOSSIBLE__ . show 285 286-- | @warningUsage@ generated using @warningNameDescription@ 287 288usageWarning :: String 289usageWarning = intercalate "\n" 290 [ "The -W or --warning option can be used to disable or enable\ 291 \ different warnings. The flag -W error (or --warning=error)\ 292 \ can be used to turn all warnings into errors, while -W noerror\ 293 \ turns this off again." 294 , "" 295 , "A group of warnings can be enabled by -W group, where group is\ 296 \ one of the following:" 297 , "" 298 , untable (fmap (fst &&& snd . snd) warningSets) 299 , "Individual benign warnings can be turned on and off by -W Name and\ 300 \ -W noName, respectively, where Name comes from the following\ 301 \ list (warnings marked with 'd' are turned on by default, and 'b'\ 302 \ stands for \"benign warning\"):" 303 , "" 304 , untable $ forMaybe [minBound..maxBound] $ \ w -> 305 let wnd = warningNameDescription w in 306 ( warningName2String w 307 , (if w `Set.member` usualWarnings then "d" else " ") ++ 308 (if not (w `Set.member` errorWarnings) then "b" else " ") ++ 309 " " ++ 310 wnd 311 ) <$ guard (not $ null wnd) 312 ] 313 314 where 315 316 untable :: [(String, String)] -> String 317 untable rows = 318 let len = maximum (map (length . fst) rows) in 319 unlines $ flip map rows $ \ (hdr, cnt) -> 320 concat [ hdr, replicate (1 + len - length hdr) ' ', cnt ] 321 322-- | @WarningName@ descriptions used for generating usage information 323-- Leave String empty to skip that name. 324 325warningNameDescription :: WarningName -> String 326warningNameDescription = \case 327 -- Parser Warnings 328 OverlappingTokensWarning_ -> "Multi-line comments spanning one or more literate text blocks." 329 UnsupportedAttribute_ -> "Unsupported attributes." 330 MultipleAttributes_ -> "Multiple attributes." 331 -- Library Warnings 332 LibUnknownField_ -> "Unknown field in library file." 333 -- Nicifer Warnings 334 EmptyAbstract_ -> "Empty `abstract' blocks." 335 EmptyConstructor_ -> "Empty `constructor' blocks." 336 EmptyField_ -> "Empty `field` blocks." 337 EmptyGeneralize_ -> "Empty `variable' blocks." 338 EmptyInstance_ -> "Empty `instance' blocks." 339 EmptyMacro_ -> "Empty `macro' blocks." 340 EmptyMutual_ -> "Empty `mutual' blocks." 341 EmptyPostulate_ -> "Empty `postulate' blocks." 342 EmptyPrimitive_ -> "Empty `primitive' blocks." 343 EmptyPrivate_ -> "Empty `private' blocks." 344 EmptyRewritePragma_ -> "Empty `REWRITE' pragmas." 345 EmptyWhere_ -> "Empty `where' blocks." 346 InvalidCatchallPragma_ -> "`CATCHALL' pragmas before a non-function clause." 347 InvalidConstructor_ -> "`constructor' blocks may only contain type signatures for constructors." 348 InvalidConstructorBlock_ -> "No `constructor' blocks outside of `interleaved mutual' blocks." 349 InvalidCoverageCheckPragma_ -> "Coverage checking pragmas before non-function or `mutual' blocks." 350 InvalidNoPositivityCheckPragma_ -> "No positivity checking pragmas before non-`data', `record' or `mutual' blocks." 351 InvalidNoUniverseCheckPragma_ -> "No universe checking pragmas before non-`data' or `record' declaration." 352 InvalidRecordDirective_ -> "No record directive outside of record definition / below field declarations." 353 InvalidTerminationCheckPragma_ -> "Termination checking pragmas before non-function or `mutual' blocks." 354 MissingDefinitions_ -> "Declarations not associated to a definition." 355 NotAllowedInMutual_ -> "Declarations not allowed in a mutual block." 356 OpenPublicAbstract_ -> "'open public' directive in an 'abstract' block." 357 OpenPublicPrivate_ -> "'open public' directive in a 'private' block." 358 PolarityPragmasButNotPostulates_ -> "Polarity pragmas for non-postulates." 359 PragmaCompiled_ -> "'COMPILE' pragmas not allowed in safe mode." 360 PragmaNoTerminationCheck_ -> "`NO_TERMINATION_CHECK' pragmas are deprecated" 361 ShadowingInTelescope_ -> "Repeated variable name in telescope." 362 UnknownFixityInMixfixDecl_ -> "Mixfix names without an associated fixity declaration." 363 UnknownNamesInFixityDecl_ -> "Names not declared in the same scope as their syntax or fixity declaration." 364 UnknownNamesInPolarityPragmas_ -> "Names not declared in the same scope as their polarity pragmas." 365 UselessAbstract_ -> "`abstract' blocks where they have no effect." 366 UselessHiding_ -> "Names in `hiding' directive that are anyway not imported." 367 UselessInline_ -> "`INLINE' pragmas where they have no effect." 368 UselessInstance_ -> "`instance' blocks where they have no effect." 369 UselessPrivate_ -> "`private' blocks where they have no effect." 370 UselessPublic_ -> "`public' blocks where they have no effect." 371 UselessPatternDeclarationForRecord_ -> "`pattern' attributes where they have no effect." 372 -- Scope and Type Checking Warnings 373 AbsurdPatternRequiresNoRHS_ -> "A clause with an absurd pattern does not need a Right Hand Side." 374 AsPatternShadowsConstructorOrPatternSynonym_ -> "@-patterns that shadow constructors or pattern synonyms." 375 CantGeneralizeOverSorts_ -> "Attempt to generalize over sort metas in 'variable' declaration." 376 ClashesViaRenaming_ -> "Clashes introduced by `renaming'." -- issue #4154 377 CoverageIssue_ -> "Failed coverage checks." 378 CoverageNoExactSplit_ -> "Failed exact split checks." 379 DeprecationWarning_ -> "Feature deprecation." 380 GenericNonFatalError_ -> "" 381 GenericUseless_ -> "Useless code." 382 GenericWarning_ -> "" 383 IllformedAsClause_ -> "Illformed `as'-clauses in `import' statements." 384 InstanceNoOutputTypeName_ -> "instance arguments whose type does not end in a named or variable type are never considered by instance search." 385 InstanceArgWithExplicitArg_ -> "instance arguments with explicit arguments are never considered by instance search." 386 InstanceWithExplicitArg_ -> "`instance` declarations with explicit arguments are never considered by instance search." 387 InversionDepthReached_ -> "Inversions of pattern-matching failed due to exhausted inversion depth." 388 NoGuardednessFlag_ -> "Coinductive record but no --guardedness flag." 389 ModuleDoesntExport_ -> "Imported name is not actually exported." 390 DuplicateUsing_ -> "Repeated names in using directive." 391 FixityInRenamingModule_ -> "Found fixity annotation in renaming directive for module." 392 NotInScope_ -> "Out of scope name." 393 NotStrictlyPositive_ -> "Failed strict positivity checks." 394 OldBuiltin_ -> "Deprecated `BUILTIN' pragmas." 395 PragmaCompileErased_ -> "`COMPILE' pragma targeting an erased symbol." 396 RewriteMaybeNonConfluent_ -> "Failed local confluence check while computing overlap." 397 RewriteNonConfluent_ -> "Failed local confluence check while joining critical pairs." 398 RewriteAmbiguousRules_ -> "Failed global confluence check because of overlapping rules." 399 RewriteMissingRule_ -> "Failed global confluence check because of missing rule." 400 SafeFlagEta_ -> "`ETA' pragmas with the safe flag." 401 SafeFlagInjective_ -> "`INJECTIVE' pragmas with the safe flag." 402 SafeFlagNoCoverageCheck_ -> "`NON_COVERING` pragmas with the safe flag." 403 SafeFlagNonTerminating_ -> "`NON_TERMINATING' pragmas with the safe flag." 404 SafeFlagNoPositivityCheck_ -> "`NO_POSITIVITY_CHECK' pragmas with the safe flag." 405 SafeFlagNoUniverseCheck_ -> "`NO_UNIVERSE_CHECK' pragmas with the safe flag." 406 SafeFlagPolarity_ -> "`POLARITY' pragmas with the safe flag." 407 SafeFlagPostulate_ -> "`postulate' blocks with the safe flag." 408 SafeFlagPragma_ -> "Unsafe `OPTIONS' pragmas with the safe flag." 409 SafeFlagTerminating_ -> "`TERMINATING' pragmas with the safe flag." 410 SafeFlagWithoutKFlagPrimEraseEquality_ -> "`primEraseEquality' used with the safe and without-K flags." 411 TerminationIssue_ -> "Failed termination checks." 412 UnreachableClauses_ -> "Unreachable function clauses." 413 UnsolvedConstraints_ -> "Unsolved constraints." 414 UnsolvedInteractionMetas_ -> "Unsolved interaction meta variables." 415 UnsolvedMetaVariables_ -> "Unsolved meta variables." 416 UserWarning_ -> "User-defined warning added using one of the 'WARNING_ON_*' pragmas." 417 WithoutKFlagPrimEraseEquality_ -> "`primEraseEquality' usages with the without-K flags." 418 WrongInstanceDeclaration_ -> "Terms marked as eligible for instance search should end with a name." 419 -- Checking consistency of options 420 CoInfectiveImport_ -> "Importing a file not using e.g. `--safe' from one which does." 421 InfectiveImport_ -> "Importing a file using e.g. `--cubical' into one which doesn't." 422 -- Record field warnings 423 DuplicateFieldsWarning_ -> "Record expression with duplicate field names." 424 TooManyFieldsWarning_ -> "Record expression with invalid field names." 425 -- System call warnings 426 ExeNotFoundWarning_ -> "Trusted executable cannot be found." 427 ExeNotExecutableWarning_ -> "Trusted executable does not have permission to execute." 428