{-# LANGUAGE TypeFamilies #-}

-- | Extract all names from things.

module Agda.Syntax.Internal.Names where

import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set

import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.Syntax.Internal
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Abstract as A

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.CompiledClause


import Agda.Utils.Impossible

class NamesIn a where
  namesIn :: a -> Set QName

  default namesIn :: (Foldable f, NamesIn b, f b ~ a) => a -> Set QName
  namesIn = (b -> Set QName) -> f b -> Set QName
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap b -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn

instance NamesIn a => NamesIn (Maybe a)              where
instance NamesIn a => NamesIn [a]                    where
instance NamesIn a => NamesIn (NonEmpty a)           where
instance NamesIn a => NamesIn (Arg a)                where
instance NamesIn a => NamesIn (Dom a)                where
instance NamesIn a => NamesIn (Named n a)            where
instance NamesIn a => NamesIn (Abs a)                where
instance NamesIn a => NamesIn (WithArity a)          where
instance NamesIn a => NamesIn (Tele a)               where
instance NamesIn a => NamesIn (C.FieldAssignment' a) where

instance (NamesIn a, NamesIn b) => NamesIn (a, b) where
  namesIn :: (a, b) -> Set QName
namesIn (a
x, b
y) = Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
Set.union (a -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn a
x) (b -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn b
y)

instance (NamesIn a, NamesIn b, NamesIn c) => NamesIn (a, b, c) where
  namesIn :: (a, b, c) -> Set QName
namesIn (a
x, b
y, c
z) = (a, (b, c)) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (a
x, (b
y, c
z))

instance (NamesIn a, NamesIn b, NamesIn c, NamesIn d) => NamesIn (a, b, c, d) where
  namesIn :: (a, b, c, d) -> Set QName
namesIn (a
x, b
y, c
z, d
u) = ((a, b), (c, d)) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn ((a
x, b
y), (c
z, d
u))

instance NamesIn CompKit where
  namesIn :: CompKit -> Set QName
namesIn (CompKit Maybe QName
a Maybe QName
b) = (Maybe QName, Maybe QName) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Maybe QName
a,Maybe QName
b)

-- Andreas, 2017-07-27
-- In the following clauses, the choice of fields is not obvious
-- to the reader.  Please comment on the choices.
--
-- Also, this would be more robust if these were constructor-style
-- matches instead of record-style matches.
-- If someone adds a field containing names, this would go unnoticed.

instance NamesIn Definition where
  namesIn :: Definition -> Set QName
namesIn Definition
def = (Type, Defn, [LocalDisplayForm]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Definition -> Type
defType Definition
def, Definition -> Defn
theDef Definition
def, Definition -> [LocalDisplayForm]
defDisplay Definition
def)

instance NamesIn Defn where
  namesIn :: Defn -> Set QName
namesIn Defn
def = case Defn
def of
    Defn
Axiom -> Set QName
forall a. Set a
Set.empty
    DataOrRecSig{} -> Set QName
forall a. Set a
Set.empty
    GeneralizableVar{} -> Set QName
forall a. Set a
Set.empty
    -- Andreas 2017-07-27, Q: which names can be in @cc@ which are not already in @cl@?
    Function    { funClauses :: Defn -> [Clause]
funClauses = [Clause]
cl, funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc }              -> ([Clause], Maybe CompiledClauses) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn ([Clause]
cl, Maybe CompiledClauses
cc)
    Datatype    { dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
cl, dataCons :: Defn -> [QName]
dataCons = [QName]
cs, dataSort :: Defn -> Sort
dataSort = Sort
s }   -> (Maybe Clause, [QName], Sort) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Maybe Clause
cl, [QName]
cs, Sort
s)
    Record      { recClause :: Defn -> Maybe Clause
recClause = Maybe Clause
cl, recConHead :: Defn -> ConHead
recConHead = ConHead
c, recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs, recComp :: Defn -> CompKit
recComp = CompKit
comp } -> (Maybe Clause, ConHead, [Dom QName], CompKit) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Maybe Clause
cl, ConHead
c, [Dom QName]
fs, CompKit
comp)
      -- Don't need recTel since those will be reachable from the constructor
    Constructor { conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c, conData :: Defn -> QName
conData = QName
d, conComp :: Defn -> CompKit
conComp = CompKit
kit, conProj :: Defn -> Maybe [QName]
conProj = Maybe [QName]
fs }        -> (ConHead, QName, CompKit, Maybe [QName]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (ConHead
c, QName
d, CompKit
kit, Maybe [QName]
fs)
    Primitive   { primClauses :: Defn -> [Clause]
primClauses = [Clause]
cl, primCompiled :: Defn -> Maybe CompiledClauses
primCompiled = Maybe CompiledClauses
cc }            -> ([Clause], Maybe CompiledClauses) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn ([Clause]
cl, Maybe CompiledClauses
cc)
    AbstractDefn{} -> Set QName
forall a. HasCallStack => a
__IMPOSSIBLE__

instance NamesIn Clause where
  namesIn :: Clause -> Set QName
namesIn Clause{ clauseTel :: Clause -> Telescope
clauseTel = Telescope
tel, namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
ps, clauseBody :: Clause -> Maybe Term
clauseBody = Maybe Term
b, clauseType :: Clause -> Maybe (Arg Type)
clauseType = Maybe (Arg Type)
t } =
    (Telescope, NAPs, Maybe Term, Maybe (Arg Type)) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Telescope
tel, NAPs
ps, Maybe Term
b, Maybe (Arg Type)
t)

