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

-- | Returns every meta-variable occurrence in the given type, except
-- for those in 'Sort's.
allMetas :: (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
allMetas :: (MetaId -> m) -> a -> m
allMetas MetaId -> m
singl = (Term -> m) -> a -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
metas
  where
  metas :: Term -> m
metas (MetaV MetaId
m Elims
_) = MetaId -> m
singl MetaId
m
  metas (Level Level
l)   = Level -> m
forall t. Level' t -> m
levelMetas Level
l
  metas Term
_           = m
forall a. Monoid a => a
mempty

  levelMetas :: Level' t -> m
levelMetas (Max Integer
_ [PlusLevel' t]
as) = (PlusLevel' t -> m) -> [PlusLevel' t] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap PlusLevel' t -> m
forall t. PlusLevel' t -> m
plusLevelMetas [PlusLevel' t]
as

  plusLevelMetas :: PlusLevel' t -> m
plusLevelMetas (Plus Integer
_ LevelAtom' t
l)    = LevelAtom' t -> m
forall t. LevelAtom' t -> m
levelAtomMetas LevelAtom' t
l

  levelAtomMetas :: LevelAtom' t -> m
levelAtomMetas (MetaLevel MetaId
m [Elim' t]
_) = MetaId -> m
singl MetaId
m
  levelAtomMetas LevelAtom' t
_               = m
forall a. Monoid a => a
mempty

-- | Returns 'allMetas' in a list.
--   @allMetasList = allMetas (:[])@.
--
--   Note: this resulting list is computed via difference lists.
--   Thus, use this function if you actually need the whole list of metas.
--   Otherwise, use 'allMetas' with a suitable monoid.
allMetasList :: TermLike a => a -> [MetaId]
allMetasList :: a -> [MetaId]
allMetasList a
t = (MetaId -> Endo [MetaId]) -> a -> Endo [MetaId]
forall a m. (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
allMetas MetaId -> Endo [MetaId]
forall el coll. Singleton el coll => el -> coll
singleton a
t Endo [MetaId] -> [MetaId] -> [MetaId]
forall a. Endo a -> a -> a
`appEndo` []

-- | 'True' if thing contains no metas.
--   @noMetas = null . allMetasList@.
noMetas :: TermLike a => a -> Bool
noMetas :: a -> Bool
noMetas = All -> Bool
getAll (All -> Bool) -> (a -> All) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> All) -> a -> All
forall a m. (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
allMetas (\ MetaId
_m -> Bool -> All
All Bool
False)

-- | Returns the first meta it find in the thing, if any.
--   @firstMeta == listToMaybe . allMetasList@.
firstMeta :: TermLike a => a -> Maybe MetaId
firstMeta :: a -> Maybe MetaId
firstMeta = First MetaId -> Maybe MetaId
forall a. First a -> Maybe a
getFirst (First MetaId -> Maybe MetaId)
-> (a -> First MetaId) -> a -> Maybe MetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> First MetaId) -> a -> First MetaId
forall a m. (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
allMetas (Maybe MetaId -> First MetaId
forall a. Maybe a -> First a
First (Maybe MetaId -> First MetaId)
-> (MetaId -> Maybe MetaId) -> MetaId -> First MetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just)