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
mi <- MetaId -> m MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m
case 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
FindInstance MetaId
m Maybe [Candidate]
mcands -> do
t <- MetaId -> m Type
forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m
TelV tel _ <- telViewUpTo' (-1) notVisible t
sep [ "Resolve instance argument" <?> prettyCmp ":" m t
, addContext tel 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
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
vcat [ "Check definition of" <+> prettyTCM q <+> ":" <+> prettyTCM t
, nest 2 $ "stuck because" <?> prettyTCM 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
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
prettyTCM (A.App A.defaultAppInfo_ (A.Unquote A.exprNoRange) (defaultNamedArg 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
m <- MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
case mvJudgement 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
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)