module Agda.Utils.Generics
( module Data.Generics
, isString
, everythingBut
, everywhereBut'
, everywhereButM'
) where
import Data.Generics
(GenericQ, mkQ, extQ, gmapQ, GenericT, gmapT, GenericM, gmapM)
isString :: GenericQ Bool
isString = mkQ False (const True :: String -> Bool)
everythingBut :: (r -> r -> r) -> GenericQ Bool -> GenericQ r -> GenericQ r
everythingBut (+) stop collect x
| stop x = collect x
| otherwise = foldr1 (+) $
collect x : gmapQ (everythingBut (+) stop collect) x
everywhereBut' :: GenericQ Bool -> GenericT -> GenericT
everywhereBut' q f x
| q x = f x
| otherwise = f (gmapT (everywhereBut' q f) x)
everywhereButM' :: Monad m => GenericQ Bool -> GenericM m -> GenericM m
everywhereButM' q f x
| q x = f x
| otherwise = f =<< gmapM (everywhereButM' q f) x