module Agda.TypeChecking.Pretty.Call where

import Prelude hiding ( null )

import Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views
import Agda.Syntax.Common
import Agda.Syntax.Fixity
import qualified Agda.Syntax.Concrete.Definitions as D
import qualified Agda.Syntax.Info as A
import Agda.Syntax.Position
import Agda.Syntax.Scope.Monad
import Agda.Syntax.Translation.AbstractToConcrete

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Pretty

import Agda.Utils.Function
import Agda.Utils.Null
import qualified Agda.Utils.Pretty as P

import Agda.Utils.Impossible

sayWhere :: MonadPretty m => HasRange a => a -> m Doc -> m Doc
sayWhere :: a -> m Doc -> m Doc
sayWhere a
x m Doc
d = Bool -> (m Doc -> m Doc) -> m Doc -> m Doc
forall a. Bool -> (a -> a) -> a -> a
applyUnless (Range -> Bool
forall a. Null a => a -> Bool
null Range
r) (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
d
  where r :: Range
r = a -> Range
forall a. HasRange a => a -> Range
getRange a
x

sayWhen :: MonadPretty m => Range -> Maybe (Closure Call) -> m Doc -> m Doc
sayWhen :: Range -> Maybe (Closure Call) -> m Doc -> m Doc
sayWhen Range
r Maybe (Closure Call)
Nothing   m Doc
m = Range -> m Doc -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, HasRange a) =>
a -> m Doc -> m Doc
sayWhere Range
r m Doc
m
sayWhen Range
r (Just Closure Call
cl) m Doc
m = Range -> m Doc -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, HasRange a) =>
a -> m Doc -> m Doc
sayWhere Range
r (m Doc
m m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Closure Call -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Closure Call
cl)

instance PrettyTCM CallInfo where
  prettyTCM :: CallInfo -> m Doc
prettyTCM CallInfo
c = do
    let call :: m Doc
call = Closure Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Closure Term -> m Doc) -> Closure Term -> m Doc
forall a b. (a -> b) -> a -> b
$ CallInfo -> Closure Term
callInfoCall CallInfo
c
        r :: Range
r    = CallInfo -> Range
callInfoRange CallInfo
c
    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
call
      else m Doc
call 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
"(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 a. Semigroup a => a -> a -> a
<> m Doc
")"

instance PrettyTCM Call where
  prettyTCM :: Call -> m Doc
prettyTCM = Precedence -> m Doc -> m Doc
forall (m :: * -> *) a. ReadTCState m => Precedence -> m a -> m a
withContextPrecedence Precedence
TopCtx (m Doc -> m Doc) -> (Call -> m Doc) -> Call -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case

    CheckClause Type
t SpineClause
cl -> do

      VerboseKey -> Int -> m () -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> m () -> m ()
verboseS  VerboseKey
"error.checkclause" Int
40 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
        VerboseKey -> Int -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"error.checkclause" Int
