module Agda.TypeChecking.Pretty.Constraint where

import Prelude hiding (null)

import qualified Data.Set as Set
import Data.Foldable (Foldable)
import qualified Data.Foldable as Foldable
import qualified Data.List as List
import Data.Function (on)

import Control.Monad

import Agda.Syntax.Common
import Agda.Syntax.Position
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Info     as A
import Agda.Syntax.Fixity
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Internal

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope

import Agda.Utils.Null
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Utils.Impossible

prettyConstraint :: MonadPretty m => ProblemConstraint -> m Doc
prettyConstraint :: forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Doc
prettyConstraint ProblemConstraint
c = m Doc -> m Doc
forall (m :: * -> *). MonadPretty m => m Doc -> m Doc
f (Lens' TCState Bool -> (Bool -> Bool) -> m Doc -> m Doc
forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
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
forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Doc
prettyTCM ProblemConstraint
c)
  where
    r :: Range
r   = ProblemConstraint -> Range
forall a. HasRange a => a -> Range
getRange ProblemConstraint
c
    f :: MonadPretty m => m Doc -> m Doc
    f :: forall (m :: * -> *). MonadPretty m => 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
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM Range
r m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"]")
{-# SPECIALIZE prettyConstraint :: ProblemConstraint -> TCM 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 MetaId
mi) = Bool
False
  go Constraint
_            = Bool
True

prettyInterestingConstraints :: MonadPretty m => [ProblemConstraint] -> m [Doc]
prettyInterestingConstraints :: forall (m :: * -> *).
MonadPretty m =>
[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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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
. Set ProblemId -> Bool
forall a. Null a => a -> Bool
null (Set ProblemId -> Bool)
-> (ProblemConstraint -> Set ProblemId)
-> ProblemConstraint
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> Set ProblemId
allBlockingProblems (Blocker -> Set ProblemId)
-> (ProblemConstraint -> Blocker)
-> ProblemConstraint
-> Set ProblemId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Blocker
constraintUnblocker
    cs' :: [ProblemConstraint]
cs' = (ProblemConstraint -> Bool)
-> [ProblemConstraint] -> [ProblemConstraint]
forall a. (a -> Bool) -> [a] -> [a]
filter ProblemConstraint -> Bool
interestingConstraint [ProblemConstraint]
cs
    interestingPids :: Set ProblemId
interestingPids = [Set ProblemId] -> Set ProblemId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set ProblemId] -> Set ProblemId)
-> [Set ProblemId] -> Set ProblemId
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint -> Set ProblemId)
-> [ProblemConstraint] -> [Set ProblemId]
forall a b. (a -> b) -> [a] -> [b]
map (Blocker -> Set ProblemId
allBlockingProblems (Blocker -> Set ProblemId)
-> (ProblemConstraint -> Blocker)
-> ProblemConstraint
-> Set ProblemId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Blocker
constraintUnblocker) [ProblemConstraint]
cs'
    stripPids :: ProblemConstraint -> ProblemConstraint
stripPids (PConstr Set ProblemId
pids Blocker
unblock Closure Constraint
c) = Set ProblemId -> Blocker -> 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) Blocker
unblock Closure Constraint
c
{-# SPECIALIZE prettyInterestingConstraints :: [ProblemConstraint] -> TCM [Doc] #-}

prettyRangeConstraint ::
  (MonadPretty m, Foldable f, Null (f ProblemId)) => Range -> f ProblemId -> Blocker -> Doc -> m Doc
prettyRangeConstraint :: forall (m :: * -> *) (f :: * -> *).
(MonadPretty m, Foldable f, Null (f ProblemId)) =>
Range -> f ProblemId -> Blocker -> Doc -> m Doc
prettyRangeConstraint Range
r f ProblemId
pids Blocker
unblock Doc
c =
  Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
c 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
sep [ Range -> m Doc
forall {a} {f :: * -> *}. (Pretty a, Applicative f) => a -> f Doc
prange Range
r
      , m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parensNonEmpty (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
sep
          [ Blocker -> m Doc
blockedOn Blocker
unblock
          , [ProblemId] -> m Doc
forall {m :: * -> *} {a}.
(Null (m Doc), IsString (m Doc), PrettyTCM a, MonadFresh NameId m,
 MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
 Semigroup (m Doc)) =>
[a] -> m Doc
prPids (f ProblemId -> [ProblemId]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList f ProblemId
pids)
          ]
      ]
  where
  prPids :: [a] -> m Doc
prPids []    = m Doc
forall a. Null a => a
empty
  prPids [a
pid] = m Doc
"belongs to problem" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
pid
  prPids [a]
pids  = m Doc
"belongs to problems" 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
fsep (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
$ (a -> m Doc) -> [a] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM [a]
pids)

  comma :: m Doc
comma | f ProblemId -> Bool
forall a. Null a => a -> Bool
null f ProblemId
pids = m Doc
forall a. Null a => a
empty
        | Bool
otherwise = m Doc
","

  blockedOn :: Blocker -> m Doc
blockedOn (UnblockOnAll Set Blocker
bs) | Set Blocker -> Bool
forall a. Set a -> Bool
Set.null Set Blocker
bs = m Doc
forall a. Null a => a
empty
  blockedOn (UnblockOnAny Set Blocker
bs) | Set Blocker -> Bool
forall a. Set a -> Bool
Set.null Set Blocker
bs = m Doc
"stuck" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
comma
  blockedOn Blocker
u = m Doc
"blocked on" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Blocker -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
prettyTCM Blocker
u m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
comma)

  prange :: a -> f Doc
prange a
r | String -> Bool
forall a. Null a => a -> Bool
null String
s    = Doc -> f Doc
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
forall a. Null a => a
empty
           | Bool
otherwise = String -> f Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> f Doc) -> String -> f Doc
forall a b. (a -> b) -> a -> b
$ String
" [ at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ]"
    where s :: String
