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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Pretty.Warning

Contents

- Orphan instances

Synopsis

- prettyWarning :: MonadPretty m => Warning -> m Doc
- prettyRecordFieldWarning :: MonadPretty m => RecordFieldWarning -> m Doc
- prettyDuplicateFields :: MonadPretty m => [Name] -> m Doc
- prettyTooManyFields :: MonadPretty m => QName -> [Name] -> [Name] -> m Doc
- prettyNotInScopeNames :: (MonadPretty m, Pretty a, HasRange a) => Bool -> (a -> m Doc) -> [a] -> m Doc
- didYouMean :: (MonadPretty m, Pretty a, Pretty b) => [QName] -> (a -> b) -> a -> Maybe (m Doc)
- prettyTCWarnings :: [TCWarning] -> TCM String
- prettyTCWarnings' :: [TCWarning] -> TCM [String]
- filterTCWarnings :: [TCWarning] -> [TCWarning]
- tcWarningsToError :: [TCWarning] -> TCM ()
- applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> [TCWarning] -> m [TCWarning]
- applyFlagsToTCWarnings :: HasOptions m => [TCWarning] -> m [TCWarning]
- getAllUnsolvedWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => m [TCWarning]
- getAllWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => WhichWarnings -> m [TCWarning]
- getAllWarningsPreserving :: (MonadFail m, ReadTCState m, MonadWarning m) => Set WarningName -> WhichWarnings -> m [TCWarning]
- getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]

# Documentation

prettyWarning :: MonadPretty m => Warning -> m Doc Source #

prettyRecordFieldWarning :: MonadPretty m => RecordFieldWarning -> m Doc Source #

prettyDuplicateFields :: MonadPretty m => [Name] -> m Doc Source #

prettyTooManyFields :: MonadPretty m => QName -> [Name] -> [Name] -> m Doc Source #

prettyNotInScopeNames Source #

Arguments

:: (MonadPretty m, Pretty a, HasRange a) |
=> Bool | Print range?
-> (a -> m Doc) | Correction suggestion generator.
-> [a] | Names that are not in scope.
-> m Doc |

Report a number of names that are not in scope.

didYouMean Source #

Arguments

:: (MonadPretty m, Pretty a, Pretty b) |
=> [QName] | Names in scope.
-> (a -> b) | Canonization function for similarity search.
-> a | A name which is not in scope.
-> Maybe (m Doc) | "did you mean" hint.

Suggest some corrections to a misspelled name.

prettyTCWarnings :: [TCWarning] -> TCM String Source #

prettyTCWarnings' :: [TCWarning] -> TCM [String] Source #

filterTCWarnings :: [TCWarning] -> [TCWarning] Source #

If there are several warnings, remove the unsolved-constraints warning in case there are no interesting constraints to list.

tcWarningsToError :: [TCWarning] -> TCM () Source #

Turns warnings, if any, into errors.

applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> [TCWarning] -> m [TCWarning] Source #

Depending which flags are set, one may happily ignore some warnings.

applyFlagsToTCWarnings :: HasOptions m => [TCWarning] -> m [TCWarning] Source #

getAllUnsolvedWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => m [TCWarning] Source #

getAllWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => WhichWarnings -> m [TCWarning] Source #

Collect all warnings that have accumulated in the state.

getAllWarningsPreserving :: (MonadFail m, ReadTCState m, MonadWarning m) => Set WarningName -> WhichWarnings -> m [TCWarning] Source #

getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning] Source #

# Orphan instances

PrettyTCM TCWarning Source # |
Instance details Methods prettyTCM :: MonadPretty m => TCWarning -> m Doc Source #