Safe Haskell	Safe
Language	Haskell2010

Agda.Interaction.Options.Warnings

Synopsis

data WarningMode = WarningMode {
- _warningSet :: Set WarningName
- _warn2Error :: Bool
}
warningSet :: Lens' (Set WarningName) WarningMode
warn2Error :: Lens' Bool WarningMode
defaultWarningSet :: String
allWarnings :: Set WarningName
usualWarnings :: Set WarningName
noWarnings :: Set WarningName
unsolvedWarnings :: Set WarningName
incompleteMatchWarnings :: Set WarningName
errorWarnings :: Set WarningName
defaultWarningMode :: WarningMode
warningModeUpdate :: String -> Maybe (WarningMode -> WarningMode)
warningSets :: [(String, (Set WarningName, String))]
data WarningName
warningName2String :: WarningName -> String
string2WarningName :: String -> Maybe WarningName
usageWarning :: String

Documentation

data WarningMode Source #

A WarningMode has two components: a set of warnings to be displayed and a flag stating whether warnings should be turned into fatal errors.

Constructors

WarningMode
Fields _warningSet :: Set WarningName _warn2Error :: Bool

Instances

Eq WarningMode Source #
Instance details Defined in Agda.Interaction.Options.Warnings Methods (==) :: WarningMode -> WarningMode -> Bool # (/=) :: WarningMode -> WarningMode -> Bool #
Show WarningMode Source #
Instance details Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningMode -> ShowS # show :: WarningMode -> String # showList :: [WarningMode] -> ShowS #
EmbPrj WarningMode Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningMode -> S Int32 Source # icod_ :: WarningMode -> S Int32 Source # value :: Int32 -> R WarningMode Source #

warningSet :: Lens' (Set WarningName) WarningMode Source #

warn2Error :: Lens' Bool WarningMode Source #

defaultWarningSet :: String Source #

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

allWarnings :: Set WarningName Source #

usualWarnings :: Set WarningName Source #

noWarnings :: Set WarningName Source #

unsolvedWarnings :: Set WarningName Source #

incompleteMatchWarnings :: Set WarningName Source #

errorWarnings :: Set WarningName Source #

defaultWarningMode :: WarningMode Source #

warningModeUpdate :: String -> Maybe (WarningMode -> WarningMode) Source #

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

warningSets :: [(String, (Set WarningName, String))] Source #

Common sets of warnings

data WarningName Source #

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

Constructors

OverlappingTokensWarning_
LibUnknownField_
EmptyAbstract_
EmptyField_
EmptyGeneralize_
EmptyInstance_
EmptyMacro_
EmptyMutual_
EmptyPostulate_
EmptyPrimitive_
EmptyPrivate_
EmptyRewritePragma_
InvalidCatchallPragma_
InvalidCoverageCheckPragma_
InvalidNoPositivityCheckPragma_
InvalidNoUniverseCheckPragma_
InvalidTerminationCheckPragma_
MissingDefinitions_
NotAllowedInMutual_
OpenPublicAbstract_
OpenPublicPrivate_
PolarityPragmasButNotPostulates_
PragmaCompiled_
PragmaNoTerminationCheck_
ShadowingInTelescope_
UnknownFixityInMixfixDecl_
UnknownNamesInFixityDecl_
UnknownNamesInPolarityPragmas_
UselessAbstract_
UselessInstance_
UselessPrivate_
AbsurdPatternRequiresNoRHS_
CantGeneralizeOverSorts_
ClashesViaRenaming_
CoverageIssue_
CoverageNoExactSplit_
DeprecationWarning_
FixityInRenamingModule_
GenericNonFatalError_
GenericWarning_
IllformedAsClause_
InstanceArgWithExplicitArg_
InstanceWithExplicitArg_
InstanceNoOutputTypeName_
InversionDepthReached_
ModuleDoesntExport_
NotInScope_
NotStrictlyPositive_
OldBuiltin_
PragmaCompileErased_
RewriteMaybeNonConfluent_
RewriteNonConfluent_
SafeFlagEta_
SafeFlagInjective_
SafeFlagNoCoverageCheck_
SafeFlagNonTerminating_
SafeFlagNoPositivityCheck_
SafeFlagNoUniverseCheck_
SafeFlagPolarity_
SafeFlagPostulate_
SafeFlagPragma_
SafeFlagTerminating_
SafeFlagWithoutKFlagPrimEraseEquality_
TerminationIssue_
UnreachableClauses_
UnsolvedConstraints_
UnsolvedInteractionMetas_
UnsolvedMetaVariables_
UselessInline_
UselessPublic_
UserWarning_
WithoutKFlagPrimEraseEquality_
WrongInstanceDeclaration_
CoInfectiveImport_
InfectiveImport_

Instances

Bounded WarningName Source #
Instance details Defined in Agda.Interaction.Options.Warnings Methods minBound :: WarningName # maxBound :: WarningName #
Enum WarningName Source #
Instance details Defined in Agda.Interaction.Options.Warnings Methods succ :: WarningName -> WarningName # pred :: WarningName -> WarningName # toEnum :: Int -> WarningName # fromEnum :: WarningName -> Int # enumFrom :: WarningName -> [WarningName] # enumFromThen :: WarningName -> WarningName -> [WarningName] # enumFromTo :: WarningName -> WarningName -> [WarningName] # enumFromThenTo :: WarningName -> WarningName -> WarningName -> [WarningName] #
Eq WarningName Source #
Instance details Defined in Agda.Interaction.Options.Warnings Methods (==) :: WarningName -> WarningName -> Bool # (/=) :: WarningName -> WarningName -> Bool #
Ord WarningName Source #
Instance details Defined in Agda.Interaction.Options.Warnings Methods compare :: WarningName -> WarningName -> Ordering # (<) :: WarningName -> WarningName -> Bool # (<=) :: WarningName -> WarningName -> Bool # (>) :: WarningName -> WarningName -> Bool # (>=) :: WarningName -> WarningName -> Bool # max :: WarningName -> WarningName -> WarningName # min :: WarningName -> WarningName -> WarningName #
Read WarningName Source #
Instance details Defined in Agda.Interaction.Options.Warnings Methods readsPrec :: Int -> ReadS WarningName # readList :: ReadS [WarningName] # readPrec :: ReadPrec WarningName # readListPrec :: ReadPrec [WarningName] #
Show WarningName Source #
Instance details Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningName -> ShowS # show :: WarningName -> String # showList :: [WarningName] -> ShowS #
EmbPrj WarningName Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningName -> S Int32 Source # icod_ :: WarningName -> S Int32 Source # value :: Int32 -> R WarningName Source #

warningName2String :: WarningName -> String Source #

string2WarningName :: String -> Maybe WarningName Source #

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

usageWarning :: String Source #

warningUsage generated using warningNameDescription