Safe Haskell	Safe-Inferred
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
data WarningModeError
- = Unknown String
- | NoNoError String
prettyWarningModeError :: WarningModeError -> String
warningModeUpdate :: String -> Either WarningModeError WarningModeUpdate
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

Instances details

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 #
Generic WarningMode Source #
Instance details Defined in Agda.Interaction.Options.Warnings Associated Types type Rep WarningMode :: Type -> Type # Methods from :: WarningMode -> Rep WarningMode x # to :: Rep WarningMode x -> WarningMode #
Show WarningMode Source #
Instance details Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningMode -> ShowS # show :: WarningMode -> String # showList :: [WarningMode] -> ShowS #
NFData WarningMode Source #
Instance details Defined in Agda.Interaction.Options.Warnings Methods rnf :: WarningMode -> () #
Eq WarningMode Source #
Instance details Defined in Agda.Interaction.Options.Warnings Methods (==) :: WarningMode -> WarningMode -> Bool # (/=) :: WarningMode -> WarningMode -> Bool #
type Rep WarningMode Source #
Instance details Defined in Agda.Interaction.Options.Warnings type Rep WarningMode = D1 ('MetaData "WarningMode" "Agda.Interaction.Options.Warnings" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "WarningMode" 'PrefixI 'True) (S1 ('MetaSel ('Just "_warningSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set WarningName)) :*: S1 ('MetaSel ('Just "_warn2Error") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

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 #

data WarningModeError Source #

Some warnings are errors and cannot be turned off.

Constructors

Unknown String
NoNoError String

prettyWarningModeError :: WarningModeError -> String Source #

warningModeUpdate :: String -> Either WarningModeError WarningModeUpdate 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_
UnsupportedAttribute_
MultipleAttributes_
LibUnknownField_
EmptyAbstract_
EmptyConstructor_
EmptyField_
EmptyGeneralize_
EmptyInstance_
EmptyMacro_
EmptyMutual_
EmptyPostulate_
EmptyPrimitive_
EmptyPrivate_
EmptyRewritePragma_
EmptyWhere_
InvalidCatchallPragma_
InvalidConstructor_
InvalidConstructorBlock_
InvalidCoverageCheckPragma_
InvalidNoPositivityCheckPragma_
InvalidNoUniverseCheckPragma_
InvalidRecordDirective_
InvalidTerminationCheckPragma_
MissingDeclarations_
MissingDefinitions_
NotAllowedInMutual_
OpenPublicAbstract_
OpenPublicPrivate_
PolarityPragmasButNotPostulates_
PragmaCompiled_
PragmaNoTerminationCheck_
ShadowingInTelescope_
UnknownFixityInMixfixDecl_
UnknownNamesInFixityDecl_
UnknownNamesInPolarityPragmas_
UselessAbstract_
UselessInstance_
UselessPrivate_
AbsurdPatternRequiresNoRHS_
AsPatternShadowsConstructorOrPatternSynonym_
CantGeneralizeOverSorts_
ClashesViaRenaming_
CoverageIssue_
CoverageNoExactSplit_
DeprecationWarning_
DuplicateUsing_
FixityInRenamingModule_
GenericNonFatalError_
GenericUseless_
GenericWarning_
IllformedAsClause_
InstanceArgWithExplicitArg_
InstanceWithExplicitArg_
InstanceNoOutputTypeName_
InversionDepthReached_
ModuleDoesntExport_
NoGuardednessFlag_
NotInScope_
NotStrictlyPositive_
OldBuiltin_
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_
CoInfectiveImport_
InfectiveImport_
DuplicateFieldsWarning_
TooManyFieldsWarning_

Instances

Instances details

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 #
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] #
Generic WarningName Source #
Instance details Defined in Agda.Interaction.Options.Warnings Associated Types type Rep WarningName :: Type -> Type # Methods from :: WarningName -> Rep WarningName x # to :: Rep WarningName x -> 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 #
NFData WarningName Source #
Instance details Defined in Agda.Interaction.Options.Warnings Methods rnf :: 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 #
type Rep WarningName Source #
Instance details Defined in Agda.Interaction.Options.Warnings type Rep WarningName = D1 ('MetaData "WarningName" "Agda.Interaction.Options.Warnings" "Agda-2.6.2.1.20220320-inplace" 'False) ((((((C1 ('MetaCons "OverlappingTokensWarning_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsupportedAttribute_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "MultipleAttributes_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "LibUnknownField_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyAbstract_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "EmptyConstructor_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyField_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyGeneralize_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "EmptyInstance_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyMacro_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyMutual_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "EmptyPostulate_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyPrimitive_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyPrivate_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "EmptyRewritePragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyWhere_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidCatchallPragma_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "InvalidConstructor_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "InvalidConstructorBlock_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidCoverageCheckPragma_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "InvalidNoPositivityCheckPragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "InvalidNoUniverseCheckPragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidRecordDirective_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "InvalidTerminationCheckPragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MissingDeclarations_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "MissingDefinitions_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotAllowedInMutual_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OpenPublicAbstract_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "OpenPublicPrivate_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PolarityPragmasButNotPostulates_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PragmaCompiled_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "PragmaNoTerminationCheck_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ShadowingInTelescope_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnknownFixityInMixfixDecl_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "UnknownNamesInFixityDecl_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UnknownNamesInPolarityPragmas_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessAbstract_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "UselessInstance_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UselessPrivate_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AbsurdPatternRequiresNoRHS_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "AsPatternShadowsConstructorOrPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CantGeneralizeOverSorts_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ClashesViaRenaming_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "CoverageIssue_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CoverageNoExactSplit_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DeprecationWarning_" 'PrefixI 'False) (U1 :: Type -> Type))))))) :+: (((((C1 ('MetaCons "DuplicateUsing_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FixityInRenamingModule_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "GenericNonFatalError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "GenericUseless_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GenericWarning_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "IllformedAsClause_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "InstanceArgWithExplicitArg_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InstanceWithExplicitArg_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "InstanceNoOutputTypeName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "InversionDepthReached_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ModuleDoesntExport_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "NoGuardednessFlag_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotInScope_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotStrictlyPositive_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "OldBuiltin_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PragmaCompileErased_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteMaybeNonConfluent_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "RewriteNonConfluent_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "RewriteAmbiguousRules_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteMissingRule_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "SafeFlagEta_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SafeFlagInjective_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SafeFlagNoCoverageCheck_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "SafeFlagNonTerminating_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SafeFlagNoPositivityCheck_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SafeFlagNoUniverseCheck_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "SafeFlagPolarity_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SafeFlagPostulate_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SafeFlagPragma_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "SafeFlagTerminating_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SafeFlagWithoutKFlagPrimEraseEquality_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TerminationIssue_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "UnreachableClauses_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UnsolvedConstraints_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsolvedInteractionMetas_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "UnsolvedMetaVariables_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UselessHiding_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessInline_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "UselessPatternDeclarationForRecord_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UselessPublic_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UserWarning_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "WithoutKFlagPrimEraseEquality_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WrongInstanceDeclaration_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoInfectiveImport_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "InfectiveImport_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DuplicateFieldsWarning_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TooManyFieldsWarning_" 'PrefixI 'False) (U1 :: Type -> Type))))))))

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