module Agda.Interaction.Options.Warnings
       (
         WarningMode (..)
       , warningSet
       , warn2Error
       , lensSingleWarning
       , defaultWarningSet
       , allWarnings
       , usualWarnings
       , noWarnings
       , unsolvedWarnings
       , incompleteMatchWarnings
       , errorWarnings
       , exactSplitWarnings
       , defaultWarningMode
       , WarningModeError(..)
       , prettyWarningModeError
       , warningModeUpdate
       , warningSets
       , WarningName (..)
       , warningName2String
       , string2WarningName
       , usageWarning
       )
where

import Control.Arrow ( (&&&) )
import Control.DeepSeq
import Control.Monad ( guard, when )

import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.HashMap.Strict as HMap
import Data.List ( stripPrefix, intercalate, partition, sort )

import GHC.Generics (Generic)

import Agda.Utils.Either ( maybeToEither )
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe

import Agda.Utils.Impossible


-- | A @WarningMode@ has two components: a set of warnings to be displayed
-- and a flag stating whether warnings should be turned into fatal errors.
data WarningMode = WarningMode
  { WarningMode -> Set WarningName
_warningSet :: Set WarningName
  , WarningMode -> Bool
_warn2Error :: Bool
  } deriving (WarningMode -> WarningMode -> Bool
(WarningMode -> WarningMode -> Bool)
-> (WarningMode -> WarningMode -> Bool) -> Eq WarningMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: WarningMode -> WarningMode -> Bool
== :: WarningMode -> WarningMode -> Bool
$c/= :: WarningMode -> WarningMode -> Bool
/= :: WarningMode -> WarningMode -> Bool
Eq, Int -> WarningMode -> ShowS
[WarningMode] -> ShowS
WarningMode -> String
(Int -> WarningMode -> ShowS)
-> (WarningMode -> String)
-> ([WarningMode] -> ShowS)
-> Show WarningMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WarningMode -> ShowS
showsPrec :: Int -> WarningMode -> ShowS
$cshow :: WarningMode -> String
show :: WarningMode -> String
$cshowList :: [WarningMode] -> ShowS
showList :: [WarningMode] -> ShowS
Show, (forall x. WarningMode -> Rep WarningMode x)
-> (forall x. Rep WarningMode x -> WarningMode)
-> Generic WarningMode
forall x. Rep WarningMode x -> WarningMode
forall x. WarningMode -> Rep WarningMode x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. WarningMode -> Rep WarningMode x
from :: forall x. WarningMode -> Rep WarningMode x
$cto :: forall x. Rep WarningMode x -> WarningMode
to :: forall x. Rep WarningMode x -> WarningMode
Generic)

instance NFData WarningMode

-- Lenses

warningSet :: Lens' WarningMode (Set WarningName)
warningSet :: Lens' WarningMode (Set WarningName)
warningSet Set WarningName -> f (Set WarningName)
f WarningMode
o = (\ Set WarningName
ws -> WarningMode
o { _warningSet = ws }) (Set WarningName -> WarningMode)
-> f (Set WarningName) -> f WarningMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set WarningName -> f (Set WarningName)
f (WarningMode -> Set WarningName
_warningSet WarningMode
o)

warn2Error :: Lens' WarningMode Bool
warn2Error :: Lens' WarningMode Bool
warn2Error Bool -> f Bool
f WarningMode
o = (\ Bool
ws -> WarningMode
o { _warn2Error = ws }) (Bool -> WarningMode) -> f Bool -> f WarningMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> f Bool
f (WarningMode -> Bool
_warn2Error WarningMode
o)

lensSingleWarning :: WarningName -> Lens' WarningMode Bool
lensSingleWarning :: WarningName -> Lens' WarningMode Bool
lensSingleWarning WarningName
w = (Set WarningName -> f (Set WarningName))
-> WarningMode -> f WarningMode
Lens' WarningMode (Set WarningName)
warningSet ((Set WarningName -> f (Set WarningName))
 -> WarningMode -> f WarningMode)
-> ((Bool -> f Bool) -> Set WarningName -> f (Set WarningName))
-> (Bool -> f Bool)
-> WarningMode
-> f WarningMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WarningName -> Lens' (Set WarningName) Bool
forall k. Ord k => k -> Lens' (Set k) Bool
contains WarningName
w

-- | The @defaultWarningMode@ is a curated set of warnings covering non-fatal
-- errors and disabling style-related ones

defaultWarningSet :: String
defaultWarningSet :: String
defaultWarningSet = String
"warn"

defaultWarningMode :: WarningMode
defaultWarningMode :: WarningMode
defaultWarningMode = Set WarningName -> Bool -> WarningMode
WarningMode Set WarningName
ws Bool
False where
  ws :: Set WarningName
