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 = forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
_ Elims
args   -> forall t. MentionsMeta t => t -> Bool
mm Elims
args
    Lam ArgInfo
_ Abs Term
b      -> forall t. MentionsMeta t => t -> Bool
mm Abs Term
b
    Lit{}        -> Bool
False
    Def QName
_ Elims
args   -> forall t. MentionsMeta t => t -> Bool
mm Elims
args
    Con ConHead
_ ConInfo
_ Elims
args -> forall t. MentionsMeta t => t -> Bool
mm Elims
args
    Pi Dom Type
a Abs Type
b       -> forall t. MentionsMeta t => t -> Bool
mm (Dom Type
a, Abs Type
b)
    Sort Sort
s       -> forall t. MentionsMeta t => t -> Bool
mm Sort
s
    Level Level
l      -> 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 -> forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member MetaId
y HashSet MetaId
xs Bool -> Bool -> 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 :: forall t. MentionsMeta t => t -> Bool
      mm :: forall t. MentionsMeta t => t -> Bool
mm = forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs

instance MentionsMeta Level where
  mentionsMetas :: HashSet MetaId -> Level -> Bool
mentionsMetas HashSet MetaId
xs (Max Integer
_ [PlusLevel' Term]
as) = 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) = 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)  = forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Blocker
bs
  mentionsMetas HashSet MetaId
xs (UnblockOnAny Set Blocker
bs)  = forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Blocker
bs
  mentionsMetas HashSet MetaId
xs (UnblockOnMeta MetaId
x)  = forall a. (Eq 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
s Term
t) = 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 = \case
    Type Level
l     -> forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Level
l
    Prop Level
l     -> forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Level
l
    Inf IsFibrant
_ Integer
_    -> Bool
False
    SSet Level
l     -> forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Level
l
    Sort
SizeUniv   -> Bool
False
    Sort
LockUniv   -> Bool
False
    Sort
IntervalUniv -> Bool
False
    PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (Dom' Term Term
a, Sort
s1, Abs Sort
s2)
    FunSort Sort
s1 Sort
s2 -> forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (Sort
s1, Sort
s2)
    UnivSort Sort
s -> forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Sort
s
    MetaS MetaId
m Elims
es -> forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member MetaId
m HashSet MetaId
xs Bool -> Bool -> Bool
|| forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs Elims
es
    DefS QName
d Elims
es  -> 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 = forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 | 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 = forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (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 = forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom

instance MentionsMeta t => MentionsMeta [t] where
  mentionsMetas :: HashSet MetaId -> [t] -> Bool
mentionsMetas HashSet MetaId
xs = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (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 = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (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) = forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs a
a Bool -> Bool -> 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) = forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs a
a Bool -> Bool -> Bool
|| forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs b
b Bool -> Bool -> 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 = forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs (forall a. Closure a -> a
clValue Closure a
cl)

instance MentionsMeta Elim where
  mentionsMetas :: HashSet MetaId -> Elim' Term -> Bool
mentionsMetas HashSet MetaId
xs Proj{} = Bool
False
  mentionsMetas HashSet MetaId
xs (Apply Arg Term
v) = 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) = 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) = 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 = forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
mentionsMetas HashSet MetaId
xs 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 = \case
    ValueCmp Comparison
_ CompareAs
t Term
u Term
v    -> forall t. MentionsMeta t => t -> Bool
mm (CompareAs
t, Term
u, Term
v)
    ValueCmpOnFace Comparison
_ Term
p Type
t Term
u Term
v    -> 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 -> forall t. MentionsMeta t => t -> Bool
mm ((Type
t, Term
v), (Elims
as, Elims
bs))
    LevelCmp Comparison
_ Level
u Level
v      -> forall t. MentionsMeta t => t -> Bool
mm (Level
u, Level
v)
    SortCmp Comparison
_ Sort
a Sort
b       -> forall t. MentionsMeta t => t -> Bool
mm (Sort
a, Sort
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
    IsEmpty Range
r Type
t         -> forall t. MentionsMeta t => t -> Bool
mm Type
t
    CheckSizeLtSat Term
t    -> forall t. MentionsMeta t => t -> Bool
mm Term
t
    CheckFunDef{}       -> Bool
True   -- not sure what metas this depends on
    HasBiggerSort Sort
a     -> forall t. MentionsMeta t => t -> Bool
mm Sort
a
    HasPTSRule Dom Type
a Abs Sort
b      -> forall t. MentionsMeta t => t -> Bool
mm (Dom Type
a, Abs Sort
b)
    UnquoteTactic Term
tac Term
hole Type
goal -> Bool
False
    CheckDataSort QName
q Sort
s   -> forall t. MentionsMeta t => t -> Bool
mm Sort
s
    CheckMetaInst MetaId
m     -> Bool
True   -- TODO
    CheckType Type
t         -> forall t. MentionsMeta t => t -> Bool
mm Type
t
    CheckLockedVars Term
a Type
b Arg Term
c Type
d -> forall t. MentionsMeta t => t -> Bool
mm ((Term
a, Type
b), (Arg Term
c, Type
d))
    UsableAtModality WhyCheckModality
_ Maybe Sort
ms Modality
mod Term
t -> forall t. MentionsMeta t => t -> Bool
mm (Maybe Sort
ms, Term
t)
    where
      mm :: forall t. MentionsMeta t => t -> Bool
      mm :: forall t. MentionsMeta t => t -> Bool
mm = 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 -> 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