{-# LANGUAGE Rank2Types #-}
{-| Contains some generic utility functions.
-}
module Agda.Utils.Generics where

import Data.Generics

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

-- | Same as everywhereBut except that when the stop condition becomes
--   true, the function is called on the top level term (but not on the
--   children).
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