s = a -> String
forall a. Pretty a => a -> String
P.prettyShow a
r

instance PrettyTCM ProblemConstraint where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Doc
prettyTCM (PConstr Set ProblemId
pids Blocker
unblock Closure Constraint
c) =
    Range -> Set ProblemId -> Blocker -> Doc -> m Doc
forall (m :: * -> *) (f :: * -> *).
(MonadPretty m, Foldable f, Null (f ProblemId)) =>
Range -> f ProblemId -> Blocker -> Doc -> m Doc
prettyRangeConstraint Range
forall a. Range' a
noRange Set ProblemId
pids Blocker
unblock (Doc -> m Doc) -> m Doc -> m Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Closure Constraint -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Closure Constraint -> m Doc
prettyTCM Closure Constraint
c

instance PrettyTCM Constraint where
    prettyTCM :: forall (m :: * -> *). MonadPretty m => Constraint -> m Doc
prettyTCM = \case
        ValueCmp Comparison
cmp CompareAs
ty Term
s Term
t -> m Doc -> Term -> Term -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (Comparison -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
prettyTCM Comparison
cmp) Term
s Term
t m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> CompareAs -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => CompareAs -> m Doc
prettyTCM CompareAs
ty
        ValueCmpOnFace Comparison
cmp Term
p Type
ty Term
s Term
t ->
            [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
p m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"|"
                , m Doc -> Term -> Term -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (Comparison -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
prettyTCM Comparison
cmp) Term
s Term
t ]
            m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Precedence -> Type -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx Type
ty)
        ElimCmp [Polarity]
cmps [IsForced]
fs Type
t Term
v [Elim]
us [Elim]
vs -> m Doc -> [Elim] -> [Elim] -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp m Doc
"~~" [Elim]
us [Elim]
vs   m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Precedence -> Type -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx Type
t)
        LevelCmp Comparison
cmp Level
a Level
b         -> m Doc -> Level -> Level -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (Comparison -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
prettyTCM Comparison
cmp) Level
a Level
b
        SortCmp Comparison
cmp Sort
s1 Sort
s2        -> m Doc -> Sort -> Sort -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (Comparison -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
prettyTCM Comparison
cmp) Sort
s1 Sort
s2
        UnBlock MetaId
m   -> do
            -- BlockedConst t <- mvInstantiation <$> lookupMeta m
            MetaInstantiation
mi <- MetaId -> m MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m
            case MetaInstantiation
mi of
              BlockedConst Term
t -> m Doc -> MetaId -> Term -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp m Doc
":=" MetaId
m Term
t
              PostponedTypeCheckingProblem Closure TypeCheckingProblem
cl -> Closure TypeCheckingProblem
-> (TypeCheckingProblem -> m Doc) -> m Doc
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeCheckingProblem
cl ((TypeCheckingProblem -> m Doc) -> m Doc)
-> (TypeCheckingProblem -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \TypeCheckingProblem
p ->
                m Doc -> MetaId -> TypeCheckingProblem -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp m Doc
":=" MetaId
m TypeCheckingProblem
p
              OpenMeta{}  -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
              InstV{} -> m Doc
forall a. Null a => a
empty
              -- Andreas, 2017-01-11, issue #2637:
              -- The size solver instantiates some metas with infinity
              -- without cleaning up the UnBlock constraints.
              -- Thus, this case is not IMPOSSIBLE.
              --
              -- InstV args t -> do
              --   reportS "impossible" 10
              --     [ "UnBlock meta " ++ show m ++ " surprisingly has InstV instantiation:"
              --     , show m ++ show args ++ " := " ++ show t
              --     ]
              --   __IMPOSSIBLE__

        FindInstance MetaId
m Maybe [Candidate]
mcands -> do
          Type
t <- MetaId -> m Type
forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
 MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m
          TelV Tele (Dom Type)
tel Type
_ <- Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) Dom Type -> Bool
forall a. LensHiding a => a -> Bool
notVisible Type
t
          [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ m Doc
"Resolve instance argument" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> m Doc -> MetaId -> Type -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp m Doc
":" MetaId
m Type
t
                -- #4071: Non-visible arguments to the meta are in scope of the candidates add
                --        those here to not get out of scope deBruijn indices when printing
                --        unsolved constraints.
              , Tele (Dom Type) -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
tel m Doc
cands
              ]
          where
            overlap :: Candidate -> a
