-- | Extract all names from things.

module Agda.Syntax.Internal.Names where

import Data.List.NonEmpty (NonEmpty(..))
import Data.Map (Map)
import Data.Set (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.Singleton
import Agda.Utils.Impossible

namesIn :: (NamesIn a, Collection QName m) => a -> m
namesIn :: forall a m. (NamesIn a, Collection QName m) => a -> m
namesIn = (QName -> m) -> a -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
forall el coll. Singleton el coll => el -> coll
singleton

class NamesIn a where
  namesIn' :: Monoid m => (QName -> m) -> a -> m

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

-- Generic collections
instance NamesIn a => NamesIn (Maybe a)
instance NamesIn a => NamesIn [a]
instance NamesIn a => NamesIn (NonEmpty a)
instance NamesIn a => NamesIn (Set a)
instance NamesIn a => NamesIn (Map k a)

-- Decorations
instance NamesIn a => NamesIn (Arg a)
instance NamesIn a => NamesIn (Dom a)
instance NamesIn a => NamesIn (Named n a)
instance NamesIn a => NamesIn (Abs a)
instance NamesIn a => NamesIn (WithArity a)
instance NamesIn a => NamesIn (Open a)
instance NamesIn a => NamesIn (C.FieldAssignment' a)

-- Specific collections
instance NamesIn a => NamesIn (Tele a)

-- Tuples

instance (NamesIn a, NamesIn b) => NamesIn (a, b) where
  namesIn' :: forall m. Monoid m => (QName -> m) -> (a, b) -> m
namesIn' QName -> m
sg (a
x, b
y) = m -> m -> m
forall a. Monoid a => a -> a -> a
mappend ((QName -> m) -> a -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg a
x) ((QName -> m) -> b -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg b
y)

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

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

instance NamesIn CompKit where
  namesIn' :: forall m. Monoid m => (QName -> m) -> CompKit -> m
namesIn' QName -> m
sg (CompKit Maybe QName
a Maybe QName
b) = (QName -> m) -> (Maybe QName, Maybe QName) -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg (Maybe QName
a,Maybe QName
b)

-- Base case

instance NamesIn QName where
  namesIn' :: forall m. Monoid m => (QName -> m) -> QName -> m
namesIn' QName -> m
sg QName
x = QName -> m
sg QName
x  -- interesting case!

instance NamesIn ConHead where
  namesIn' :: forall m. Monoid m => (QName -> m) -> ConHead -> m
namesIn' QName -> m
sg ConHead
h = (QName -> m) -> QName -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg (ConHead -> QName
conName ConHead
h)

-- 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' :: forall m. Monoid m => (QName -> m) -> Definition -> m
namesIn' QName -> m
sg Definition
def = (QName -> m) -> (Type, Defn, [LocalDisplayForm]) -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg (Definition -> Type
defType Definition
def, Definition -> Defn
theDef Definition
def, Definition -> [LocalDisplayForm]
defDisplay Definition
def)

instance NamesIn Defn where
  namesIn' :: forall m. Monoid m => (QName -> m) -> Defn -> m
namesIn' QName -> m
sg = \case
    Axiom Bool
_            -> m
forall a. Monoid a => a
mempty
    DataOrRecSig{}     -> m
forall a. Monoid a => a
mempty
    GeneralizableVar{} -> m
forall a. Monoid a => a
mempty
    PrimitiveSort{}    -> m
forall a. Monoid a => a
mempty
    AbstractDefn{}     -> m
forall a. HasCallStack => a
__IMPOSSIBLE__
    -- 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 }
      -> (QName -> m) -> ([Clause], Maybe CompiledClauses) -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg ([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 }
      -> (QName -> m) -> (Maybe Clause, [QName], Sort) -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg (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 }
      -> (QName -> m) -> (Maybe Clause, ConHead, [Dom QName], CompKit) -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg (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 }
      -> (QName -> m) -> (ConHead, QName, CompKit, Maybe [QName]) -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg (ConHead
c, QName
d, CompKit
kit, Maybe [QName]
fs)
    Primitive   { primClauses :: Defn -> [Clause]
primClauses = [Clause]
cl, primCompiled :: Defn -> Maybe CompiledClauses
primCompiled = Maybe CompiledClauses
cc }
      -> (QName -> m) -> ([Clause], Maybe CompiledClauses) -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg ([Clause]
cl, Maybe CompiledClauses
cc)

instance NamesIn Clause where
  namesIn' :: forall m. Monoid m => (QName -> m) -> Clause -> m
namesIn' QName -> m
sg 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 } =
    (QName -> m)
-> (Telescope, NAPs, Maybe Term, Maybe (Arg Type)) -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg (Telescope
tel, NAPs
ps, Maybe Term
b, Maybe (Arg Type)
t)

instance NamesIn CompiledClauses where
  namesIn' :: forall m. Monoid m => (QName -> m) -> CompiledClauses -> m
namesIn' QName -> m
sg (Case Arg Int
_ Case CompiledClauses
c) = (QName -> m) -> Case CompiledClauses -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg Case CompiledClauses
c
  namesIn' QName -> m
sg (Done [Arg ArgName]
_ Term
v) = (QName -> m) -> Term -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg Term
v
  namesIn' QName -> m
sg Fail{}     = m
forall a. Monoid a => a
mempty

-- Andreas, 2017-07-27
-- Why ignoring the litBranches?
instance NamesIn a => NamesIn (Case a) where
  namesIn' :: forall m. Monoid m => (QName -> m) -> Case a -> m
namesIn' QName -> m
sg 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 -> m) -> (Map QName (WithArity a), Maybe a) -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg (Map QName (WithArity a)
bs, Maybe a
c)

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

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