ws = (Set WarningName, String) -> Set WarningName
forall a b. (a, b) -> a
fst ((Set WarningName, String) -> Set WarningName)
-> (Set WarningName, String) -> Set WarningName
forall a b. (a -> b) -> a -> b
$ (Set WarningName, String)
-> Maybe (Set WarningName, String) -> (Set WarningName, String)
forall a. a -> Maybe a -> a
fromMaybe (Set WarningName, String)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Set WarningName, String) -> (Set WarningName, String))
-> Maybe (Set WarningName, String) -> (Set WarningName, String)
forall a b. (a -> b) -> a -> b
$ String
-> [(String, (Set WarningName, String))]
-> Maybe (Set WarningName, String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
defaultWarningSet [(String, (Set WarningName, String))]
warningSets

-- | Some warnings are errors and cannot be turned off.
data WarningModeError = Unknown String | NoNoError String

prettyWarningModeError :: WarningModeError -> String
prettyWarningModeError :: WarningModeError -> String
prettyWarningModeError = \case
  Unknown String
str -> [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
"Unknown warning flag: ", String
str, String
"." ]
  NoNoError String
str -> [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
"You may only turn off benign warnings. The warning "
                          , String
str
                          ,String
" is a non-fatal error and thus cannot be ignored." ]

-- | From user-given directives we compute WarningMode updates
type WarningModeUpdate = WarningMode -> WarningMode

-- | @warningModeUpdate str@ computes the action of @str@ over the current
-- @WarningMode@: it may reset the set of warnings, add or remove a specific
-- flag or demand that any warning be turned into an error

warningModeUpdate :: String -> Either WarningModeError WarningModeUpdate
warningModeUpdate :: String -> Either WarningModeError WarningModeUpdate
warningModeUpdate String
str = case String
str of
  String
"error"   -> WarningModeUpdate -> Either WarningModeError WarningModeUpdate
forall a. a -> Either WarningModeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WarningModeUpdate -> Either WarningModeError WarningModeUpdate)
-> WarningModeUpdate -> Either WarningModeError WarningModeUpdate
forall a b. (a -> b) -> a -> b
$ Lens' WarningMode Bool -> LensSet WarningMode Bool
forall o i. Lens' o i -> LensSet o i
set (Bool -> f Bool) -> WarningMode -> f WarningMode
Lens' WarningMode Bool
warn2Error Bool
True
  String
"noerror" -> WarningModeUpdate -> Either WarningModeError WarningModeUpdate
forall a. a -> Either WarningModeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WarningModeUpdate -> Either WarningModeError WarningModeUpdate)
-> WarningModeUpdate -> Either WarningModeError WarningModeUpdate
forall a b. (a -> b) -> a -> b
$ Lens' WarningMode Bool -> LensSet WarningMode Bool
forall o i. Lens' o i -> LensSet o i
set (Bool -> f Bool) -> WarningMode -> f WarningMode
Lens' WarningMode Bool
warn2Error Bool
False
  String
_ | Just Set WarningName
ws <- (Set WarningName, String) -> Set WarningName
forall a b. (a, b) -> a
fst ((Set WarningName, String) -> Set WarningName)
-> Maybe (Set WarningName, String) -> Maybe (Set WarningName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> [(String, (Set WarningName, String))]
-> Maybe (Set WarningName, String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
str [(String, (Set WarningName, String))]
warningSets
            -> WarningModeUpdate -> Either WarningModeError WarningModeUpdate
forall a. a -> Either WarningModeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WarningModeUpdate -> Either WarningModeError WarningModeUpdate)
-> WarningModeUpdate -> Either WarningModeError WarningModeUpdate
forall a b. (a -> b) -> a -> b
$ Lens' WarningMode (Set WarningName)
-> LensSet WarningMode (Set WarningName)
forall o i. Lens' o i -> LensSet o i
set (Set WarningName -> f (Set WarningName))
-> WarningMode -> f WarningMode
Lens' WarningMode (Set WarningName)
warningSet Set WarningName
ws
  String
_ -> case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix String
"no" String
str of
    Maybe String
Nothing   -> do
      WarningName
wname :: WarningName <- WarningModeError
-> Maybe WarningName -> Either WarningModeError WarningName
forall e a. e -> Maybe a -> Either e a
maybeToEither (String -> WarningModeError
Unknown String
str) (Maybe WarningName -> Either WarningModeError WarningName)
-> Maybe WarningName -> Either WarningModeError WarningName
forall a b. (a -> b) -> a -> b
$ String -> Maybe WarningName
string2WarningName String
str
      WarningModeUpdate -> Either WarningModeError WarningModeUpdate
forall a. a -> Either WarningModeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Lens' WarningMode (Set WarningName)
-> LensMap WarningMode (Set WarningName)
forall o i. Lens' o i -> LensMap o i
over (Set WarningName -> f (Set WarningName))
-> WarningMode -> f WarningMode
Lens' WarningMode (Set WarningName)
warningSet LensMap WarningMode (Set WarningName)
-> LensMap WarningMode (Set WarningName)
forall a b. (a -> b) -> a -> b
$ WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => a -> Set a -> Set a
Set.insert WarningName
wname)
    Just String
str' -> do
      WarningName
