module Agda.TypeChecking.MetaVars.Mention where import Agda.Syntax.Common import Agda.Syntax.Internal import Agda.TypeChecking.Monad class MentionsMeta t where mentionsMeta :: MetaId -> t -> Bool instance MentionsMeta Term where mentionsMeta x v = case v of Var _ args -> mm args Lam _ b -> mm b Lit{} -> False Def _ args -> mm args Con _ _ args -> mm args Pi a b -> mm (a, b) Sort s -> mm s Level l -> mm l Dummy{} -> False DontCare v -> False -- we don't have to look inside don't cares when deciding to wake constraints MetaV y args -> x == y || mm args -- TODO: we really only have to look one level deep at meta args where mm v = mentionsMeta x v instance MentionsMeta Level where mentionsMeta x (Max as) = mentionsMeta x as instance MentionsMeta PlusLevel where mentionsMeta x ClosedLevel{} = False mentionsMeta x (Plus _ a) = mentionsMeta x a instance MentionsMeta LevelAtom where mentionsMeta x l = case l of MetaLevel m vs -> x == m || mentionsMeta x vs BlockedLevel m _ -> x == m -- if it's blocked on a different meta it doesn't matter if it mentions the meta somewhere else UnreducedLevel l -> mentionsMeta x l NeutralLevel _ l -> mentionsMeta x l instance MentionsMeta Type where mentionsMeta x (El s t) = mentionsMeta x (s, t) instance MentionsMeta Sort where mentionsMeta x s = case s of Type l -> mentionsMeta x l Prop l -> mentionsMeta x l Inf -> False SizeUniv -> False PiSort s1 s2 -> mentionsMeta x (s1, s2) UnivSort s -> mentionsMeta x s MetaS m es -> x == m || mentionsMeta x es DefS d es -> mentionsMeta x es DummyS{} -> False instance MentionsMeta t => MentionsMeta (Abs t) where mentionsMeta x = mentionsMeta x . unAbs instance MentionsMeta t => MentionsMeta (Arg t) where mentionsMeta x a | isIrrelevant a = False -- ^ we don't have to look inside irrelevant arguments when deciding to wake constraints mentionsMeta x a = mentionsMeta x (unArg a) instance MentionsMeta t => MentionsMeta (Dom t) where mentionsMeta x = mentionsMeta x . unDom instance MentionsMeta t => MentionsMeta [t] where mentionsMeta x = any (mentionsMeta x) instance MentionsMeta t => MentionsMeta (Maybe t) where mentionsMeta x = maybe False (mentionsMeta x) instance (MentionsMeta a, MentionsMeta b) => MentionsMeta (a, b) where mentionsMeta x (a, b) = mentionsMeta x a || mentionsMeta x b instance (MentionsMeta a, MentionsMeta b, MentionsMeta c) => MentionsMeta (a, b, c) where mentionsMeta x (a, b, c) = mentionsMeta x a || mentionsMeta x b || mentionsMeta x c instance MentionsMeta a => MentionsMeta (Closure a) where mentionsMeta x cl = mentionsMeta x (clValue cl) instance MentionsMeta Elim where mentionsMeta x Proj{} = False mentionsMeta x (Apply v) = mentionsMeta x v mentionsMeta x (IApply y0 y1 v) = mentionsMeta x (y0,y1,v) instance MentionsMeta a => MentionsMeta (Tele a) where mentionsMeta x EmptyTel = False mentionsMeta x (ExtendTel a b) = mentionsMeta x (a, b) instance MentionsMeta ProblemConstraint where mentionsMeta x = mentionsMeta x . theConstraint instance MentionsMeta Constraint where mentionsMeta x c = case c of ValueCmp _ t u v -> mm (t, u, v) ValueCmpOnFace _ p t u v -> mm ((p,t), u, v) ElimCmp _ _ t v as bs -> mm ((t, v), (as, bs)) LevelCmp _ u v -> mm (u, v) TypeCmp _ a b -> mm (a, b) TelCmp a b _ u v -> mm ((a, b), (u, v)) SortCmp _ a b -> mm (a, b) Guarded{} -> False -- This gets woken up when the problem it's guarded by is solved UnBlock _ -> True -- this might be a postponed typechecking -- problem and we don't have a handle on -- what metas it depends on FindInstance{} -> True -- this needs to be woken up for any meta IsEmpty r t -> mm t CheckSizeLtSat t -> mm t CheckFunDef{} -> True -- not sure what metas this depends on HasBiggerSort a -> mm a HasPTSRule a b -> mm (a, b) UnquoteTactic bl tac hole goal -> Just x == bl where mm v = mentionsMeta x v -- instance (Ord k, MentionsMeta e) => MentionsMeta (Map k e) where -- mentionsMeta = traverse mentionsMeta