-- | Extract all names and meta-variables from things.

module Agda.Syntax.Internal.Names where

import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HMap
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.Syntax.Treeless

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

import Agda.Utils.List1 (List1)
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Singleton
import Agda.Utils.Impossible

-- | Some or all of the 'QName's that can be found in the given thing.

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

-- | Some or all of the 'QName's that can be found in the given thing.

namesIn' :: (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' :: forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> m
f = (Either QName MetaId -> m) -> a -> m
forall m. Monoid m => (Either QName MetaId -> m) -> a -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' ((QName -> m) -> (MetaId -> m) -> Either QName MetaId -> m
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either QName -> m
f MetaId -> m
forall a. Monoid a => a
mempty)

-- | Some or all of the meta-variables that can be found in the given
-- thing.

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

-- | Some or all of the meta-variables that can be found in the given
-- thing.

-- TODO: Does this function make
-- Agda.Syntax.Internal.MetaVars.allMetas superfluous? Maybe not,
-- allMetas ignores the first argument of PiSort.

metasIn' :: (NamesIn a, Monoid m) => (MetaId -> m) -> a -> m
metasIn' :: forall a m. (NamesIn a, Monoid m) => (MetaId -> m) -> a -> m
metasIn' MetaId -> m
f = (Either QName MetaId -> m) -> a -> m
forall m. Monoid m => (Either QName MetaId -> m) -> a -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' ((QName -> m) -> (MetaId -> m) -> Either QName MetaId -> m
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either QName -> m
forall a. Monoid a => a
mempty MetaId -> m
f)

-- | Some or all of the names and meta-variables that can be found in
-- the given thing.

namesAndMetasIn ::
  (NamesIn a, Collection QName m1, Collection MetaId m2) =>
  a -> (m1, m2)
namesAndMetasIn :: forall a m1 m2.
(NamesIn a, Collection QName m1, Collection MetaId m2) =>
a -> (m1, m2)
namesAndMetasIn =
  (Either QName MetaId -> (m1, m2)) -> a -> (m1, m2)
forall m. Monoid m => (Either QName MetaId -> m) -> a -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn'
    ((QName -> (m1, m2))
-> (MetaId -> (m1, m2)) -> Either QName MetaId -> (m1, m2)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\QName
x -> (QName -> m1
forall el coll. Singleton el coll => el -> coll
singleton QName
x, m2
forall a. Monoid a => a
mempty))
            (\MetaId
m -> (m1
forall a. Monoid a => a
mempty, MetaId -> m2
forall el coll. Singleton el coll => el -> coll
singleton MetaId
m)))

class NamesIn a where
  -- | Some or all of the names and meta-variables that can be found
  -- in the given thing.
  namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> a -> m

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