wname :: WarningName <- WarningModeError
-> Maybe WarningName -> Either WarningModeError WarningName
forall e a. e -> Maybe a -> Either e a
maybeToEither (String -> WarningModeError
Unknown String
str') (Maybe WarningName -> Either WarningModeError WarningName)
-> Maybe WarningName -> Either WarningModeError WarningName
forall a b. (a -> b) -> a -> b
$ String -> Maybe WarningName
string2WarningName String
str'
      Bool -> Either WarningModeError () -> Either WarningModeError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (WarningName
wname WarningName -> Set WarningName -> Bool
forall a. Eq a => a -> Set a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set WarningName
errorWarnings) (WarningModeError -> Either WarningModeError ()
forall a b. a -> Either a b
Left (String -> WarningModeError
NoNoError String
str'))
      WarningModeUpdate -> Either WarningModeError WarningModeUpdate
forall a. a -> Either WarningModeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Lens' WarningMode (Set WarningName)
-> LensMap WarningMode (Set WarningName)
forall o i. Lens' o i -> LensMap o i
over (Set WarningName -> f (Set WarningName))
-> WarningMode -> f WarningMode
Lens' WarningMode (Set WarningName)
warningSet LensMap WarningMode (Set WarningName)
-> LensMap WarningMode (Set WarningName)
forall a b. (a -> b) -> a -> b
$ WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => a -> Set a -> Set a
Set.delete WarningName
wname)

-- | Common sets of warnings

warningSets :: [(String, (Set WarningName, String))]
warningSets :: [(String, (Set WarningName, String))]
warningSets = [ (String
"all"   , (Set WarningName
allWarnings, String
"All of the existing warnings"))
              , (String
"warn"  , (Set WarningName
usualWarnings, String
"Default warning level"))
              , (String
"ignore", (Set WarningName
errorWarnings, String
"Ignore all the benign warnings"))
              ]

noWarnings :: Set WarningName
noWarnings :: Set WarningName
noWarnings = Set WarningName
forall a. Set a
Set.empty

unsolvedWarnings :: Set WarningName
unsolvedWarnings :: Set WarningName
unsolvedWarnings = [WarningName] -> Set WarningName
forall a. Ord a => [a] -> Set a
Set.fromList
                 [ WarningName
UnsolvedMetaVariables_
                 , WarningName
UnsolvedInteractionMetas_
                 , WarningName
UnsolvedConstraints_
                 ]

incompleteMatchWarnings :: Set WarningName
incompleteMatchWarnings :: Set WarningName
incompleteMatchWarnings = [WarningName] -> Set WarningName
forall a. Ord a => [a] -> Set a
Set.fromList [ WarningName
CoverageIssue_ ]

errorWarnings :: Set WarningName
errorWarnings :: Set WarningName
errorWarnings = [WarningName] -> Set WarningName
forall a. Ord a => [a] -> Set a
Set.fromList
  [ WarningName
CoverageIssue_
  , WarningName
InvalidCharacterLiteral_
  , WarningName
MissingDefinitions_
  , WarningName
MissingDeclarations_
  , WarningName
NotAllowedInMutual_
  , WarningName
NotStrictlyPositive_
  , WarningName
OverlappingTokensWarning_
  , WarningName
PragmaCompiled_
  , WarningName
SafeFlagPostulate_
  , WarningName
SafeFlagPragma_
  , WarningName
SafeFlagNonTerminating_
  , WarningName
SafeFlagTerminating_
  , WarningName
SafeFlagWithoutKFlagPrimEraseEquality_
  , WarningName
SafeFlagNoPositivityCheck_
  , WarningName
SafeFlagPolarity_
  , WarningName
SafeFlagNoUniverseCheck_
  , WarningName
SafeFlagEta_
  , WarningName
SafeFlagInjective_
  , WarningName
SafeFlagNoCoverageCheck_
  , WarningName
TerminationIssue_
  , WarningName
UnsolvedMetaVariables_
  , WarningName
UnsolvedInteractionMetas_
  , WarningName
UnsolvedConstraints_
  , WarningName
InfectiveImport_
  , WarningName
CoInfectiveImport_
  , WarningName
RewriteNonConfluent_
  , WarningName
RewriteMaybeNonConfluent_
  , WarningName
RewriteAmbiguousRules_
  , WarningName
RewriteMissingRule_
  ]

allWarnings :: Set WarningName
allWarnings :: Set WarningName
allWarnings = [WarningName] -> Set WarningName
forall a. Ord a => [a] -> Set a
Set.fromList [WarningName
forall a. Bounded a => a
minBound..WarningName
forall a. Bounded a => a
maxBound]

usualWarnings :: Set WarningName
usualWarnings :: Set WarningName
usualWarnings =
  Set WarningName
allWarnings Set WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set WarningName
exactSplitWarnings Set WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ [WarningName] -> Set WarningName
forall a. Ord a => [a] -> Set a
Set.fromList
    [ WarningName
UnknownFixityInMixfixDecl_
    , WarningName
ShadowingInTelescope_
    ]

-- | Warnings enabled by @--exact-split@.
--
exactSplitWarnings :: Set WarningName
exactSplitWarnings :: Set WarningName
exactSplitWarnings = [WarningName] -> Set WarningName
forall a. Ord a => [a] -> Set a
Set.fromList
  [ WarningName
CoverageNoExactSplit_
  , WarningName
InlineNoExactSplit_
  ]

-- | The @WarningName@ data enumeration is meant to have a one-to-one correspondance
-- to existing warnings in the codebase.

data WarningName
  -- Option Warnings
  = OptionRenamed_
  -- Parser Warnings
  | OverlappingTokensWarning_
  | UnsupportedAttribute_
  | MultipleAttributes_
  -- Library Warnings
  | LibUnknownField_
  -- Nicifer Warnings
  | EmptyAbstract_
  | EmptyConstructor_
  | EmptyField_
  | EmptyGeneralize_
  | EmptyInstance_
  | EmptyMacro_
  | EmptyMutual_
  | EmptyPostulate_
  | EmptyPrimitive_
  | EmptyPrivate_
  | EmptyRewritePragma_
  | EmptyWhere_
  | HiddenGeneralize_
  | InvalidCatchallPragma_
  | InvalidConstructor_
  | InvalidConstructorBlock_
  | InvalidCoverageCheckPragma_
  | InvalidNoPositivityCheckPragma_
  | InvalidNoUniverseCheckPragma_
  | InvalidRecordDirective_
  | InvalidTerminationCheckPragma_
  | MissingDeclarations_
  | MissingDefinitions_
  | NotAllowedInMutual_
  | OpenPublicAbstract_
  | OpenPublicPrivate_
  | PolarityPragmasButNotPostulates_
  | PragmaCompiled_
  | PragmaNoTerminationCheck_
  | ShadowingInTelescope_
  | UnknownFixityInMixfixDecl_
  | UnknownNamesInFixityDecl_
  | UnknownNamesInPolarityPragmas_
  | UselessAbstract_
  | UselessInstance_
  | UselessPrivate_
  -- Scope and Type Checking Warnings
  | AbsurdPatternRequiresNoRHS_
  | AsPatternShadowsConstructorOrPatternSynonym_
  | PatternShadowsConstructor_
  | CantGeneralizeOverSorts_
  | ClashesViaRenaming_                -- issue #4154
  | CoverageIssue_
  | CoverageNoExactSplit_
  | InlineNoExactSplit_
  | DeprecationWarning_
  | DuplicateUsing_
  | FixityInRenamingModule_
  | InvalidCharacterLiteral_
  | UselessPragma_
  | GenericWarning_
  | IllformedAsClause_
  | InstanceArgWithExplicitArg_
  | InstanceWithExplicitArg_
  | InstanceNoOutputTypeName_
  | InteractionMetaBoundaries_
  | InversionDepthReached_
  | ModuleDoesntExport_
  | NoGuardednessFlag_
  | NotInScope_
  | NotStrictlyPositive_
  | UnsupportedIndexedMatch_
  | OldBuiltin_
  | PlentyInHardCompileTimeMode_
  | PragmaCompileErased_
  | RewriteMaybeNonConfluent_
  | RewriteNonConfluent_
  | RewriteAmbiguousRules_
  | RewriteMissingRule_
  | SafeFlagEta_
  | SafeFlagInjective_
  | SafeFlagNoCoverageCheck_
  | SafeFlagNonTerminating_
  | SafeFlagNoPositivityCheck_
  | SafeFlagNoUniverseCheck_
  | SafeFlagPolarity_
  | SafeFlagPostulate_
  | SafeFlagPragma_
  | SafeFlagTerminating_
  | SafeFlagWithoutKFlagPrimEraseEquality_
  | TerminationIssue_
  | UnreachableClauses_
  | UnsolvedConstraints_
  | UnsolvedInteractionMetas_
  | UnsolvedMetaVariables_
  | UselessHiding_
  | UselessInline_
  | UselessPatternDeclarationForRecord_
  | UselessPublic_
  | UserWarning_
  | WithoutKFlagPrimEraseEquality_
  | WrongInstanceDeclaration_
  -- Checking consistency of options
  | CoInfectiveImport_
  | InfectiveImport_
  -- Record field warnings
  | DuplicateFields_
  | TooManyFields_
  -- Opaque/unfolding
  | NotAffectedByOpaque_
  | UnfoldTransparentName_
  | UselessOpaque_
  -- Cubical
  | FaceConstraintCannotBeHidden_
  | FaceConstraintCannotBeNamed_
  deriving (WarningName -> WarningName -> Bool
(WarningName -> WarningName -> Bool)
-> (WarningName -> WarningName -> Bool) -> Eq WarningName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: WarningName -> WarningName -> Bool
== :: WarningName -> WarningName -> Bool
$c/= :: WarningName -> WarningName -> Bool
/= :: WarningName -> WarningName -> Bool
Eq, Eq WarningName
Eq WarningName =>
(WarningName -> WarningName -> Ordering)
-> (WarningName -> WarningName -> Bool)
-> (WarningName -> WarningName -> Bool)
-> (WarningName -> WarningName -> Bool)
-> (WarningName -> WarningName -> Bool)
-> (WarningName -> WarningName -> WarningName)
-> (WarningName -> WarningName -> WarningName)
-> Ord WarningName
WarningName -> WarningName -> Bool
WarningName -> WarningName -> Ordering
WarningName -> WarningName -> WarningName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: WarningName -> WarningName -> Ordering
compare :: WarningName -> WarningName -> Ordering
$c< :: WarningName -> WarningName -> Bool
< :: WarningName -> WarningName -> Bool
$c<= :: WarningName -> WarningName -> Bool
<= :: WarningName -> WarningName -> Bool
$c> :: WarningName -> WarningName -> Bool
> :: WarningName -> WarningName -> Bool
$c>= :: WarningName -> WarningName -> Bool
>= :: WarningName -> WarningName -> Bool
$cmax :: WarningName -> WarningName -> WarningName
max :: WarningName -> WarningName -> WarningName
$cmin :: WarningName -> WarningName -> WarningName
min :: WarningName -> WarningName -> WarningName
Ord, Int -> WarningName -> ShowS
[WarningName] -> ShowS
WarningName -> String
(Int -> WarningName -> ShowS)
-> (WarningName -> String)
-> ([WarningName] -> ShowS)
-> Show WarningName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WarningName -> ShowS
showsPrec :: Int -> WarningName -> ShowS
$cshow :: WarningName -> String
show :: WarningName -> String
$cshowList :: [WarningName] -> ShowS
showList :: [WarningName] -> ShowS
Show, ReadPrec [WarningName]
ReadPrec WarningName
Int -> ReadS WarningName
ReadS [WarningName]
(Int -> ReadS WarningName)
-> ReadS [WarningName]
-> ReadPrec WarningName
-> ReadPrec [WarningName]
-> Read WarningName
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS WarningName
readsPrec :: Int -> ReadS WarningName
$creadList :: ReadS [WarningName]
readList :: ReadS [WarningName]
$creadPrec :: ReadPrec WarningName
readPrec :: ReadPrec WarningName
$creadListPrec :: ReadPrec [WarningName]
readListPrec :: ReadPrec [WarningName]
Read, Int -> WarningName
WarningName -> Int
WarningName -> [WarningName]
WarningName -> WarningName
WarningName -> WarningName -> [WarningName]
WarningName -> WarningName -> WarningName -> [WarningName]
(WarningName -> WarningName)
-> (WarningName -> WarningName)
-> (Int -> WarningName)
-> (WarningName -> Int)
-> (WarningName -> [WarningName])
-> (WarningName -> WarningName -> [WarningName])
-> (WarningName -> WarningName -> [WarningName])
-> (WarningName -> WarningName -> WarningName -> [WarningName])
-> Enum WarningName
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: WarningName -> WarningName
succ :: WarningName -> WarningName
$cpred :: WarningName -> WarningName
pred :: WarningName -> WarningName
$ctoEnum :: Int -> WarningName
toEnum :: Int -> WarningName
$cfromEnum :: WarningName -> Int
fromEnum :: WarningName -> Int
$cenumFrom :: WarningName -> [WarningName]
enumFrom :: WarningName -> [WarningName]
$cenumFromThen :: WarningName -> WarningName -> [WarningName]
enumFromThen :: WarningName -> WarningName -> [WarningName]
$cenumFromTo :: WarningName -> WarningName -> [WarningName]
enumFromTo :: WarningName -> WarningName -> [WarningName]
$cenumFromThenTo :: WarningName -> WarningName -> WarningName -> [WarningName]
enumFromThenTo :: WarningName -> WarningName -> WarningName -> [WarningName]
Enum, WarningName
WarningName -> WarningName -> Bounded WarningName
forall a. a -> a -> Bounded a
$cminBound :: WarningName
minBound :: WarningName
$cmaxBound :: WarningName
maxBound :: WarningName
Bounded, (forall x. WarningName -> Rep WarningName x)
-> (forall x. Rep WarningName x -> WarningName)
-> Generic WarningName
forall x. Rep WarningName x -> WarningName
forall x. WarningName -> Rep WarningName x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. WarningName -> Rep WarningName x
from :: forall x. WarningName -> Rep WarningName x
$cto :: forall x. Rep WarningName x -> WarningName
to :: forall x. Rep WarningName x -> WarningName
Generic)

instance NFData WarningName

-- | The flag corresponding to a warning is precisely the name of the constructor
-- minus the trailing underscore.

string2WarningName :: String -> Maybe WarningName
string2WarningName :: String -> Maybe WarningName
string2WarningName = (String -> HashMap String WarningName -> Maybe WarningName
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
`HMap.lookup` HashMap String WarningName
warnings) where
  warnings :: HashMap String WarningName
warnings = [(String, WarningName)] -> HashMap String WarningName
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HMap.fromList ([(String, WarningName)] -> HashMap String WarningName)
-> [(String, WarningName)] -> HashMap String WarningName
forall a b. (a -> b) -> a -> b
$ (WarningName -> (String, WarningName))
-> [WarningName] -> [(String, WarningName)]
forall a b. (a -> b) -> [a] -> [b]
map (\WarningName
x -> (WarningName -> String
warningName2String WarningName
x, WarningName
x)) [WarningName
forall a. Bounded a => a
minBound..WarningName
forall a. Bounded a => a
maxBound]

warningName2String :: WarningName -> String
warningName2String :: WarningName -> String
warningName2String = String -> ShowS
forall a. [a] -> [a] -> [a]
initWithDefault String
forall a. HasCallStack => a
__IMPOSSIBLE__ ShowS -> (WarningName -> String) -> WarningName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WarningName -> String
forall a. Show a => a -> String
show

-- | @warningUsage@ generated using @warningNameDescription@

usageWarning :: String
usageWarning :: String
usageWarning = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n"
  [ String
"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."
  , String
""
  , String
"A group of warnings can be enabled by -W group, where group is\
    \ one of the following:"
  , String
""
  , [(String, String)] -> String
untable (((String, (Set WarningName, String)) -> (String, String))
-> [(String, (Set WarningName, String))] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((String, (Set WarningName, String)) -> String
forall a b. (a, b) -> a
fst ((String, (Set WarningName, String)) -> String)
-> ((String, (Set WarningName, String)) -> String)
-> (String, (Set WarningName, String))
-> (String, String)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (Set WarningName, String) -> String
forall a b. (a, b) -> b
snd ((Set WarningName, String) -> String)
-> ((String, (Set WarningName, String))
    -> (Set WarningName, String))
-> (String, (Set WarningName, String))
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, (Set WarningName, String)) -> (Set WarningName, String)
forall a b. (a, b) -> b
snd) [(String, (Set WarningName, String))]
warningSets)

  , String
"Individual benign warnings can be turned on and off by -W Name and\
    \ -W noName, respectively, where Name comes from the following\
    \ list (warnings marked with 'd' are turned on by default):"
  , String
""
  , Bool -> [WarningName] -> String
forall {b}. IsBool b => b -> [WarningName] -> String
warningTable Bool
True [WarningName]
benign

  , String
"Error warnings are always on and cannot be turned off:"
  , String
""
  , Bool -> [WarningName] -> String
forall {b}. IsBool b => b -> [WarningName] -> String
warningTable Bool
False [WarningName]
severe
  ]

  where

    ([WarningName]
severe, [WarningName]
benign) = (WarningName -> Bool)
-> [WarningName] -> ([WarningName], [WarningName])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (WarningName -> Set WarningName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set WarningName
errorWarnings) [WarningName
forall a. Bounded a => a
minBound..WarningName
forall a. Bounded a => a
maxBound]

    warningTable :: b -> [WarningName] -> String
warningTable b
printD [WarningName]
ws =
      [(String, String)] -> String
untable ([(String, String)] -> String) -> [(String, String)] -> String
forall a b. (a -> b) -> a -> b
$ [WarningName]
-> (WarningName -> Maybe (String, String)) -> [(String, String)]
forall a b. [a] -> (a -> Maybe b) -> [b]
forMaybe [WarningName]
ws ((WarningName -> Maybe (String, String)) -> [(String, String)])
-> (WarningName -> Maybe (String, String)) -> [(String, String)]
forall a b. (a -> b) -> a -> b
$ \ WarningName
w ->
        let wnd :: String
wnd = WarningName -> String
warningNameDescription WarningName
w in
        ( WarningName -> String
warningName2String WarningName
w
        , b -> ShowS -> ShowS
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen b
printD ((if WarningName
w WarningName -> Set WarningName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set WarningName
usualWarnings then String
"d" else String
" ") String -> ShowS
forall a. [a] -> [a] -> [a]
++)
          String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++
          String
wnd
        ) (String, String) -> Maybe () -> Maybe (String, String)
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
wnd)

    untable :: [(String, String)] -> String
    untable :: [(String, String)] -> String
