Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

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
- errorWarnings :: Set WarningName
- defaultWarningMode :: WarningMode
- warningModeUpdate :: String -> Maybe (WarningMode -> WarningMode)
- warningSets :: [(String, (Set WarningName, String))]
- data WarningName
  - = OverlappingTokensWarning_
  - | LibUnknownField_
  - | EmptyAbstract_
  - | EmptyInstance_
  - | EmptyMacro_
  - | EmptyMutual_
  - | EmptyPostulate_
  - | EmptyPrivate_
  - | EmptyGeneralize_
  - | EmptyPrimitive_
  - | InvalidCatchallPragma_
  - | InvalidNoUniverseCheckPragma_
  - | InvalidTerminationCheckPragma_
  - | InvalidNoPositivityCheckPragma_
  - | MissingDefinitions_
  - | NotAllowedInMutual_
  - | PolarityPragmasButNotPostulates_
  - | PragmaNoTerminationCheck_
  - | PragmaCompiled_
  - | UnknownFixityInMixfixDecl_
  - | UnknownNamesInFixityDecl_
  - | UnknownNamesInPolarityPragmas_
  - | UselessAbstract_
  - | UselessInstance_
  - | UselessPrivate_
  - | OldBuiltin_
  - | EmptyRewritePragma_
  - | IllformedAsClause_
  - | UselessPublic_
  - | UnreachableClauses_
  - | UselessInline_
  - | WrongInstanceDeclaration_
  - | InstanceWithExplicitArg_
  - | InstanceNoOutputTypeName_
  - | InstanceArgWithExplicitArg_
  - | GenericWarning_
  - | DeprecationWarning_
  - | InversionDepthReached_
  - | TerminationIssue_
  - | CoverageIssue_
  - | CoverageNoExactSplit_
  - | ModuleDoesntExport_
  - | NotStrictlyPositive_
  - | UnsolvedMetaVariables_
  - | UnsolvedInteractionMetas_
  - | UnsolvedConstraints_
  - | GenericNonFatalError_
  - | SafeFlagPostulate_
  - | SafeFlagPragma_
  - | SafeFlagNonTerminating_
  - | SafeFlagTerminating_
  - | SafeFlagWithoutKFlagPrimEraseEquality_
  - | SafeFlagNoPositivityCheck_
  - | SafeFlagPolarity_
  - | SafeFlagNoUniverseCheck_
  - | UserWarning_
  - | WithoutKFlagPrimEraseEquality_
  - | CantGeneralizeOverSorts_
  - | AbsurdPatternRequiresNoRHS_
  - | InfectiveImport_
  - | CoInfectiveImport_
- 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 Source # (/=) :: WarningMode -> WarningMode -> Bool Source #
Show WarningMode Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningMode -> ShowS Source # show :: WarningMode -> String Source # showList :: [WarningMode] -> ShowS Source #
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 #

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_ |
EmptyInstance_ |
EmptyMacro_ |
EmptyMutual_ |
EmptyPostulate_ |
EmptyPrivate_ |
EmptyGeneralize_ |
EmptyPrimitive_ |
InvalidCatchallPragma_ |
InvalidNoUniverseCheckPragma_ |
InvalidTerminationCheckPragma_ |
InvalidNoPositivityCheckPragma_ |
MissingDefinitions_ |
NotAllowedInMutual_ |
PolarityPragmasButNotPostulates_ |
PragmaNoTerminationCheck_ |
PragmaCompiled_ |
UnknownFixityInMixfixDecl_ |
UnknownNamesInFixityDecl_ |
UnknownNamesInPolarityPragmas_ |
UselessAbstract_ |
UselessInstance_ |
UselessPrivate_ |
OldBuiltin_ |
EmptyRewritePragma_ |
IllformedAsClause_ |
UselessPublic_ |
UnreachableClauses_ |
UselessInline_ |
WrongInstanceDeclaration_ |
InstanceWithExplicitArg_ |
InstanceNoOutputTypeName_ |
InstanceArgWithExplicitArg_ |
GenericWarning_ |
DeprecationWarning_ |
InversionDepthReached_ |
TerminationIssue_ |
CoverageIssue_ |
CoverageNoExactSplit_ |
ModuleDoesntExport_ |
NotStrictlyPositive_ |
UnsolvedMetaVariables_ |
UnsolvedInteractionMetas_ |
UnsolvedConstraints_ |
GenericNonFatalError_ |
SafeFlagPostulate_ |
SafeFlagPragma_ |
SafeFlagNonTerminating_ |
SafeFlagTerminating_ |
SafeFlagWithoutKFlagPrimEraseEquality_ |
SafeFlagNoPositivityCheck_ |
SafeFlagPolarity_ |
SafeFlagNoUniverseCheck_ |
UserWarning_ |
WithoutKFlagPrimEraseEquality_ |
CantGeneralizeOverSorts_ |
AbsurdPatternRequiresNoRHS_ |
InfectiveImport_ |
CoInfectiveImport_ |

Instances

Bounded WarningName Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods minBound :: WarningName Source # maxBound :: WarningName Source #
Enum WarningName Source # |

Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

succ :: WarningName -> WarningName Source #

pred :: WarningName -> WarningName Source #

toEnum :: Int -> WarningName Source #

fromEnum :: WarningName -> Int Source #

enumFrom :: WarningName -> [WarningName] Source #

enumFromThen :: WarningName -> WarningName -> [WarningName] Source #

enumFromTo :: WarningName -> WarningName -> [WarningName] Source #

enumFromThenTo :: WarningName -> WarningName -> WarningName -> [WarningName] Source #

Eq WarningName Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods (==) :: WarningName -> WarningName -> Bool Source # (/=) :: WarningName -> WarningName -> Bool Source #
Ord WarningName Source # |

Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

compare :: WarningName -> WarningName -> Ordering Source #

(<) :: WarningName -> WarningName -> Bool Source #

(<=) :: WarningName -> WarningName -> Bool Source #

(>) :: WarningName -> WarningName -> Bool Source #

(>=) :: WarningName -> WarningName -> Bool Source #

max :: WarningName -> WarningName -> WarningName Source #

min :: WarningName -> WarningName -> WarningName Source #

Read WarningName Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods readsPrec :: Int -> ReadS WarningName Source # readList :: ReadS [WarningName] Source # readPrec :: ReadPrec WarningName Source # readListPrec :: ReadPrec [WarningName] Source #
Show WarningName Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningName -> ShowS Source # show :: WarningName -> String Source # showList :: [WarningName] -> ShowS Source #
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`