{-# LANGUAGE CPP #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.Utils.ListT where
import Control.Applicative ( Alternative((<|>), empty) )
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State
import Data.Semigroup
import Agda.Utils.Maybe
newtype ListT m a = ListT { runListT :: m (Maybe (a, ListT m a)) }
deriving (Functor)
mapListT :: (m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))) -> ListT m a -> ListT n b
mapListT f = ListT . f . runListT
nilListT :: Monad m => ListT m a
nilListT = ListT $ return Nothing
consListT :: Monad m => a -> ListT m a -> ListT m a
consListT a l = ListT $ return $ Just (a, l)
sgListT :: Monad m => a -> ListT m a
sgListT a = consListT a nilListT
caseListT :: Monad m => ListT m a -> m b -> (a -> ListT m a -> m b) -> m b
caseListT l nil cons = caseMaybeM (runListT l) nil $ uncurry cons
foldListT :: Monad m => (a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT cons nil = loop where
loop l = caseListT l nil $ \ a l' -> cons a $ loop l'
concatListT :: Monad m => ListT m (ListT m a) -> ListT m a
concatListT = ListT . foldListT append (return Nothing)
where append l = runListT . mappend l . ListT
runMListT :: Monad m => m (ListT m a) -> ListT m a
runMListT ml = ListT $ runListT =<< ml
consMListT :: Monad m => m a -> ListT m a -> ListT m a
consMListT ma l = ListT $ (Just . (,l)) `liftM` ma
sgMListT :: Monad m => m a -> ListT m a
sgMListT ma = consMListT ma nilListT
mapMListT :: Monad m => (a -> m b) -> ListT m a -> ListT m b
mapMListT f (ListT ml) = ListT $ do
caseMaybeM ml (return Nothing) $ \ (a, as) -> do
b <- f a
return $ Just (b , mapMListT f as)
mapMListT_alt :: Monad m => (a -> m b) -> ListT m a -> ListT m b
mapMListT_alt f = runMListT . foldListT cons (return nilListT)
where cons a ml = consMListT (f a) <$> ml
liftListT :: (Monad m, Monad m') => (forall a. m a -> m' a) -> ListT m a -> ListT m' a
liftListT lift xs = runMListT $ caseMaybeM (lift $ runListT xs) (return nilListT) $
\(x,xs) -> return $ consListT x $ liftListT lift xs
instance Monad m => Semigroup (ListT m a) where
l1 <> l2 = ListT $ foldListT cons (runListT l2) l1
where cons a = runListT . consListT a . ListT
instance Monad m => Monoid (ListT m a) where
mempty = nilListT
mappend = (<>)
instance (Functor m, Applicative m, Monad m) => Alternative (ListT m) where
empty = mempty
(<|>) = mappend
instance (Functor m, Applicative m, Monad m) => MonadPlus (ListT m) where
mzero = mempty
mplus = mappend
instance (Functor m, Applicative m, Monad m) => Applicative (ListT m) where
pure = sgListT
(<*>) = ap
instance (Functor m, Applicative m, Monad m) => Monad (ListT m) where
return = pure
l >>= k = concatListT $ k <$> l
instance MonadTrans ListT where
lift = sgMListT
instance (Applicative m, MonadIO m) => MonadIO (ListT m) where
liftIO = lift . liftIO
instance (Applicative m, MonadReader r m) => MonadReader r (ListT m) where
ask = lift ask
local f = ListT . local f . runListT
instance (Applicative m, MonadState s m) => MonadState s (ListT m) where
get = lift get
put = lift . put