-- Generic collections
instance NamesIn a => NamesIn (Maybe a)
instance NamesIn a => NamesIn (Strict.Maybe a)
instance NamesIn a => NamesIn [a]
instance NamesIn a => NamesIn (List1 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 (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)

instance (NamesIn a, NamesIn b) => NamesIn (Dom' a b) where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Dom' a b -> m
namesAndMetasIn' Either QName MetaId -> m
sg (Dom ArgInfo
_ Maybe NamedName
_ Bool
_ Maybe a
t b
e) =
    m -> m -> m
forall a. Monoid a => a -> a -> a
mappend ((Either QName MetaId -> m) -> Maybe a -> m
forall m. Monoid m => (Either QName MetaId -> m) -> Maybe a -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Maybe a
t) ((Either QName MetaId -> m) -> b -> m
forall m. Monoid m => (Either QName MetaId -> m) -> b -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg b
e)


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

-- Tuples

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

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

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

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

instance
  (NamesIn a, NamesIn b, NamesIn c, NamesIn d, NamesIn e, NamesIn f) =>
  NamesIn (a, b, c, d, e, f) where
  namesAndMetasIn' :: forall m.
Monoid m =>
(Either QName MetaId -> m) -> (a, b, c, d, e, f) -> m
namesAndMetasIn' Either QName MetaId -> m
sg (a
x, b
y, c
z, d
u, e
v, f
w) =
    (Either QName MetaId -> m) -> ((a, (b, c)), (d, (e, f))) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> ((a, (b, c)), (d, (e, f))) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg ((a
x, (b
y, c
z)), (d
u, (e
v, f
w)))

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

-- Base cases

instance NamesIn QName where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> QName -> m
namesAndMetasIn' Either QName MetaId -> m
sg QName
x = Either QName MetaId -> m
sg (QName -> Either QName MetaId
forall a b. a -> Either a b
Left QName
x)  -- interesting case!

instance NamesIn MetaId where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> MetaId -> m
namesAndMetasIn' Either QName MetaId -> m
sg MetaId
x = Either QName MetaId -> m
sg (MetaId -> Either QName MetaId
forall a b. b -> Either a b
Right MetaId
x)

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

instance NamesIn Bool where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Bool -> m
namesAndMetasIn' Either QName MetaId -> m
_ Bool
_ = m
forall a. Monoid a => a
mempty

-- Andreas, 2017-07-27
-- In the following clauses, the choice of fields is not obvious
-- to the reader.  Please comment on the choices.

instance NamesIn Definition where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Definition -> m
namesAndMetasIn' Either QName MetaId -> m
sg
    (Defn ArgInfo
_ QName
_ Type
t [Polarity]
_ [Occurrence]
_ NumGeneralizableArgs
_ [Maybe Name]
_ [LocalDisplayForm]
disp MutualId
_ CompiledRepresentation
_ Maybe QName
_ Bool
_ Set QName
_ Bool
_ Bool
_ Bool
_ Blocked_
_ Language
_ Defn
def) =
    (Either QName MetaId -> m) -> (Type, Defn, [LocalDisplayForm]) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> (Type, Defn, [LocalDisplayForm]) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (Type
t, Defn
def, [LocalDisplayForm]
disp)

instance NamesIn Defn where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Defn -> m
namesAndMetasIn' Either QName MetaId -> m
sg = \case
    Axiom Bool
_            -> m
forall a. Monoid a => a
mempty
    DataOrRecSig Int
_     -> m
forall a. Monoid a => a
mempty
    Defn
GeneralizableVar   -> m
forall a. Monoid a => a
mempty
    PrimitiveSort String
_ Sort
s  -> (Either QName MetaId -> m) -> Sort -> m
forall m. Monoid m => (Either QName MetaId -> m) -> Sort -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Sort
s
    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 [Clause]
cl Maybe CompiledClauses
cc Maybe SplitTree
_ Maybe Compiled
_ [Clause]
_ FunctionInverse
_ Maybe [QName]
_ IsAbstract
_ Delayed
_ Either ProjectionLikenessMissing Projection
_ Set FunctionFlag
_ Maybe Bool
_ Maybe ExtLamInfo
el Maybe QName
_ Maybe QName
_
      -> (Either QName MetaId -> m)
-> ([Clause], Maybe CompiledClauses, Maybe ExtLamInfo) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m)
-> ([Clause], Maybe CompiledClauses, Maybe ExtLamInfo) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg ([Clause]
cl, Maybe CompiledClauses
cc, Maybe ExtLamInfo
el)
    Datatype Int
_ Int
_ Maybe Clause
cl [QName]
cs Sort
s Maybe [QName]
_ IsAbstract
_ [QName]
_ Maybe QName
trX Maybe QName
trD
      -> (Either QName MetaId -> m)
-> (Maybe Clause, [QName], Sort, Maybe QName, Maybe QName) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m)
-> (Maybe Clause, [QName], Sort, Maybe QName, Maybe QName) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (Maybe Clause
cl, [QName]
cs, Sort
s, Maybe QName
trX, Maybe QName
trD)
    Record Int
_ Maybe Clause
cl ConHead
c Bool
_ [Dom QName]
fs Telescope
recTel Maybe [QName]
_ EtaEquality
_ PatternOrCopattern
_ Maybe Induction
_ Maybe Bool
_ IsAbstract
_ CompKit
comp
      -> (Either QName MetaId -> m)
-> (Maybe Clause, ConHead, [Dom QName], Telescope, CompKit) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m)
-> (Maybe Clause, ConHead, [Dom QName], Telescope, CompKit) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (Maybe Clause
cl, ConHead
c, [Dom QName]
fs, Telescope
recTel, CompKit
comp)
    Constructor Int
_ Int
_ ConHead
c QName
d IsAbstract
_ Induction
_ CompKit
kit Maybe [QName]
fs [IsForced]
_ Maybe [Bool]
_
      -> (Either QName MetaId -> m)
-> (ConHead, QName, CompKit, Maybe [QName]) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m)
-> (ConHead, QName, CompKit, Maybe [QName]) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (ConHead
c, QName
d, CompKit
kit, Maybe [QName]
fs)
    Primitive IsAbstract
_ String
_ [Clause]
cl FunctionInverse
_ Maybe CompiledClauses
cc
      -> (Either QName MetaId -> m)
