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 = forall (m :: * -> *). MonadPretty m => m Doc -> m Doc
f (forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> m b -> m b
locallyTCState Lens' Bool TCState
stInstantiateBlocking (forall a b. a -> b -> a
const Bool
True) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ProblemConstraint
c)
where
r :: Range
r = 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 forall a. Null a => a -> Bool
null forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
P.pretty Range
r
then m Doc
d
else m Doc
d forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 (m Doc
"[ at" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Range
r forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"]")
interestingConstraint :: ProblemConstraint -> Bool
interestingConstraint :: ProblemConstraint -> Bool
interestingConstraint ProblemConstraint
pc = Constraint -> Bool
go forall a b. (a -> b) -> a -> b
$ 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 = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Doc
prettyConstraint forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> ProblemConstraint
stripPids) forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (forall a. Ord a => a -> a -> Ordering
compare 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Null a => a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> Set ProblemId
allBlockingProblems forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Blocker
constraintUnblocker
cs' :: [ProblemConstraint]
cs' = forall a. (a -> Bool) -> [a] -> [a]
filter ProblemConstraint -> Bool
interestingConstraint [ProblemConstraint]
cs
interestingPids :: Set ProblemId
interestingPids = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Blocker -> Set ProblemId
allBlockingProblems 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 (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) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Closure Constraint
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *). Functor m => m Doc -> m Doc
parensNonEmpty (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [Blocker -> m Doc
blockedOn Blocker
unblock, 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 (forall a. Set a -> [a]
Set.toList Set ProblemId
pids)])
where
prPids :: [a] -> m Doc
prPids [] = forall a. Null a => a
empty
prPids [a
pid] = m Doc
"belongs to problem" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
pid
prPids [a]
pids = m Doc
"belongs to problems" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
"," forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [a]
pids)
comma :: m Doc
comma | forall a. Null a => a -> Bool
null Set ProblemId
pids = forall a. Null a => a
empty
| Bool
otherwise = m Doc
","
blockedOn :: Blocker -> m Doc
blockedOn (UnblockOnAll Set Blocker
bs) | forall a. Set a -> Bool
Set.null Set Blocker
bs = forall a. Null a => a
empty
blockedOn (UnblockOnAny Set Blocker
bs) | forall a. Set a -> Bool
Set.null Set Blocker
bs = m Doc
"stuck" forall a. Semigroup a => a -> a -> a
<> m Doc
comma
blockedOn Blocker
u = m Doc
"blocked on" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Blocker
u 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 -> forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp) Term
s Term
t forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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 ->
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
p forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"|"
, forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp) Term
s Term
t ]
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (m Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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 -> forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp m Doc
"~~" [Elim]
us [Elim]
vs forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (m Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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 -> forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp) Level
a Level
b
SortCmp Comparison
cmp Sort
s1 Sort
s2 -> forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp) Sort
s1 Sort
s2
UnBlock MetaId
m -> do
MetaInstantiation
mi <- MetaVariable -> MetaInstantiation
mvInstantiation forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
case MetaInstantiation
mi of
BlockedConst Term
t -> 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 -> forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeCheckingProblem
cl forall a b. (a -> b) -> a -> b
$ \TypeCheckingProblem
p ->
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp m Doc
":=" MetaId
m TypeCheckingProblem
p
Open{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
OpenInstance{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
InstV{} -> forall a. Null a => a
empty
FindInstance MetaId
m Maybe [Candidate]
mcands -> do
Type
t <- forall (m :: * -> *).
(MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m,
HasBuiltins m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m
TelV Tele (Dom Type)
tel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) forall a. LensHiding a => a -> Bool
notVisible Type
t
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ m Doc
"Resolve instance argument" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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
, 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 ->
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang m Doc
"Candidates" Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang (forall {a}. (IsString a, Null a) => Candidate -> a
overlap Candidate
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":") Int
2 forall a b. (a -> b) -> a -> b
$
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 = forall a. Null a => a
empty
IsEmpty Range
r Type
t ->
m Doc
"Is empty:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ m Doc
"Check definition of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ m Doc
"stuck because" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM TCErr
err ]
HasBiggerSort Sort
a -> m Doc
"Has bigger sort:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> case Abs Sort
b of
NoAbs ArgName
_ Sort
b -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Dom Type
a,Sort
b)
Abs ArgName
x Sort
b -> m Doc
"(" forall a. Semigroup a => a -> a -> a
<> (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
a forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"," forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ArgName
x (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
b)) forall a. Semigroup a => a -> a -> a
<> m Doc
")"
UnquoteTactic Term
v Term
_ Type
_ -> do
Expr
e <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
v
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) (forall a. a -> NamedArg a
defaultNamedArg Expr
e))
CheckMetaInst MetaId
x -> do
MetaVariable
m <- 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 } -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
IsSort{} -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"is a sort"
CheckType Type
t ->
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t 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" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Arg Term
lk forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"|-" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx Term
t forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Modality
mod forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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 = forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx a
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (m Doc
cmp forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx b
y)