instance NamesIn Sort where
  namesIn' :: forall m. Monoid m => (QName -> m) -> Sort -> m
namesIn' QName -> m
sg = \case
    Type Level' Term
l      -> (QName -> m) -> Level' Term -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg Level' Term
l
    Prop Level' Term
l      -> (QName -> m) -> Level' Term -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg Level' Term
l
    Inf IsFibrant
_ Integer
_     -> m
forall a. Monoid a => a
mempty
    SSet Level' Term
l      -> (QName -> m) -> Level' Term -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg Level' Term
l
    Sort
SizeUniv    -> m
forall a. Monoid a => a
mempty
    Sort
LockUniv    -> m
forall a. Monoid a => a
mempty
    PiSort Dom' Term Term
a Sort
b Abs Sort
c  -> (QName -> m) -> (Dom' Term Term, Sort, Abs Sort) -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg (Dom' Term Term
a, Sort
b, Abs Sort
c)
    FunSort Sort
a Sort
b -> (QName -> m) -> (Sort, Sort) -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg (Sort
a, Sort
b)
    UnivSort Sort
a  -> (QName -> m) -> Sort -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg Sort
a
    MetaS MetaId
_ [Elim' Term]
es  -> (QName -> m) -> [Elim' Term] -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg [Elim' Term]
es
    DefS QName
d [Elim' Term]
es   -> (QName -> m) -> (QName, [Elim' Term]) -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg (QName
d, [Elim' Term]
es)
    DummyS{}    -> m
forall a. Monoid a => a
mempty

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

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

instance NamesIn PlusLevel where
  namesIn' :: forall m. Monoid m => (QName -> m) -> PlusLevel' Term -> m
namesIn' QName -> m
sg (Plus Integer
_ Term
l) = (QName -> m) -> Term -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg Term
l

-- For QName literals!
instance NamesIn Literal where
  namesIn' :: forall m. Monoid m => (QName -> m) -> Literal -> m
namesIn' QName -> m
sg = \case
    LitNat{}      -> m
forall a. Monoid a => a
mempty
    LitWord64{}   -> m
forall a. Monoid a => a
mempty
    LitString{}   -> m
forall a. Monoid a => a
mempty
    LitChar{}     -> m
forall a. Monoid a => a
mempty
    LitFloat{}    -> m
forall a. Monoid a => a
mempty
    LitQName    QName
x -> (QName -> m) -> QName -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg QName
x
    LitMeta{}     -> m
forall a. Monoid a => a
mempty

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

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

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

-- Pattern synonym stuff --

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

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

instance NamesIn AmbiguousQName where
  namesIn' :: forall m. Monoid m => (QName -> m) -> AmbiguousQName -> m
namesIn' QName -> m
sg (AmbQ List1 QName
cs) = (QName -> m) -> List1 QName -> m
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
sg List1 QName
cs