module Agda.TypeChecking.Pretty.Warning where

import Prelude hiding ( null )

import Data.Char ( toLower )
import Data.Function
import qualified Data.Set as Set
import qualified Data.List as List

import Agda.TypeChecking.Monad.Base
import {-# SOURCE #-} Agda.TypeChecking.Errors
import Agda.TypeChecking.Monad.MetaVars
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.State ( getScope )
import Agda.TypeChecking.Positivity () --instance only
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Pretty.Call

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 {-# SOURCE #-} Agda.Interaction.Imports
import Agda.Interaction.Options
import Agda.Interaction.Options.Warnings

import Agda.Utils.Lens
import Agda.Utils.List ( editDistance )
import Agda.Utils.Null
import qualified Agda.Utils.Pretty as P

instance PrettyTCM TCWarning where
  prettyTCM :: TCWarning -> m Doc
prettyTCM = Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> m Doc) -> (TCWarning -> Doc) -> TCWarning -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Doc
tcWarningPrintedWarning

instance PrettyTCM Warning where
  prettyTCM :: Warning -> m Doc
prettyTCM = Warning -> m Doc
forall (m :: * -> *). MonadPretty m => Warning -> m Doc
prettyWarning

prettyConstraint :: MonadPretty m => ProblemConstraint -> m Doc
prettyConstraint :: ProblemConstraint -> m Doc
prettyConstraint ProblemConstraint
c = m Doc -> m Doc
forall (m :: * -> *). MonadPretty m => m Doc -> m Doc
f (Lens' Bool TCState -> (Bool -> Bool) -> m Doc -> m Doc
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> m b -> m b
locallyTCState Lens' Bool TCState
stInstantiateBlocking (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ ProblemConstraint -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ProblemConstraint
c)
  where
    r :: Range
r   = ProblemConstraint -> Range
forall t. HasRange t => t -> Range
getRange ProblemConstraint
c
    f :: MonadPretty m => m Doc -> m Doc
    f :: m Doc -> m Doc
f m Doc
d = if Doc -> Bool
forall a. Null a => a -> Bool
null (Doc -> Bool) -> Doc -> Bool
forall a b. (a -> b) -> a -> b
$ Range -> Doc
forall a. Pretty a => a -> Doc
P.pretty Range
r
          then m Doc
d
          else m Doc
d m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 (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
prettyTCM Range
r m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"]")

interestingConstraint :: ProblemConstraint -> Bool
interestingConstraint :: ProblemConstraint -> Bool
interestingConstraint ProblemConstraint
pc = Constraint -> Bool
go (Constraint -> Bool) -> Constraint -> Bool
forall a b. (a -> b) -> a -> b
$ Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
pc)
  where
    go :: Constraint -> Bool
go UnBlock{}     = Bool
False
    go (Guarded Constraint
c ProblemId
_) = Constraint -> Bool
go Constraint
c
    go Constraint
_             = Bool
True

prettyInterestingConstraints :: MonadPretty m => [ProblemConstraint] -> m [Doc]
prettyInterestingConstraints :: [ProblemConstraint] -> m [Doc]
prettyInterestingConstraints [ProblemConstraint]
cs = (ProblemConstraint -> m Doc) -> [ProblemConstraint] -> m [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ProblemConstraint -> m Doc
forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Doc
prettyConstraint (ProblemConstraint -> m Doc)
-> (ProblemConstraint -> ProblemConstraint)
-> ProblemConstraint
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> ProblemConstraint
stripPids) ([ProblemConstraint] -> m [Doc]) -> [ProblemConstraint] -> m [Doc]
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint -> ProblemConstraint -> Ordering)
-> [ProblemConstraint] -> [ProblemConstraint]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Bool -> Bool -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Bool -> Bool -> Ordering)
-> (ProblemConstraint -> Bool)
-> ProblemConstraint
-> ProblemConstraint
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ProblemConstraint -> Bool
isBlocked) [ProblemConstraint]
cs'
  where
    isBlocked :: ProblemConstraint -> Bool
