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 = 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 (AllMetas a, AllMetas b) => AllMetas (Dom' a b) where
  allMetas :: forall m. Monoid m => (MetaId -> m) -> Dom' a b -> m
allMetas MetaId -> m
f (Dom ArgInfo
_ Maybe NamedName
_ Bool
_ Maybe a
t b
e) = forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> m
f Maybe a
t forall a. Semigroup a => a -> a -> a
<> forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> m
f b
e

-- 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   = forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> m
f 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   = forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> m
f 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 = forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> m
f (forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
0 [PlusLevel
l])

instance {-# OVERLAPPING #-} AllMetas String where
  allMetas :: forall m. Monoid m => (MetaId -> m) -> String -> m
allMetas MetaId -> m
f String
_ = forall a. Monoid a => a
mempty

-- 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) = forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> m
f a
x forall a. Semigroup a => a -> a -> a
<> 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) = 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) = 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 = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (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 = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (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 = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (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 = 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
_           = forall a. Monoid a => a
mempty

  sortMetas :: Sort -> m
sortMetas Type{}        = forall a. Monoid a => a
mempty
  sortMetas Prop{}        = forall a. Monoid a => a
mempty
  sortMetas SSet{}        = forall a. Monoid a => a
mempty
  sortMetas Inf{}         = forall a. Monoid a => a
mempty
  sortMetas SizeUniv{}    = forall a. Monoid a => a
mempty
  sortMetas LockUniv{}    = forall a. Monoid a => a
mempty
  sortMetas IntervalUniv{} = forall a. Monoid a => a
mempty
  sortMetas (PiSort Dom' Term Term
_ Sort
s1 Abs Sort
s2)  = Sort -> m
sortMetas Sort
s1 forall a. Semigroup a => a -> a -> a
<> Sort -> m
sortMetas (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 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{}        = forall a. Monoid a => a
mempty
  sortMetas DummyS{}      = 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 = forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas forall el coll. Singleton el coll => el -> coll
singleton a
t 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a. First a -> Maybe a
getFirst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas (forall a. Maybe a -> First a
First forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a b. (a -> b) -> a -> b
$ forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas 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 forall a b. (a -> b) -> a -> b
$ forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas forall a. a -> Set a
Set.singleton t
t