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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Warnings

Synopsis

- class (MonadPretty m, MonadError TCErr m) => MonadWarning m where
  - addWarning :: TCWarning -> m ()
- genericWarning :: MonadWarning m => Doc -> m ()
- genericNonFatalError :: MonadWarning m => Doc -> 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) => [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 -> [TCWarning]
- nonFatalErrors :: WarningsAndNonFatalErrors -> [TCWarning]
- emptyWarningsAndNonFatalErrors :: WarningsAndNonFatalErrors
- classifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors
- runPM :: PM a -> TCM a

# Documentation

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

Minimal complete definition

Nothing

Methods

addWarning :: TCWarning -> m () Source #

Store a warning and generate highlighting from it.

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

#### Instances

Instances details

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

genericWarning :: MonadWarning m => Doc -> m () Source #

genericNonFatalError :: MonadWarning m => Doc -> 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) => [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

tcWarnings :: WarningsAndNonFatalErrors -> [TCWarning] Source #

nonFatalErrors :: WarningsAndNonFatalErrors -> [TCWarning] Source #

emptyWarningsAndNonFatalErrors :: WarningsAndNonFatalErrors Source #

The only way to construct a empty WarningsAndNonFatalErrors

classifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors Source #

runPM :: PM a -> TCM a Source #

running the Parse monad