isBlocked = Bool -> Bool
not (Bool -> Bool)
-> (ProblemConstraint -> Bool) -> ProblemConstraint -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ProblemId] -> Bool
forall a. Null a => a -> Bool
null ([ProblemId] -> Bool)
-> (ProblemConstraint -> [ProblemId]) -> ProblemConstraint -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> [ProblemId]
blocking (Constraint -> [ProblemId])
-> (ProblemConstraint -> Constraint)
-> ProblemConstraint
-> [ProblemId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (Closure Constraint -> Constraint)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint
    cs' :: [ProblemConstraint]
cs' = (ProblemConstraint -> Bool)
-> [ProblemConstraint] -> [ProblemConstraint]
forall a. (a -> Bool) -> [a] -> [a]
filter ProblemConstraint -> Bool
interestingConstraint [ProblemConstraint]
cs
    interestingPids :: Set ProblemId
interestingPids = [ProblemId] -> Set ProblemId
forall a. Ord a => [a] -> Set a
Set.fromList ([ProblemId] -> Set ProblemId) -> [ProblemId] -> Set ProblemId
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint -> [ProblemId])
-> [ProblemConstraint] -> [ProblemId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Constraint -> [ProblemId]
blocking (Constraint -> [ProblemId])
-> (ProblemConstraint -> Constraint)
-> ProblemConstraint
-> [ProblemId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (Closure Constraint -> Constraint)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) [ProblemConstraint]
cs'
    stripPids :: ProblemConstraint -> ProblemConstraint
stripPids (PConstr Set ProblemId
pids Closure Constraint
c) = Set ProblemId -> Closure Constraint -> ProblemConstraint
PConstr (Set ProblemId -> Set ProblemId -> Set ProblemId
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set ProblemId
pids Set ProblemId
interestingPids) Closure Constraint
c
    blocking :: Constraint -> [ProblemId]
blocking (Guarded Constraint
c ProblemId
pid) = ProblemId
pid ProblemId -> [ProblemId] -> [ProblemId]
forall a. a -> [a] -> [a]
: Constraint -> [ProblemId]
blocking Constraint
c
    blocking Constraint
_               = []

{-# SPECIALIZE prettyWarning :: Warning -> TCM Doc #-}
prettyWarning :: MonadPretty m => Warning -> m Doc
prettyWarning :: Warning -> m Doc
prettyWarning Warning
wng = case Warning
wng of

    UnsolvedMetaVariables [Range]
ms  ->
      [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ( String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Unsolved metas at the following locations:" )
      m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *). Monad m => [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
prettyTCM [Range]
ms)

    UnsolvedInteractionMetas [Range]
is ->
      [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ( String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Unsolved interaction metas at the following locations:" )
      m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *). Monad m => [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
prettyTCM [Range]
is)

    UnsolvedConstraints [ProblemConstraint]
cs -> do
      [Doc]
pcs <- [ProblemConstraint] -> m [Doc]
forall (m :: * -> *).
MonadPretty m =>
[ProblemConstraint] -> m [Doc]
prettyInterestingConstraints [ProblemConstraint]
cs
      if [Doc] -> Bool
forall a. Null a => a -> Bool
null [Doc]
pcs
        then [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Unsolved constraints"  -- #4065: keep minimal warning text
        else [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
          [ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Failed to solve the following constraints:"
          , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
P.vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> [Doc]
forall a. Eq a => [a] -> [a]
List.nub [Doc]
pcs
          ]

    TerminationIssue [TerminationError]
because -> do
      QName -> QName
dropTopLevel <- m (QName -> QName)
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
m (QName -> QName)
topLevelModuleDropper
      String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords String
"Termination checking failed for the following functions:"
        m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ (Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Monad m => m Doc
comma ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
             (QName -> m Doc) -> [QName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (QName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty (QName -> m Doc) -> (QName -> QName) -> QName -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> QName
dropTopLevel) ([QName] -> [m Doc]) -> [QName] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
               (TerminationError -> [QName]) -> [TerminationError] -> [QName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TerminationError -> [QName]
termErrFunctions [TerminationError]
because)
        m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords String
"Problematic calls:"
        m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ (Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Doc] -> Doc
P.vcat ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> [Doc]
forall a. Eq a => [a] -> [a]
List.nub) (m [Doc] -> m Doc) -> m [Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
              (CallInfo -> m Doc) -> [CallInfo] -> m [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CallInfo -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([CallInfo] -> m [Doc]) -> [CallInfo] -> m [Doc]
forall a b. (a -> b) -> a -> b
$ (CallInfo -> CallInfo -> Ordering) -> [CallInfo] -> [CallInfo]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Range -> Range -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Range -> Range -> Ordering)
-> (CallInfo -> Range) -> CallInfo -> CallInfo -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` CallInfo -> Range
callInfoRange) ([CallInfo] -> [CallInfo]) -> [CallInfo] -> [CallInfo]
forall a b. (a -> b) -> a -> b
$
              (TerminationError -> [CallInfo])
-> [TerminationError] -> [CallInfo]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TerminationError -> [CallInfo]
termErrCalls [TerminationError]
because)

    UnreachableClauses QName
f [Range]
pss -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Unreachable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords (Int -> String -> String
forall a. (Num a, Eq a) => a -> String -> String
plural ([Range] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Range]
pss) String
"clause")
        where
          plural :: a -> String -> String
plural a
1 String
thing = String
thing
          plural a
n String
thing = String
thing String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"s"

    CoverageIssue QName
f [(Telescope, [NamedArg DeBruijnPattern])]
pss -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"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
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]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Missing cases:") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *). Monad m => [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
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m, MonadInteractionPoints m,
 MonadFresh NameId m, HasConstInfo m, HasBuiltins m,
 MonadStConcreteNames m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc)) =>
(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
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 :: Telescope
clauseTel = Telescope
tel, namedClausePats :: [NamedArg DeBruijnPattern]
namedClausePats = [NamedArg DeBruijnPattern]
ps }

    CoverageNoExactSplit QName
f [Clause]
cs -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [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 :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Exact splitting is enabled, but the following" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords ([Clause] -> String -> String -> String
forall a c. Sized a => a -> c -> c -> c
P.singPlural [Clause]
cs String
"clause" String
"clauses") [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
               String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"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 (Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
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
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

    NotStrictlyPositive QName
d Seq OccursWhere
ocs -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [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
prettyTCM QName
d] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"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
prettyTCM Seq OccursWhere
ocs]

    CantGeneralizeOverSorts [MetaId]
ms -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
            [ String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
"Cannot generalize over unsolved sort metas:"
            , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat [ MetaId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
"at" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Range -> m Doc
forall (m :: * -> *) a. (Monad 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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Range
getMetaRange MetaId
x) | MetaId
x <- [MetaId]
ms ]
            , [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Suggestion: add a `variable Any : Set _` and replace unsolved metas by Any"
            ]

    AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern]
ps -> String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$
      String
"The right-hand side must be omitted if there " String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
"is an absurd pattern, () or {}, in the left-hand side."

    OldBuiltin String
old String
new -> String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$
      String
"Builtin " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
old String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" no longer exists. " String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
"It is now bound by BUILTIN " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
new

    Warning
EmptyRewritePragma -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> (String -> [m Doc]) -> String -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"Empty REWRITE pragma"

    IllformedAsClause String
s -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> (String -> [m Doc]) -> String -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$
      String
"`as' must be followed by an identifier" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s

    ClashesViaRenaming NameOrModule
nm [Name]
xs -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [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" ]
      , String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"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
prettyTCM [Name]
xs
      ]

    Warning
UselessPublic -> String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"Keyword `public' is ignored here"

    UselessInline QName
q -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"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
prettyTCM QName
q] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"to have a separate Haskell definition"

    Warning
WrongInstanceDeclaration -> String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords String
"Terms marked as eligible for instance search should end with a name, so `instance' is ignored here."

    InstanceWithExplicitArg QName
q -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Instance declarations with explicit arguments are never considered by instance search," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"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
prettyTCM QName
q] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"into an instance has no effect."

    InstanceNoOutputTypeName Doc
b -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Instance arguments whose type does not end in a named or variable type are never considered by instance search," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"so having an instance argument" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
b] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"has no effect."

    InstanceArgWithExplicitArg Doc
b -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Instance arguments with explicit arguments are never considered by instance search," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"so having an instance argument" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
b] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"has no effect."

    InversionDepthReached QName
f -> do
      Int
maxDepth <- m Int
forall (m :: * -> *). HasOptions m => m Int
maxInversionDepth
      [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Refusing to invert pattern matching of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords (String
"because the maximum depth (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
maxDepth String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") has been reached.") [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Most likely this means you have an unsatisfiable constraint, but it could" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"also mean that you need to increase the maximum depth using the flag" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"--inversion-max-depth=N"

    GenericWarning Doc
d -> Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d

    GenericNonFatalError Doc
d -> Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d

    SafeFlagPostulate Name
e -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Cannot postulate" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Name
e] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"with safe flag"

    SafeFlagPragma [String]
xs ->
      let plural :: String
plural | [String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = String
""
                 | Bool
otherwise      = String
"s"
      in [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords (String
"Cannot set OPTIONS pragma" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
plural)]
                [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ (String -> m Doc) -> [String] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text [String]
xs [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords String
"with safe flag."]

    Warning
SafeFlagNonTerminating -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Cannot use NON_TERMINATING pragma with safe flag."

    Warning
SafeFlagTerminating -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Cannot use TERMINATING pragma with safe flag."

    Warning
SafeFlagWithoutKFlagPrimEraseEquality -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Cannot use primEraseEquality with safe and without-K flags.")

    Warning
WithoutKFlagPrimEraseEquality -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Using primEraseEquality with the without-K flag is inconsistent.")

    Warning
SafeFlagNoPositivityCheck -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Cannot use NO_POSITIVITY_CHECK pragma with safe flag."

    Warning
SafeFlagPolarity -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Cannot use POLARITY pragma with safe flag."

    Warning
SafeFlagNoUniverseCheck -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Cannot use NO_UNIVERSE_CHECK pragma with safe flag."

    Warning
SafeFlagEta -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Cannot use ETA pragma with safe flag."

    Warning
SafeFlagInjective -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Cannot use INJECTIVE pragma with safe flag."

    Warning
SafeFlagNoCoverageCheck -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Cannot use NON_COVERING pragma with safe flag."

    ParseWarning ParseWarning
pw -> ParseWarning -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty ParseWarning
pw

    DeprecationWarning String
old String
new String
version -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
old] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"has been deprecated. Use" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
new] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords
      String
"instead. This will be an error in Agda" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
version m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]

    NicifierIssue DeclarationWarning
w -> Range -> m Doc -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, HasRange a) =>
a -> m Doc -> m Doc
sayWhere (DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty DeclarationWarning
w

    UserWarning String
str -> String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
str

    ModuleDoesntExport QName
m [ImportedName]
xs -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"The module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty QName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"doesn't export the following:" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Monad m => m Doc
comma ((ImportedName -> m Doc) -> [ImportedName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ImportedName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty [ImportedName]
xs)

    FixityInRenamingModule NonEmpty Range
_rs -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Modules do not have fixity"

    LibraryWarning LibWarning
lw -> LibWarning -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty LibWarning
lw

    InfectiveImport String
o ModuleName
m -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Importing module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ModuleName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty ModuleName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"using the" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [String -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty String
o] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"flag from a module which does not."

    CoInfectiveImport String
o ModuleName
m -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Importing module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ModuleName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty ModuleName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"not using the" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [String -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty String
o] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"flag from a module which does."

    RewriteNonConfluent Term
lhs Term
rhs1 Term
rhs2 Doc
err -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep
      [ m Doc
"Confluence check failed:"
      , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
lhs , m Doc
"reduces to both"
      , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
rhs1 , m Doc
"and" , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
rhs2
      , m Doc
"which are not equal because"
      , Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
err
      ]

    RewriteMaybeNonConfluent Term
lhs1 Term
lhs2 [Doc]
cs -> do
      [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [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 :: * -> *). Monad m => [m Doc] -> m Doc
fsep
           [ m Doc
"Couldn't determine overlap between left-hand sides"
           , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
lhs1 , m Doc
"and" , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
lhs2
           , m Doc
"because of unsolved constraints:"
           ]
        ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ (Doc -> m Doc) -> [Doc] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
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 (m :: * -> *) a. Monad m => a -> m a
return) [Doc]
cs

    PragmaCompileErased String
bn QName
qn -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"The backend" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
bn] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"erases" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
qn]
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"so the COMPILE pragma will be ignored."

    NotInScopeW [QName]
xs -> do
      [QName]
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
      [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"Not in scope:") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (QName -> m Doc) -> [QName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([QName] -> QName -> m Doc
forall (m :: * -> *).
(IsString (m Doc), MonadReduce m, MonadAddContext m,
 MonadInteractionPoints m, MonadFresh NameId m, HasConstInfo m,
 HasBuiltins m, MonadStConcreteNames m, Null (m Doc),
 Semigroup (m Doc)) =>
[QName] -> QName -> m Doc
name [QName]
inscope) [QName]
xs)
      where
      name :: [QName] -> QName -> m Doc
name [QName]
inscope QName
x =
        [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep [ QName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty QName
x
             , 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
prettyTCM (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
x)
             , [QName] -> QName -> m Doc
forall (m :: * -> *).
(Null (m Doc), Monad m, IsString (m Doc), Semigroup (m Doc)) =>
[QName] -> QName -> m Doc
suggestion [QName]
inscope QName
x
             ]
      suggestion :: [QName] -> QName -> m Doc
suggestion [QName]
inscope QName
x = Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
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), Monad m) => [m Doc] -> m Doc
par ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
        [ m Doc
"did you forget space around the ':'?"  | Char
':' Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
s ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
        [ m Doc
"did you forget space around the '->'?" | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
List.isInfixOf String
"->" String
s ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
        [ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ m Doc
"did you mean"
              , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat (m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate m Doc
" or"
                       ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ (String -> m Doc) -> [String] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ String
y -> String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"'" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'") [String]
ys)
              m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"?" ]
          | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [String] -> Bool
forall a. Null a => a -> Bool
null [String]
ys ]
        where
          s :: String
s = QName -> String
forall a. Pretty a => a -> String
P.prettyShow QName
x
          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 :: * -> *). Monad m => [m Doc] -> m Doc
vcat [m Doc]
ds

          strip :: QName -> String
strip QName
x = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'_') (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Pretty a => a -> String
P.prettyShow (Name -> String) -> Name -> String
forall a b. (a -> b) -> a -> b
$ QName -> Name
C.unqualify QName
x
          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] -> Int
forall a. Eq a => [a] -> [a] -> Int
editDistance [a]
a [a]
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> Int
forall a. Integral a => a -> a
maxDist ([a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
a)
          ys :: [String]
ys = (QName -> String) -> [QName] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map QName -> String
forall a. Pretty a => a -> String
P.prettyShow ([QName] -> [String]) -> [QName] -> [String]
forall a b. (a -> b) -> a -> b
$ (QName -> Bool) -> [QName] -> [QName]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
close (QName -> String
strip QName
x) (String -> Bool) -> (QName -> String) -> QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> String
strip) [QName]
inscope


prettyTCWarnings :: [TCWarning] -> TCM String
prettyTCWarnings :: [TCWarning] -> TCM String
prettyTCWarnings = ([String] -> String) -> TCMT IO [String] -> TCM String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([String] -> String
unlines ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> [String]
forall a. a -> [a] -> [a]
List.intersperse String
"") (TCMT IO [String] -> TCM String)
-> ([TCWarning] -> TCMT IO [String]) -> [TCWarning] -> TCM String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> TCMT IO [String]
prettyTCWarnings'

prettyTCWarnings' :: [TCWarning] -> TCM [String]
prettyTCWarnings' :: [TCWarning] -> TCMT IO [String]
prettyTCWarnings' = (TCWarning -> TCM String) -> [TCWarning] -> TCMT IO [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Doc -> String) -> TCMT IO Doc -> TCM String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> String
P.render (TCMT IO Doc -> TCM String)
-> (TCWarning -> TCMT IO Doc) -> TCWarning -> TCM String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM) ([TCWarning] -> TCMT IO [String])
-> ([TCWarning] -> [TCWarning]) -> [TCWarning] -> TCMT IO [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> [TCWarning]
filterTCWarnings

-- | If there are several warnings, remove the unsolved-constraints warning
-- in case there are no interesting constraints to list.
filterTCWarnings :: [TCWarning] -> [TCWarning]
filterTCWarnings :: [TCWarning] -> [TCWarning]
filterTCWarnings = \case
  -- #4065: Always keep the only warning
  [TCWarning
w] -> [TCWarning
w]
  -- Andreas, 2019-09-10, issue #4065:
  -- If there are several warnings, remove the unsolved-constraints warning
  -- in case there are no interesting constraints to list.
  [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 [ProblemConstraint]
cs -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [ProblemConstraint] -> Bool
forall a. Null a => a -> Bool
null ([ProblemConstraint] -> Bool) -> [ProblemConstraint] -> Bool
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint -> Bool)
-> [ProblemConstraint] -> [ProblemConstraint]
forall a. (a -> Bool) -> [a] -> [a]
filter ProblemConstraint -> Bool
interestingConstraint [ProblemConstraint]
cs
    Warning
_ -> Bool
True


-- | Turns all warnings into errors.
tcWarningsToError :: [TCWarning] -> TCM a
tcWarningsToError :: [TCWarning] -> TCM a
tcWarningsToError [TCWarning]
ws = TypeError -> TCM a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> TypeError -> TCM a
forall a b. (a -> b) -> a -> b
$ case [TCWarning]
ws of
  [] -> TypeError
SolvedButOpenHoles
  [TCWarning]
_  -> [TCWarning] -> TypeError
NonFatalErrors [TCWarning]
ws


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

applyFlagsToTCWarnings' :: MainInterface -> [TCWarning] -> TCM [TCWarning]
applyFlagsToTCWarnings' :: MainInterface -> [TCWarning] -> TCM [TCWarning]
applyFlagsToTCWarnings' MainInterface
isMain [TCWarning]
ws = do

  -- For some reason some SafeFlagPragma seem to be created multiple times.
  -- This is a way to collect all of them and remove duplicates.
  let pragmas :: TCWarning -> ([TCWarning], [String])
pragmas TCWarning
w = case TCWarning -> Warning
tcWarning TCWarning
w of { SafeFlagPragma [String]
ps -> ([TCWarning
w], [String]
ps); Warning
_ -> ([], []) }
  let sfp :: [TCWarning]
sfp = case ([String] -> [String])
-> ([TCWarning], [String]) -> ([TCWarning], [String])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [String] -> [String]
forall a. Eq a => [a] -> [a]
List.nub ((TCWarning -> ([TCWarning], [String]))
-> [TCWarning] -> ([TCWarning], [String])
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TCWarning -> ([TCWarning], [String])
pragmas [TCWarning]
ws) of
              (TCWarning Range
r Warning
w Doc
p Bool
b:[TCWarning]
_, [String]
sfp) ->
                 [Range -> Warning -> Doc -> Bool -> TCWarning
TCWarning Range
r ([String] -> Warning
SafeFlagPragma [String]
sfp) Doc
p Bool
b]
              ([TCWarning], [String])
_                        -> []

  Set WarningName
warnSet <- do
    PragmaOptions
opts <- TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
    let warnSet :: Set WarningName
warnSet = PragmaOptions -> WarningMode
optWarningMode PragmaOptions
opts WarningMode
-> Lens' (Set WarningName) WarningMode -> Set WarningName
forall o i. o -> Lens' i o -> i
^. Lens' (Set WarningName) WarningMode
warningSet
    Set WarningName -> TCMT IO (Set WarningName)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set WarningName -> TCMT IO (Set WarningName))
