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
allUsedNames :: Expr -> Set Name
allUsedNames :: Expr -> Set Name
allUsedNames = BoundAndUsedNames -> Set Name
usedNames forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed
data BoundAndUsedNames = BoundAndUsedNames
{ BoundAndUsedNames -> Set Name
boundNames :: Set Name
, BoundAndUsedNames -> Set Name
usedNames :: Set Name }
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 forall a. Semigroup a => a -> a -> a
<> Set Name
bound2) (Set Name
used1 forall a. Semigroup a => a -> a -> a
<> 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 forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
mappend :: BoundAndUsedNames -> BoundAndUsedNames -> BoundAndUsedNames
mappend = forall a. Semigroup a => a -> a -> a
(<>)
singleUse :: Name -> BoundAndUsedNames
singleUse :: Name -> BoundAndUsedNames
singleUse Name
x = Set Name -> Set Name -> BoundAndUsedNames
BoundAndUsedNames forall a. Monoid a => a
mempty (forall a. a -> Set a
Set.singleton Name
x)
singleBind :: Name -> BoundAndUsedNames
singleBind :: Name -> BoundAndUsedNames
singleBind Name
x = Set Name -> Set Name -> BoundAndUsedNames
BoundAndUsedNames (forall a. a -> Set a
Set.singleton Name
x) forall a. Monoid a => a
mempty
noBindings :: BoundAndUsedNames -> BoundAndUsedNames
noBindings :: BoundAndUsedNames -> BoundAndUsedNames
noBindings BoundAndUsedNames
names = BoundAndUsedNames
names{ boundNames :: Set Name
boundNames = forall a. Monoid a => a
mempty }
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 forall a. Semigroup a => a -> a -> a
<> Set Name
bound2) (Set Name
used1 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 = forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed a
a BoundAndUsedNames -> BoundAndUsedNames -> BoundAndUsedNames
`parB` 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a b.
(BoundAndUsed a, BoundAndUsed b) =>
a -> b -> BoundAndUsedNames
parBindings 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 = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed
instance BoundAndUsed BoundAndUsedNames where
boundAndUsed :: BoundAndUsedNames -> BoundAndUsedNames
boundAndUsed = 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 = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed
instance BoundAndUsed ModuleName where
boundAndUsed :: ModuleName -> BoundAndUsedNames
boundAndUsed ModuleName
_ = forall a. Monoid a => a
mempty
instance (BoundAndUsed a, BoundAndUsed b) => BoundAndUsed (a, b) where
boundAndUsed :: (a, b) -> BoundAndUsedNames
boundAndUsed (a
a, b
b) = forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed a
a forall a. Semigroup a => a -> a -> a
<> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed b
b
instance BoundAndUsed Expr where
boundAndUsed :: Expr -> BoundAndUsedNames
boundAndUsed = BoundAndUsedNames -> BoundAndUsedNames
noBindings forall b c a. (b -> c) -> (a -> b) -> a -> c
. \ case
Var Name
x -> Name -> BoundAndUsedNames
singleUse Name
x
Def'{} -> forall a. Monoid a => a
mempty
Proj{} -> forall a. Monoid a => a
mempty
Con{} -> forall a. Monoid a => a
mempty
PatternSyn{} -> forall a. Monoid a => a
mempty
Macro{} -> forall a. Monoid a => a
mempty
Lit{} -> forall a. Monoid a => a
mempty
QuestionMark{} -> forall a. Monoid a => a
mempty
Underscore{} -> forall a. Monoid a => a
mempty
Dot ExprInfo
_ Expr
expr -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Expr
expr
App AppInfo
_ Expr
expr NamedArg Expr
arg -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (Expr
expr, NamedArg Expr
arg)
WithApp ExprInfo
_ Expr
expr [Expr]
exprs -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (Expr
expr, [Expr]
exprs)
Lam ExprInfo
_ LamBinding
bind Expr
expr -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (LamBinding
bind, Expr
expr)
AbsurdLam{} -> forall a. Monoid a => a
mempty
ExtendedLam ExprInfo
_ DefInfo
_ Erased
_ QName
_ List1 Clause
cs -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed List1 Clause
cs
Pi ExprInfo
_ Telescope1
tel Expr
expr -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (Telescope1
tel, Expr
expr)
Generalized Set QName
_ Expr
expr -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Expr
expr
Fun ExprInfo
_ Arg Expr
arg Expr
expr -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (Arg Expr
arg, Expr
expr)
Let ExprInfo
_ List1 LetBinding
binds Expr
expr -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (List1 LetBinding
binds, Expr
expr)
Rec ExprInfo
_ RecordAssigns
as -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed RecordAssigns
as
RecUpdate ExprInfo
_ Expr
expr Assigns
as -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Expr
expr forall a. Semigroup a => a -> a -> a
<> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Assigns
as
ScopedExpr ScopeInfo
_ Expr
expr -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Expr
expr
Quote{} -> forall a. Monoid a => a
mempty
QuoteTerm{} -> forall a. Monoid a => a
mempty
Unquote{} -> forall a. Monoid a => a
mempty
DontCare Expr
expr -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Expr
expr
instance BoundAndUsed lhs => BoundAndUsed (Clause' lhs) where
boundAndUsed :: Clause' lhs -> BoundAndUsedNames
boundAndUsed Clause{ clauseLHS :: forall lhs. Clause' lhs -> lhs
clauseLHS = lhs
lhs, clauseRHS :: forall lhs. Clause' lhs -> RHS
clauseRHS = RHS
rhs } = 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
_ -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Expr
body
RHS
AbsurdRHS -> forall a. Monoid a => a
mempty
WithRHS QName
_ [WithExpr]
es List1 Clause
cs -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed ([WithExpr]
es, List1 Clause
cs)
RewriteRHS [RewriteEqn]
eqns [ProblemEq]
_ RHS
rhs WhereDeclarations
_ -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed ([RewriteEqn]
eqns, RHS
rhs)
instance BoundAndUsed LHS where
boundAndUsed :: LHS -> BoundAndUsedNames
boundAndUsed = forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed 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 -> 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 forall a b.
(BoundAndUsed a, BoundAndUsed b) =>
a -> b -> BoundAndUsedNames
`parBindings` 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 forall a b.
(BoundAndUsed a, BoundAndUsed b) =>
a -> b -> BoundAndUsedNames
`parBindings` forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed [Arg (Pattern' e)]
wps
forall a b.
(BoundAndUsed a, BoundAndUsed b) =>
a -> b -> BoundAndUsedNames
`parBindings` 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) = forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd 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) = forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed (forall name a. Named name a -> a
namedThing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 (Named x (p, e))
bs) forall a. Semigroup a => a -> a -> a
<> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (forall name a. Named name a -> Maybe name
nameOf 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
LetBind LetInfo
_ ArgInfo
_ BindName
x Expr
ty Expr
e -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed ((Expr
ty, Expr
e), BindName
x)
LetPatBind LetInfo
_ Pattern' Expr
p Expr
e -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (Expr
e, Pattern' Expr
p)
LetApply ModuleInfo
_ Erased
_ ModuleName
_ ModuleApplication
app ScopeCopyInfo
_ ImportDirective
_ -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed ModuleApplication
app
LetOpen{} -> forall a. Monoid a => a
mempty
LetDeclaredVariable{} -> forall a. Monoid a => a
mempty
instance BoundAndUsed LamBinding where
boundAndUsed :: LamBinding -> BoundAndUsedNames
boundAndUsed (DomainFree TacticAttr
_ NamedArg Binder
b) = forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed NamedArg Binder
b
boundAndUsed (DomainFull TypedBinding
b) = 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) = forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (Expr
ty, List1 (NamedArg Binder)
bs)
boundAndUsed (TLet Range
_ List1 LetBinding
bs) = 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) = 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 -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed BindName
x
ConP ConPatInfo
_ AmbiguousQName
_ NAPs e
ps -> forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed NAPs e
ps
ProjP{} -> forall a. Monoid a => a
mempty
DefP PatInfo
_ AmbiguousQName
_ NAPs e
ps -> forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed NAPs e
ps
WildP{} -> forall a. Monoid a => a
mempty
AsP PatInfo
_ BindName
x Pattern' e
p -> forall a b.
(BoundAndUsed a, BoundAndUsed b) =>
a -> b -> BoundAndUsedNames
parBindings BindName
x Pattern' e
p
DotP PatInfo
_ e
e -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed e
e
AbsurdP{} -> forall a. Monoid a => a
mempty
LitP{} -> forall a. Monoid a => a
mempty
PatternSynP PatInfo
_ AmbiguousQName
_ NAPs e
ps -> forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed NAPs e
ps
RecP PatInfo
_ [FieldAssignment' (Pattern' e)]
as -> forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed [FieldAssignment' (Pattern' e)]
as
EqualP PatInfo
_ [(e, e)]
eqs -> forall (f :: * -> *) a.
(Foldable f, BoundAndUsed a) =>
f a -> BoundAndUsedNames
parBoundAndUsed [(e, e)]
eqs
WithP PatInfo
_ Pattern' e
p -> forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed Pattern' e
p
AnnP PatInfo
_ e
ty Pattern' e
p -> 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) = 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 forall a b. (a -> b) -> a -> b
$ forall a. BoundAndUsed a => a -> BoundAndUsedNames
boundAndUsed (Telescope
tel, [NamedArg Expr]
es)
boundAndUsed RecordModuleInstance{} = forall a. Monoid a => a
mempty