{-# LANGUAGE TypeFamilies #-}
module Agda.Syntax.Internal.Names where
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.Syntax.Internal
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Abstract as A
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.CompiledClause
import Agda.Utils.Impossible
class NamesIn a where
namesIn :: a -> Set QName
default namesIn :: (Foldable f, NamesIn b, f b ~ a) => a -> Set QName
namesIn = (b -> Set QName) -> f b -> Set QName
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap b -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn
instance NamesIn a => NamesIn (Maybe a) where
instance NamesIn a => NamesIn [a] where
instance NamesIn a => NamesIn (NonEmpty a) where
instance NamesIn a => NamesIn (Arg a) where
instance NamesIn a => NamesIn (Dom a) where
instance NamesIn a => NamesIn (Named n a) where
instance NamesIn a => NamesIn (Abs a) where
instance NamesIn a => NamesIn (WithArity a) where
instance NamesIn a => NamesIn (Tele a) where
instance NamesIn a => NamesIn (C.FieldAssignment' a) where
instance (NamesIn a, NamesIn b) => NamesIn (a, b) where
namesIn :: (a, b) -> Set QName
namesIn (x :: a
x, y :: b
y) = Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
Set.union (a -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn a
x) (b -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn b
y)
instance (NamesIn a, NamesIn b, NamesIn c) => NamesIn (a, b, c) where
namesIn :: (a, b, c) -> Set QName
namesIn (x :: a
x, y :: b
y, z :: c
z) = (a, (b, c)) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (a
x, (b
y, c
z))
instance (NamesIn a, NamesIn b, NamesIn c, NamesIn d) => NamesIn (a, b, c, d) where
namesIn :: (a, b, c, d) -> Set QName
namesIn (x :: a
x, y :: b
y, z :: c
z, u :: d
u) = ((a, b), (c, d)) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn ((a
x, b
y), (c
z, d
u))
instance NamesIn CompKit where
namesIn :: CompKit -> Set QName
namesIn (CompKit a :: Maybe QName
a b :: Maybe QName
b) = (Maybe QName, Maybe QName) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Maybe QName
a,Maybe QName
b)
instance NamesIn Definition where
namesIn :: Definition -> Set QName
namesIn def :: Definition
def = (Type, Defn, [LocalDisplayForm]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Definition -> Type
defType Definition
def, Definition -> Defn
theDef Definition
def, Definition -> [LocalDisplayForm]
defDisplay Definition
def)
instance NamesIn Defn where
namesIn :: Defn -> Set QName
namesIn def :: Defn
def = case Defn
def of
Axiom -> Set QName
forall a. Set a
Set.empty
DataOrRecSig{} -> Set QName
forall a. Set a
Set.empty
GeneralizableVar{} -> Set QName
forall a. Set a
Set.empty
Function { funClauses :: Defn -> [Clause]
funClauses = [Clause]
cl, funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc } -> ([Clause], Maybe CompiledClauses) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn ([Clause]
cl, Maybe CompiledClauses
cc)
Datatype { dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
cl, dataCons :: Defn -> [QName]
dataCons = [QName]
cs, dataSort :: Defn -> Sort
dataSort = Sort
s } -> (Maybe Clause, [QName], Sort) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Maybe Clause
cl, [QName]
cs, Sort
s)
Record { recClause :: Defn -> Maybe Clause
recClause = Maybe Clause
cl, recConHead :: Defn -> ConHead
recConHead = ConHead
c, recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs, recComp :: Defn -> CompKit
recComp = CompKit
comp } -> (Maybe Clause, ConHead, [Dom QName], CompKit) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Maybe Clause
cl, ConHead
c, [Dom QName]
fs, CompKit
comp)
Constructor { conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c, conData :: Defn -> QName
conData = QName
d, conComp :: Defn -> CompKit
conComp = CompKit
kit, conProj :: Defn -> Maybe [QName]
conProj = Maybe [QName]
fs } -> (ConHead, QName, CompKit, Maybe [QName]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (ConHead
c, QName
d, CompKit
kit, Maybe [QName]
fs)
Primitive { primClauses :: Defn -> [Clause]
primClauses = [Clause]
cl, primCompiled :: Defn -> Maybe CompiledClauses
primCompiled = Maybe CompiledClauses
cc } -> ([Clause], Maybe CompiledClauses) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn ([Clause]
cl, Maybe CompiledClauses
cc)
AbstractDefn{} -> Set QName
forall a. HasCallStack => a
__IMPOSSIBLE__
instance NamesIn Clause where
namesIn :: Clause -> Set QName
namesIn Clause{ clauseTel :: Clause -> Telescope
clauseTel = Telescope
tel, namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
ps, clauseBody :: Clause -> Maybe Term
clauseBody = Maybe Term
b, clauseType :: Clause -> Maybe (Arg Type)
clauseType = Maybe (Arg Type)
t } =
(Telescope, NAPs, Maybe Term, Maybe (Arg Type)) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Telescope
tel, NAPs
ps, Maybe Term
b, Maybe (Arg Type)
t)
instance NamesIn CompiledClauses where
namesIn :: CompiledClauses -> Set QName
namesIn (Case _ c :: Case CompiledClauses
c) = Case CompiledClauses -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Case CompiledClauses
c
namesIn (Done _ v :: Term
v) = Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
namesIn Fail = Set QName
forall a. Set a
Set.empty
instance NamesIn a => NamesIn (Case a) where
namesIn :: Case a -> Set QName
namesIn Branches{ conBranches :: forall c. Case c -> Map QName (WithArity c)
conBranches = Map QName (WithArity a)
bs, catchAllBranch :: forall c. Case c -> Maybe c
catchAllBranch = Maybe a
c } =
([(QName, WithArity a)], Maybe a) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Map QName (WithArity a) -> [(QName, WithArity a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map QName (WithArity a)
bs, Maybe a
c)
instance NamesIn (Pattern' a) where
namesIn :: Pattern' a -> Set QName
namesIn p :: Pattern' a
p = case Pattern' a
p of
VarP{} -> Set QName
forall a. Set a
Set.empty
LitP _ l :: Literal
l -> Literal -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Literal
l
DotP _ v :: Term
v -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
ConP c :: ConHead
c _ args :: [NamedArg (Pattern' a)]
args -> (ConHead, [NamedArg (Pattern' a)]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (ConHead
c, [NamedArg (Pattern' a)]
args)
DefP o :: PatternInfo
o q :: QName
q args :: [NamedArg (Pattern' a)]
args -> (QName, [NamedArg (Pattern' a)]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (QName
q, [NamedArg (Pattern' a)]
args)
ProjP _ f :: QName
f -> QName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn QName
f
IApplyP _ t :: Term
t u :: Term
u _ -> (Term, Term) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Term
t, Term
u)
instance NamesIn a => NamesIn (Type' a) where
namesIn :: Type' a -> Set QName
namesIn (El s :: Sort
s t :: a
t) = (Sort, a) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Sort
s, a
t)
instance NamesIn Sort where
namesIn :: Sort -> Set QName
namesIn s :: Sort
s = case Sort
s of
Type l :: Level' Term
l -> Level' Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Level' Term
l
Prop l :: Level' Term
l -> Level' Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Level' Term
l
Inf -> Set QName
forall a. Set a
Set.empty
SizeUniv -> Set QName
forall a. Set a
Set.empty
PiSort a :: Dom' Term Type
a b :: Abs Sort
b -> (Dom' Term Type, Abs Sort) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Dom' Term Type
a, Abs Sort
b)
FunSort a :: Sort
a b :: Sort
b -> (Sort, Sort) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Sort
a, Sort
b)
UnivSort a :: Sort
a -> Sort -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Sort
a
MetaS _ es :: [Elim' Term]
es -> [Elim' Term] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [Elim' Term]
es
DefS d :: QName
d es :: [Elim' Term]
es -> (QName, [Elim' Term]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (QName
d, [Elim' Term]
es)
DummyS{} -> Set QName
forall a. Set a
Set.empty
instance NamesIn Term where
namesIn :: Term -> Set QName
namesIn v :: Term
v = case Term
v of
Var _ args :: [Elim' Term]
args -> [Elim' Term] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [Elim' Term]
args
Lam _ b :: Abs Term
b -> Abs Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Abs Term
b
Lit l :: Literal
l -> Literal -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Literal
l
Def f :: QName
f args :: [Elim' Term]
args -> (QName, [Elim' Term]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (QName
f, [Elim' Term]
args)
Con c :: ConHead
c _ args :: [Elim' Term]
args -> (ConHead, [Elim' Term]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (ConHead
c, [Elim' Term]
args)
Pi a :: Dom' Term Type
a b :: Abs Type
b -> (Dom' Term Type, Abs Type) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (Dom' Term Type
a, Abs Type
b)
Sort s :: Sort
s -> Sort -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Sort
s
Level l :: Level' Term
l -> Level' Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Level' Term
l
MetaV _ args :: [Elim' Term]
args -> [Elim' Term] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [Elim' Term]
args
DontCare v :: Term
v -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
Dummy{} -> Set QName
forall a. Set a
Set.empty
instance NamesIn Level where
namesIn :: Level' Term -> Set QName
namesIn (Max _ ls :: [PlusLevel' Term]
ls) = [PlusLevel' Term] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [PlusLevel' Term]
ls
instance NamesIn PlusLevel where
namesIn :: PlusLevel' Term -> Set QName
namesIn (Plus _ l :: LevelAtom' Term
l) = LevelAtom' Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn LevelAtom' Term
l
instance NamesIn LevelAtom where
namesIn :: LevelAtom' Term -> Set QName
namesIn l :: LevelAtom' Term
l = case LevelAtom' Term
l of
MetaLevel _ args :: [Elim' Term]
args -> [Elim' Term] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [Elim' Term]
args
BlockedLevel _ v :: Term
v -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
NeutralLevel _ v :: Term
v -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
UnreducedLevel v :: Term
v -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
instance NamesIn Literal where
namesIn :: Literal -> Set QName
namesIn l :: Literal
l = case Literal
l of
LitNat{} -> Set QName
forall a. Set a
Set.empty
LitWord64{} -> Set QName
forall a. Set a
Set.empty
LitString{} -> Set QName
forall a. Set a
Set.empty
LitChar{} -> Set QName
forall a. Set a
Set.empty
LitFloat{} -> Set QName
forall a. Set a
Set.empty
LitQName _ x :: QName
x -> QName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn QName
x
LitMeta{} -> Set QName
forall a. Set a
Set.empty
instance NamesIn a => NamesIn (Elim' a) where
namesIn :: Elim' a -> Set QName
namesIn (Apply arg :: Arg a
arg) = Arg a -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Arg a
arg
namesIn (Proj _ f :: QName
f) = QName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn QName
f
namesIn (IApply x :: a
x y :: a
y arg :: a
arg) = (a, a, a) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (a
x, a
y, a
arg)
instance NamesIn QName where namesIn :: QName -> Set QName
namesIn x :: QName
x = QName -> Set QName
forall a. a -> Set a
Set.singleton QName
x
instance NamesIn ConHead where namesIn :: ConHead -> Set QName
namesIn h :: ConHead
h = QName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (ConHead -> QName
conName ConHead
h)
instance NamesIn a => NamesIn (Open a) where
instance NamesIn DisplayForm where
namesIn :: DisplayForm -> Set QName
namesIn (Display _ ps :: [Elim' Term]
ps v :: DisplayTerm
v) = ([Elim' Term], DisplayTerm) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn ([Elim' Term]
ps, DisplayTerm
v)
instance NamesIn DisplayTerm where
namesIn :: DisplayTerm -> Set QName
namesIn v :: DisplayTerm
v = case DisplayTerm
v of
DWithApp v :: DisplayTerm
v us :: [DisplayTerm]
us es :: [Elim' Term]
es -> (DisplayTerm, [DisplayTerm], [Elim' Term]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (DisplayTerm
v, [DisplayTerm]
us, [Elim' Term]
es)
DCon c :: ConHead
c _ vs :: [Arg DisplayTerm]
vs -> (ConHead, [Arg DisplayTerm]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (ConHead
c, [Arg DisplayTerm]
vs)
DDef f :: QName
f es :: [Elim' DisplayTerm]
es -> (QName, [Elim' DisplayTerm]) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (QName
f, [Elim' DisplayTerm]
es)
DDot v :: Term
v -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
DTerm v :: Term
v -> Term -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Term
v
newtype PSyn = PSyn A.PatternSynDefn
instance NamesIn PSyn where
namesIn :: PSyn -> Set QName
namesIn (PSyn (_args :: [Arg Name]
_args, p :: Pattern' Void
p)) = Pattern' Void -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Pattern' Void
p
instance NamesIn (A.Pattern' a) where
namesIn :: Pattern' a -> Set QName
namesIn p :: Pattern' a
p = case Pattern' a
p of
A.VarP{} -> Set QName
forall a. Set a
Set.empty
A.ConP _ c :: AmbiguousQName
c args :: NAPs a
args -> (AmbiguousQName, NAPs a) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (AmbiguousQName
c, NAPs a
args)
A.ProjP _ _ d :: AmbiguousQName
d -> AmbiguousQName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn AmbiguousQName
d
A.DefP _ f :: AmbiguousQName
f args :: NAPs a
args -> (AmbiguousQName, NAPs a) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (AmbiguousQName
f, NAPs a
args)
A.WildP{} -> Set QName
forall a. Set a
Set.empty
A.AsP _ _ p :: Pattern' a
p -> Pattern' a -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Pattern' a
p
A.AbsurdP{} -> Set QName
forall a. Set a
Set.empty
A.LitP l :: Literal
l -> Literal -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Literal
l
A.PatternSynP _ c :: AmbiguousQName
c args :: NAPs a
args -> (AmbiguousQName, NAPs a) -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn (AmbiguousQName
c, NAPs a
args)
A.RecP _ fs :: [FieldAssignment' (Pattern' a)]
fs -> [FieldAssignment' (Pattern' a)] -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn [FieldAssignment' (Pattern' a)]
fs
A.DotP{} -> Set QName
forall a. HasCallStack => a
__IMPOSSIBLE__
A.EqualP{} -> Set QName
forall a. HasCallStack => a
__IMPOSSIBLE__
A.WithP _ p :: Pattern' a
p -> Pattern' a -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Pattern' a
p
instance NamesIn AmbiguousQName where
namesIn :: AmbiguousQName -> Set QName
namesIn (AmbQ cs :: NonEmpty QName
cs) = NonEmpty QName -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn NonEmpty QName
cs