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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Warnings

Synopsis

- class (MonadPretty m, MonadError TCErr m) => MonadWarning (m :: Type -> Type) where
  - addWarning :: Bool -> TCWarning -> m ()
- warning'_ :: MonadWarning m => CallStack -> Warning -> m TCWarning
- warning_ :: (HasCallStack, MonadWarning m) => Warning -> m TCWarning
- warning' :: MonadWarning m => CallStack -> Warning -> m ()
- warning :: (HasCallStack, MonadWarning m) => Warning -> m ()
- warnings :: (HasCallStack, MonadWarning m) => List1 Warning -> m ()
- raiseWarningsOnUsage :: (MonadWarning m, ReadTCState m) => QName -> m ()
- isUnsolvedWarning :: Warning -> Bool
- isMetaWarning :: Warning -> Bool
- isMetaTCWarning :: TCWarning -> Bool
- onlyShowIfUnsolved :: Warning -> Bool
- data WhichWarnings
  - = ErrorWarnings
  - | AllWarnings
- classifyWarning :: Warning -> WhichWarnings
- data WarningsAndNonFatalErrors
- tcWarnings :: WarningsAndNonFatalErrors -> Set TCWarning
- nonFatalErrors :: WarningsAndNonFatalErrors -> Set TCWarning
- classifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors

# Documentation

class (MonadPretty m, MonadError TCErr m) => MonadWarning (m :: Type -> Type) where Source #

Minimal complete definition

Nothing

Methods

addWarning Source #

Arguments

:: Bool | Is the warning enabled?
-> TCWarning | The warning.
-> m () |

Store a warning and generate highlighting from it.

default addWarning :: forall (n :: Type -> Type) (t :: (Type -> Type) -> Type -> Type). (MonadWarning n, MonadTrans t, t n ~ m) => Bool -> TCWarning -> m () Source #

#### Instances

Instances details

MonadWarning TCM Source # |
Instance details Defined in Agda.TypeChecking.Warnings Methods addWarning :: Bool -> TCWarning -> TCM () Source #
PureTCM m => MonadWarning (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods addWarning :: Bool -> TCWarning -> PureConversionT m () Source #
MonadWarning m => MonadWarning (MaybeT m) Source # |
Instance details Defined in Agda.TypeChecking.Warnings Methods addWarning :: Bool -> TCWarning -> MaybeT m () Source #
MonadWarning m => MonadWarning (ReaderT r m) Source # |
Instance details Defined in Agda.TypeChecking.Warnings Methods addWarning :: Bool -> TCWarning -> ReaderT r m () Source #
MonadWarning m => MonadWarning (StateT s m) Source # |
Instance details Defined in Agda.TypeChecking.Warnings Methods addWarning :: Bool -> TCWarning -> StateT s m () Source #
(MonadWarning m, Monoid w) => MonadWarning (WriterT w m) Source # |
Instance details Defined in Agda.TypeChecking.Warnings Methods addWarning :: Bool -> TCWarning -> WriterT w m () Source #

warning'_ :: MonadWarning m => CallStack -> Warning -> m TCWarning Source #

warning_ :: (HasCallStack, MonadWarning m) => Warning -> m TCWarning Source #

warning' :: MonadWarning m => CallStack -> Warning -> m () Source #

warning :: (HasCallStack, MonadWarning m) => Warning -> m () Source #

warnings :: (HasCallStack, MonadWarning m) => List1 Warning -> m () Source #

raiseWarningsOnUsage :: (MonadWarning m, ReadTCState m) => QName -> m () Source #

Raise every `WARNING_ON_USAGE` connected to a name.

isUnsolvedWarning :: Warning -> Bool Source #

isMetaWarning :: Warning -> Bool Source #

isMetaTCWarning :: TCWarning -> Bool Source #

onlyShowIfUnsolved :: Warning -> Bool Source #

data WhichWarnings Source #

Classifying warnings: some are benign, others are (non-fatal) errors

Constructors

ErrorWarnings | warnings that will be turned into errors
AllWarnings | all warnings, including errors and benign ones Note: order of constructors is important for the derived Ord instance

#### Instances

Instances details

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

Instance details

Defined in Agda.TypeChecking.Warnings

Methods

compare :: WhichWarnings -> WhichWarnings -> Ordering Source #

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

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

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

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

max :: WhichWarnings -> WhichWarnings -> WhichWarnings Source #

min :: WhichWarnings -> WhichWarnings -> WhichWarnings Source #

classifyWarning :: Warning -> WhichWarnings Source #

data WarningsAndNonFatalErrors Source #

Assorted warnings and errors to be displayed to the user

#### Instances

Instances details

EncodeTCM DisplayInfo Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: DisplayInfo -> TCM Value Source #
EncodeTCM Response Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Response -> TCM Value Source #
Null WarningsAndNonFatalErrors Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: WarningsAndNonFatalErrors Source # null :: WarningsAndNonFatalErrors -> Bool Source #

tcWarnings :: WarningsAndNonFatalErrors -> Set TCWarning Source #

nonFatalErrors :: WarningsAndNonFatalErrors -> Set TCWarning Source #

classifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors Source #