untable [(String, String)]
rows =
      let len :: Int
len = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (((String, String) -> Int) -> [(String, String)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int)
-> ((String, String) -> String) -> (String, String) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, String) -> String
forall a b. (a, b) -> a
fst) [(String, String)]
rows) in
      [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [(String, String)] -> ((String, String) -> String) -> [String]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for ([(String, String)] -> [(String, String)]
forall a. Ord a => [a] -> [a]
sort [(String, String)]
rows) (((String, String) -> String) -> [String])
-> ((String, String) -> String) -> [String]
forall a b. (a -> b) -> a -> b
$ \ (String
hdr, String
cnt) ->
        [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
hdr, Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
hdr) Char
' ', String
cnt ]


-- | @WarningName@ descriptions used for generating usage information
-- Leave String empty to skip that name.
--
-- The description should be a completion of the sentence "This warning is about ...".
-- So, typically the subject is in plural.
--
warningNameDescription :: WarningName -> String
warningNameDescription :: WarningName -> String
warningNameDescription = \case
  -- Option Warnings
  WarningName
OptionRenamed_                   -> String
"Renamed options."
  -- Parser Warnings
  WarningName
OverlappingTokensWarning_        -> String
"Multi-line comments spanning one or more literate text blocks."
  WarningName
UnsupportedAttribute_            -> String
"Unsupported attributes."
  WarningName
