{-# LANGUAGE UndecidableInstances  #-}  -- Due to limitations of funct.dep.
{-# LANGUAGE CPP  #-}

-- | @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

#if __GLASGOW_HASKELL__ < 804
import Data.Semigroup
#endif

import Agda.Utils.Maybe

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

-- * List operations

-- | The empty lazy list.
nilListT :: Monad m => ListT m a
nilListT :: 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 (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 :: 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 (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 :: 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 :: 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 :: (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'

-- | Force all values in the lazy list, effects left-to-right
sequenceListT :: Monad m => ListT m a -> m [a]
sequenceListT :: 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 (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 :: 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 -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a))
forall (m :: * -> *) a.
Monad m =>
ListT m a -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a))
append (Maybe (a, ListT m a) -> m (Maybe (a, ListT m a))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, ListT m a)
forall a. Maybe a
Nothing)
  where append :: ListT m a -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a))
append ListT m a
l = 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 (Maybe (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 ListT m a
l (ListT m a -> ListT m a)
-> (m (Maybe (a, ListT m a)) -> ListT m a)
-> m (Maybe (a, ListT m a))
-> ListT m a
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

-- * 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 :: 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 :: 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 (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` 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 :: 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 :: (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 (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
b  <- a -> m b
f a
a
    Maybe (b, ListT m b) -> m (Maybe (b, ListT m b))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (b, ListT m b) -> m (Maybe (b, ListT m b)))
-> Maybe (b, ListT m b) -> m (Maybe (b, ListT m b))
forall a b. (a -> b) -> a -> b
$ (b, ListT m b) -> Maybe (b, ListT m b)
forall a. a -> Maybe a
Just (b
b , (a -> m b) -> ListT m a -> ListT m b
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ListT m a -> ListT m b
mapMListT a -> m b
f ListT m a
as)

-- | Alternative implementation using 'foldListT'.
mapMListT_alt :: Monad m => (a -> m b) -> ListT m a -> ListT m b
mapMListT_alt :: (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)
forall (f :: * -> *).
Functor f =>
a -> f (ListT m b) -> f (ListT m b)
cons (ListT m b -> m (ListT m b)
forall (m :: * -> *) a. Monad m => a -> m a
return ListT m b
forall (m :: * -> *) a. Monad m => ListT m a
nilListT)
  where cons :: a -> f (ListT m b) -> f (ListT m b)
cons a
a f (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) -> f (ListT m b) -> f (ListT m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (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 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 (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 (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 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 a -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a))
forall (m :: * -> *) a.
Monad m =>
a -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a))
cons (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
    where cons :: a -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a))
cons a
a = 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 (Maybe (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
. 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 -> ListT m a)
-> (m (Maybe (a, ListT m a)) -> ListT m a)
-> m (Maybe (a, ListT m a))
-> ListT m a
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
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
  mappend :: ListT m a -> ListT m a -> ListT m a
mappend = ListT m a -> ListT m a -> ListT m a
forall a. Semigroup a => a -> a -> a
(<>)

instance (Functor m, Applicative m, Monad m) => Alternative (ListT m) where
  empty :: ListT m a
empty = ListT m a
forall a. Monoid a => a
mempty
  <|> :: 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 :: ListT m a
mzero = ListT m a
forall a. Monoid a => a
mempty
  mplus :: 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 :: a -> ListT m a
pure  = a -> ListT m a
forall (m :: * -> *) a. Monad m => a -> ListT m a
sgListT
  <*> :: 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 :: a -> ListT m a
return  = a -> ListT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  ListT m a
l >>= :: 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 :: 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 :: IO a -> ListT m a
liftIO = 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 (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 (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 :: (r -> r) -> ListT m a -> ListT m a
local r -> r
f = 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 a -> m (Maybe (a, ListT m a)))
-> 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 r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local r -> r
f (m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a)))
-> (ListT m a -> m (Maybe (a, ListT m a)))
-> ListT m a
-> m (Maybe (a, ListT m a))
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

instance (Applicative m, MonadState s m) => MonadState s (ListT m) where
  get :: ListT m s
get = m s -> ListT m s
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 (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 :: String -> ListT m a
fail String
_ = ListT m a
forall (f :: * -> *) a. Alternative f => f a
empty