{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}
module Agda.Syntax.Internal.Names where
import Data.Foldable
import Data.Map (Map)
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.Functor
import Agda.Utils.NonemptyList
import Agda.Utils.Impossible
#include "undefined.h"
class NamesIn a where
namesIn :: a -> Set QName
default namesIn :: (Foldable f, NamesIn b, f b ~ a) => a -> Set QName
namesIn = foldMap namesIn
instance NamesIn a => NamesIn (Maybe a) where
instance NamesIn a => NamesIn [a] where
instance NamesIn a => NamesIn (NonemptyList 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 (x, y) = Set.union (namesIn x) (namesIn y)
instance (NamesIn a, NamesIn b, NamesIn c) => NamesIn (a, b, c) where
namesIn (x, y, z) = namesIn (x, (y, z))
instance NamesIn Definition where
namesIn def = namesIn (defType def, theDef def, defDisplay def)
instance NamesIn Defn where
namesIn def = case def of
Axiom -> Set.empty
Function { funClauses = cl, funCompiled = cc } -> namesIn (cl, cc)
Datatype { dataClause = cl, dataCons = cs, dataSort = s } -> namesIn (cl, cs, s)
Record { recClause = cl, recConHead = c, recFields = fs } -> namesIn (cl, c, fs)
Constructor { conSrcCon = c, conData = d } -> namesIn (c, d)
Primitive { primClauses = cl, primCompiled = cc } -> namesIn (cl, cc)
AbstractDefn{} -> __IMPOSSIBLE__
instance NamesIn Clause where
namesIn Clause{ clauseTel = tel, namedClausePats = ps, clauseBody = b, clauseType = t } =
namesIn ((tel, ps, b), t)
instance NamesIn CompiledClauses where
namesIn (Case _ c) = namesIn c
namesIn (Done _ v) = namesIn v
namesIn Fail = Set.empty
instance NamesIn a => NamesIn (Case a) where
namesIn Branches{ conBranches = bs, catchAllBranch = c } =
namesIn (Map.toList bs, c)
instance NamesIn (Pattern' a) where
namesIn p = case p of
VarP{} -> Set.empty
LitP l -> namesIn l
DotP _ v -> namesIn v
ConP c _ args -> namesIn (c, args)
ProjP _ f -> namesIn f
instance NamesIn a => NamesIn (Type' a) where
namesIn (El s t) = namesIn (s, t)
instance NamesIn Sort where
namesIn s = case s of
Type l -> namesIn l
Prop -> Set.empty
Inf -> Set.empty
SizeUniv -> Set.empty
PiSort a b -> namesIn (a, b)
UnivSort a -> namesIn a
MetaS _ es -> namesIn es
instance NamesIn Term where
namesIn v = case v of
Var _ args -> namesIn args
Lam _ b -> namesIn b
Lit l -> namesIn l
Def f args -> namesIn (f, args)
Con c _ args -> namesIn (c, args)
Pi a b -> namesIn (a, b)
Sort s -> namesIn s
Level l -> namesIn l
MetaV _ args -> namesIn args
DontCare v -> namesIn v
instance NamesIn Level where
namesIn (Max ls) = namesIn ls
instance NamesIn PlusLevel where
namesIn ClosedLevel{} = Set.empty
namesIn (Plus _ l) = namesIn l
instance NamesIn LevelAtom where
namesIn l = case l of
MetaLevel _ args -> namesIn args
BlockedLevel _ v -> namesIn v
NeutralLevel _ v -> namesIn v
UnreducedLevel v -> namesIn v
instance NamesIn Literal where
namesIn l = case l of
LitNat{} -> Set.empty
LitWord64{} -> Set.empty
LitString{} -> Set.empty
LitChar{} -> Set.empty
LitFloat{} -> Set.empty
LitQName _ x -> namesIn x
LitMeta{} -> Set.empty
instance NamesIn a => NamesIn (Elim' a) where
namesIn (Apply arg) = namesIn arg
namesIn (Proj _ f) = namesIn f
instance NamesIn QName where namesIn x = Set.singleton x
instance NamesIn ConHead where namesIn h = namesIn (conName h)
instance NamesIn a => NamesIn (Open a) where
instance NamesIn DisplayForm where
namesIn (Display _ ps v) = namesIn (ps, v)
instance NamesIn DisplayTerm where
namesIn v = case v of
DWithApp v us es -> namesIn (v, us, es)
DCon c _ vs -> namesIn (c, vs)
DDef f es -> namesIn (f, es)
DDot v -> namesIn v
DTerm v -> namesIn v
newtype PSyn = PSyn A.PatternSynDefn
instance NamesIn PSyn where
namesIn (PSyn (_args, p)) = namesIn p
instance NamesIn (A.Pattern' a) where
namesIn p = case p of
A.VarP{} -> Set.empty
A.ConP _ c args -> namesIn (c, args)
A.ProjP _ _ d -> namesIn d
A.DefP _ f args -> namesIn (f, args)
A.WildP{} -> Set.empty
A.AsP _ _ p -> namesIn p
A.AbsurdP{} -> Set.empty
A.LitP l -> namesIn l
A.PatternSynP _ c args -> namesIn (c, args)
A.RecP _ fs -> namesIn fs
A.DotP{} -> __IMPOSSIBLE__
A.WithP _ p -> namesIn p
instance NamesIn AmbiguousQName where
namesIn (AmbQ cs) = namesIn cs