MultipleAttributes_              -> String
"Multiple attributes."
  -- Library Warnings
  WarningName
LibUnknownField_                 -> String
"Unknown fields in library files."
  -- Nicifer Warnings
  WarningName
EmptyAbstract_                   -> String
"Empty `abstract' blocks."
  WarningName
EmptyConstructor_                -> String
"Empty `constructor' blocks."
  WarningName
EmptyField_                      -> String
"Empty `field` blocks."
  WarningName
EmptyGeneralize_                 -> String
"Empty `variable' blocks."
  WarningName
EmptyInstance_                   -> String
"Empty `instance' blocks."
  WarningName
EmptyMacro_                      -> String
"Empty `macro' blocks."
  WarningName
EmptyMutual_                     -> String
"Empty `mutual' blocks."
  WarningName
EmptyPostulate_                  -> String
"Empty `postulate' blocks."
  WarningName
EmptyPrimitive_                  -> String
"Empty `primitive' blocks."
  WarningName
EmptyPrivate_                    -> String
"Empty `private' blocks."
  WarningName
EmptyRewritePragma_              -> String
"Empty `REWRITE' pragmas."
  WarningName
EmptyWhere_                      -> String
"Empty `where' blocks."
  WarningName
HiddenGeneralize_                -> String
"Hidden identifiers in variable blocks."
  WarningName