-> Set WarningName -> TCMT IO (Set WarningName)
forall a b. (a -> b) -> a -> b
$ if MainInterface
isMain MainInterface -> MainInterface -> Bool
forall a. Eq a => a -> a -> Bool
/= MainInterface
NotMainInterface
           then Set WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set WarningName
warnSet Set WarningName
unsolvedWarnings
           else Set WarningName
warnSet

  -- filter out the warnings the flags told us to ignore
  let cleanUp :: Warning -> Bool
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 [ProblemConstraint]
ucs      -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [ProblemConstraint] -> Bool
forall a. Null a => a -> Bool
null [ProblemConstraint]
ucs
          Warning
_                            -> Bool
True

  [TCWarning] -> TCM [TCWarning]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TCWarning] -> TCM [TCWarning]) -> [TCWarning] -> TCM [TCWarning]
forall a b. (a -> b) -> a -> b
$ [TCWarning]
sfp [TCWarning] -> [TCWarning] -> [TCWarning]
forall a. [a] -> [a] -> [a]
++ (TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter (Warning -> Bool
cleanUp (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) [TCWarning]
ws

applyFlagsToTCWarnings :: [TCWarning] -> TCM [TCWarning]
applyFlagsToTCWarnings :: [TCWarning] -> TCM [TCWarning]
applyFlagsToTCWarnings = MainInterface -> [TCWarning] -> TCM [TCWarning]
applyFlagsToTCWarnings' MainInterface
NotMainInterface