-> ([Clause], Maybe CompiledClauses) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m)
-> ([Clause], Maybe CompiledClauses) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg ([Clause]
cl, Maybe CompiledClauses
cc)

instance NamesIn Clause where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Clause -> m
namesAndMetasIn' Either QName MetaId -> m
sg (Clause Range
_ Range
_ Telescope
tel NAPs
ps Maybe Term
b Maybe (Arg Type)
t Bool
_ Maybe Bool
_ Maybe Bool
_ Maybe Bool
_ ExpandedEllipsis
_ Maybe ModuleName
_) =
    (Either QName MetaId -> m)
-> (Telescope, NAPs, Maybe Term, Maybe (Arg Type)) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m)
-> (Telescope, NAPs, Maybe Term, Maybe (Arg Type)) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (Telescope
tel, NAPs
ps, Maybe Term
b, Maybe (Arg Type)
t)

instance NamesIn CompiledClauses where
  namesAndMetasIn' :: forall m.
Monoid m =>
(Either QName MetaId -> m) -> CompiledClauses -> m
namesAndMetasIn' Either QName MetaId -> m
sg (Case Arg Int
_ Case CompiledClauses
c) = (Either QName MetaId -> m) -> Case CompiledClauses -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> Case CompiledClauses -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Case CompiledClauses
c
  namesAndMetasIn' Either QName MetaId -> m
sg (Done [Arg String]
_ Term
v) = (Either QName MetaId -> m) -> Term -> m
forall m. Monoid m => (Either QName MetaId -> m) -> Term -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Term
v
  namesAndMetasIn' Either QName MetaId -> m
sg (Fail [Arg String]
_)   = m
forall a. Monoid a => a
mempty

-- Andreas, 2017-07-27
-- Why ignoring the litBranches?
instance NamesIn a => NamesIn (Case a) where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Case a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (Branches Bool
_ Map QName (WithArity a)
bs Maybe (ConHead, WithArity a)
_ Map Literal a
_ Maybe a
c Maybe Bool
_ Bool
_) =
    (Either QName MetaId -> m)
-> (Map QName (WithArity a), Maybe a) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m)
-> (Map QName (WithArity a), Maybe a) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (Map QName (WithArity a)
bs, Maybe a
c)

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

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

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

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

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

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

-- For QName and Meta literals!
instance NamesIn Literal where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Literal -> m
namesAndMetasIn' Either QName MetaId -> m
sg = \case
    LitNat Integer
_    -> m
forall a. Monoid a => a
mempty
    LitWord64 Word64
_ -> m
forall a. Monoid a => a
mempty
    LitString Text
_ -> m
forall a. Monoid a => a
mempty
    LitChar Char
_   -> m
forall a. Monoid a => a
mempty
    LitFloat Double
_  -> m
forall a. Monoid a => a
mempty
    LitQName QName
x  -> (Either QName MetaId -> m) -> QName -> m
forall m. Monoid m => (Either QName MetaId -> m) -> QName -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg QName
x
    LitMeta TopLevelModuleName
_ MetaId
m -> (Either QName MetaId -> m) -> MetaId -> m
forall m. Monoid m => (Either QName MetaId -> m) -> MetaId -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg MetaId
m

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