InvalidCatchallPragma_           -> String
"`CATCHALL' pragmas before a non-function clause."
  WarningName
InvalidConstructor_              -> String
"`constructor' blocks that contain declarations other than type signatures for constructors."
  WarningName
InvalidConstructorBlock_         -> String
"`constructor' blocks outside of `interleaved mutual' blocks."
  WarningName
InvalidCoverageCheckPragma_      -> String
"Coverage checking pragmas before non-function or `mutual' blocks."
  WarningName
InvalidNoPositivityCheckPragma_  -> String
"Positivity checking pragmas before non-`data', `record' or `mutual' blocks."
  WarningName
InvalidNoUniverseCheckPragma_    -> String
"Universe checking pragmas before non-`data' or `record' declaration."
  WarningName
InvalidRecordDirective_          -> String
"Record directives outside of record definitions or below field declarations."
  WarningName
InvalidTerminationCheckPragma_   -> String
"Termination checking pragmas before non-function or `mutual' blocks."
  WarningName
MissingDeclarations_             -> String
"Definitions not associated to a declaration."
  WarningName
MissingDefinitions_              -> String
"Declarations not associated to a definition."
  WarningName
NotAllowedInMutual_              -> String
"Declarations not allowed in a mutual block."
  WarningName
OpenPublicAbstract_              -> String
"'open public' directives in 'abstract' blocks."
  WarningName
