module Agda.TypeChecking.Pretty.Constraint where

import Prelude hiding (null)

import qualified Data.Set as Set
import qualified Data.List as List
import Data.Function

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.Utils.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' 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 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
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 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)
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

instance PrettyTCM ProblemConstraint where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Doc
prettyTCM (PConstr Set ProblemId
pids Blocker
unblock Closure Constraint
c) = Closure Constraint -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Closure Constraint
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parensNonEmpty ([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, PureTCM m,
 MonadInteractionPoints m, MonadFresh NameId m,
 MonadStConcreteNames m, Semigroup (m Doc)) =>
[a] -> m Doc
prPids (Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList Set 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
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
prettyTCM [a]
pids)

      comma :: m Doc
comma | Set ProblemId -> Bool
forall a. Null a => a -> Bool
null Set 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
prettyTCM Blocker
u m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
comma)

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
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
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
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
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
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
prettyTCM Comparison
cmp) Sort
s1 Sort
s2
        UnBlock MetaId
m   -> do
            -- BlockedConst t <- mvInstantiation <$> lookupMeta m
            MetaInstantiation
mi <- MetaVariable -> MetaInstantiation
mvInstantiation (MetaVariable -> MetaInstantiation)
-> m MetaVariable -> m MetaInstantiation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta 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 :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
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
              Open{}  -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
              OpenInstance{} -> 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 :: * -> *).
(MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m,
 HasBuiltins 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
addContext Tele (Dom Type)
tel m Doc
cands
                ]
          where
            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
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
prettyTCM (Candidate -> Type
candidateType Candidate
c) | Candidate
c <- [Candidate]
cnds ]
              where overlap :: Candidate -> a
overlap Candidate
c | Candidate -> Bool
candidateOverlappable Candidate
c = a
"overlap"
                              | Bool
otherwise               = a
forall a. Null a => a
empty
        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 Delayed
d 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
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
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
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
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 ArgName
_ Sort
b -> (Dom Type, Sort) -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Dom Type
a,Sort
b)
          Abs ArgName
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
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
<+> ArgName -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ArgName
x (Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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)
reify Term
v
          Expr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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))
        CheckMetaInst MetaId
x -> do
          MetaVariable
m <- MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta 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
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
prettyTCM Type
t
            IsSort{} -> 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
<+> m Doc
"is a sort"
        CheckType Type
t ->
          Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
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
prettyTCM Type
ty
        UsableAtModality 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
<+> Modality -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Modality
mod 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
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t

      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)