module Agda.Syntax.Abstract.UsedNames
  ( allUsedNames
  ) where

import Data.Foldable (foldMap)
import Data.Semigroup (Semigroup, (<>))
import Data.Set (Set)
import qualified Data.Set as Set

import Agda.Syntax.Common
import Agda.Syntax.Abstract
import Agda.Syntax.Concrete (FieldAssignment'(..))
import Agda.Utils.List1 (List1)

import Agda.Utils.Impossible

-- | All names used in an abstract expression. This is used when rendering clauses to figure out
--   which (implicit) pattern variables must be preserved. For example, the for @f : Nat → Nat@, the
--   clause @f {n} = 0@ can be printed as @f = 0@ (dropping the @n@), but @f {n} = n@ must preserve
--   the @n@.
allUsedNames :: Expr -> Set Name
allUsedNames :: Expr -> Set Name
allUsedNames = BoundAndUsedNames -> Set Name
usedNames (BoundAndUsedNames -> Set Name)
-> (Expr -> BoundAndUsedNames) -> Expr -> Set Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed

data BoundAndUsedNames = BoundAndUsedNames
  { BoundAndUsedNames -> Set Name
boundNames :: Set Name
  , BoundAndUsedNames -> Set Name
usedNames  :: Set Name }

-- | Bound names in first argument scope over second argument.
instance Semigroup BoundAndUsedNames where
  BoundAndUsedNames Set Name
bound1 Set Name
used1 <> :: BoundAndUsedNames -> BoundAndUsedNames -> BoundAndUsedNames
<> BoundAndUsedNames Set Name
bound2 Set Name
used2 =
    Set Name -> Set Name -> BoundAndUsedNames
BoundAndUsedNames (Set Name
bound1 Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Set Name
bound2) (Set Name
used1 Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set Name
used2 Set Name
bound1)

instance Monoid BoundAndUsedNames where
  mempty :: BoundAndUsedNames
mempty  = Set Name -> Set Name -> BoundAndUsedNames
BoundAndUsedNames Set Name
forall a. Monoid a => a
mempty Set Name
forall a. Monoid a => a
mempty
  mappend :: BoundAndUsedNames -> BoundAndUsedNames -> BoundAndUsedNames
mappend = BoundAndUsedNames -> BoundAndUsedNames -> BoundAndUsedNames
forall a. Semigroup a => a -> a -> a
(<>)

singleUse :: Name -> BoundAndUsedNames
singleUse :: Name -> BoundAndUsedNames
singleUse Name
x = Set Name -> Set Name -> BoundAndUsedNames
BoundAndUsedNames Set Name
forall a. Monoid a => a
mempty (Name -> Set Name
forall a. a -> Set a
Set.singleton Name
x)

singleBind :: Name -> BoundAndUsedNames
singleBind :: Name -> BoundAndUsedNames
singleBind Name
x = Set Name -> Set Name -> BoundAndUsedNames
BoundAndUsedNames (Name -> Set Name
forall a. a -> Set a
Set.singleton Name
x) Set Name
forall a. Monoid a => a
mempty

noBindings :: BoundAndUsedNames -> BoundAndUsedNames
noBindings :: BoundAndUsedNames -> BoundAndUsedNames
noBindings BoundAndUsedNames
names = BoundAndUsedNames
names{ boundNames = mempty }

-- | Bound names in first argument do *not* scope over second argument.
parB :: BoundAndUsedNames -> BoundAndUsedNames -> BoundAndUsedNames
parB :: BoundAndUsedNames -> BoundAndUsedNames -> BoundAndUsedNames
parB (BoundAndUsedNames Set Name
bound1 Set Name
used1) (BoundAndUsedNames Set Name
bound2 Set Name
used2) =
  Set Name -> Set Name -> BoundAndUsedNames
BoundAndUsedNames (Set Name
bound1 Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Set Name
bound2) (Set Name
used1 Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Set Name
used2)

parBindings :: (BoundAndUsed a, BoundAndUsed b) => a -> b -> BoundAndUsedNames
parBindings :: forall a b.
(BoundAndUsed a, BoundAndUsed b) =>
a -> b -> BoundAndUsedNames
parBindings a
a b
b = a -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed a
a BoundAndUsedNames -> BoundAndUsedNames -> BoundAndUsedNames
`parB` b -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed b
b

parBoundAndUsed :: (Foldable f, BoundAndUsed a) => f a -> BoundAndUsedNames
parBoundAndUsed :: forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed = (a -> BoundAndUsedNames -> BoundAndUsedNames)
-> BoundAndUsedNames -> f a -> BoundAndUsedNames
forall a b. (a -> b -> b) -> b -> f a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> BoundAndUsedNames -> BoundAndUsedNames
forall a b.
(BoundAndUsed a, BoundAndUsed b) =>
a -> b -> BoundAndUsedNames
parBindings BoundAndUsedNames
forall a. Monoid a => a
mempty

class BoundAndUsed a where
  boundAndUsed :: a -> BoundAndUsedNames

  default boundAndUsed :: (a ~ f b, Foldable f, BoundAndUsed b) => a -> BoundAndUsedNames
  boundAndUsed = (b -> BoundAndUsedNames) -> f b -> BoundAndUsedNames
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 -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed

instance BoundAndUsed BoundAndUsedNames where
  boundAndUsed :: BoundAndUsedNames -> BoundAndUsedNames
boundAndUsed = BoundAndUsedNames -> BoundAndUsedNames
forall a. a -> a
id

instance BoundAndUsed a => BoundAndUsed (Arg a)
instance BoundAndUsed a => BoundAndUsed (Named n a)
instance BoundAndUsed a => BoundAndUsed (List1 a)
instance BoundAndUsed a => BoundAndUsed [a]
instance BoundAndUsed a => BoundAndUsed (Maybe a)

instance (BoundAndUsed a, BoundAndUsed b) => BoundAndUsed (Either a b) where
  boundAndUsed :: Either a b -> BoundAndUsedNames
boundAndUsed = (a -> BoundAndUsedNames)
-> (b -> BoundAndUsedNames) -> Either a b -> BoundAndUsedNames
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed b -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed

instance BoundAndUsed ModuleName where
  boundAndUsed :: ModuleName -> BoundAndUsedNames
boundAndUsed ModuleName
_ = BoundAndUsedNames
forall a. Monoid a => a
mempty

instance (BoundAndUsed a, BoundAndUsed b) => BoundAndUsed (a, b) where
  boundAndUsed :: (a, b) -> BoundAndUsedNames
boundAndUsed (a
a, b
b) = a -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed a
a BoundAndUsedNames -> BoundAndUsedNames -> BoundAndUsedNames
forall a. Semigroup a => a -> a -> a
<> b -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed b
b

instance BoundAndUsed Expr where
  boundAndUsed :: Expr -> BoundAndUsedNames
boundAndUsed = BoundAndUsedNames -> BoundAndUsedNames
noBindings (BoundAndUsedNames -> BoundAndUsedNames)
-> (Expr -> BoundAndUsedNames) -> Expr -> BoundAndUsedNames
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \ case
    Var Name
x                  -> Name -> BoundAndUsedNames
singleUse Name
x
    Def'{}                 -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    Proj{}                 -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    Con{}                  -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    PatternSyn{}           -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    Macro{}                -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    Lit{}                  -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    QuestionMark{}         -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    Underscore{}           -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    Dot ExprInfo
_ Expr
expr             -> Expr -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Expr
expr
    App AppInfo
_ Expr
expr NamedArg Expr
arg         -> (Expr, NamedArg Expr) -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (Expr
expr, NamedArg Expr
arg)
    WithApp ExprInfo
_ Expr
expr [Expr]
exprs   -> (Expr, [Expr]) -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (Expr
expr, [Expr]
exprs)
    Lam ExprInfo
_ LamBinding
bind Expr
expr        -> (LamBinding, Expr) -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (LamBinding
bind, Expr
expr)
    AbsurdLam{}            -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    ExtendedLam ExprInfo
_ DefInfo
_ Erased
_ QName
_ List1 Clause
cs -> List1 Clause -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed List1 Clause
cs
    Pi ExprInfo
_ Telescope1
tel Expr
expr          -> (Telescope1, Expr) -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (Telescope1
tel, Expr
expr)
    Generalized Set QName
_ Expr
expr     -> Expr -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Expr
expr
    Fun ExprInfo
_ Arg Expr
arg Expr
expr         -> (Arg Expr, Expr) -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (Arg Expr
arg, Expr
expr)
    Let ExprInfo
_ List1 LetBinding
binds Expr
expr       -> (List1 LetBinding, Expr) -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (List1 LetBinding
binds, Expr
expr)
    Rec ExprInfo
_ RecordAssigns
as               -> RecordAssigns -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed RecordAssigns
as
    RecUpdate ExprInfo
_ Expr
expr Assigns
as    -> Expr -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Expr
expr BoundAndUsedNames -> BoundAndUsedNames -> BoundAndUsedNames
forall a. Semigroup a => a -> a -> a
<> Assigns -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Assigns
as
    ScopedExpr ScopeInfo
_ Expr
expr      -> Expr -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Expr
expr
    Quote{}                -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    QuoteTerm{}            -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    Unquote{}              -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    DontCare Expr
expr          -> Expr -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Expr
expr

instance BoundAndUsed lhs => BoundAndUsed (Clause' lhs) where
  -- Note: where declarations are ignored. We use this only on expressions coming from
  --       InternalToAbstract where there are no where decls.
  boundAndUsed :: Clause' lhs -> BoundAndUsedNames
boundAndUsed Clause{ clauseLHS :: forall lhs. Clause' lhs -> lhs
clauseLHS = lhs
lhs, clauseRHS :: forall lhs. Clause' lhs -> RHS
clauseRHS = RHS
rhs } = (lhs, RHS) -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (lhs
lhs, RHS
rhs)

instance BoundAndUsed RHS where
  boundAndUsed :: RHS -> BoundAndUsedNames
boundAndUsed = \ case
    RHS Expr
body Maybe Expr
_              -> Expr -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Expr
body
    RHS
AbsurdRHS               -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    WithRHS QName
_ [WithExpr]
es List1 Clause
cs         -> ([WithExpr], List1 Clause) -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed ([WithExpr]
es, List1 Clause
cs)
    RewriteRHS [RewriteEqn]
eqns [ProblemEq]
_ RHS
rhs WhereDeclarations
_ -> ([RewriteEqn], RHS) -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed ([RewriteEqn]
eqns, RHS
rhs)

instance BoundAndUsed LHS where
  boundAndUsed :: LHS -> BoundAndUsedNames
boundAndUsed = LHSCore -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (LHSCore -> BoundAndUsedNames)
-> (LHS -> LHSCore) -> LHS -> BoundAndUsedNames
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHS -> LHSCore
lhsCore

instance BoundAndUsed e => BoundAndUsed (LHSCore' e) where
  boundAndUsed :: LHSCore' e -> BoundAndUsedNames
boundAndUsed = \ case
    LHSHead QName
_ [NamedArg (Pattern' e)]
ps       -> [NamedArg (Pattern' e)] -> BoundAndUsedNames
forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed [NamedArg (Pattern' e)]
ps
    LHSProj AmbiguousQName
_ NamedArg (LHSCore' e)
lhs [NamedArg (Pattern' e)]
ps   -> NamedArg (LHSCore' e)
lhs NamedArg (LHSCore' e) -> BoundAndUsedNames -> BoundAndUsedNames
forall a b.
(BoundAndUsed a, BoundAndUsed b) =>
a -> b -> BoundAndUsedNames
`parBindings` [NamedArg (Pattern' e)] -> BoundAndUsedNames
forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed [NamedArg (Pattern' e)]
ps
    LHSWith LHSCore' e
lhs [Arg (Pattern' e)]
wps [NamedArg (Pattern' e)]
ps -> LHSCore' e
lhs LHSCore' e -> BoundAndUsedNames -> BoundAndUsedNames
forall a b.
(BoundAndUsed a, BoundAndUsed b) =>
a -> b -> BoundAndUsedNames
`parBindings` [Arg (Pattern' e)] -> BoundAndUsedNames
forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed [Arg (Pattern' e)]
wps
                              BoundAndUsedNames -> BoundAndUsedNames -> BoundAndUsedNames
forall a b.
(BoundAndUsed a, BoundAndUsed b) =>
a -> b -> BoundAndUsedNames
`parBindings` [NamedArg (Pattern' e)] -> BoundAndUsedNames
forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed [NamedArg (Pattern' e)]
ps

instance (BoundAndUsed x, BoundAndUsed p, BoundAndUsed e) => BoundAndUsed (RewriteEqn' q x p e) where
  boundAndUsed :: RewriteEqn' q x p e -> BoundAndUsedNames
boundAndUsed (Rewrite List1 (q, e)
es)  = NonEmpty e -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (NonEmpty e -> BoundAndUsedNames)
-> NonEmpty e -> BoundAndUsedNames
forall a b. (a -> b) -> a -> b
$ (q, e) -> e
forall a b. (a, b) -> b
snd ((q, e) -> e) -> List1 (q, e) -> NonEmpty e
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 (q, e)
es
  boundAndUsed (Invert q
_ List1 (Named x (p, e))
bs) = NonEmpty (p, e) -> BoundAndUsedNames
forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed (Named x (p, e) -> (p, e)
forall name a. Named name a -> a
namedThing (Named x (p, e) -> (p, e))
-> List1 (Named x (p, e)) -> NonEmpty (p, e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 (Named x (p, e))
bs) BoundAndUsedNames -> BoundAndUsedNames -> BoundAndUsedNames
forall a. Semigroup a => a -> a -> a
<> NonEmpty (Maybe x) -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (Named x (p, e) -> Maybe x
forall name a. Named name a -> Maybe name
nameOf (Named x (p, e) -> Maybe x)
-> List1 (Named x (p, e)) -> NonEmpty (Maybe x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 (Named x (p, e))
bs)

instance BoundAndUsed LetBinding where
  boundAndUsed :: LetBinding -> BoundAndUsedNames
boundAndUsed = \ case   -- Note: binder last since it's not recursive
    LetBind LetInfo
_ ArgInfo
_ BindName
x Expr
ty Expr
e     -> ((Expr, Expr), BindName) -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed ((Expr
ty, Expr
e), BindName
x)
    LetPatBind LetInfo
_ Pattern' Expr
p Expr
e       -> (Expr, Pattern' Expr) -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (Expr
e, Pattern' Expr
p)
    LetApply ModuleInfo
_ Erased
_ ModuleName
_ ModuleApplication
app ScopeCopyInfo
_ ImportDirective
_ -> ModuleApplication -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed ModuleApplication
app
    LetOpen{}              -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    LetDeclaredVariable{}  -> BoundAndUsedNames
forall a. Monoid a => a
mempty   -- Only used for highlighting

instance BoundAndUsed LamBinding where
  boundAndUsed :: LamBinding -> BoundAndUsedNames
boundAndUsed (DomainFree TacticAttr
_ NamedArg Binder
b) = NamedArg Binder -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed NamedArg Binder
b
  boundAndUsed (DomainFull TypedBinding
b)   = TypedBinding -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed TypedBinding
b

instance BoundAndUsed TypedBinding where
  boundAndUsed :: TypedBinding -> BoundAndUsedNames
boundAndUsed (TBind Range
_ TypedBindingInfo
_ List1 (NamedArg Binder)
bs Expr
ty) = (Expr, List1 (NamedArg Binder)) -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (Expr
ty, List1 (NamedArg Binder)
bs)
  boundAndUsed (TLet Range
_ List1 LetBinding
bs)       = List1 LetBinding -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed List1 LetBinding
bs

instance BoundAndUsed name => BoundAndUsed (Binder' name) where
  boundAndUsed :: Binder' name -> BoundAndUsedNames
boundAndUsed (Binder Maybe (Pattern' Expr)
p name
x) = Maybe (Pattern' Expr) -> name -> BoundAndUsedNames
forall a b.
(BoundAndUsed a, BoundAndUsed b) =>
a -> b -> BoundAndUsedNames
parBindings Maybe (Pattern' Expr)
p name
x

instance BoundAndUsed BindName where
  boundAndUsed :: BindName -> BoundAndUsedNames
boundAndUsed BindName
x = Name -> BoundAndUsedNames
singleBind (BindName -> Name
unBind BindName
x)

instance BoundAndUsed e => BoundAndUsed (Pattern' e) where
  boundAndUsed :: Pattern' e -> BoundAndUsedNames
boundAndUsed = \ case
    VarP BindName
x             -> BindName -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed BindName
x
    ConP ConPatInfo
_ AmbiguousQName
_ NAPs e
ps        -> NAPs e -> BoundAndUsedNames
forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed NAPs e
ps
    ProjP{}            -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    DefP PatInfo
_ AmbiguousQName
_ NAPs e
ps        -> NAPs e -> BoundAndUsedNames
forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed NAPs e
ps
    WildP{}            -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    AsP PatInfo
_ BindName
x Pattern' e
p          -> BindName -> Pattern' e -> BoundAndUsedNames
forall a b.
(BoundAndUsed a, BoundAndUsed b) =>
a -> b -> BoundAndUsedNames
parBindings BindName
x Pattern' e
p
    DotP PatInfo
_ e
e           -> e -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed e
e
    AbsurdP{}          -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    LitP{}             -> BoundAndUsedNames
forall a. Monoid a => a
mempty
    PatternSynP PatInfo
_ AmbiguousQName
_ NAPs e
ps -> NAPs e -> BoundAndUsedNames
forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed NAPs e
ps
    RecP PatInfo
_ [FieldAssignment' (Pattern' e)]
as          -> [FieldAssignment' (Pattern' e)] -> BoundAndUsedNames
forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed [FieldAssignment' (Pattern' e)]
as
    EqualP PatInfo
_ [(e, e)]
eqs       -> [(e, e)] -> BoundAndUsedNames
forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed [(e, e)]
eqs
    WithP PatInfo
_ Pattern' e
p          -> Pattern' e -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Pattern' e
p
    AnnP PatInfo
_ e
ty Pattern' e
p        -> (e, Pattern' e) -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (e
ty, Pattern' e
p)

instance BoundAndUsed e => BoundAndUsed (FieldAssignment' e) where
  boundAndUsed :: FieldAssignment' e -> BoundAndUsedNames
boundAndUsed (FieldAssignment Name
_ e
e) = e -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed e
e

instance BoundAndUsed ModuleApplication where
  boundAndUsed :: ModuleApplication -> BoundAndUsedNames
boundAndUsed (SectionApp Telescope
tel ModuleName
_ [NamedArg Expr]
es)  = BoundAndUsedNames -> BoundAndUsedNames
noBindings (BoundAndUsedNames -> BoundAndUsedNames)
-> BoundAndUsedNames -> BoundAndUsedNames
forall a b. (a -> b) -> a -> b
$ (Telescope, [NamedArg Expr]) -> BoundAndUsedNames
forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (Telescope
tel, [NamedArg Expr]
es)
  boundAndUsed RecordModuleInstance{} = BoundAndUsedNames
forall a. Monoid a => a
mempty