overlap Candidate
c = case Candidate -> OverlapMode
candidateOverlap Candidate
c of
              OverlapMode
FieldOverlap   -> a
"overlap"
              OverlapMode
Incoherent     -> a
"[incoherent]"
              OverlapMode
Overlappable   -> a
"[overlappable]"
              OverlapMode
Overlapping    -> a
"[overlapping]"
              OverlapMode
Overlaps       -> a
"[overlaps]"
              OverlapMode
DefaultOverlap -> a
forall a. Null a => a
empty

            cands :: m Doc
cands = case Maybe [Candidate]
mcands of
              Maybe [Candidate]
Nothing -> m Doc
"No candidates yet"
              Just [Candidate]
cnds -> m Doc -> Int -> m Doc -> m Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang m Doc
"Candidates" Int
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 -> Int -> m Doc -> m Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang (Candidate -> m Doc
forall {a}. (IsString a, Null a) => Candidate -> a
overlap Candidate
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Candidate -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM Candidate
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":") 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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Candidate -> Type
candidateType Candidate
c)
                | Candidate
c <- [Candidate]
cnds
                ]

        ResolveInstanceHead QName
q ->
            m Doc
"Resolve target type of instance: " 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
        IsEmpty Range
r Type
t ->
            m Doc
"Is empty:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Precedence -> Type -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx Type
t
        CheckSizeLtSat Term
t ->
            m Doc
"Is not empty type of sizes:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Precedence -> Term -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx Term
t
        CheckFunDef DefInfo
i QName
q [Clause]
cs TCErr
err -> do
            Type
t <- Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
            [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ m Doc
"Check definition of" 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
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
                 , 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
"stuck because" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> TCErr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err ]
        HasBiggerSort Sort
a -> m Doc
"Has bigger sort:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
a
        HasPTSRule Dom Type
a Abs Sort
b -> m Doc
"Has PTS rule:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> case Abs Sort
b of
          NoAbs String
_ Sort
b -> (Dom Type, Sort) -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => (Dom Type, Sort) -> m Doc
prettyTCM (Dom Type
a,Sort
b)
          Abs String
x Sort
b   -> m Doc
"(" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> (Dom Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom Type
a m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"," m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => String -> m a -> m a
addContext String
x (Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
b)) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
")"
        UnquoteTactic Term
v Term
_ Type
_ -> do
          Expr
e <- Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
v
          Expr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM (AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
A.defaultAppInfo_ (ExprInfo -> Expr
A.Unquote ExprInfo
A.exprNoRange) (Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg Expr
e))
        CheckDataSort QName
q Sort
s -> do
          [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ m Doc
"Sort", Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s, m Doc
"of", 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
"admits data/record definitions." ]
        CheckMetaInst MetaId
x -> do
          MetaVariable
m <- MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
          case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
m of
            HasType{ jMetaType :: forall a. Judgement a -> Type
jMetaType = Type
t } -> 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
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
            IsSort{} -> 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
<+> m Doc
"is a sort"
        CheckType Type
t ->
          Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"is a well-formed type"
        CheckLockedVars Term
t Type
ty Arg Term
lk Type
lk_ty -> do
          m Doc
"Lock" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Arg Term
lk m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"|-" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Precedence -> Term -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx Term
t m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ty
        UsableAtModality WhyCheckModality
_ Maybe Sort
ms Modality
mod Term
t -> m Doc
"Is usable at" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Modality -> String
forall a. Verbalize a => a -> String
verbalize Modality
mod) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"modality:" 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
t
          -- TODO: print @ms : Maybe Sort@ as well?

      where
        prettyCmp
          :: (PrettyTCM a, PrettyTCM b, MonadPretty m)
          => m Doc -> a -> b -> m Doc
        prettyCmp :: forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp m Doc
cmp a
x b
y = Precedence -> a -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx a
x m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (m Doc
cmp m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Precedence -> b -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx b
y)