module Agda.TypeChecking.MetaVars.Mention where

import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad

class MentionsMeta t where
  mentionsMetas :: HashSet MetaId -> t -> Bool

mentionsMeta :: MentionsMeta t => MetaId -> t -> Bool
mentionsMeta :: MetaId -> t -> Bool
mentionsMeta = HashSet MetaId -> t -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas (HashSet MetaId -> t -> Bool)
-> (MetaId -> HashSet MetaId) -> MetaId -> t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> HashSet MetaId
forall a. Hashable a => a -> HashSet a
HashSet.singleton

instance MentionsMeta Term where
  mentionsMetas :: HashSet MetaId -> Term -> Bool
mentionsMetas HashSet MetaId
xs Term
v = case Term
v of
    Var Int
_ Elims
args   -> Elims -> Bool
forall t. MentionsMeta t => t -> Bool
mm Elims
args
    Lam ArgInfo
_ Abs Term
b      -> Abs Term -> Bool
forall t. MentionsMeta t => t -> Bool
mm Abs Term
b
    Lit{}        -> Bool
False
    Def QName
_ Elims
args   -> Elims -> Bool
forall t. MentionsMeta t => t -> Bool
mm Elims
args
    Con ConHead
_ ConInfo
_ Elims
args -> Elims -> Bool
forall t. MentionsMeta t => t -> Bool
mm Elims
args
    Pi Dom Type
a Abs Type
b       -> (Dom Type, Abs Type) -> Bool
forall t. MentionsMeta t => t -> Bool
mm (Dom Type
a, Abs Type
b)
    Sort Sort
s       -> Sort -> Bool
forall t. MentionsMeta t => t -> Bool
mm Sort
s
    Level Level
l      -> Level -> Bool
forall t. MentionsMeta t => t -> Bool
mm Level
l
    Dummy{}      -> Bool
False
    DontCare Term
v   -> Bool
False   -- we don't have to look inside don't cares when deciding to wake constraints
    MetaV MetaId
y Elims
args -> MetaId -> HashSet MetaId -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member MetaId
y HashSet MetaId
xs Bool -> Bool -> Bool
|| Elims -> Bool
forall t. MentionsMeta t => t -> Bool
mm Elims
args   -- TODO: we really only have to look one level deep at meta args
    where
      mm :: t -> Bool
mm t
v = HashSet MetaId -> t -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs t
v

instance MentionsMeta Level where
  mentionsMetas :: HashSet MetaId -> Level -> Bool