60 (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"prettyTCM CheckClause: cl = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ SpineClause -> VerboseKey
forall a. Show a => a -> VerboseKey
show (SpineClause -> SpineClause
forall a. ExprLike a => a -> a
deepUnscope SpineClause
cl)
        [Declaration]
clc <- SpineClause -> m (ConOfAbs SpineClause)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ SpineClause
cl
        VerboseKey -> Int -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"error.checkclause" Int
40 (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"cl (Concrete) = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [Declaration] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [Declaration]
clc

      [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
$
        VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking that the clause"
        [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [SpineClause -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA SpineClause
cl] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"has type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t]

    CheckLHS SpineLHS
lhs -> [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
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking the clause left hand side"
      , SpineLHS -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (SpineLHS -> m Doc) -> SpineLHS -> m Doc
forall a b. (a -> b) -> a -> b
$ SpineLHS
lhs { spLhsInfo :: LHSInfo
A.spLhsInfo = (SpineLHS -> LHSInfo
A.spLhsInfo SpineLHS
lhs) { lhsEllipsis :: ExpandedEllipsis
A.lhsEllipsis = ExpandedEllipsis
NoEllipsis } }
      ]

    CheckPattern Pattern
p Telescope
tel Type
t -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking that the pattern"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"has type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t]

    CheckPatternLinearityType Name
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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking that all occurrences of pattern variable"
      [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
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"have the same type"

    CheckPatternLinearityValue Name
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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking that all occurrences of pattern variable"
      [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
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"have the same value"

    CheckLetBinding LetBinding
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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking the let binding" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [LetBinding -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA LetBinding
b]

    InferExpr Expr
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
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when inferring the type of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e]

    CheckExprCall Comparison
cmp Expr
e Type
t -> [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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking that the expression"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"has type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t]

    IsTypeCall Comparison
cmp Expr
e Sort
s -> [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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking that the expression"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"is a type of sort" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s]

    IsType_ Expr
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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking that the expression"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"is a type"

    CheckProjection Range
_ QName
x Type
t -> [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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking the projection" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> 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
$ Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t ] ]

    CheckArguments Range
r [NamedArg Expr]
es Type
t0 Maybe Type
t1 -> [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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking that" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      (NamedArg Expr -> m Doc) -> [NamedArg Expr] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Expr -> m Doc
forall (m :: * -> *). MonadPretty m => NamedArg Expr -> m Doc
hPretty [NamedArg Expr]
es [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords ([NamedArg Expr] -> VerboseKey -> VerboseKey -> VerboseKey
forall a c. Sized a => a -> c -> c -> c
P.singPlural [NamedArg Expr]
es VerboseKey
"is a valid argument" VerboseKey
"are valid arguments") [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"to a function of type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0]

    CheckMetaSolution Range
r MetaId
m Type
a Term
v -> [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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking that the solution" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"of metavariable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [MetaId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"has the expected type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a]

    CheckTargetType Range
r Type
infTy Type
expTy -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ m Doc
"when checking that the inferred type of an application"
      , 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
$ Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
infTy
      , m Doc
"matches the expected type"
      , 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
$ Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
expTy ]

    CheckRecDef Range
_ QName
x [LamBinding]
ps [Constructor]
cs ->
      [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
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking the definition 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
x]

    CheckDataDef Range
_ QName
x [LamBinding]
ps [Constructor]
cs ->
      [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
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking the definition 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
x]

    CheckConstructor QName
d Telescope
_ Sort
_ (A.Axiom KindOfName
_ DefInfo
_ ArgInfo
_ Maybe [Occurrence]
_ QName
c Expr
_) -> [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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking 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
prettyTCM QName
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"in the declaration 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
d]

    CheckConstructor{} -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__

    CheckConstructorFitsIn QName
c Type
t Sort
s -> [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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking that the type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"of 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
prettyTCM QName
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"fits in the sort" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"of the datatype."

    CheckFunDefCall Range
_ QName
f [Clause]
_ Bool
_ ->
      [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
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking the definition 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]

    CheckPragma Range
_ Pragma
p ->
      [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
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking the pragma"
             [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [RangeAndPragma -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (RangeAndPragma -> m Doc) -> RangeAndPragma -> m Doc
forall a b. (a -> b) -> a -> b
$ Range -> Pragma -> RangeAndPragma
RangeAndPragma Range
forall a. Range' a
noRange Pragma
p]

    CheckPrimitive Range
_ QName
x Expr
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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking that the type of the primitive 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
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"is" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e]

    CheckWithFunctionType Type
a -> [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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking that the type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"of the generated with function is well-formed"

    CheckDotPattern Expr
e Term
v -> [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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking that the given dot pattern" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"matches the inferred value" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v]

    CheckNamedWhere ModuleName
m -> [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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking the named where block" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ModuleName -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA ModuleName
m]

    InferVar Name
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
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when inferring the type of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Name
x]

    InferDef QName
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
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when inferring the type 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
x]

    CheckIsEmpty Range
r Type
t ->
      [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
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking that" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"has no constructors"

    CheckConfluence QName
r1 QName
r2 ->
      [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
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking confluence of the rewrite rule" [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
r1] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"with" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             if QName
r1 QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
r2 then VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"itself" else [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
r2]

    ScopeCheckExpr Expr
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
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when scope checking" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e]

    ScopeCheckDeclaration NiceDeclaration
d ->
      VerboseKey -> m Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
fwords (VerboseKey
"when scope checking the declaration" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
suffix) 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 :: * -> *) (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
$ (Declaration -> m Doc) -> [Declaration] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Declaration]
ds)
      where
      ds :: [Declaration]
ds     = NiceDeclaration -> [Declaration]
D.notSoNiceDeclarations NiceDeclaration
d
      suffix :: VerboseKey
suffix = case [Declaration]
ds of
        [Declaration
_] -> VerboseKey
""
        [Declaration]
_   -> VerboseKey
"s"

    ScopeCheckLHS QName
x Pattern
p ->
      [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
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when scope checking the left-hand side" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"in the definition of" [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
x]

    Call
NoHighlighting -> m Doc
forall a. Null a => a
empty

    SetRange Range
r -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when doing something 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

    CheckSectionApplication Range
_ ModuleName
m1 ModuleApplication
modapp -> [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
$
      VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when checking the module application" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Constructor -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Constructor -> m Doc) -> Constructor -> m Doc
forall a b. (a -> b) -> a -> b
$ ModuleInfo
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> Constructor
A.Apply ModuleInfo
info ModuleName
m1 ModuleApplication
modapp ScopeCopyInfo
initCopyInfo ImportDirective
forall a. Null a => a
empty]
      where
      info :: ModuleInfo
info = Range
-> Range
-> Maybe Name
-> Maybe OpenShortHand
-> Maybe ImportDirective
-> ModuleInfo
A.ModuleInfo Range
forall a. Range' a
noRange Range
forall a. Range' a
noRange Maybe Name
forall a. Maybe a
Nothing Maybe OpenShortHand
forall a. Maybe a
Nothing Maybe ImportDirective
forall a. Maybe a
Nothing

    Call
ModuleContents -> [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
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"when retrieving the contents of a module"

    where
    hPretty :: MonadPretty m => Arg (Named_ Expr) -> m Doc
    hPretty :: NamedArg Expr -> m Doc
hPretty NamedArg Expr
a = do
      Precedence -> m Doc -> m Doc
forall (m :: * -> *) a. ReadTCState m => Precedence -> m a -> m a
withContextPrecedence (ParenPreference -> Precedence
ArgumentCtx ParenPreference
PreferParen) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
        Arg (Named (WithOrigin (Ranged VerboseKey)) Expr) -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Arg (Named (WithOrigin (Ranged VerboseKey)) Expr) -> m Doc)
-> m (Arg (Named (WithOrigin (Ranged VerboseKey)) Expr)) -> m Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< NamedArg Expr -> NamedArg Expr -> m (ConOfAbs (NamedArg Expr))
forall i a (m :: * -> *).
(LensHiding i, ToConcrete a, MonadAbsToCon m) =>
i -> a -> m (ConOfAbs a)
abstractToConcreteHiding NamedArg Expr
a NamedArg Expr
a