{-# 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
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'
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
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
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)
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
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` []
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)
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)
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
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