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