module Agda.TypeChecking.Pretty.Warning where
import Prelude hiding ( null )
import Control.Monad ( guard, filterM, (<=<) )
import Control.Monad.Fail ( MonadFail )
import Data.Char ( toLower )
import Data.Function (on)
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.Maybe
import qualified Data.Set as Set
import Data.Set (Set)
import qualified Data.List as List
import qualified Data.Text as T
import Agda.TypeChecking.Monad.Base
import qualified Agda.TypeChecking.Monad.Base.Warning as W
import Agda.TypeChecking.Monad.Builtin
import {-# SOURCE #-} Agda.TypeChecking.Errors
import Agda.TypeChecking.Monad.MetaVars
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Constraints
import Agda.TypeChecking.Monad.State ( getScope )
import Agda.TypeChecking.Monad ( localTCState, enterClosure )
import Agda.TypeChecking.Positivity ()
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Pretty.Call ()
import {-# SOURCE #-} Agda.TypeChecking.Pretty.Constraint (prettyInterestingConstraints, interestingConstraint)
import Agda.TypeChecking.Warnings (MonadWarning, isUnsolvedWarning, onlyShowIfUnsolved, classifyWarning, WhichWarnings(..), warning_)
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
import Agda.Syntax.Common ( IsOpaque(OpaqueDef, TransparentDef), getHiding, ImportedName'(..), fromImportedName, partitionImportedNames )
import Agda.Syntax.Position
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Scope.Base ( concreteNamesInScope, NameOrModule(..) )
import Agda.Syntax.Internal
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Interaction.Options
import Agda.Interaction.Options.Warnings
import Agda.Utils.FileName ( filePath )
import Agda.Utils.Functor ( (<.>) )
import Agda.Utils.Lens
import Agda.Utils.List ( editDistance )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty ( Pretty, prettyShow, singPlural )
import qualified Agda.Syntax.Common.Pretty as P
instance PrettyTCM TCWarning where
prettyTCM :: forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM w :: TCWarning
w@(TCWarning CallStack
loc Range
_ Warning
_ Doc
_ Bool
_) = do
[Char] -> VerboseLevel -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"warning" VerboseLevel
2 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Warning raised at " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CallStack -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow CallStack
loc
Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ TCWarning -> Doc
tcWarningPrintedWarning TCWarning
w
{-# SPECIALIZE prettyWarningName :: WarningName -> TCM Doc #-}
prettyWarningName :: MonadPretty m => WarningName -> m Doc
prettyWarningName :: forall (m :: * -> *). MonadPretty m => WarningName -> m Doc
prettyWarningName WarningName
w = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hcat
[ m Doc
"warning: -W[no]"
, [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ WarningName -> [Char]
warningName2String WarningName
w
]
{-# SPECIALIZE prettyWarning :: Warning -> TCM Doc #-}
prettyWarning :: MonadPretty m => Warning -> m Doc
prettyWarning :: forall (m :: * -> *). MonadPretty m => Warning -> m Doc
prettyWarning = \case
UnsolvedMetaVariables [Range]
ms ->
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Unsolved metas at the following locations:" )
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (Range -> m Doc) -> [Range] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM [Range]
ms)
UnsolvedInteractionMetas [Range]
is ->
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Unsolved interaction metas at the following locations:" )
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (Range -> m Doc) -> [Range] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM [Range]
is)
InteractionMetaBoundaries [Range]
is ->
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Interaction meta(s) at the following location(s) have unsolved boundary constraints:" )
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (Range -> m Doc) -> [Range] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM (Set Range -> [Range]
forall a. Set a -> [a]
Set.toList ([Range] -> Set Range
forall a. Ord a => [a] -> Set a
Set.fromList [Range]
is)))
UnsolvedConstraints Constraints
cs -> do
pcs <- Constraints -> m [Doc]
forall (m :: * -> *). MonadPretty m => Constraints -> m [Doc]
prettyInterestingConstraints Constraints
cs
if null pcs
then fsep $ pwords "Unsolved constraints"
else vcat
[ fsep $ pwords "Failed to solve the following constraints:"
, nest 2 $ return $ P.vcat $ List.nub pcs
]
TerminationIssue [TerminationError]
because -> do
dropTopLevel <- m (QName -> QName)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, ReadTCState m) =>
m (QName -> QName)
topLevelModuleDropper
fwords "Termination checking failed for the following functions:"
$$ nest 2 (fsep $ punctuate comma $
map (pretty . dropTopLevel) $
concatMap termErrFunctions because)
$$ fwords "Problematic calls:"
$$ nest 2 (fmap (P.vcat . List.nub) $
mapM prettyTCM $ List.sortOn getRange $
concatMap termErrCalls because)
UnreachableClauses QName
f [Range]
pss -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Unreachable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords (VerboseLevel -> [Char] -> [Char]
forall {a}. (Num a, Eq a) => a -> [Char] -> [Char]
plural ([Range] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Range]
pss) [Char]
"clause")
where
plural :: a -> [Char] -> [Char]
plural a
1 [Char]
thing = [Char]
thing
plural a
n [Char]
thing = [Char]
thing [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"s"
CoverageIssue QName
f [(Telescope, [NamedArg DeBruijnPattern])]
pss -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Incomplete pattern matching for" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Missing cases:") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ ((Telescope, [NamedArg DeBruijnPattern]) -> m Doc)
-> [(Telescope, [NamedArg DeBruijnPattern])] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display [(Telescope, [NamedArg DeBruijnPattern])]
pss)
where
display :: (Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display (Telescope
tel, [NamedArg DeBruijnPattern]
ps) = NamedClause -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
prettyTCM (NamedClause -> m Doc) -> NamedClause -> m Doc
forall a b. (a -> b) -> a -> b
$ QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True (Clause -> NamedClause) -> Clause -> NamedClause
forall a b. (a -> b) -> a -> b
$
Clause
forall a. Null a => a
empty { clauseTel = tel, namedClausePats = ps }
CoverageNoExactSplit QName
f [Clause]
cs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Exact splitting is enabled, but the following" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Clause] -> [Char] -> [Char] -> [Char]
forall a c. Sized a => a -> c -> c -> c
P.singPlural [Clause]
cs [Char]
"clause" [Char]
"clauses") [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"could not be preserved as definitional equalities in the translation to a case tree:"
) m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
:
(Clause -> m Doc) -> [Clause] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> (Clause -> m Doc) -> Clause -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedClause -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
prettyTCM (NamedClause -> m Doc)
-> (Clause -> NamedClause) -> Clause -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True) [Clause]
cs
InlineNoExactSplit QName
f Clause
c -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Exact splitting is enabled, but the following clause" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is no longer a definitional equality because it was translated to a copattern match:"
, VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> (Clause -> m Doc) -> Clause -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedClause -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
prettyTCM (NamedClause -> m Doc)
-> (Clause -> NamedClause) -> Clause -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True (Clause -> m Doc) -> Clause -> m Doc
forall a b. (a -> b) -> a -> b
$ Clause
c
]
NotStrictlyPositive QName
d Seq OccursWhere
ocs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not strictly positive, because it occurs"
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Seq OccursWhere -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Seq OccursWhere -> m Doc
prettyTCM Seq OccursWhere
ocs]
ConstructorDoesNotFitInData QName
c Sort
s1 Sort
s2 TCErr
err -> TCErr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err
CoinductiveEtaRecord QName
name -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Not switching on eta-equality for coinductive records."
, [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"If you must, use pragma" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ m Doc
"{-# ETA", QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
name, m Doc
"#-}" ]
]
UnsupportedIndexedMatch Doc
doc -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"This clause uses pattern-matching features that are not yet supported by Cubical Agda,"
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"the function to which it belongs will not compute when applied to transports."
)
, m Doc
""
, m Doc
"Reason:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
doc
, m Doc
""
]
CantGeneralizeOverSorts [MetaId]
ms -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Cannot generalize over unsolved sort metas:"
, VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ MetaId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"at" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Range -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Range -> m Doc) -> m Range -> m Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> m Range
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange MetaId
x) | MetaId
x <- [MetaId]
ms ]
, [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Suggestion: add a `variable Any : Set _` and replace unsolved metas by Any"
]
AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern]
ps -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char]
"The right-hand side must be omitted if there " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
"is an absurd pattern, () or {}, in the left-hand side."
OldBuiltin BuiltinId
old BuiltinId
new -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char]
"Builtin " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BuiltinId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
old [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" no longer exists. " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
"It is now bound by BUILTIN " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BuiltinId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
new
BuiltinDeclaresIdentifier BuiltinId
b -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char]
"BUILTIN " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BuiltinId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" declares an identifier " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
"(no longer expects an already defined identifier)"
Warning
EmptyRewritePragma -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> ([Char] -> [m Doc]) -> [Char] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Empty REWRITE pragma"
Warning
EmptyWhere -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> ([Char] -> [m Doc]) -> [Char] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Empty `where' block (ignored)"
IllformedAsClause [Char]
s -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> ([Char] -> [m Doc]) -> [Char] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char]
"`as' must be followed by an identifier" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
ClashesViaRenaming NameOrModule
nm [Name]
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[m Doc]] -> [m Doc]) -> [[m Doc]] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
[ [ case NameOrModule
nm of NameOrModule
NameNotModule -> m Doc
"Name"; NameOrModule
ModuleNotName -> m Doc
"Module" ]
, [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"clashes introduced by `renaming':"
, (Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM [Name]
xs
]
UselessPatternDeclarationForRecord [Char]
s -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords
[ [Char]
"`pattern' attribute ignored for", [Char]
s, [Char]
"record" ]
Warning
UselessPublic -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Keyword `public' is ignored here"
UselessHiding [ImportedName]
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ignoring names in `hiding' directive:"
, m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
"," ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ (ImportedName -> m Doc) -> [ImportedName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ImportedName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [ImportedName]
xs
]
UselessInline QName
q -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"It is pointless for INLINE'd function" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"to have a separate Haskell definition"
Warning
WrongInstanceDeclaration -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char]
"Instances should be of type {Γ} → C, where C evaluates to a postulated name or the name of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
"a data or record type, so `instance' is ignored here."
InstanceWithExplicitArg QName
q -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Instance declarations with explicit arguments are never considered by instance search," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"so making" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"into an instance has no effect."
InstanceNoOutputTypeName Doc
b -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Instance arguments whose type is not {Γ} → C, where C evaluates to a postulated type, " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a parameter type or the name of a data or record type, are never considered by instance search," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"so having an instance argument" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
b] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has no effect."
InstanceArgWithExplicitArg Doc
b -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Instance arguments with explicit arguments are never considered by instance search," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"so having an instance argument" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
b] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has no effect."
InversionDepthReached QName
f -> do
maxDepth <- m VerboseLevel
forall (m :: * -> *). HasOptions m => m VerboseLevel
maxInversionDepth
fsep $ pwords "Refusing to invert pattern matching of" ++ [prettyTCM f] ++
pwords ("because the maximum depth (" ++ show maxDepth ++ ") has been reached.") ++
pwords "Most likely this means you have an unsatisfiable constraint, but it could" ++
pwords "also mean that you need to increase the maximum depth using the flag" ++
pwords "--inversion-max-depth=N"
NoGuardednessFlag QName
q ->
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is declared coinductive, but option" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"--guardedness is not enabled. Coinductive functions on" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"this type will likely be rejected by the termination" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"checker unless this flag is enabled."
InvalidCharacterLiteral Char
c -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Invalid character literal" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ Char -> [Char]
forall a. Show a => a -> [Char]
show Char
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"(surrogate code points are not supported)"
UselessPragma Range
_r Doc
d -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d
SafeFlagPostulate Name
e -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot postulate" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Name
e] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"with safe flag"
SafeFlagPragma [[Char]]
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[Char]]
-> ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall a c. Sized a => a -> c -> c -> c
singPlural ([Char] -> [[Char]]
words ([Char] -> [[Char]]) -> [[Char]] -> [[Char]]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [[Char]]
xs) [Char] -> [Char]
forall a. a -> a
id ([Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"s") [Char]
"Cannot set OPTIONS pragma" ]
, ([Char] -> m Doc) -> [[Char]] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [[Char]]
xs
, [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"with safe flag." ]
]
Warning
SafeFlagWithoutKFlagPrimEraseEquality -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot use primEraseEquality with safe and without-K flags.")
Warning
WithoutKFlagPrimEraseEquality -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Using primEraseEquality with the without-K flag is inconsistent.")
ConflictingPragmaOptions [Char]
a [Char]
b -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords
[ [Char]
"Conflicting options", [Char] -> [Char]
yes [Char]
a, [Char]
"and", [Char] -> [Char]
no [Char]
b, [Char]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
yes [Char]
a, [Char]
"implies", [Char] -> [Char]
yes [Char]
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")."
, [Char]
"Ignoring", [Char] -> [Char]
no [Char]
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"." ]
where
yes :: [Char] -> [Char]
yes [Char]
s = [Char]
"--" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
no :: [Char] -> [Char]
no (Char
'n' : Char
'o' : Char
'-' : [Char]
s) = [Char]
"--" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
no [Char]
s = [Char]
"--no-" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
OptionWarning OptionWarning
ow -> OptionWarning -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty OptionWarning
ow
ParseWarning ParseWarning
pw -> ParseWarning -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ParseWarning
pw
DuplicateInterfaceFiles AbsolutePath
selected AbsolutePath
ignored -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"There are two interface files:"
, VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
4 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [Char]
filePath AbsolutePath
selected
, VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
4 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [Char]
filePath AbsolutePath
ignored
, VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Using" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [Char]
filePath AbsolutePath
selected] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"for now but please remove at least one of them."
]
DeprecationWarning [Char]
old [Char]
new [Char]
version -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
old] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has been deprecated. Use" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
new] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords
[Char]
"instead. This will be an error in Agda" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
version m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
NicifierIssue DeclarationWarning
w -> DeclarationWarning -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty DeclarationWarning
w
UserWarning Text
str -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Text -> [Char]
T.unpack Text
str)
ModuleDoesntExport QName
m [Name]
names [Name]
modules [ImportedName]
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"doesn't export the following:"
, Bool -> (ImportedName -> m Doc) -> [ImportedName] -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, Pretty a, HasRange a) =>
Bool -> (a -> m Doc) -> [a] -> m Doc
prettyNotInScopeNames Bool
False ([Name] -> ImportedName -> m Doc
forall {m :: * -> *} {b}.
(Null (m Doc), MonadFresh NameId m, MonadInteractionPoints m,
MonadStConcreteNames m, PureTCM m, IsString (m Doc),
Semigroup (m Doc), Pretty b) =>
[Name] -> ImportedName' b b -> m Doc
suggestion [Name]
names) [ImportedName]
ys
, Bool -> (ImportedName -> m Doc) -> [ImportedName] -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, Pretty a, HasRange a) =>
Bool -> (a -> m Doc) -> [a] -> m Doc
prettyNotInScopeNames Bool
False ([Name] -> ImportedName -> m Doc
forall {m :: * -> *} {b}.
(Null (m Doc), MonadFresh NameId m, MonadInteractionPoints m,
MonadStConcreteNames m, PureTCM m, IsString (m Doc),
Semigroup (m Doc), Pretty b) =>
[Name] -> ImportedName' b b -> m Doc
suggestion [Name]
modules) [ImportedName]
ms
]
where
ys, ms :: [C.ImportedName]
ys :: [ImportedName]
ys = (Name -> ImportedName) -> [Name] -> [ImportedName]
forall a b. (a -> b) -> [a] -> [b]
map Name -> ImportedName
forall n m. n -> ImportedName' n m
ImportedName [Name]
ys0
ms :: [ImportedName]
ms = (Name -> ImportedName) -> [Name] -> [ImportedName]
forall a b. (a -> b) -> [a] -> [b]
map Name -> ImportedName
forall n m. m -> ImportedName' n m
ImportedModule [Name]
ms0
([Name]
ys0, [Name]
ms0) = [ImportedName] -> ([Name], [Name])
forall n m. [ImportedName' n m] -> ([n], [m])
partitionImportedNames [ImportedName]
xs
suggestion :: [Name] -> ImportedName' b b -> m Doc
suggestion [Name]
zs = m Doc -> (m Doc -> m Doc) -> Maybe (m Doc) -> m Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m Doc
forall a. Null a => a
empty m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (Maybe (m Doc) -> m Doc)
-> (ImportedName' b b -> Maybe (m Doc))
-> ImportedName' b b
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [QName]
-> (ImportedName' b b -> b) -> ImportedName' b b -> Maybe (m Doc)
forall (m :: * -> *) a b.
(MonadPretty m, Pretty a, Pretty b) =>
[QName] -> (a -> b) -> a -> Maybe (m Doc)
didYouMean ((Name -> QName) -> [Name] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map Name -> QName
C.QName [Name]
zs) ImportedName' b b -> b
forall a. ImportedName' a a -> a
fromImportedName
DuplicateUsing List1 ImportedName
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Duplicates in `using` directive:" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ (ImportedName -> m Doc) -> [ImportedName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ImportedName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (List1 ImportedName -> [Item (List1 ImportedName)]
forall l. IsList l => l -> [Item l]
List1.toList List1 ImportedName
xs)
FixityInRenamingModule List1 Range
_rs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Modules do not have fixity"
LibraryWarning LibWarning
lw -> LibWarning -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty LibWarning
lw
InfectiveImport Doc
msg -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
msg
CoInfectiveImport Doc
msg -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
msg
IllegalRewriteRule QName
q IllegalRewriteRuleReason
reason -> case IllegalRewriteRuleReason
reason of
IllegalRewriteRuleReason
LHSNotDefinitionOrConstructor -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q , m Doc
" is not a legal rewrite rule, since the left-hand side is neither a defined symbol nor a constructor" ]
VariablesNotBoundByLHS IntSet
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q
, m Doc
" is not a legal rewrite rule, since the following variables are not bound by the left hand side: "
, [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((VerboseLevel -> m Doc) -> [VerboseLevel] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> m Doc) -> (VerboseLevel -> Term) -> VerboseLevel -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> Term
var) ([VerboseLevel] -> [m Doc]) -> [VerboseLevel] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ IntSet -> [VerboseLevel]
IntSet.toList IntSet
xs)
]
VariablesBoundMoreThanOnce IntSet
xs -> do
(QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
" is not a legal rewrite rule, since the following parameters are bound more than once on the left hand side: "
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep (m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
List.intersperse m Doc
"," ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ (VerboseLevel -> m Doc) -> [VerboseLevel] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> m Doc) -> (VerboseLevel -> Term) -> VerboseLevel -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> Term
var) ([VerboseLevel] -> [m Doc]) -> [VerboseLevel] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ IntSet -> [VerboseLevel]
IntSet.toList IntSet
xs))
m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
". Perhaps you can use a postulate instead of a constructor as the head symbol?"
LHSReduces Term
v Term
v' -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
" is not a legal rewrite rule, since the left-hand side "
, Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
" reduces to " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v' ]
HeadSymbolIsProjection QName
f -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q , m Doc
" is not a legal rewrite rule, since the head symbol"
, QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f , m Doc
"is a projection"
]
HeadSymbolIsProjectionLikeFunction QName
f -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q , m Doc
" is not a legal rewrite rule, since the head symbol"
, m Doc
hd , m Doc
"is a projection-like function."
, m Doc
"You can turn off the projection-like optimization for", m Doc
hd
, m Doc
"with the pragma {-# NOT_PROJECTION_LIKE", m Doc
hd, m Doc
"#-}"
, m Doc
"or globally with the flag --no-projection-like"
]
where hd :: m Doc
hd = QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f
HeadSymbolIsTypeConstructor QName
f -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q , m Doc
" is not a legal rewrite rule, since the head symbol"
, QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f , m Doc
"is a type constructor."
]
HeadSymbolContainsMetas QName
f -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q , m Doc
"is not a legal rewrite rule, since the definition of the head symbol"
, QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f , m Doc
"contains unsolved metavariables and confluence checking is enabled."
]
ConstructorParametersNotGeneral ConHead
c Args
vs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
" is not a legal rewrite rule, since the constructor parameters are not fully general:"
, VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Constructor: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c
, VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Parameters: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Arg Term -> m Doc) -> Args -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Args
vs)
]
ContainsUnsolvedMetaVariables Set MetaId
ms -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q , m Doc
" is not a legal rewrite rule, since"
, m Doc
"it contains the unsolved meta variable(s)", [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((MetaId -> m Doc) -> [MetaId] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map MetaId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM ([MetaId] -> [m Doc]) -> [MetaId] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList Set MetaId
ms)
]
BlockedOnProblems Set ProblemId
ps -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q , m Doc
" is not a legal rewrite rule, since"
, m Doc
"it is blocked on problem(s)", [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((ProblemId -> m Doc) -> [ProblemId] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ProblemId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ProblemId -> m Doc
prettyTCM ([ProblemId] -> [m Doc]) -> [ProblemId] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList Set ProblemId
ps)
]
RequiresDefinitions Set QName
qs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q , m Doc
" is not a legal rewrite rule, since"
, m Doc
"it requires the definition(s) of", [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((QName -> m Doc) -> [QName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM ([QName] -> [m Doc]) -> [QName] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
qs)
]
IllegalRewriteRuleReason
DoesNotTargetRewriteRelation -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q , m Doc
" does not target rewrite relation" ]
IllegalRewriteRuleReason
BeforeFunctionDefinition -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ m Doc
"Rewrite rule from function "
, QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q
, m Doc
" cannot be added before the function definition"
]
BeforeMutualFunctionDefinition QName
r -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ m Doc
"Rewrite rule from function "
, QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q
, m Doc
" cannot be added before the definition of mutually defined"
, QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
r
]
IllegalRewriteRuleReason
DuplicateRewriteRule ->
m Doc
"Rewrite rule " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
" has already been added"
ConfluenceCheckingIncompleteBecauseOfMeta QName
f -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ m Doc
"Confluence checking incomplete because the definition of"
, QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f
, [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"contains unsolved metavariables."
]
Warning
ConfluenceForCubicalNotSupported -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
[Char]
"Confluence checking for --cubical is not yet supported, confluence checking might be incomplete"
RewriteNonConfluent Term
lhs Term
rhs1 Term
rhs2 Doc
err -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ m Doc
"Local confluence check failed:"
, Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs , m Doc
"reduces to both"
, Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs1 , m Doc
"and" , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs2
, m Doc
"which are not equal because"
, Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
err
]
RewriteMaybeNonConfluent Term
lhs1 Term
lhs2 [Doc]
cs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Couldn't determine overlap between left-hand sides"
, [ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs1 , [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"and" , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs2 ]
, [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because of unsolved constraints:"
]
]
, (Doc -> m Doc) -> [Doc] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> (Doc -> m Doc) -> Doc -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return) [Doc]
cs
]
RewriteAmbiguousRules Term
lhs Term
rhs1 Term
rhs2 -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ ( [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Global confluence check failed:" , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs]
, [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"can be rewritten to either" , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs1]
, [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"or" , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs2 m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
])
, [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Possible fix: add a rewrite rule with left-hand side"
, [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs] , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"to resolve the ambiguity."
]
]
RewriteMissingRule Term
u Term
v Term
rhou -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Global confluence check failed:" , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u]
, [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"unfolds to" , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v] , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which should further unfold to"
, [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhou] , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"but it does not."
]
, [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Possible fix: add a rule to rewrite"
, [ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v , m Doc
"to" , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhou ]
]
]
DuplicateRecordDirective RecordDirective
dir ->
m Doc
"Ignoring duplicate record directive: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> RecordDirective -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty RecordDirective
dir
PragmaCompileErased [Char]
bn QName
qn -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The backend"
, [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
bn
, m Doc
"erases"
, QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
qn
]
, [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"so the COMPILE pragma will be ignored."
]
Warning
PragmaCompileList -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords
[Char]
"Ignoring GHC pragma for builtin lists; they always compile to Haskell lists."
Warning
PragmaCompileMaybe -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords
[Char]
"Ignoring GHC pragma for builtin MAYBE; it always compiles to Haskell Maybe."
NoMain TopLevelModuleName
topLevelModule -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"No main function defined in" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [TopLevelModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TopLevelModuleName -> m Doc
prettyTCM TopLevelModuleName
topLevelModule m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
, [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Use option --no-main to suppress this warning."
]
NotInScopeW [QName]
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Not in scope:"
, do
inscope <- Set QName -> [QName]
forall a. Set a -> [a]
Set.toList (Set QName -> [QName])
-> (ScopeInfo -> Set QName) -> ScopeInfo -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> Set QName
concreteNamesInScope (ScopeInfo -> [QName]) -> m ScopeInfo -> m [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
prettyNotInScopeNames True (suggestion inscope) xs
]
where
suggestion :: [QName] -> QName -> m Doc
suggestion [QName]
inscope QName
x = VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall {m :: * -> *}.
(Null (m Doc), Applicative m) =>
[m Doc] -> m Doc
par ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [ m Doc
"did you forget space around the ':'?" | Char
':' Char -> [Char] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char]
s ]
, [ m Doc
"did you forget space around the '->'?" | [Char]
"->" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isInfixOf` [Char]
s ]
, Maybe (m Doc) -> [m Doc]
forall a. Maybe a -> [a]
maybeToList (Maybe (m Doc) -> [m Doc]) -> Maybe (m Doc) -> [m Doc]
forall a b. (a -> b) -> a -> b
$ [QName] -> (QName -> Name) -> QName -> Maybe (m Doc)
forall (m :: * -> *) a b.
(MonadPretty m, Pretty a, Pretty b) =>
[QName] -> (a -> b) -> a -> Maybe (m Doc)
didYouMean [QName]
inscope QName -> Name
C.unqualify QName
x
]
where
par :: [m Doc] -> m Doc
par [] = m Doc
forall a. Null a => a
empty
par [m Doc
d] = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens m Doc
d
par [m Doc]
ds = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [m Doc]
ds
s :: [Char]
s = QName -> [Char]
forall a. Pretty a => a -> [Char]
P.prettyShow QName
x
AsPatternShadowsConstructorOrPatternSynonym LHSOrPatSyn
patsyn -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Name bound in @-pattern ignored because it shadows"
, case LHSOrPatSyn
patsyn of
LHSOrPatSyn
IsPatSyn -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"pattern synonym"
LHSOrPatSyn
IsLHS -> [ m Doc
"constructor" ]
]
PatternShadowsConstructor Name
x QName
c -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The pattern variable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM Name
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has the same name as the constructor" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c]
PlentyInHardCompileTimeMode QωOrigin
o -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ignored use of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QωOrigin -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QωOrigin
o] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in hard compile-time mode"
RecordFieldWarning RecordFieldWarning
w -> RecordFieldWarning -> m Doc
forall (m :: * -> *). MonadPretty m => RecordFieldWarning -> m Doc
prettyRecordFieldWarning RecordFieldWarning
w
MissingTypeSignatureForOpaque QName
name IsOpaque
isOpaque -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ m Doc
"Missing type signature for" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
what m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"definition" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
name m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
".")
, [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
[Char]
"Types of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
what [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" definitions are never inferred since this would leak " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
"information that should be " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
what [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"."
]
where
what :: [Char]
what = case IsOpaque
isOpaque of
IsOpaque
TransparentDef -> [Char]
"abstract"
OpaqueDef OpaqueId
_ -> [Char]
"opaque"
Warning
NotAffectedByOpaque -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Only function definitions can be marked opaque. This definition will be treated as transparent."
UnfoldTransparentName QName
qn -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The name" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
qn m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
","] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"mentioned by an unfolding clause, does not belong to an opaque block. This has no effect."
Warning
UselessOpaque -> m Doc
"This `opaque` block has no effect."
FaceConstraintCannotBeHidden ArgInfo
ai -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Face constraint patterns cannot be" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ Hiding -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
ai), m Doc
"arguments"]
FaceConstraintCannotBeNamed NamedName
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ignoring name" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [m Doc
"`" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> NamedName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty NamedName
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"`"] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"given to face constraint pattern"
CustomBackendWarning [Char]
backend Doc
warn -> ([Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
backend m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
":") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
warn
{-# SPECIALIZE prettyRecordFieldWarning :: RecordFieldWarning -> TCM Doc #-}
prettyRecordFieldWarning :: MonadPretty m => RecordFieldWarning -> m Doc
prettyRecordFieldWarning :: forall (m :: * -> *). MonadPretty m => RecordFieldWarning -> m Doc
prettyRecordFieldWarning = \case
W.DuplicateFields [(Name, Range)]
xrs -> [Name] -> m Doc
forall (m :: * -> *). MonadPretty m => [Name] -> m Doc
prettyDuplicateFields ([Name] -> m Doc) -> [Name] -> m Doc
forall a b. (a -> b) -> a -> b
$ ((Name, Range) -> Name) -> [(Name, Range)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Range) -> Name
forall a b. (a, b) -> a
fst [(Name, Range)]
xrs
W.TooManyFields QName
q [Name]
ys [(Name, Range)]
xrs -> QName -> [Name] -> [Name] -> m Doc
forall (m :: * -> *).
MonadPretty m =>
QName -> [Name] -> [Name] -> m Doc
prettyTooManyFields QName
q [Name]
ys ([Name] -> m Doc) -> [Name] -> m Doc
forall a b. (a -> b) -> a -> b
$ ((Name, Range) -> Name) -> [(Name, Range)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Range) -> Name
forall a b. (a, b) -> a
fst [(Name, Range)]
xrs
prettyDuplicateFields :: MonadPretty m => [C.Name] -> m Doc
prettyDuplicateFields :: forall (m :: * -> *). MonadPretty m => [Name] -> m Doc
prettyDuplicateFields [Name]
xs = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Duplicate"
, [Name] -> [m Doc]
forall {a} {m :: * -> *}. (Sized a, Applicative m) => a -> [m Doc]
fields [Name]
xs
, m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Applicative m => m Doc
comma ((Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
xs)
, [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in record"
]
where
fields :: a -> [m Doc]
fields a
ys = a -> [m Doc] -> [m Doc] -> [m Doc]
forall a c. Sized a => a -> c -> c -> c
P.singPlural a
ys [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"field"] [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"fields"]
{-# SPECIALIZE prettyTooManyFields :: QName -> [C.Name] -> [C.Name] -> TCM Doc #-}
prettyTooManyFields :: MonadPretty m => QName -> [C.Name] -> [C.Name] -> m Doc
prettyTooManyFields :: forall (m :: * -> *).
MonadPretty m =>
QName -> [Name] -> [Name] -> m Doc
prettyTooManyFields QName
r [Name]
missing [Name]
xs = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The record type"
, [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
r]
, [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"does not have the"
, [Name] -> [m Doc]
forall {a} {m :: * -> *}. (Sized a, Applicative m) => a -> [m Doc]
fields [Name]
xs
, m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Applicative m => m Doc
comma ((Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
xs)
, if [Name] -> Bool
forall a. Null a => a -> Bool
null [Name]
missing then [] else [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"but it would have the"
, [Name] -> [m Doc]
forall {a} {m :: * -> *}. (Sized a, Applicative m) => a -> [m Doc]
fields [Name]
missing
, m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Applicative m => m Doc
comma ((Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
missing)
]
]
where
fields :: a -> [m Doc]
fields a
ys = a -> [m Doc] -> [m Doc] -> [m Doc]
forall a c. Sized a => a -> c -> c -> c
P.singPlural a
ys [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"field"] [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"fields"]
{-# SPECIALIZE prettyNotInScopeNames :: (Pretty a, HasRange a) => Bool -> (a -> TCM Doc) -> [a] -> TCM Doc #-}
prettyNotInScopeNames
:: (MonadPretty m, Pretty a, HasRange a)
=> Bool
-> (a -> m Doc)
-> [a]
-> m Doc
prettyNotInScopeNames :: forall (m :: * -> *) a.
(MonadPretty m, Pretty a, HasRange a) =>
Bool -> (a -> m Doc) -> [a] -> m Doc
prettyNotInScopeNames Bool
printRange a -> m Doc
suggestion [a]
xs = VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (a -> m Doc) -> [a] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> m Doc
name [a]
xs
where
name :: a -> m Doc
name a
x = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ a -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty a
x
, if Bool
printRange then m Doc
"at" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM (a -> Range
forall a. HasRange a => a -> Range
getRange a
x) else m Doc
forall a. Null a => a
empty
, a -> m Doc
suggestion a
x
]
{-# SPECIALIZE didYouMean :: (Pretty a, Pretty b) => [C.QName] -> (a -> b) -> a -> Maybe (TCM Doc) #-}
didYouMean
:: (MonadPretty m, Pretty a, Pretty b)
=> [C.QName]
-> (a -> b)
-> a
-> Maybe (m Doc)
didYouMean :: forall (m :: * -> *) a b.
(MonadPretty m, Pretty a, Pretty b) =>
[QName] -> (a -> b) -> a -> Maybe (m Doc)
didYouMean [QName]
inscope a -> b
canon a
x
| [[Char]] -> Bool
forall a. Null a => a -> Bool
null [[Char]]
ys = Maybe (m Doc)
forall a. Maybe a
Nothing
| Bool
otherwise = m Doc -> Maybe (m Doc)
forall a. a -> Maybe a
Just (m Doc -> Maybe (m Doc)) -> m Doc -> Maybe (m Doc)
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ m Doc
"did you mean"
, VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
" or" ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
([Char] -> m Doc) -> [[Char]] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ [Char]
y -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"'" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
y [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"'") [[Char]]
ys)
m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"?"
]
where
strip :: Pretty b => b -> String
strip :: forall a. Pretty a => a -> [Char]
strip = (Char -> Char) -> [Char] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower ([Char] -> [Char]) -> (b -> [Char]) -> b -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'_') ([Char] -> [Char]) -> (b -> [Char]) -> b -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow
maxDist :: a -> a
maxDist a
n = a -> a -> a
forall a. Integral a => a -> a -> a
div a
n a
3
close :: [a] -> [a] -> Bool
close [a]
a [a]
b = [a] -> [a] -> VerboseLevel
forall a. Eq a => [a] -> [a] -> VerboseLevel
editDistance [a]
a [a]
b VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel -> VerboseLevel
forall {a}. Integral a => a -> a
maxDist ([a] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [a]
a)
ys :: [[Char]]
ys = (QName -> [Char]) -> [QName] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ([QName] -> [[Char]]) -> [QName] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (QName -> Bool) -> [QName] -> [QName]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
close (b -> [Char]
forall a. Pretty a => a -> [Char]
strip (b -> [Char]) -> b -> [Char]
forall a b. (a -> b) -> a -> b
$ a -> b
canon a
x) ([Char] -> Bool) -> (QName -> [Char]) -> QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
forall a. Pretty a => a -> [Char]
strip (Name -> [Char]) -> (QName -> Name) -> QName -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
C.unqualify) [QName]
inscope
prettyTCWarnings :: [TCWarning] -> TCM String
prettyTCWarnings :: [TCWarning] -> TCM [Char]
prettyTCWarnings = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"\n" ([[Char]] -> [Char])
-> ([TCWarning] -> TCMT IO [[Char]]) -> [TCWarning] -> TCM [Char]
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> (Doc -> [Char]) -> [Doc] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> [Char]
forall a. Doc a -> [Char]
P.render ([Doc] -> [[Char]])
-> ([TCWarning] -> TCMT IO [Doc])
-> [TCWarning]
-> TCMT IO [[Char]]
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> [TCWarning] -> TCMT IO [Doc]
prettyTCWarnings'
prettyTCWarnings' :: [TCWarning] -> TCM [Doc]
prettyTCWarnings' :: [TCWarning] -> TCMT IO [Doc]
prettyTCWarnings' = (TCWarning -> TCMT IO Doc) -> [TCWarning] -> TCMT IO [Doc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM ([TCWarning] -> TCMT IO [Doc])
-> ([TCWarning] -> [TCWarning]) -> [TCWarning] -> TCMT IO [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> [TCWarning]
filterTCWarnings
filterTCWarnings :: [TCWarning] -> [TCWarning]
filterTCWarnings :: [TCWarning] -> [TCWarning]
filterTCWarnings = \case
[TCWarning
w] -> [TCWarning
w]
[TCWarning]
ws -> ((TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
`filter` [TCWarning]
ws) ((TCWarning -> Bool) -> [TCWarning])
-> (TCWarning -> Bool) -> [TCWarning]
forall a b. (a -> b) -> a -> b
$ \ TCWarning
w -> case TCWarning -> Warning
tcWarning TCWarning
w of
UnsolvedConstraints Constraints
cs -> (ProblemConstraint -> Bool) -> Constraints -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ProblemConstraint -> Bool
interestingConstraint Constraints
cs
Warning
_ -> Bool
True
tcWarningsToError :: [TCWarning] -> TCM ()
tcWarningsToError :: [TCWarning] -> TCM ()
tcWarningsToError [TCWarning]
mws = case ([TCWarning]
unsolvedHoles, [TCWarning]
otherWarnings) of
([], []) -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(_unsolvedHoles :: [TCWarning]
_unsolvedHoles@(TCWarning
_:[TCWarning]
_), []) -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
SolvedButOpenHoles
([TCWarning]
_, ws :: [TCWarning]
ws@(TCWarning
_:[TCWarning]
_)) -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCWarning] -> TypeError
NonFatalErrors [TCWarning]
ws
where
([TCWarning]
unsolvedHoles, [TCWarning]
otherWarnings) = (TCWarning -> Bool) -> [TCWarning] -> ([TCWarning], [TCWarning])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (Warning -> Bool
isUnsolvedIM (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) [TCWarning]
mws
isUnsolvedIM :: Warning -> Bool
isUnsolvedIM UnsolvedInteractionMetas{} = Bool
True
isUnsolvedIM Warning
_ = Bool
False
applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> [TCWarning] -> m [TCWarning]
applyFlagsToTCWarningsPreserving :: forall (m :: * -> *).
HasOptions m =>
Set WarningName -> [TCWarning] -> m [TCWarning]
applyFlagsToTCWarningsPreserving Set WarningName
additionalKeptWarnings [TCWarning]
ws = do
let pragmas :: TCWarning -> ([TCWarning], [[Char]])
pragmas TCWarning
w = case TCWarning -> Warning
tcWarning TCWarning
w of { SafeFlagPragma [[Char]]
ps -> ([TCWarning
w], [[Char]]
ps); Warning
_ -> ([], []) }
let sfp :: [TCWarning]
sfp = case ([[Char]] -> [[Char]])
-> ([TCWarning], [[Char]]) -> ([TCWarning], [[Char]])
forall a b. (a -> b) -> ([TCWarning], a) -> ([TCWarning], b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Char]] -> [[Char]]
forall a. Eq a => [a] -> [a]
List.nub ((TCWarning -> ([TCWarning], [[Char]]))
-> [TCWarning] -> ([TCWarning], [[Char]])
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TCWarning -> ([TCWarning], [[Char]])
pragmas [TCWarning]
ws) of
(TCWarning CallStack
loc Range
r Warning
w Doc
p Bool
b:[TCWarning]
_, [[Char]]
sfp) ->
[CallStack -> Range -> Warning -> Doc -> Bool -> TCWarning
TCWarning CallStack
loc Range
r ([[Char]] -> Warning
SafeFlagPragma [[Char]]
sfp) Doc
p Bool
b]
([TCWarning], [[Char]])
_ -> []
pragmaWarnings <- (WarningMode
-> Lens' WarningMode (Set WarningName) -> Set WarningName
forall o i. o -> Lens' o i -> i
^. (Set WarningName -> f (Set WarningName))
-> WarningMode -> f WarningMode
Lens' WarningMode (Set WarningName)
warningSet) (WarningMode -> Set WarningName)
-> (PragmaOptions -> WarningMode)
-> PragmaOptions
-> Set WarningName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WarningMode
optWarningMode (PragmaOptions -> Set WarningName)
-> m PragmaOptions -> m (Set WarningName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
let warnSet = Set WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set WarningName
pragmaWarnings Set WarningName
additionalKeptWarnings
let cleanUp Warning
w = let wName :: WarningName
wName = Warning -> WarningName
warningName Warning
w in
WarningName
wName WarningName -> WarningName -> Bool
forall a. Eq a => a -> a -> Bool
/= WarningName
SafeFlagPragma_
Bool -> Bool -> Bool
&& WarningName
wName WarningName -> Set WarningName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set WarningName
warnSet
Bool -> Bool -> Bool
&& case Warning
w of
UnsolvedMetaVariables [Range]
ums -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Range] -> Bool
forall a. Null a => a -> Bool
null [Range]
ums
UnsolvedInteractionMetas [Range]
uis -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Range] -> Bool
forall a. Null a => a -> Bool
null [Range]
uis
UnsolvedConstraints Constraints
ucs -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Constraints -> Bool
forall a. Null a => a -> Bool
null Constraints
ucs
Warning
_ -> Bool
True
return $ sfp ++ filter (cleanUp . tcWarning) ws
applyFlagsToTCWarnings :: HasOptions m => [TCWarning] -> m [TCWarning]
applyFlagsToTCWarnings :: forall (m :: * -> *). HasOptions m => [TCWarning] -> m [TCWarning]
applyFlagsToTCWarnings = Set WarningName -> [TCWarning] -> m [TCWarning]
forall (m :: * -> *).
HasOptions m =>
Set WarningName -> [TCWarning] -> m [TCWarning]
applyFlagsToTCWarningsPreserving Set WarningName
forall a. Set a
Set.empty
{-# SPECIALIZE isBoundaryConstraint :: ProblemConstraint -> TCM (Maybe Range) #-}
isBoundaryConstraint :: (ReadTCState m, MonadTCM m) => ProblemConstraint -> m (Maybe Range)
isBoundaryConstraint :: forall (m :: * -> *).
(ReadTCState m, MonadTCM m) =>
ProblemConstraint -> m (Maybe Range)
isBoundaryConstraint ProblemConstraint
c =
Closure Constraint
-> (Constraint -> m (Maybe Range)) -> m (Maybe Range)
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure (ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c) ((Constraint -> m (Maybe Range)) -> m (Maybe Range))
-> (Constraint -> m (Maybe Range)) -> m (Maybe Range)
forall a b. (a -> b) -> a -> b
$ \case
ValueCmp Comparison
_ CompareAs
_ (MetaV MetaId
mid Elims
xs) Term
y | Just Args
xs <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
xs ->
((MetaVariable, IntMap Bool, SubstCand, Substitution) -> Range)
-> Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution)
-> Maybe Range
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (MetaVariable, IntMap Bool, SubstCand, Substitution) -> Range
forall {a} {b} {c} {d}. HasRange a => (a, b, c, d) -> Range
g (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution)
-> Maybe Range)
-> m (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
-> m (Maybe Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
-> m (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
forall a. TCM a -> m a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (MetaId
-> Args
-> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
isFaceConstraint MetaId
mid Args
xs)
ValueCmp Comparison
_ CompareAs
_ Term
y (MetaV MetaId
mid Elims
xs) | Just Args
xs <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
xs ->
((MetaVariable, IntMap Bool, SubstCand, Substitution) -> Range)
-> Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution)
-> Maybe Range
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (MetaVariable, IntMap Bool, SubstCand, Substitution) -> Range
forall {a} {b} {c} {d}. HasRange a => (a, b, c, d) -> Range
g (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution)
-> Maybe Range)
-> m (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
-> m (Maybe Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
-> m (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
forall a. TCM a -> m a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (MetaId
-> Args
-> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
isFaceConstraint MetaId
mid Args
xs)
Constraint
_ -> Maybe Range -> m (Maybe Range)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Range
forall a. Maybe a
Nothing
where
g :: (a, b, c, d) -> Range
g (a
a, b
_, c
_, d
_) = a -> Range
forall a. HasRange a => a -> Range
getRange a
a
{-# SPECIALIZE getAllUnsolvedWarnings :: TCM [TCWarning] #-}
getAllUnsolvedWarnings :: (MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) => m [TCWarning]
getAllUnsolvedWarnings :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
m [TCWarning]
getAllUnsolvedWarnings = do
unsolvedInteractions <- m [Range]
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
m [Range]
getUnsolvedInteractionMetas
allCons <- getAllConstraints
unsolvedConstraints <- filterM (fmap isNothing . isBoundaryConstraint) allCons
interactionBoundary <- catMaybes <$> traverse isBoundaryConstraint allCons
unsolvedMetas <- getUnsolvedMetas
let checkNonEmpty a -> a
c a
rs = a -> a
c a
rs a -> f () -> f a
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> f ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a -> Bool
forall a. Null a => a -> Bool
null a
rs)
mapM warning_ $ catMaybes
[ checkNonEmpty UnsolvedInteractionMetas unsolvedInteractions
, checkNonEmpty UnsolvedMetaVariables unsolvedMetas
, checkNonEmpty UnsolvedConstraints unsolvedConstraints
, checkNonEmpty InteractionMetaBoundaries interactionBoundary
]
{-# SPECIALIZE getAllWarnings :: WhichWarnings -> TCM [TCWarning] #-}
getAllWarnings :: (MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) => WhichWarnings -> m [TCWarning]
getAllWarnings :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings = Set WarningName -> WhichWarnings -> m [TCWarning]
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
Set WarningName -> WhichWarnings -> m [TCWarning]
getAllWarningsPreserving Set WarningName
forall a. Set a
Set.empty
{-# SPECIALIZE getAllWarningsPreserving :: Set WarningName -> WhichWarnings -> TCM [TCWarning] #-}
getAllWarningsPreserving ::
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) => Set WarningName -> WhichWarnings -> m [TCWarning]
getAllWarningsPreserving :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
Set WarningName -> WhichWarnings -> m [TCWarning]
getAllWarningsPreserving Set WarningName
keptWarnings WhichWarnings
ww = do
unsolved <- m [TCWarning]
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
m [TCWarning]
getAllUnsolvedWarnings
collectedTCWarnings <- useTC stTCWarnings
let showWarn Warning
w = Warning -> WhichWarnings
classifyWarning Warning
w WhichWarnings -> WhichWarnings -> Bool
forall a. Ord a => a -> a -> Bool
<= WhichWarnings
ww Bool -> Bool -> Bool
&&
Bool -> Bool
not ([TCWarning] -> Bool
forall a. Null a => a -> Bool
null [TCWarning]
unsolved Bool -> Bool -> Bool
&& Warning -> Bool
onlyShowIfUnsolved Warning
w)
fmap (filter (showWarn . tcWarning))
$ applyFlagsToTCWarningsPreserving keptWarnings
$ reverse $ unsolved ++ collectedTCWarnings
getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]
getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]
getAllWarningsOfTCErr TCErr
err = case TCErr
err of
TypeError CallStack
_ TCState
tcst Closure TypeError
cls -> case Closure TypeError -> TypeError
forall a. Closure a -> a
clValue Closure TypeError
cls of
NonFatalErrors{} -> [TCWarning] -> TCM [TCWarning]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
TypeError
_ -> TCM [TCWarning] -> TCM [TCWarning]
forall a. TCM a -> TCM a
localTCState (TCM [TCWarning] -> TCM [TCWarning])
-> TCM [TCWarning] -> TCM [TCWarning]
forall a b. (a -> b) -> a -> b
$ do
TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
tcst
ws <- WhichWarnings -> TCM [TCWarning]
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
return $ filter (not . isUnsolvedWarning . tcWarning) ws
TCErr
_ -> [TCWarning] -> TCM [TCWarning]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []