{-# 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 (x :: a
x, y :: 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 (x :: a
x, y :: b
y, z :: 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 (x :: a
x, y :: b
y, z :: c
z, u :: 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 a :: Maybe QName
a b :: 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 def :: 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 def :: Defn
def = case Defn
def of
    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 _ c :: Case CompiledClauses
c) = Case CompiledClauses -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Case CompiledClauses
c
  namesIn (Done _ v :: Term
v) = Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
  namesIn 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 p :: Pattern' a
p = case Pattern' a
p of
    VarP{}        -> Set QName
forall a. Set a
Set.empty
    LitP _ l :: Literal
l      -> Literal -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Literal
l
    DotP _ v :: Term
v      -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
    ConP c :: ConHead
c _ args :: [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 o :: PatternInfo
o q :: QName
q args :: [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 _ f :: QName
f     -> QName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn QName
f
    IApplyP _ t :: Term
t u :: Term
u _ -> (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 s :: Sort
s t :: 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 s :: Sort
s = case Sort
s of
    Type l :: Level' Term
l   -> Level' Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Level' Term
l
    Prop l :: Level' Term
l   -> Level' Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Level' Term
l
    Inf      -> Set QName
forall a. Set a
Set.empty
    SizeUniv -> Set QName
forall a. Set a
Set.empty
    PiSort a :: Dom' Term Type
a b :: 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 a :: Sort
a b :: Sort
b -> (Sort, Sort) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Sort
a, Sort
b)
    UnivSort a :: Sort
a -> Sort -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Sort
a
    MetaS _ es :: [Elim' Term]
es -> [Elim' Term] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [Elim' Term]
es
    DefS d :: QName
d es :: [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 v :: Term
v = case Term
v of
    Var _ args :: [Elim' Term]
args   -> [Elim' Term] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [Elim' Term]
args
    Lam _ b :: Abs Term
b      -> Abs Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Abs Term
b
    Lit l :: Literal
l        -> Literal -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Literal
l
    Def f :: QName
f args :: [Elim' Term]
args   -> (QName, [Elim' Term]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (QName
f, [Elim' Term]
args)
    Con c :: ConHead
c _ args :: [Elim' Term]
args -> (ConHead, [Elim' Term]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (ConHead
c, [Elim' Term]
args)
    Pi a :: Dom' Term Type
a b :: 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 s :: Sort
s       -> Sort -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Sort
s
    Level l :: Level' Term
l      -> Level' Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Level' Term
l
    MetaV _ args :: [Elim' Term]
args -> [Elim' Term] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [Elim' Term]
args
    DontCare v :: 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 _ ls :: [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 _ l :: 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 l :: LevelAtom' Term
l = case LevelAtom' Term
l of
    MetaLevel _ args :: [Elim' Term]
args -> [Elim' Term] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [Elim' Term]
args
    BlockedLevel _ v :: Term
v -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
    NeutralLevel _ v :: Term
v -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
    UnreducedLevel v :: 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 l :: 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 _  x :: 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 :: Arg a
arg) = Arg a -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Arg a
arg
  namesIn (Proj _ f :: QName
f)  = QName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn QName
f
  namesIn (IApply x :: a
x y :: a
y arg :: 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 x :: 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 h :: 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 _ ps :: [Elim' Term]
ps v :: 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 v :: DisplayTerm
v = case DisplayTerm
v of
    DWithApp v :: DisplayTerm
v us :: [DisplayTerm]
us es :: [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 c :: ConHead
c _ vs :: [Arg DisplayTerm]
vs      -> (ConHead, [Arg DisplayTerm]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (ConHead
c, [Arg DisplayTerm]
vs)
    DDef f :: QName
f es :: [Elim' DisplayTerm]
es        -> (QName, [Elim' DisplayTerm]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (QName
f, [Elim' DisplayTerm]
es)
    DDot v :: Term
v           -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
    DTerm v :: 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 (_args :: [Arg Name]
_args, p :: 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 p :: Pattern' a
p = case Pattern' a
p of
    A.VarP{}               -> Set QName
forall a. Set a
Set.empty
    A.ConP _ c :: AmbiguousQName
c args :: NAPs a
args        -> (AmbiguousQName, NAPs a) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (AmbiguousQName
c, NAPs a
args)
    A.ProjP _ _ d :: AmbiguousQName
d          -> AmbiguousQName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn AmbiguousQName
d
    A.DefP _ f :: AmbiguousQName
f args :: 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 _ _ p :: 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 l :: Literal
l               -> Literal -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Literal
l
    A.PatternSynP _ c :: AmbiguousQName
c args :: NAPs a
args -> (AmbiguousQName, NAPs a) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (AmbiguousQName
c, NAPs a
args)
    A.RecP _ fs :: [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 _ p :: 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 cs :: NonEmpty QName
cs) = NonEmpty QName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn NonEmpty QName
cs