OpenPublicPrivate_               -> String
"'open public' directives in 'private' blocks."
  WarningName
PolarityPragmasButNotPostulates_ -> String
"Polarity pragmas for non-postulates."
  WarningName
PragmaCompiled_                  -> String
"'COMPILE' pragmas in safe mode."
  WarningName
PragmaNoTerminationCheck_        -> String
"`NO_TERMINATION_CHECK' pragmas; such are deprecated."
  WarningName
ShadowingInTelescope_            -> String
"Repeated variable names in telescopes."
  WarningName
UnknownFixityInMixfixDecl_       -> String
"Mixfix names without an associated fixity declaration."
  WarningName
UnknownNamesInFixityDecl_        -> String
"Names not declared in the same scope as their syntax or fixity declaration."
  WarningName
UnknownNamesInPolarityPragmas_   -> String
"Names not declared in the same scope as their polarity pragmas."
  WarningName
UselessAbstract_                 -> String
"`abstract' blocks where they have no effect."
  WarningName
UselessHiding_                   -> String
"Names in `hiding' directive that are anyway not imported."
  WarningName
UselessInline_                   -> String
"`INLINE' pragmas where they have no effect."
  WarningName
UselessInstance_                 -> String
"`instance' blocks where they have no effect."
  WarningName
UselessPrivate_                  -> String
"`private' blocks where they have no effect."
  WarningName
UselessPublic_                   -> String
"`public' blocks where they have no effect."
  WarningName
UselessPatternDeclarationForRecord_ -> String
"`pattern' attributes where they have no effect."
  -- Scope and Type Checking Warnings
  WarningName
AbsurdPatternRequiresNoRHS_      -> String
"Clauses with an absurd pattern that have a right hand side."
  WarningName
AsPatternShadowsConstructorOrPatternSynonym_ -> String
"@-patterns that shadow constructors or pattern synonyms."
  WarningName
PatternShadowsConstructor_       -> String
"Pattern variables that shadow constructors."
  WarningName
CantGeneralizeOverSorts_         -> String
"Attempts to generalize over sort metas in 'variable' declaration."
  WarningName
ClashesViaRenaming_              -> String
"Clashes introduced by `renaming'."  -- issue #4154
  WarningName
CoverageIssue_                   -> String
"Failed coverage checks."
  WarningName
CoverageNoExactSplit_            -> String
"Failed exact split checks."
  WarningName
InlineNoExactSplit_              -> String
"Failed exact split checks after inlining record constructors."
  WarningName
DeprecationWarning_              -> String
"Deprecated features."
  WarningName
InvalidCharacterLiteral_         -> String
"Illegal character literals."
  WarningName
UselessPragma_                   -> String
"Pragmas that get ignored."
  WarningName
GenericWarning_                  -> String
""
  WarningName
IllformedAsClause_               -> String
"Illformed `as'-clauses in `import' statements."
  WarningName
