module Agda.Utils.ListT where
import Control.Applicative
import Control.Arrow
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans
import Data.Functor
import Data.Monoid
import Agda.Utils.Maybe
import Agda.Utils.Monad
newtype ListT m a = ListT { runListT :: m (Maybe (a, ListT m a)) }
deriving (Functor)
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
#if __GLASGOW_HASKELL__ <= 708
, Functor m
#endif
) => (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
#if __GLASGOW_HASKELL__ <= 708
, Functor m
#endif
) => (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
instance Monad m => Monoid (ListT m a) where
mempty = nilListT
mappend l1 l2 = ListT $ foldListT cons (runListT l2) l1
where cons a = runListT . consListT a . ListT
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 = return
(<*>) = ap
instance (Functor m, Applicative m, Monad m) => Monad (ListT m) where
return = sgListT
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