mentionsMetas HashSet MetaId
xs (Max Integer
_ [PlusLevel' Term]
as) = HashSet MetaId -> [PlusLevel' Term] -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs [PlusLevel' Term]
as

instance MentionsMeta PlusLevel where
  mentionsMetas :: HashSet MetaId -> PlusLevel' Term -> Bool
mentionsMetas HashSet MetaId
xs (Plus Integer
_ LevelAtom' Term
a) = HashSet MetaId -> LevelAtom' Term -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs LevelAtom' Term
a

instance MentionsMeta LevelAtom where
  mentionsMetas :: HashSet MetaId -> LevelAtom' Term -> Bool
mentionsMetas HashSet MetaId
xs LevelAtom' Term
l = case LevelAtom' Term
l of
    MetaLevel MetaId
m Elims
vs   -> MetaId -> HashSet MetaId -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member MetaId
m HashSet MetaId
xs Bool -> Bool -> Bool
|| HashSet MetaId -> Elims -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Elims
vs
    BlockedLevel MetaId
m Term
_ -> MetaId -> HashSet MetaId -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member MetaId
m HashSet MetaId
xs  -- if it's blocked on a different meta it doesn't matter if it mentions the meta somewhere else
    UnreducedLevel Term
l -> HashSet MetaId -> Term -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Term
l
    NeutralLevel NotBlocked
_ Term
l -> HashSet MetaId -> Term -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Term
l

instance MentionsMeta Type where
    mentionsMetas :: HashSet MetaId -> Type -> Bool
mentionsMetas HashSet MetaId
xs (El Sort
s Term
t) = HashSet MetaId -> (Sort, Term) -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (Sort
s, Term
t)

instance MentionsMeta Sort where
  mentionsMetas :: HashSet MetaId -> Sort -> Bool
mentionsMetas HashSet MetaId
xs Sort
s = case Sort
s of
    Type Level
l     -> HashSet MetaId -> Level -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Level
l
    Prop Level
l     -> HashSet MetaId -> Level -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Level
l
    Sort
Inf        -> Bool
False
    Sort
SizeUniv   -> Bool
False
    PiSort Dom Type
a Abs Sort
s -> HashSet MetaId -> (Dom Type, Abs Sort) -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (Dom Type
a, Abs Sort
s)
    FunSort Sort
s1 Sort
s2 -> HashSet MetaId -> (Sort, Sort) -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (Sort
s1, Sort
s2)
    UnivSort Sort
s -> HashSet MetaId -> Sort -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Sort
s
    MetaS MetaId
m Elims
es -> MetaId -> HashSet MetaId -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member MetaId
m HashSet MetaId
xs Bool -> Bool -> Bool
|| HashSet MetaId -> Elims -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Elims
es
    DefS QName
d Elims
es  -> HashSet MetaId -> Elims -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Elims
es
    DummyS{}   -> Bool
False

instance MentionsMeta t => MentionsMeta (Abs t) where
  mentionsMetas :: HashSet MetaId -> Abs t -> Bool
mentionsMetas HashSet MetaId
xs = HashSet MetaId -> t -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (t -> Bool) -> (Abs t -> t) -> Abs t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Abs t -> t
forall a. Abs a -> a
unAbs

instance MentionsMeta t => MentionsMeta (Arg t) where
  mentionsMetas :: HashSet MetaId -> Arg t -> Bool
mentionsMetas HashSet MetaId
xs Arg t
a | Arg t -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Arg t
a = Bool
False
  -- ^ we don't have to look inside irrelevant arguments when deciding to wake constraints
  mentionsMetas HashSet MetaId
xs Arg t
a = HashSet MetaId -> t -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (Arg t -> t
forall e. Arg e -> e
unArg Arg t
a)

instance MentionsMeta t => MentionsMeta (Dom t) where
  mentionsMetas :: HashSet MetaId -> Dom t -> Bool
mentionsMetas HashSet MetaId
xs = HashSet MetaId -> t -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (t -> Bool) -> (Dom t -> t) -> Dom t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom t -> t
forall t e. Dom' t e -> e
unDom

instance MentionsMeta t => MentionsMeta [t] where
  mentionsMetas :: HashSet MetaId -> [t] -> Bool
mentionsMetas HashSet MetaId
xs = (t -> Bool) -> [t] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (HashSet MetaId -> t -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs)

instance MentionsMeta t => MentionsMeta (Maybe t) where
  mentionsMetas :: HashSet MetaId -> Maybe t -> Bool
mentionsMetas HashSet MetaId
xs = Bool -> (t -> Bool) -> Maybe t -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (HashSet MetaId -> t -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs)

instance (MentionsMeta a, MentionsMeta b) => MentionsMeta (a, b) where
  mentionsMetas :: HashSet MetaId -> (a, b) -> Bool
mentionsMetas HashSet MetaId
xs (a
a, b
b) = HashSet MetaId -> a -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs a
a Bool -> Bool -> Bool
|| HashSet MetaId -> b -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs b
b

instance (MentionsMeta a, MentionsMeta b, MentionsMeta c) => MentionsMeta (a, b, c) where
  mentionsMetas :: HashSet MetaId -> (a, b, c) -> Bool
mentionsMetas HashSet MetaId
xs (a
a, b
b, c
c) = HashSet MetaId -> a -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs a
a Bool -> Bool -> Bool
|| HashSet MetaId -> b -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs b
b Bool -> Bool -> Bool
|| HashSet MetaId -> c -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs c
c

instance MentionsMeta a => MentionsMeta (Closure a) where
  mentionsMetas :: HashSet MetaId -> Closure a -> Bool
mentionsMetas HashSet MetaId
xs Closure a
cl = HashSet MetaId -> a -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (Closure a -> a
forall a. Closure a -> a
clValue Closure a
cl)

instance MentionsMeta Elim where
  mentionsMetas :: HashSet MetaId -> Elim -> Bool
mentionsMetas HashSet MetaId
xs Proj{} = Bool
False
  mentionsMetas HashSet MetaId
xs (Apply Arg Term
v) = HashSet MetaId -> Arg Term -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Arg Term
v
  mentionsMetas HashSet MetaId
xs (IApply Term
y0 Term
y1 Term
v) = HashSet MetaId -> (Term, Term, Term) -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (Term
y0,Term
y1,Term
v)

instance MentionsMeta a => MentionsMeta (Tele a) where
  mentionsMetas :: HashSet MetaId -> Tele a -> Bool
mentionsMetas HashSet MetaId
xs Tele a
EmptyTel = Bool
False
  mentionsMetas HashSet MetaId
xs (ExtendTel a
a Abs (Tele a)
b) = HashSet MetaId -> (a, Abs (Tele a)) -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (a
a, Abs (Tele a)
b)

instance MentionsMeta ProblemConstraint where
  mentionsMetas :: HashSet MetaId -> ProblemConstraint -> Bool
mentionsMetas HashSet MetaId
xs = HashSet MetaId -> Closure Constraint -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (Closure Constraint -> Bool)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint

instance MentionsMeta Constraint where
  mentionsMetas :: HashSet MetaId -> Constraint -> Bool
mentionsMetas HashSet MetaId
xs Constraint
c = case Constraint
c of
    ValueCmp Comparison
_ CompareAs
t Term
u Term
v    -> (CompareAs, Term, Term) -> Bool
forall t. MentionsMeta t => t -> Bool
mm (CompareAs
t, Term
u, Term
v)
    ValueCmpOnFace Comparison
_ Term
p Type
t Term
u Term
v    -> ((Term, Type), Term, Term) -> Bool
forall t. MentionsMeta t => t -> Bool
mm ((Term
p,Type
t), Term
u, Term
v)
    ElimCmp [Polarity]
_ [IsForced]
_ Type
t Term
v Elims
as Elims
bs -> ((Type, Term), (Elims, Elims)) -> Bool
forall t. MentionsMeta t => t -> Bool
mm ((Type
t, Term
v), (Elims
as, Elims
bs))
    LevelCmp Comparison
_ Level
u Level
v      -> (Level, Level) -> Bool
forall t. MentionsMeta t => t -> Bool
mm (Level
u, Level
v)
    TelCmp Type
a Type
b Comparison
_ Telescope
u Telescope
v    -> ((Type, Type), (Telescope, Telescope)) -> Bool
forall t. MentionsMeta t => t -> Bool
mm ((Type
a, Type
b), (Telescope
u, Telescope
v))
    SortCmp Comparison
_ Sort
a Sort
b       -> (Sort, Sort) -> Bool
forall t. MentionsMeta t => t -> Bool
mm (Sort
a, Sort
b)
    Guarded{}           -> Bool
False  -- This gets woken up when the problem it's guarded by is solved
    UnBlock MetaId
_           -> Bool
True   -- this might be a postponed typechecking
                                  -- problem and we don't have a handle on
                                  -- what metas it depends on
    FindInstance{}      -> Bool
True   -- this needs to be woken up for any meta
    IsEmpty Range
r Type
t         -> Type -> Bool
forall t. MentionsMeta t => t -> Bool
mm Type
t
    CheckSizeLtSat Term
t    -> Term -> Bool
forall t. MentionsMeta t => t -> Bool
mm Term
t
    CheckFunDef{}       -> Bool
True   -- not sure what metas this depends on
    HasBiggerSort Sort
a     -> Sort -> Bool
forall t. MentionsMeta t => t -> Bool
mm Sort
a
    HasPTSRule Dom Type
a Abs Sort
b      -> (Dom Type, Abs Sort) -> Bool
forall t. MentionsMeta t => t -> Bool
mm (Dom Type
a, Abs Sort
b)
    UnquoteTactic Maybe MetaId
bl Term
tac Term
hole Type
goal -> case Maybe MetaId
bl of
      Maybe MetaId
Nothing -> Bool
False
      Just MetaId
m  -> MetaId -> HashSet MetaId -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member MetaId
m HashSet MetaId
xs
    CheckMetaInst MetaId
m     -> Bool
True   -- TODO
    where
      mm :: t -> Bool
mm t
v = HashSet MetaId -> t -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs t
v

instance MentionsMeta CompareAs where
  mentionsMetas :: HashSet MetaId -> CompareAs -> Bool
mentionsMetas HashSet MetaId
xs = \case
    AsTermsOf Type
a -> HashSet MetaId -> Type -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Type
a
    CompareAs
AsSizes -> Bool
False
    CompareAs
AsTypes -> Bool
False

-- instance (Ord k, MentionsMeta e) => MentionsMeta (Map k e) where
--   mentionsMeta = traverse mentionsMeta