InstanceNoOutputTypeName_        -> String
"Instance arguments whose type does not end in a named or variable type; those are never considered by instance search."
  WarningName
InstanceArgWithExplicitArg_      -> String
"Instance arguments with explicit arguments; those are never considered by instance search."
  WarningName
InstanceWithExplicitArg_         -> String
"`instance` declarations with explicit arguments; those are never considered by instance search."
  WarningName
InversionDepthReached_           -> String
"Inversions of pattern-matching failures due to exhausted inversion depth."
  WarningName
NoGuardednessFlag_               -> String
"Coinductive records without --guardedness flag."
  WarningName
ModuleDoesntExport_              -> String
"Imported names that are not actually exported."
  WarningName
DuplicateUsing_                  -> String
"Repeated names in using directive."
  WarningName
FixityInRenamingModule_          -> String
"Fixity annotations in `renaming' directive for `module'."
  WarningName
NotInScope_                      -> String
"Out of scope names."
  WarningName
NotStrictlyPositive_             -> String
"Failed strict positivity checks."
  WarningName
UnsupportedIndexedMatch_         -> String
"Failures to compute full equivalence when splitting on indexed family."
  WarningName
OldBuiltin_                      -> String
"Deprecated `BUILTIN' pragmas."
  WarningName
PlentyInHardCompileTimeMode_     -> String
"Uses of @ω or @plenty in hard compile-time mode."
  WarningName
PragmaCompileErased_             -> String
"`COMPILE' pragmas targeting an erased symbol."
  WarningName
RewriteMaybeNonConfluent_        -> String
"Failed local confluence checks while computing overlap."
  WarningName
RewriteNonConfluent_             -> String
"Failed local confluence checks while joining critical pairs."
  WarningName
RewriteAmbiguousRules_           -> String
"Failed global confluence checks because of overlapping rules."
  WarningName
RewriteMissingRule_              -> String
"Failed global confluence checks because of missing rule."
  WarningName
SafeFlagEta_                     -> String
"`ETA' pragmas with the safe flag."
  WarningName
SafeFlagInjective_               -> String
"`INJECTIVE' pragmas with the safe flag."
  WarningName
SafeFlagNoCoverageCheck_         -> String
"`NON_COVERING` pragmas with the safe flag."
  WarningName
SafeFlagNonTerminating_          -> String
"`NON_TERMINATING' pragmas with the safe flag."
  WarningName
SafeFlagNoPositivityCheck_       -> String
"`NO_POSITIVITY_CHECK' pragmas with the safe flag."
  WarningName
SafeFlagNoUniverseCheck_         -> String
"`NO_UNIVERSE_CHECK' pragmas with the safe flag."
  WarningName
SafeFlagPolarity_                -> String
"`POLARITY' pragmas with the safe flag."
  WarningName
SafeFlagPostulate_               -> String
"`postulate' blocks with the safe flag."
  WarningName
SafeFlagPragma_                  -> String
"Unsafe `OPTIONS' pragmas with the safe flag."
  WarningName
SafeFlagTerminating_             -> String
"`TERMINATING' pragmas with the safe flag."
  WarningName
SafeFlagWithoutKFlagPrimEraseEquality_ -> String
"`primEraseEquality' used with the safe and without-K flags."
  WarningName
TerminationIssue_                -> String
"Failed termination checks."
  WarningName
UnreachableClauses_              -> String
"Unreachable function clauses."
  WarningName
UnsolvedConstraints_             -> String
"Unsolved constraints."
  WarningName
UnsolvedInteractionMetas_        -> String
"Unsolved interaction meta variables."
  WarningName
InteractionMetaBoundaries_       -> String
"Interaction meta variables that have unsolved boundary constraints."
  WarningName
UnsolvedMetaVariables_           -> String
"Unsolved meta variables."
  WarningName
UserWarning_                     -> String
"User-defined warnings via one of the 'WARNING_ON_*' pragmas."
  WarningName
WithoutKFlagPrimEraseEquality_   -> String
"Uses of `primEraseEquality' with the without-K flags."
  WarningName
WrongInstanceDeclaration_        -> String
"Instances that do not adhere to the required format."
  -- Checking consistency of options
  WarningName
CoInfectiveImport_               -> String
"Importing a file not using e.g. `--safe'  from one which does."
  WarningName
InfectiveImport_                 -> String
"Importing a file using e.g. `--cubical' into one which does not."
  -- Record field warnings
  WarningName
DuplicateFields_                 -> String
"Record expressions with duplicate field names."
  WarningName
TooManyFields_                   -> String
"Record expressions with invalid field names."
  -- Opaque/unfolding warnings
  WarningName
NotAffectedByOpaque_             -> String
"Declarations unaffected by enclosing `opaque` blocks."
  WarningName
UnfoldTransparentName_           -> String
"Non-`opaque` names mentioned in an `unfolding` clause."
  WarningName
UselessOpaque_                   -> String
"`opaque` blocks that have no effect."
  -- Cubical
  WarningName
FaceConstraintCannotBeHidden_    -> String
"Face constraint patterns that are given as implicit arguments."
  WarningName
FaceConstraintCannotBeNamed_     -> String
"Face constraint patterns that are given as named arguments."