module Agda.Syntax.Internal.MetaVars where
import Data.Monoid
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic
import Agda.Utils.Singleton
allMetas :: (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
allMetas singl = foldTerm metas
where
metas (MetaV m _) = singl m
metas (Level l) = levelMetas l
metas _ = mempty
levelMetas (Max _ as) = foldMap plusLevelMetas as
plusLevelMetas (Plus _ l) = levelAtomMetas l
levelAtomMetas (MetaLevel m _) = singl m
levelAtomMetas _ = mempty
allMetasList :: TermLike a => a -> [MetaId]
allMetasList t = allMetas singleton t `appEndo` []
noMetas :: TermLike a => a -> Bool
noMetas = getAll . allMetas (\ _m -> All False)
firstMeta :: TermLike a => a -> Maybe MetaId
firstMeta = getFirst . allMetas (First . Just)