{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.MetaVars.Mention where

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

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 :: forall t. MentionsMeta t => 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 = \case
    Var Int
_ [Elim]
args   -> [Elim] -> Bool
forall t. MentionsMeta t => t -> Bool
mm [Elim]
args
    Lam ArgInfo
_ Abs Term
b      -> Abs Term -> Bool
forall t. MentionsMeta t => t -> Bool
mm Abs Term
b
    Lit{}        -> Bool
False
    Def QName
_ [Elim]
args   -> [Elim] -> Bool
forall t. MentionsMeta t => t -> Bool
mm [Elim]
args
    Con ConHead
_ ConInfo
_ [Elim]
args -> [Elim] -> Bool
forall t. MentionsMeta t => t -> Bool
mm [Elim]
args
    Pi Dom' Term Type
a Abs Type
b       -> (Dom' Term Type, Abs Type) -> Bool
forall t. MentionsMeta t => t -> Bool
mm (Dom' Term Type
a, Abs Type
b)
    Sort Sort' Term
s       -> Sort' Term -> Bool
forall t. MentionsMeta t => t -> Bool
mm Sort' Term
s
    Level Level' Term
l      -> Level' Term -> Bool
forall t. MentionsMeta t => t -> Bool
mm Level' Term
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 [Elim]
args -> MetaId -> HashSet MetaId -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
HashSet.member MetaId
y HashSet MetaId
xs Bool -> Bool -> Bool
|| [Elim] -> Bool
forall t. MentionsMeta t => t -> Bool
mm [Elim]
args   -- TODO: we really only have to look one level deep at meta args
    where
      mm :: forall t. MentionsMeta t => t -> Bool
      mm :: forall t. MentionsMeta t => t -> Bool
mm = HashSet MetaId -> t -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs

instance MentionsMeta Level where
  mentionsMetas :: HashSet MetaId -> Level' Term -> 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
_ Term
a) = HashSet MetaId -> Term -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Term
a

instance MentionsMeta Blocker where
  mentionsMetas :: HashSet MetaId -> Blocker -> Bool
mentionsMetas HashSet MetaId
xs (UnblockOnAll Set Blocker
bs)  = HashSet MetaId -> [Blocker] -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs ([Blocker] -> Bool) -> [Blocker] -> Bool
forall a b. (a -> b) -> a -> b
$ Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
bs
  mentionsMetas HashSet MetaId
xs (UnblockOnAny Set Blocker
bs)  = HashSet MetaId -> [Blocker] -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs ([Blocker] -> Bool) -> [Blocker] -> Bool
forall a b. (a -> b) -> a -> b
$ Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
bs
  mentionsMetas HashSet MetaId
xs (UnblockOnMeta MetaId
x)  = MetaId -> HashSet MetaId -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
HashSet.member MetaId
x HashSet MetaId
xs
  mentionsMetas HashSet MetaId
xs UnblockOnProblem{} = Bool
False
  mentionsMetas HashSet MetaId
xs UnblockOnDef{}     = Bool
False

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

instance MentionsMeta Sort where
  mentionsMetas :: HashSet MetaId -> Sort' Term -> Bool
mentionsMetas HashSet MetaId
xs = \case
    Univ Univ
_ Level' Term
l   -> HashSet MetaId -> Level' Term -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Level' Term
l
    Inf Univ
_ Integer
_    -> Bool
False
    Sort' Term
SizeUniv   -> Bool
False
    Sort' Term
LockUniv   -> Bool
False
    Sort' Term
LevelUniv  -> Bool
False
    Sort' Term
IntervalUniv -> Bool
False
    PiSort Dom' Term Term
a Sort' Term
s1 Abs (Sort' Term)
s2 -> HashSet MetaId
-> (Dom' Term Term, Sort' Term, Abs (Sort' Term)) -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (Dom' Term Term
a, Sort' Term
s1, Abs (Sort' Term)
s2)
    FunSort Sort' Term
s1 Sort' Term
s2 -> HashSet MetaId -> (Sort' Term, Sort' Term) -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (Sort' Term
s1, Sort' Term
s2)
    UnivSort Sort' Term
s -> HashSet MetaId -> Sort' Term -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Sort' Term
s
    MetaS MetaId
m [Elim]
es -> MetaId -> HashSet MetaId -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
HashSet.member MetaId
m HashSet MetaId
xs Bool -> Bool -> Bool
|| HashSet MetaId -> [Elim] -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs [Elim]
es
    DefS QName
d [Elim]
es  -> HashSet MetaId -> [Elim] -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs [Elim]
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 b, MentionsMeta c, MentionsMeta d)
  => MentionsMeta (a, b, c, d) where
  mentionsMetas :: HashSet MetaId -> (a, b, c, d) -> Bool
mentionsMetas HashSet MetaId
xs (a
a, b
b, c
c, d
d) =
    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 Bool -> Bool -> Bool
||
    HashSet MetaId -> d -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs d
d

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 LocalEquation where
  mentionsMetas :: HashSet MetaId -> LocalEquation -> Bool
mentionsMetas HashSet MetaId
xs (LocalEquation Tele (Dom' Term Type)
g Term
t Term
u Type
a) = HashSet MetaId -> (Tele (Dom' Term Type), Term, Term, Type) -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (Tele (Dom' Term Type)
g, Term
t, Term
u, Type
a)

instance MentionsMeta Constraint where
  mentionsMetas :: HashSet MetaId -> Constraint -> Bool
mentionsMetas HashSet MetaId
xs = \case
    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 [Elim]
as [Elim]
bs -> ((Type, Term), ([Elim], [Elim])) -> Bool
forall t. MentionsMeta t => t -> Bool
mm ((Type
t, Term
v), ([Elim]
as, [Elim]
bs))
    LevelCmp Comparison
_ Level' Term
u Level' Term
v      -> (Level' Term, Level' Term) -> Bool
forall t. MentionsMeta t => t -> Bool
mm (Level' Term
u, Level' Term
v)
    SortCmp Comparison
_ Sort' Term
a Sort' Term
b       -> (Sort' Term, Sort' Term) -> Bool
forall t. MentionsMeta t => t -> Bool
mm (Sort' Term
a, Sort' Term
b)
    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
    ResolveInstanceHead{} -> Bool
True -- TODO
    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' Term
a     -> Sort' Term -> Bool
forall t. MentionsMeta t => t -> Bool
mm Sort' Term
a
    HasPTSRule Dom' Term Type
a Abs (Sort' Term)
b      -> (Dom' Term Type, Abs (Sort' Term)) -> Bool
forall t. MentionsMeta t => t -> Bool
mm (Dom' Term Type
a, Abs (Sort' Term)
b)
    UnquoteTactic Term
tac Term
hole Type
goal -> Bool
False
    CheckDataSort QName
q Sort' Term
s   -> Sort' Term -> Bool
forall t. MentionsMeta t => t -> Bool
mm Sort' Term
s
    CheckMetaInst MetaId
m     -> Bool
True   -- TODO
    CheckType Type
t         -> Type -> Bool
forall t. MentionsMeta t => t -> Bool
mm Type
t
    CheckLockedVars Term
a Type
b Arg Term
c Type
d -> ((Term, Type), (Arg Term, Type)) -> Bool
forall t. MentionsMeta t => t -> Bool
mm ((Term
a, Type
b), (Arg Term
c, Type
d))
    UsableAtModality WhyCheckModality
_ Maybe (Sort' Term)
ms Modality
mod Term
t -> (Maybe (Sort' Term), Term) -> Bool
forall t. MentionsMeta t => t -> Bool
mm (Maybe (Sort' Term)
ms, Term
t)
    RewConstraint LocalEquation
e     -> LocalEquation -> Bool
forall t. MentionsMeta t => t -> Bool
mm LocalEquation
e
    where
      mm :: forall t. MentionsMeta t => t -> Bool
      mm :: forall t. MentionsMeta t => t -> Bool
mm = HashSet MetaId -> t -> Bool
forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs

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