instance NamesIn CompiledClauses where
  namesIn :: CompiledClauses -> Set QName
namesIn (Case Arg Int
_ Case CompiledClauses
c) = Case CompiledClauses -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Case CompiledClauses
c
  namesIn (Done [Arg ArgName]
_ Term
v) = Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
  namesIn CompiledClauses
Fail       = Set QName
forall a. Set a
Set.empty

-- Andreas, 2017-07-27
-- Why ignoring the litBranches?
instance NamesIn a => NamesIn (Case a) where
  namesIn :: Case a -> Set QName
namesIn Branches{ conBranches :: forall c. Case c -> Map QName (WithArity c)
conBranches = Map QName (WithArity a)
bs, catchAllBranch :: forall c. Case c -> Maybe c
catchAllBranch = Maybe a
c } =
    ([(QName, WithArity a)], Maybe a) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Map QName (WithArity a) -> [(QName, WithArity a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map QName (WithArity a)
bs, Maybe a
c)

instance NamesIn (Pattern' a) where
  namesIn :: Pattern' a -> Set QName
namesIn Pattern' a
p = case Pattern' a
p of
    VarP{}        -> Set QName
forall a. Set a
Set.empty
    LitP PatternInfo
_ Literal
l      -> Literal -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Literal
l
    DotP PatternInfo
_ Term
v      -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
    ConP ConHead
c ConPatternInfo
_ [NamedArg (Pattern' a)]
args -> (ConHead, [NamedArg (Pattern' a)]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (ConHead
c, [NamedArg (Pattern' a)]
args)
    DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
args -> (QName, [NamedArg (Pattern' a)]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (QName
q, [NamedArg (Pattern' a)]
args)
    ProjP ProjOrigin
_ QName
f     -> QName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn QName
f
    IApplyP PatternInfo
_ Term
t Term
u a
_ -> (Term, Term) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Term
t, Term
u)

instance NamesIn a => NamesIn (Type' a) where
  namesIn :: Type' a -> Set QName
namesIn (El Sort
s a
t) = (Sort, a) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Sort
s, a
t)

instance NamesIn Sort where
  namesIn :: Sort -> Set QName
namesIn Sort
s = case Sort
s of
    Type Level' Term
l   -> Level' Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Level' Term
l
    Prop Level' Term
l   -> Level' Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Level' Term
l
    Sort
Inf      -> Set QName
forall a. Set a
Set.empty
    Sort
SizeUniv -> Set QName
forall a. Set a
Set.empty
    PiSort Dom' Term Type
a Abs Sort
b -> (Dom' Term Type, Abs Sort) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Dom' Term Type
a, Abs Sort
b)
    FunSort Sort
a Sort
b -> (Sort, Sort) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Sort
a, Sort
b)
    UnivSort Sort
a -> Sort -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Sort
a
    MetaS MetaId
_ [Elim' Term]
es -> [Elim' Term] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [Elim' Term]
es
    DefS QName
d [Elim' Term]
es  -> (QName, [Elim' Term]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (QName
d, [Elim' Term]
es)
    DummyS{}   -> Set QName
forall a. Set a
Set.empty

instance NamesIn Term where
  namesIn :: Term -> Set QName
namesIn Term
v = case Term
v of
    Var Int
_ [Elim' Term]
args   -> [Elim' Term] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [Elim' Term]
args
    Lam ArgInfo
_ Abs Term
b      -> Abs Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Abs Term
b
    Lit Literal
l        -> Literal -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Literal
l
    Def QName
f [Elim' Term]
args   -> (QName, [Elim' Term]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (QName
f, [Elim' Term]
args)
    Con ConHead
c ConInfo
_ [Elim' Term]
args -> (ConHead, [Elim' Term]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (ConHead
c, [Elim' Term]
args)
    Pi Dom' Term Type
a Abs Type
b       -> (Dom' Term Type, Abs Type) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Dom' Term Type
a, Abs Type
b)
    Sort Sort
s       -> Sort -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Sort
s
    Level Level' Term
l      -> Level' Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Level' Term
l
    MetaV MetaId
_ [Elim' Term]
args -> [Elim' Term] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [Elim' Term]
args
    DontCare Term
v   -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
    Dummy{}      -> Set QName
forall a. Set a
Set.empty

instance NamesIn Level where
  namesIn :: Level' Term -> Set QName
namesIn (Max Integer
_ [PlusLevel' Term]
ls) = [PlusLevel' Term] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [PlusLevel' Term]
ls

instance NamesIn PlusLevel where
  namesIn :: PlusLevel' Term -> Set QName
namesIn (Plus Integer
_ LevelAtom' Term
l) = LevelAtom' Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn LevelAtom' Term
l

instance NamesIn LevelAtom where
  namesIn :: LevelAtom' Term -> Set QName
namesIn LevelAtom' Term
l = case LevelAtom' Term
l of
    MetaLevel MetaId
_ [Elim' Term]
args -> [Elim' Term] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [Elim' Term]
args
    BlockedLevel MetaId
_ Term
v -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
    NeutralLevel NotBlocked
_ Term
v -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
    UnreducedLevel Term
v -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v

-- For QName literals!
instance NamesIn Literal where
  namesIn :: Literal -> Set QName
namesIn Literal
l = case Literal
l of
    LitNat{}      -> Set QName
forall a. Set a
Set.empty
    LitWord64{}   -> Set QName
forall a. Set a
Set.empty
    LitString{}   -> Set QName
forall a. Set a
Set.empty
    LitChar{}     -> Set QName
forall a. Set a
Set.empty
    LitFloat{}    -> Set QName
forall a. Set a
Set.empty
    LitQName Range
_  QName
x -> QName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn QName
x
    LitMeta{}     -> Set QName
forall a. Set a
Set.empty

instance NamesIn a => NamesIn (Elim' a) where
  namesIn :: Elim' a -> Set QName
namesIn (Apply Arg a
arg) = Arg a -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Arg a
arg
  namesIn (Proj ProjOrigin
_ QName
f)  = QName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn QName
f
  namesIn (IApply a
x a
y a
arg) = (a, a, a) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (a
x, a
y, a
arg)

instance NamesIn QName   where namesIn :: QName -> Set QName
namesIn QName
x = QName -> Set QName
forall a. a -> Set a
Set.singleton QName
x  -- interesting case
instance NamesIn ConHead where namesIn :: ConHead -> Set QName
namesIn ConHead
h = QName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (ConHead -> QName
conName ConHead
h)

instance NamesIn a => NamesIn (Open a)  where

instance NamesIn DisplayForm where
  namesIn :: DisplayForm -> Set QName
namesIn (Display Int
_ [Elim' Term]
ps DisplayTerm
v) = ([Elim' Term], DisplayTerm) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn ([Elim' Term]
ps, DisplayTerm
v)

instance NamesIn DisplayTerm where
  namesIn :: DisplayTerm -> Set QName
namesIn DisplayTerm
v = case DisplayTerm
v of
    DWithApp DisplayTerm
v [DisplayTerm]
us [Elim' Term]
es -> (DisplayTerm, [DisplayTerm], [Elim' Term]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (DisplayTerm
v, [DisplayTerm]
us, [Elim' Term]
es)
    DCon ConHead
c ConInfo
_ [Arg DisplayTerm]
vs      -> (ConHead, [Arg DisplayTerm]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (ConHead
c, [Arg DisplayTerm]
vs)
    DDef QName
f [Elim' DisplayTerm]
es        -> (QName, [Elim' DisplayTerm]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (QName
f, [Elim' DisplayTerm]
es)
    DDot Term
v           -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
    DTerm Term
v          -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v

-- Pattern synonym stuff --

newtype PSyn = PSyn A.PatternSynDefn
instance NamesIn PSyn where
  namesIn :: PSyn -> Set QName
namesIn (PSyn ([Arg Name]
_args, Pattern' Void
p)) = Pattern' Void -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Pattern' Void
p

instance NamesIn (A.Pattern' a) where
  namesIn :: Pattern' a -> Set QName
namesIn Pattern' a
p = case Pattern' a
p of
    A.VarP{}               -> Set QName
forall a. Set a
Set.empty
    A.ConP ConPatInfo
_ AmbiguousQName
c NAPs a
args        -> (AmbiguousQName, NAPs a) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (AmbiguousQName
c, NAPs a
args)
    A.ProjP PatInfo
_ ProjOrigin
_ AmbiguousQName
d          -> AmbiguousQName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn AmbiguousQName
d
    A.DefP PatInfo
_ AmbiguousQName
f NAPs a
args        -> (AmbiguousQName, NAPs a) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (AmbiguousQName
f, NAPs a
args)
    A.WildP{}              -> Set QName
forall a. Set a
Set.empty
    A.AsP PatInfo
_ BindName
_ Pattern' a
p            -> Pattern' a -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Pattern' a
p
    A.AbsurdP{}            -> Set QName
forall a. Set a
Set.empty
    A.LitP Literal
l               -> Literal -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Literal
l
    A.PatternSynP PatInfo
_ AmbiguousQName
c NAPs a
args -> (AmbiguousQName, NAPs a) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (AmbiguousQName
c, NAPs a
args)
    A.RecP PatInfo
_ [FieldAssignment' (Pattern' a)]
fs            -> [FieldAssignment' (Pattern' a)] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [FieldAssignment' (Pattern' a)]
fs
    A.DotP{}               -> Set QName
forall a. HasCallStack => a
__IMPOSSIBLE__    -- Dot patterns are not allowed in pattern synonyms
    A.EqualP{}             -> Set QName
forall a. HasCallStack => a
__IMPOSSIBLE__    -- Andrea: should we allow these in pattern synonyms?
    A.WithP PatInfo
_ Pattern' a
p            -> Pattern' a -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Pattern' a
p

instance NamesIn AmbiguousQName where
  namesIn :: AmbiguousQName -> Set QName
namesIn (AmbQ NonEmpty QName
cs) = NonEmpty QName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn NonEmpty QName
cs