{-# OPTIONS_GHC -Wunused-imports #-}

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 (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) = (MetaId -> m) -> Maybe a -> m
forall m. Monoid m => (MetaId -> m) -> Maybe a -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> m
f Maybe a
t m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (MetaId -> m) -> b -> m
forall m. Monoid m => (MetaId -> m) -> b -> m
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   = (MetaId -> m) -> Term -> m
forall m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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])

instance {-# OVERLAPPING #-} AllMetas String where
  allMetas :: forall m. Monoid m => (MetaId -> m) -> String -> m
allMetas MetaId -> m
f String
_ = m
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) = (MetaId -> m) -> a -> m
forall m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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 m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((MetaId -> m) -> a -> m
forall m. Monoid m => (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 m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((MetaId -> m) -> a -> m
forall m. Monoid m => (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 m a. Monoid m => (a -> m) -> Arg a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((MetaId -> m) -> a -> m
forall m. Monoid m => (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 m. Monoid m => (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 Univ{}        = 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 Sort
LevelUniv     = m
forall a. Monoid a => a
mempty
  sortMetas IntervalUniv{} = 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 m. Monoid m => (MetaId -> m) -> a -> m
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 m. Monoid m => (MetaId -> m) -> a -> m
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 m. Monoid m => (MetaId -> m) -> a -> m
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 m. Monoid m => (MetaId -> m) -> t -> m
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 m. Monoid m => (MetaId -> m) -> t -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton t
t