    module Agda.Syntax.Internal.MetaVars where

    import Data.Monoid
    import qualified Data.Set as Set

    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 annotations on types.
    class AllMetas t where
      allMetas :: Monoid m => (MetaId -> m) -> t -> m

      default allMetas :: (TermLike t, Monoid m) => (MetaId -> m) -> t -> m
      allMetas = (MetaId -> m) -> t -> m
    forall a m. (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
    allMetas'

    -- Default instances
    instance AllMetas Term
    instance AllMetas Type
    instance TermLike a => AllMetas (Elim' a)
    instance TermLike a => AllMetas (Tele a)
    instance TermLike a => AllMetas (Dom a)

    -- These types need to be packed up as a Term to get the metas.
    instance AllMetas Sort      where allMetas :: forall m. Monoid m => (MetaId -> m) -> Sort -> m
    allMetas MetaId -> m
    f   = (MetaId -> m) -> Term -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> m
    f (Term -> m) -> (Sort -> Term) -> Sort -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sort -> Term
    Sort
    instance AllMetas Level     where allMetas :: forall m. Monoid m => (MetaId -> m) -> Level -> m
    allMetas MetaId -> m
    f   = (MetaId -> m) -> Term -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> m
    f (Term -> m) -> (Level -> Term) -> Level -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Level -> Term
    Level
    instance AllMetas PlusLevel where allMetas :: forall m. Monoid m => (MetaId -> m) -> PlusLevel -> m
    allMetas MetaId -> m
    f PlusLevel
    l = (MetaId -> m) -> Level -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> m
    f (Integer -> [PlusLevel] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    0 [PlusLevel
    l])

    -- Generic instances
    instance (AllMetas a, AllMetas b) => AllMetas (a, b) where
      allMetas :: forall m. Monoid m => (MetaId -> m) -> (a, b) -> m
    allMetas MetaId -> m
    f (a
    x, b
    y) = (MetaId -> m) -> a -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> m
    f a
    x m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (MetaId -> m) -> b -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> m
    f b
    y

    instance (AllMetas a, AllMetas b, AllMetas c) => AllMetas (a, b, c) where
      allMetas :: forall m. Monoid m => (MetaId -> m) -> (a, b, c) -> m
    allMetas MetaId -> m
    f (a
    x, b
    y, c
    z) = (MetaId -> m) -> (a, (b, c)) -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> m
    f (a
    x, (b
    y, c
    z))

    instance (AllMetas a, AllMetas b, AllMetas c, AllMetas d) => AllMetas (a, b, c, d) where
      allMetas :: forall m. Monoid m => (MetaId -> m) -> (a, b, c, d) -> m
    allMetas MetaId -> m
    f (a
    x, b
    y, c
    z, d
    w) = (MetaId -> m) -> (a, (b, (c, d))) -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> m
    f (a
    x, (b
    y, (c
    z, d
    w)))

    instance AllMetas a => AllMetas [a]       where allMetas :: forall m. Monoid m => (MetaId -> m) -> [a] -> m
    allMetas MetaId -> m
    f [a]
    xs = (a -> m) -> [a] -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((MetaId -> m) -> a -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> m
    f) [a]
    xs
    instance AllMetas a => AllMetas (Maybe a) where allMetas :: forall m. Monoid m => (MetaId -> m) -> Maybe a -> m
    allMetas MetaId -> m
    f Maybe a
    xs = (a -> m) -> Maybe a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((MetaId -> m) -> a -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> m
    f) Maybe a
    xs
    instance AllMetas a => AllMetas (Arg a)   where allMetas :: forall m. Monoid m => (MetaId -> m) -> Arg a -> m
    allMetas MetaId -> m
    f Arg a
    xs = (a -> m) -> Arg a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((MetaId -> m) -> a -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> m
    f) Arg a
    xs

    allMetas' :: (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
    allMetas' :: forall a m. (TermLike a, Monoid m) => (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 (Sort Sort
    s)    = Sort -> m
    sortMetas Sort
    s
      metas Term
    _           = m
    forall a. Monoid a => a
    mempty

      sortMetas :: Sort -> m
    sortMetas Type{}        = m
    forall a. Monoid a => a
    mempty
      sortMetas Prop{}        = m
    forall a. Monoid a => a
    mempty
      sortMetas SSet{}        = m
    forall a. Monoid a => a
    mempty
      sortMetas Inf{}         = m
    forall a. Monoid a => a
    mempty
      sortMetas SizeUniv{}    = m
    forall a. Monoid a => a
    mempty
      sortMetas LockUniv{}    = m
    forall a. Monoid a => a
    mempty
      sortMetas (PiSort Dom' Term Term
    _ Sort
    s1 Abs Sort
    s2)  = Sort -> m
    sortMetas Sort
    s1 m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> Sort -> m
    sortMetas (Abs Sort -> Sort
    forall a. Abs a -> a
    unAbs Abs Sort
    s2)  -- the domain is a term so is covered by the fold
      sortMetas (FunSort Sort
    a Sort
    b) = Sort -> m
    sortMetas Sort
    a m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> Sort -> m
    sortMetas Sort
    b
      sortMetas (UnivSort Sort
    s)  = Sort -> m
    sortMetas Sort
    s
      sortMetas (MetaS MetaId
    x Elims
    _)   = MetaId -> m
    singl MetaId
    x
      sortMetas DefS{}        = m
    forall a. Monoid a => a
    mempty
      sortMetas DummyS{}      = 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 :: AllMetas a => a -> [MetaId]
    allMetasList :: forall a. AllMetas a => a -> [MetaId]
    allMetasList a
    t = (MetaId -> Endo [MetaId]) -> a -> Endo [MetaId]
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> 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 :: AllMetas a => a -> Bool
    noMetas :: forall a. AllMetas a => 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 t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas (\ MetaId
    _m -> Bool -> All
    All Bool
    False)

    -- | Returns the first meta it find in the thing, if any.
    --   @firstMeta == listToMaybe . allMetasList@.
    firstMeta :: AllMetas a => a -> Maybe MetaId
    firstMeta :: forall a. AllMetas a => 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 t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> 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)

    -- | A blocker that unblocks if any of the metas in a term are solved.
    unblockOnAnyMetaIn :: AllMetas t => t -> Blocker
    unblockOnAnyMetaIn :: forall t. AllMetas t => t -> Blocker
    unblockOnAnyMetaIn t
    t = Set MetaId -> Blocker
    unblockOnAnyMeta (Set MetaId -> Blocker) -> Set MetaId -> Blocker
    forall a b. (a -> b) -> a -> b
    $ (MetaId -> Set MetaId) -> t -> Set MetaId
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton t
    t

    -- | A blocker that unblocks if any of the metas in a term are solved.
    unblockOnAllMetasIn :: AllMetas t => t -> Blocker
    unblockOnAllMetasIn :: forall t. AllMetas t => t -> Blocker
    unblockOnAllMetasIn t
    t = Set MetaId -> Blocker
    unblockOnAllMetas (Set MetaId -> Blocker) -> Set MetaId -> Blocker
    forall a b. (a -> b) -> a -> b
    $ (MetaId -> Set MetaId) -> t -> Set MetaId
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton t
    t