{-# LANGUAGE UndecidableInstances  #-} -- Due MonadReader/MonadState fundep

-- | @ListT@ done right,
--   see https://www.haskell.org/haskellwiki/ListT_done_right_alternative
--
--   There is also the @list-t@ package on hackage (Nikita Volkov)
--   but it again depends on other packages we do not use yet,
--   so we rather implement the few bits we need afresh.

module Agda.Utils.ListT where

import Control.Applicative ( Alternative((<|>), empty) )
import Control.Monad
import Control.Monad.Fail as Fail
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.IO.Class ( MonadIO(..) )

import Agda.Utils.Maybe
import Agda.Utils.Monad

-- | Lazy monadic computation of a list of results.
newtype ListT m a = ListT { forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
runListT :: m (Maybe (a, ListT m a)) }
  deriving ((forall a b. (a -> b) -> ListT m a -> ListT m b)
-> (forall a b. a -> ListT m b -> ListT m a) -> Functor (ListT m)
forall a b. a -> ListT m b -> ListT m a
forall a b. (a -> b) -> ListT m a -> ListT m b
forall (m :: * -> *) a b. Functor m => a -> ListT m b -> ListT m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> ListT m a -> ListT m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> ListT m a -> ListT m b
fmap :: forall a b. (a -> b) -> ListT m a -> ListT m b
$c<$ :: forall (m :: * -> *) a b. Functor m => a -> ListT m b -> ListT m a
<$ :: forall a b. a -> ListT m b -> ListT m a
Functor)

-- | Boilerplate function to lift 'MonadReader' through the 'ListT' transformer.
mapListT :: (m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))) -> ListT m a -> ListT n b
mapListT :: forall (m :: * -> *) a (n :: * -> *) b.
(m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b)))
-> ListT m a -> ListT n b
mapListT m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
f = n (Maybe (b, ListT n b)) -> ListT n b
forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT (n (Maybe (b, ListT n b)) -> ListT n b)
-> (ListT m a -> n (Maybe (b, ListT n b)))
-> ListT m a
-> ListT n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
f (m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b)))
-> (ListT m a -> m (Maybe (a, ListT m a)))
-> ListT m a
-> n (Maybe (b, ListT n b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ListT m a -> m (Maybe (a, ListT m a))
forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
runListT

-- | Inverse to 'mapListT'.
unmapListT :: (ListT m a -> ListT n b) -> m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
unmapListT :: forall (m :: * -> *) a (n :: * -> *) b.
(ListT m a -> ListT n b)
-> m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
unmapListT ListT m a -> ListT n b
f = ListT n b -> n (Maybe (b, ListT n b))
forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
runListT (ListT n b -> n (Maybe (b, ListT n b)))
-> (m (Maybe (a, ListT m a)) -> ListT n b)
-> m (Maybe (a, ListT m a))
-> n (Maybe (b, ListT n b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ListT m a -> ListT n b
f (ListT m a -> ListT n b)
-> (m (Maybe (a, ListT m a)) -> ListT m a)
-> m (Maybe (a, ListT m a))
-> ListT n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (a, ListT m a)) -> ListT m a
forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT

-- * List operations

-- | The empty lazy list.
nilListT :: Monad m => ListT m a
nilListT :: forall (m :: * -> *) a. Monad m => ListT m a
nilListT = m (Maybe (a, ListT m a)) -> ListT m a
forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT (m (Maybe (a, ListT m a)) -> ListT m a)
-> m (Maybe (a, ListT m a)) -> ListT m a
forall a b. (a -> b) -> a -> b
$ Maybe (a, ListT m a) -> m (Maybe (a, ListT m a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, ListT m a)
forall a. Maybe a
Nothing

-- | Consing a value to a lazy list.
consListT :: Monad m => a -> ListT m a -> ListT m a
consListT :: forall (m :: * -> *) a. Monad m => a -> ListT m a -> ListT m a
consListT a
a ListT m a
l = m (Maybe (a, ListT m a)) -> ListT m a
forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT (m (Maybe (a, ListT m a)) -> ListT m a)
-> m (Maybe (a, ListT m a)) -> ListT m a
forall a b. (a -> b) -> a -> b
$ Maybe (a, ListT m a) -> m (Maybe (a, ListT m a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (a, ListT m a) -> m (Maybe (a, ListT m a)))
-> Maybe (a, ListT m a) -> m (Maybe (a, ListT m a))
forall a b. (a -> b) -> a -> b
$ (a, ListT m a) -> Maybe (a, ListT m a)
forall a. a -> Maybe a
Just (a
a, ListT m a
l)

-- | Singleton lazy list.
sgListT ::  Monad m => a -> ListT m a
sgListT :: forall (m :: * -> *) a. Monad m => a -> ListT m a
sgListT a
a = a -> ListT m a -> ListT m a
forall (m :: * -> *) a. Monad m => a -> ListT m a -> ListT m a
consListT a
a ListT m a
forall (m :: * -> *) a. Monad m => ListT m a
nilListT

-- | Case distinction over lazy list.
caseListT :: Monad m => ListT m a -> m b -> (a -> ListT m a -> m b) -> m b
caseListT :: forall (m :: * -> *) a b.
Monad m =>
ListT m a -> m b -> (a -> ListT m a -> m b) -> m b
caseListT ListT m a
l m b
nil a -> ListT m a -> m b
cons = m (Maybe (a, ListT m a)) -> m b -> ((a, ListT m a) -> m b) -> m b
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (ListT m a -> m (Maybe (a, ListT m a))
forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
runListT ListT m a
l) m b
nil (((a, ListT m a) -> m b) -> m b) -> ((a, ListT m a) -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ (a -> ListT m a -> m b) -> (a, ListT m a) -> m b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> ListT m a -> m b
cons

-- | Folding a lazy list, effects left-to-right.
foldListT :: Monad m => (a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT a -> m b -> m b
cons m b
nil = ListT m a -> m b
loop where
  loop :: ListT m a -> m b
loop ListT m a
l = ListT m a -> m b -> (a -> ListT m a -> m b) -> m b
forall (m :: * -> *) a b.
Monad m =>
ListT m a -> m b -> (a -> ListT m a -> m b) -> m b
caseListT ListT m a
l m b
nil ((a -> ListT m a -> m b) -> m b) -> (a -> ListT m a -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \ a
a ListT m a
l' -> a -> m b -> m b
cons a
a (m b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$ ListT m a -> m b
loop ListT m a
l'

-- | Lazy monadic disjunction of lazy monadic list, effects left-to-right
anyListT :: Monad m => ListT m a -> (a -> m Bool) -> m Bool
anyListT :: forall (m :: * -> *) a.
Monad m =>
ListT m a -> (a -> m Bool) -> m Bool
anyListT ListT m a
xs a -> m Bool
f = (a -> m Bool -> m Bool) -> m Bool -> ListT m a -> m Bool
forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT (m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
or2M (m Bool -> m Bool -> m Bool)
-> (a -> m Bool) -> a -> m Bool -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m Bool
f) (Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) ListT m a
xs

-- | Lazy monadic conjunction of lazy monadic list, effects left-to-right
allListT :: Monad m => ListT m a -> (a -> m Bool) -> m Bool
allListT :: forall (m :: * -> *) a.
Monad m =>
ListT m a -> (a -> m Bool) -> m Bool
allListT ListT m a
xs a -> m Bool
f = (a -> m Bool -> m Bool) -> m Bool -> ListT m a -> m Bool
forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT (m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
and2M (m Bool -> m Bool -> m Bool)
-> (a -> m Bool) -> a -> m Bool -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m Bool
f) (Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True) ListT m a
xs

-- | Force all values in the lazy list, effects left-to-right
sequenceListT :: Monad m => ListT m a -> m [a]
sequenceListT :: forall (m :: * -> *) a. Monad m => ListT m a -> m [a]
sequenceListT = (a -> m [a] -> m [a]) -> m [a] -> ListT m a -> m [a]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT (([a] -> [a]) -> m [a] -> m [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
(<$>) (([a] -> [a]) -> m [a] -> m [a])
-> (a -> [a] -> [a]) -> a -> m [a] -> m [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:)) (m [a] -> ListT m a -> m [a]) -> m [a] -> ListT m a -> m [a]
forall a b. (a -> b) -> a -> b
$ [a] -> m [a]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

-- | The join operation of the @ListT m@ monad.
concatListT :: Monad m => ListT m (ListT m a) -> ListT m a
concatListT :: forall (m :: * -> *) a. Monad m => ListT m (ListT m a) -> ListT m a
concatListT = m (Maybe (a, ListT m a)) -> ListT m a
forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT (m (Maybe (a, ListT m a)) -> ListT m a)
-> (ListT m (ListT m a) -> m (Maybe (a, ListT m a)))
-> ListT m (ListT m a)
-> ListT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ListT m a -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a)))
-> m (Maybe (a, ListT m a))
-> ListT m (ListT m a)
-> m (Maybe (a, ListT m a))
forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT ((ListT m a -> ListT m a)
-> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a))
forall (m :: * -> *) a (n :: * -> *) b.
(ListT m a -> ListT n b)
-> m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
unmapListT ((ListT m a -> ListT m a)
 -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a)))
-> (ListT m a -> ListT m a -> ListT m a)
-> ListT m a
-> m (Maybe (a, ListT m a))
-> m (Maybe (a, ListT m a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ListT m a -> ListT m a -> ListT m a
forall a. Monoid a => a -> a -> a
mappend) (Maybe (a, ListT m a) -> m (Maybe (a, ListT m a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, ListT m a)
forall a. Maybe a
Nothing)

-- * Monadic list operations.

-- | We can ``run'' a computation of a 'ListT' as it is monadic itself.
runMListT :: Monad m => m (ListT m a) -> ListT m a
runMListT :: forall (m :: * -> *) a. Monad m => m (ListT m a) -> ListT m a
runMListT m (ListT m a)
ml = m (Maybe (a, ListT m a)) -> ListT m a
forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT (m (Maybe (a, ListT m a)) -> ListT m a)
-> m (Maybe (a, ListT m a)) -> ListT m a
forall a b. (a -> b) -> a -> b
$ ListT m a -> m (Maybe (a, ListT m a))
forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
runListT (ListT m a -> m (Maybe (a, ListT m a)))
-> m (ListT m a) -> m (Maybe (a, ListT m a))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m (ListT m a)
ml

-- | Monadic cons.
consMListT :: Monad m => m a -> ListT m a -> ListT m a
consMListT :: forall (m :: * -> *) a. Monad m => m a -> ListT m a -> ListT m a
consMListT m a
ma ListT m a
l = m (Maybe (a, ListT m a)) -> ListT m a
forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT (m (Maybe (a, ListT m a)) -> ListT m a)
-> m (Maybe (a, ListT m a)) -> ListT m a
forall a b. (a -> b) -> a -> b
$ ((a, ListT m a) -> Maybe (a, ListT m a)
forall a. a -> Maybe a
Just ((a, ListT m a) -> Maybe (a, ListT m a))
-> (a -> (a, ListT m a)) -> a -> Maybe (a, ListT m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,ListT m a
l)) (a -> Maybe (a, ListT m a)) -> m a -> m (Maybe (a, ListT m a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
ma
-- consMListT ma l = runMListT $ liftM (`consListT` l) ma

-- simplification:
-- consMListT ma l = ListT $ runListT =<< liftM (`consListT` l) ma
-- consMListT ma l = ListT $ runListT =<< (`consListT` l) <$> ma
-- consMListT ma l = ListT $ runListT =<< do a <- ma; return $ a `consListT` l
-- consMListT ma l = ListT $ do a <- ma; runListT =<< do return $ a `consListT` l
-- consMListT ma l = ListT $ do a <- ma; runListT $ a `consListT` l
-- consMListT ma l = ListT $ do a <- ma; runListT $ ListT $ return $ Just (a, l)
-- consMListT ma l = ListT $ do a <- ma; return $ Just (a, l)
-- consMListT ma l = ListT $ Just . (,l) <$> ma

-- | Monadic singleton.
sgMListT ::  Monad m => m a -> ListT m a
sgMListT :: forall (m :: * -> *) a. Monad m => m a -> ListT m a
sgMListT m a
ma = m a -> ListT m a -> ListT m a
forall (m :: * -> *) a. Monad m => m a -> ListT m a -> ListT m a
consMListT m a
ma ListT m a
forall (m :: * -> *) a. Monad m => ListT m a
nilListT

-- | Extending a monadic function to 'ListT'.
mapMListT :: Monad m => (a -> m b) -> ListT m a -> ListT m b
mapMListT :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ListT m a -> ListT m b
mapMListT a -> m b
f (ListT m (Maybe (a, ListT m a))
ml) = m (Maybe (b, ListT m b)) -> ListT m b
forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT (m (Maybe (b, ListT m b)) -> ListT m b)
-> m (Maybe (b, ListT m b)) -> ListT m b
forall a b. (a -> b) -> a -> b
$ do
  m (Maybe (a, ListT m a))
-> m (Maybe (b, ListT m b))
-> ((a, ListT m a) -> m (Maybe (b, ListT m b)))
-> m (Maybe (b, ListT m b))
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM m (Maybe (a, ListT m a))
ml (Maybe (b, ListT m b) -> m (Maybe (b, ListT m b))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (b, ListT m b)
forall a. Maybe a
Nothing) (((a, ListT m a) -> m (Maybe (b, ListT m b)))
 -> m (Maybe (b, ListT m b)))
-> ((a, ListT m a) -> m (Maybe (b, ListT m b)))
-> m (Maybe (b, ListT m b))
forall a b. (a -> b) -> a -> b
$ \ (a
a, ListT m a
as) -> do
    b  <- a -> m b
f a
a
    return $ Just (b , mapMListT f as)

-- | Alternative implementation using 'foldListT'.
mapMListT_alt :: Monad m => (a -> m b) -> ListT m a -> ListT m b
mapMListT_alt :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ListT m a -> ListT m b
mapMListT_alt a -> m b
f = m (ListT m b) -> ListT m b
forall (m :: * -> *) a. Monad m => m (ListT m a) -> ListT m a
runMListT (m (ListT m b) -> ListT m b)
-> (ListT m a -> m (ListT m b)) -> ListT m a -> ListT m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m (ListT m b) -> m (ListT m b))
-> m (ListT m b) -> ListT m a -> m (ListT m b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT a -> m (ListT m b) -> m (ListT m b)
cons (ListT m b -> m (ListT m b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ListT m b
forall (m :: * -> *) a. Monad m => ListT m a
nilListT)
  where cons :: a -> m (ListT m b) -> m (ListT m b)
cons a
a m (ListT m b)
ml = m b -> ListT m b -> ListT m b
forall (m :: * -> *) a. Monad m => m a -> ListT m a -> ListT m a
consMListT (a -> m b
f a
a) (ListT m b -> ListT m b) -> m (ListT m b) -> m (ListT m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ListT m b)
ml

-- | Change from one monad to another
liftListT :: (Monad m, Monad m') => (forall a. m a -> m' a) -> ListT m a -> ListT m' a
liftListT :: forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a. m a -> m' a) -> ListT m a -> ListT m' a
liftListT forall a. m a -> m' a
lift ListT m a
xs = m' (ListT m' a) -> ListT m' a
forall (m :: * -> *) a. Monad m => m (ListT m a) -> ListT m a
runMListT (m' (ListT m' a) -> ListT m' a) -> m' (ListT m' a) -> ListT m' a
forall a b. (a -> b) -> a -> b
$ m' (Maybe (a, ListT m a))
-> m' (ListT m' a)
-> ((a, ListT m a) -> m' (ListT m' a))
-> m' (ListT m' a)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (m (Maybe (a, ListT m a)) -> m' (Maybe (a, ListT m a))
forall a. m a -> m' a
lift (m (Maybe (a, ListT m a)) -> m' (Maybe (a, ListT m a)))
-> m (Maybe (a, ListT m a)) -> m' (Maybe (a, ListT m a))
forall a b. (a -> b) -> a -> b
$ ListT m a -> m (Maybe (a, ListT m a))
forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
runListT ListT m a
xs) (ListT m' a -> m' (ListT m' a)
forall a. a -> m' a
forall (m :: * -> *) a. Monad m => a -> m a
return ListT m' a
forall (m :: * -> *) a. Monad m => ListT m a
nilListT) (((a, ListT m a) -> m' (ListT m' a)) -> m' (ListT m' a))
-> ((a, ListT m a) -> m' (ListT m' a)) -> m' (ListT m' a)
forall a b. (a -> b) -> a -> b
$
    \(a
x,ListT m a
xs) -> ListT m' a -> m' (ListT m' a)
forall a. a -> m' a
forall (m :: * -> *) a. Monad m => a -> m a
return (ListT m' a -> m' (ListT m' a)) -> ListT m' a -> m' (ListT m' a)
forall a b. (a -> b) -> a -> b
$ a -> ListT m' a -> ListT m' a
forall (m :: * -> *) a. Monad m => a -> ListT m a -> ListT m a
consListT a
x (ListT m' a -> ListT m' a) -> ListT m' a -> ListT m' a
forall a b. (a -> b) -> a -> b
$ (forall a. m a -> m' a) -> ListT m a -> ListT m' a
forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a. m a -> m' a) -> ListT m a -> ListT m' a
liftListT m a -> m' a
forall a. m a -> m' a
lift ListT m a
xs

-- Instances

instance Monad m => Semigroup (ListT m a) where
  ListT m a
l1 <> :: ListT m a -> ListT m a -> ListT m a
<> ListT m a
l2 = m (Maybe (a, ListT m a)) -> ListT m a
forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT (m (Maybe (a, ListT m a)) -> ListT m a)
-> m (Maybe (a, ListT m a)) -> ListT m a
forall a b. (a -> b) -> a -> b
$ (a -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a)))
-> m (Maybe (a, ListT m a))
-> ListT m a
-> m (Maybe (a, ListT m a))
forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT ((ListT m a -> ListT m a)
-> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a))
forall (m :: * -> *) a (n :: * -> *) b.
(ListT m a -> ListT n b)
-> m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
unmapListT ((ListT m a -> ListT m a)
 -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a)))
-> (a -> ListT m a -> ListT m a)
-> a
-> m (Maybe (a, ListT m a))
-> m (Maybe (a, ListT m a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ListT m a -> ListT m a
forall (m :: * -> *) a. Monad m => a -> ListT m a -> ListT m a
consListT) (ListT m a -> m (Maybe (a, ListT m a))
forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
runListT ListT m a
l2) ListT m a
l1

instance Monad m => Monoid (ListT m a) where
  mempty :: ListT m a
mempty = ListT m a
forall (m :: * -> *) a. Monad m => ListT m a
nilListT

instance (Functor m, Applicative m, Monad m) => Alternative (ListT m) where
  empty :: forall a. ListT m a
empty = ListT m a
forall a. Monoid a => a
mempty
  <|> :: forall a. ListT m a -> ListT m a -> ListT m a
(<|>) = ListT m a -> ListT m a -> ListT m a
forall a. Monoid a => a -> a -> a
mappend

instance (Functor m, Applicative m, Monad m) => MonadPlus (ListT m) where
  mzero :: forall a. ListT m a
mzero = ListT m a
forall a. Monoid a => a
mempty
  mplus :: forall a. ListT m a -> ListT m a -> ListT m a
mplus = ListT m a -> ListT m a -> ListT m a
forall a. Monoid a => a -> a -> a
mappend

instance (Functor m, Applicative m, Monad m) => Applicative (ListT m) where
  pure :: forall a. a -> ListT m a
pure  = a -> ListT m a
forall (m :: * -> *) a. Monad m => a -> ListT m a
sgListT
  <*> :: forall a b. ListT m (a -> b) -> ListT m a -> ListT m b
(<*>) = ListT m (a -> b) -> ListT m a -> ListT m b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

  -- Another Applicative, but not the canonical one.
  -- l1 <*> l2 = ListT $ loop <$> runListT l1 <*> runListT l2
  --   where
  --   loop (Just (f, l1')) (Just (a, l2')) = Just (f a, l1' <*> l2')
  --   loop _ _ = Nothing

instance (Functor m, Applicative m, Monad m) => Monad (ListT m) where
  return :: forall a. a -> ListT m a
return  = a -> ListT m a
forall a. a -> ListT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  ListT m a
l >>= :: forall a b. ListT m a -> (a -> ListT m b) -> ListT m b
>>= a -> ListT m b
k = ListT m (ListT m b) -> ListT m b
forall (m :: * -> *) a. Monad m => ListT m (ListT m a) -> ListT m a
concatListT (ListT m (ListT m b) -> ListT m b)
-> ListT m (ListT m b) -> ListT m b
forall a b. (a -> b) -> a -> b
$ a -> ListT m b
k (a -> ListT m b) -> ListT m a -> ListT m (ListT m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ListT m a
l

instance MonadTrans ListT where
  lift :: forall (m :: * -> *) a. Monad m => m a -> ListT m a
lift = m a -> ListT m a
forall (m :: * -> *) a. Monad m => m a -> ListT m a
sgMListT

instance (Applicative m, MonadIO m) => MonadIO (ListT m) where
  liftIO :: forall a. IO a -> ListT m a
liftIO = m a -> ListT m a
forall (m :: * -> *) a. Monad m => m a -> ListT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> ListT m a) -> (IO a -> m a) -> IO a -> ListT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> m a
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO

instance (Applicative m, MonadReader r m) => MonadReader r (ListT m) where
  ask :: ListT m r
ask     = m r -> ListT m r
forall (m :: * -> *) a. Monad m => m a -> ListT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m r
forall r (m :: * -> *). MonadReader r m => m r
ask
  local :: forall a. (r -> r) -> ListT m a -> ListT m a
local   = (m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a)))
-> ListT m a -> ListT m a
forall (m :: * -> *) a (n :: * -> *) b.
(m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b)))
-> ListT m a -> ListT n b
mapListT ((m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a)))
 -> ListT m a -> ListT m a)
-> ((r -> r)
    -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a)))
-> (r -> r)
-> ListT m a
-> ListT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (r -> r) -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a))
forall a. (r -> r) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local

instance (Applicative m, MonadState s m) => MonadState s (ListT m) where
  get :: ListT m s
get = m s -> ListT m s
forall (m :: * -> *) a. Monad m => m a -> ListT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m s
forall s (m :: * -> *). MonadState s m => m s
get
  put :: s -> ListT m ()
put = m () -> ListT m ()
forall (m :: * -> *) a. Monad m => m a -> ListT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ListT m ()) -> (s -> m ()) -> s -> ListT m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put

instance Monad m => MonadFail (ListT m) where
  fail :: forall a. String -> ListT m a
fail String
_ = ListT m a
forall a. ListT m a
forall (f :: * -> *) a. Alternative f => f a
empty