instance NamesIn a => NamesIn (Substitution' a) where
  namesAndMetasIn' :: forall m.
Monoid m =>
(Either QName MetaId -> m) -> Substitution' a -> m
namesAndMetasIn' Either QName MetaId -> m
sg = \case
    Substitution' a
IdS              -> m
forall a. Monoid a => a
mempty
    EmptyS Impossible
_         -> m
forall a. Monoid a => a
mempty
    a
t :# Substitution' a
s           -> (Either QName MetaId -> m) -> (a, Substitution' a) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> (a, Substitution' a) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (a
t, Substitution' a
s)
    Strengthen Impossible
_ Int
_ Substitution' a
s -> (Either QName MetaId -> m) -> Substitution' a -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> Substitution' a -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Substitution' a
s
    Wk Int
_ Substitution' a
s           -> (Either QName MetaId -> m) -> Substitution' a -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> Substitution' a -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Substitution' a
s
    Lift Int
_ Substitution' a
s         -> (Either QName MetaId -> m) -> Substitution' a -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> Substitution' a -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Substitution' a
s

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

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

instance NamesIn a => NamesIn (Builtin a) where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Builtin a -> m
namesAndMetasIn' Either QName MetaId -> m
sg = \case
    Builtin Term
t -> (Either QName MetaId -> m) -> Term -> m
forall m. Monoid m => (Either QName MetaId -> m) -> Term -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Term
t
    Prim a
x    -> (Either QName MetaId -> m) -> a -> m
forall m. Monoid m => (Either QName MetaId -> m) -> a -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg a
x
    BuiltinRewriteRelations Set QName
xs -> (Either QName MetaId -> m) -> Set QName -> m
forall m. Monoid m => (Either QName MetaId -> m) -> Set QName -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Set QName
xs

-- | Note that the 'primFunImplementation' is skipped.
instance NamesIn PrimFun where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> PrimFun -> m
namesAndMetasIn' Either QName MetaId -> m
sg = \case
    PrimFun QName
x Int
_ [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
_ -> (Either QName MetaId -> m) -> QName -> m
forall m. Monoid m => (Either QName MetaId -> m) -> QName -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg QName
x

instance NamesIn Section where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Section -> m
namesAndMetasIn' Either QName MetaId -> m
sg = \case
    Section Telescope
tel -> (Either QName MetaId -> m) -> Telescope -> m
forall m. Monoid m => (Either QName MetaId -> m) -> Telescope -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Telescope
tel

instance NamesIn NLPat where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> NLPat -> m
namesAndMetasIn' Either QName MetaId -> m
sg = \case
    PVar Int
_ [Arg Int]
_      -> m
forall a. Monoid a => a
mempty
    PDef QName
a PElims
b      -> (Either QName MetaId -> m) -> (QName, PElims) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> (QName, PElims) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (QName
a, PElims
b)
    PLam ArgInfo
_ Abs NLPat
a      -> (Either QName MetaId -> m) -> Abs NLPat -> m
forall m. Monoid m => (Either QName MetaId -> m) -> Abs NLPat -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Abs NLPat
a
    PPi Dom NLPType
a Abs NLPType
b       -> (Either QName MetaId -> m) -> (Dom NLPType, Abs NLPType) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> (Dom NLPType, Abs NLPType) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (Dom NLPType
a, Abs NLPType
b)
    PSort NLPSort
a       -> (Either QName MetaId -> m) -> NLPSort -> m
forall m. Monoid m => (Either QName MetaId -> m) -> NLPSort -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg NLPSort
a
    PBoundVar Int
_ PElims
a -> (Either QName MetaId -> m) -> PElims -> m
forall m. Monoid m => (Either QName MetaId -> m) -> PElims -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg PElims
a
    PTerm Term
a       -> (Either QName MetaId -> m) -> Term -> m
forall m. Monoid m => (Either QName MetaId -> m) -> Term -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Term
a

instance NamesIn NLPType where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> NLPType -> m
namesAndMetasIn' Either QName MetaId -> m
sg = \case
    NLPType NLPSort
a NLPat
b -> (Either QName MetaId -> m) -> (NLPSort, NLPat) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> (NLPSort, NLPat) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (NLPSort
a, NLPat
b)

instance NamesIn NLPSort where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> NLPSort -> m
namesAndMetasIn' Either QName MetaId -> m
sg = \case
    PType NLPat
a       -> (Either QName MetaId -> m) -> NLPat -> m
forall m. Monoid m => (Either QName MetaId -> m) -> NLPat -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg NLPat
a
    PProp NLPat
a       -> (Either QName MetaId -> m) -> NLPat -> m
forall m. Monoid m => (Either QName MetaId -> m) -> NLPat -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg NLPat
a
    PSSet NLPat
a       -> (Either QName MetaId -> m) -> NLPat -> m
forall m. Monoid m => (Either QName MetaId -> m) -> NLPat -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg NLPat
a
    PInf IsFibrant
_ Integer
_      -> m
forall a. Monoid a => a
mempty
    NLPSort
PSizeUniv     -> m
forall a. Monoid a => a
mempty
    NLPSort
PLockUniv     -> m
forall a. Monoid a => a
mempty
    NLPSort
PIntervalUniv -> m
forall a. Monoid a => a
mempty

instance NamesIn RewriteRule where
  namesAndMetasIn' :: forall m.
Monoid m =>
(Either QName MetaId -> m) -> RewriteRule -> m
namesAndMetasIn' Either QName MetaId -> m
sg = \case
    RewriteRule QName
a Telescope
b QName
c PElims
d Term
e Type
f Bool
_ ->
      (Either QName MetaId -> m)
-> (QName, Telescope, QName, PElims, Term, Type) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m)
-> (QName, Telescope, QName, PElims, Term, Type) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (QName
a, Telescope
b, QName
c, PElims
d, Term
e, Type
f)

instance (NamesIn a, NamesIn b) => NamesIn (HashMap a b) where
  namesAndMetasIn' :: forall m.
Monoid m =>
(Either QName MetaId -> m) -> HashMap a b -> m
namesAndMetasIn' Either QName MetaId -> m
sg = (Either QName MetaId -> m) -> [(a, b)] -> m
forall m. Monoid m => (Either QName MetaId -> m) -> [(a, b)] -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg ([(a, b)] -> m) -> (HashMap a b -> [(a, b)]) -> HashMap a b -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap a b -> [(a, b)]
forall k v. HashMap k v -> [(k, v)]
HMap.toList

instance NamesIn System where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> System -> m
namesAndMetasIn' Either QName MetaId -> m
sg (System Telescope
tel [(Face, Term)]
cs) = (Either QName MetaId -> m) -> (Telescope, [(Face, Term)]) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> (Telescope, [(Face, Term)]) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (Telescope
tel, [(Face, Term)]
cs)

instance NamesIn ExtLamInfo where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> ExtLamInfo -> m
namesAndMetasIn' Either QName MetaId -> m
sg (ExtLamInfo ModuleName
_ Bool
_ Maybe System
s) = (Either QName MetaId -> m) -> Maybe System -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> Maybe System -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Maybe System
s

instance NamesIn a => NamesIn (FunctionInverse' a) where
  namesAndMetasIn' :: forall m.
Monoid m =>
(Either QName MetaId -> m) -> FunctionInverse' a -> m
namesAndMetasIn' Either QName MetaId -> m
sg = \case
    FunctionInverse' a
NotInjective -> m
forall a. Monoid a => a
mempty
    Inverse InversionMap a
m  -> (Either QName MetaId -> m) -> InversionMap a -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> InversionMap a -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg InversionMap a
m

instance NamesIn TTerm where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> TTerm -> m
namesAndMetasIn' Either QName MetaId -> m
sg = \case
    TVar Int
_         -> m
forall a. Monoid a => a
mempty
    TPrim TPrim
_        -> m
forall a. Monoid a => a
mempty
    TDef QName
x         -> (Either QName MetaId -> m) -> QName -> m
forall m. Monoid m => (Either QName MetaId -> m) -> QName -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg QName
x
    TApp TTerm
t Args
xs      -> (Either QName MetaId -> m) -> (TTerm, Args) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> (TTerm, Args) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (TTerm
t, Args
xs)
    TLam TTerm
t         -> (Either QName MetaId -> m) -> TTerm -> m
forall m. Monoid m => (Either QName MetaId -> m) -> TTerm -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg TTerm
t
    TLit Literal
l         -> (Either QName MetaId -> m) -> Literal -> m
forall m. Monoid m => (Either QName MetaId -> m) -> Literal -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Literal
l
    TCon QName
x         -> (Either QName MetaId -> m) -> QName -> m
forall m. Monoid m => (Either QName MetaId -> m) -> QName -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg QName
x
    TLet TTerm
t1 TTerm
t2     -> (Either QName MetaId -> m) -> (TTerm, TTerm) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> (TTerm, TTerm) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (TTerm
t1, TTerm
t2)
    TCase Int
_ CaseInfo
c TTerm
t [TAlt]
ts -> (Either QName MetaId -> m) -> (CaseInfo, TTerm, [TAlt]) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> (CaseInfo, TTerm, [TAlt]) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (CaseInfo
c, TTerm
t, [TAlt]
ts)
    TTerm
TUnit          -> m
forall a. Monoid a => a
mempty
    TTerm
TSort          -> m
forall a. Monoid a => a
mempty
    TTerm
TErased        -> m
forall a. Monoid a => a
mempty
    TCoerce TTerm
t      -> (Either QName MetaId -> m) -> TTerm -> m
forall m. Monoid m => (Either QName MetaId -> m) -> TTerm -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg TTerm
t
    TError TError
_       -> m
forall a. Monoid a => a
mempty

instance NamesIn TAlt where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> TAlt -> m
namesAndMetasIn' Either QName MetaId -> m
sg = \case
    TACon QName
x Int
_ TTerm
t   -> (Either QName MetaId -> m) -> (QName, TTerm) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> (QName, TTerm) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (QName
x, TTerm
t)
    TAGuard TTerm
t1 TTerm
t2 -> (Either QName MetaId -> m) -> (TTerm, TTerm) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> (TTerm, TTerm) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (TTerm
t1, TTerm
t2)
    TALit Literal
l TTerm
t     -> (Either QName MetaId -> m) -> (Literal, TTerm) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> (Literal, TTerm) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (Literal
l, TTerm
t)

instance NamesIn CaseType where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> CaseType -> m
namesAndMetasIn' Either QName MetaId -> m
sg = \case
    CTData Quantity
_ QName
x -> (Either QName MetaId -> m) -> QName -> m
forall m. Monoid m => (Either QName MetaId -> m) -> QName -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg QName
x
    CaseType
CTNat      -> m
forall a. Monoid a => a
mempty
    CaseType
CTInt      -> m
forall a. Monoid a => a
mempty
    CaseType
CTChar     -> m
forall a. Monoid a => a
mempty
    CaseType
CTString   -> m
forall a. Monoid a => a
mempty
    CaseType
CTFloat    -> m
forall a. Monoid a => a
mempty
    CaseType
CTQName    -> m
forall a. Monoid a => a
mempty

instance NamesIn CaseInfo where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> CaseInfo -> m
namesAndMetasIn' Either QName MetaId -> m
sg (CaseInfo Bool
_ CaseType
t) = (Either QName MetaId -> m) -> CaseType -> m
forall m. Monoid m => (Either QName MetaId -> m) -> CaseType -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg CaseType
t

instance NamesIn Compiled where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Compiled -> m
namesAndMetasIn' Either QName MetaId -> m
sg (Compiled TTerm
t Maybe [ArgUsage]
_) = (Either QName MetaId -> m) -> TTerm -> m
forall m. Monoid m => (Either QName MetaId -> m) -> TTerm -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg TTerm
t

-- Pattern synonym stuff --

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

instance NamesIn (A.Pattern' a) where
  namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Pattern' a -> m
namesAndMetasIn' Either QName MetaId -> m
sg = \case
    A.VarP BindName
_               -> m
forall a. Monoid a => a
mempty
    A.ConP ConPatInfo
_ AmbiguousQName
c NAPs a
args        -> (Either QName MetaId -> m) -> (AmbiguousQName, NAPs a) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> (AmbiguousQName, NAPs a) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (AmbiguousQName
c, NAPs a
args)
    A.ProjP PatInfo
_ ProjOrigin
_ AmbiguousQName
d          -> (Either QName MetaId -> m) -> AmbiguousQName -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> AmbiguousQName -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg AmbiguousQName
d
    A.DefP PatInfo
_ AmbiguousQName
f NAPs a
args        -> (Either QName MetaId -> m) -> (AmbiguousQName, NAPs a) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> (AmbiguousQName, NAPs a) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (AmbiguousQName
f, NAPs a
args)
    A.WildP PatInfo
_              -> m
forall a. Monoid a => a
mempty
    A.AsP PatInfo
_ BindName
_ Pattern' a
p            -> (Either QName MetaId -> m) -> Pattern' a -> m
forall m. Monoid m => (Either QName MetaId -> m) -> Pattern' a -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Pattern' a
p
    A.AbsurdP PatInfo
_            -> m
forall a. Monoid a => a
mempty
    A.LitP PatInfo
_ Literal
l             -> (Either QName MetaId -> m) -> Literal -> m
forall m. Monoid m => (Either QName MetaId -> m) -> Literal -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg Literal
l
    A.PatternSynP PatInfo
_ AmbiguousQName
c NAPs a
args -> (Either QName MetaId -> m) -> (AmbiguousQName, NAPs a) -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> (AmbiguousQName, NAPs a) -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg (AmbiguousQName
c, NAPs a
args)
    A.RecP PatInfo
_ [FieldAssignment' (Pattern' a)]
fs            -> (Either QName MetaId -> m) -> [FieldAssignment' (Pattern' a)] -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> [FieldAssignment' (Pattern' a)] -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> 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            -> (Either QName MetaId -> m) -> Pattern' a -> m
forall m. Monoid m => (Either QName MetaId -> m) -> Pattern' a -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> 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
  namesAndMetasIn' :: forall m.
Monoid m =>
(Either QName MetaId -> m) -> AmbiguousQName -> m
namesAndMetasIn' Either QName MetaId -> m
sg (AmbQ List1 QName
cs) = (Either QName MetaId -> m) -> List1 QName -> m
forall m.
Monoid m =>
(Either QName MetaId -> m) -> List1 QName -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' Either QName MetaId -> m
sg List1 QName
cs