{-# LANGUAGE CPP  #-}
{-# 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(..) )

#if !(MIN_VERSION_base(4,11,0))
import Data.Semigroup (Semigroup(..))
#endif

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 -> 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
<$ :: forall a b. a -> ListT m b -> ListT m a
$c<$ :: forall (m :: * -> *) a b. Functor m => a -> ListT m b -> ListT m a
fmap :: forall a b. (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 :: 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 = forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
runListT forall b c a. (b -> c) -> (a -> b) -> a -> c
. ListT m a -> ListT n b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a. Monad m => a -> ListT m a -> ListT m a
consListT a
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 = forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
runListT ListT m a
l) m b
nil forall a b. (a -> b) -> a -> 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 = 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 forall a b. (a -> b) -> a -> b
$ \ a
a ListT m a
l' -> a -> m b -> m b
cons a
a 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 = forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT (forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
or2M forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m Bool
f) (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 = forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT (forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
and2M forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m Bool
f) (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 = forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
(<$>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:)) forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT (forall (m :: * -> *) a (n :: * -> *) b.
(ListT m a -> ListT n b)
-> m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
unmapListT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Monoid a => a -> a -> a
mappend) (forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
runListT 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 = forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT forall a b. (a -> b) -> a -> b
$ (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,ListT m a
l)) 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 = forall (m :: * -> *) a. Monad m => m a -> ListT m a -> ListT m a
consMListT m a
ma 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) = forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM m (Maybe (a, ListT m a))
ml (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ \ (a
a, ListT m a
as) -> do
    b
b  <- a -> m b
f a
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (b
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 :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ListT m a -> ListT m b
mapMListT_alt a -> m b
f = forall (m :: * -> *) a. Monad m => m (ListT m a) -> ListT m a
runMListT forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (m :: * -> *) a. Monad m => m a -> ListT m a -> ListT m a
consMListT (a -> m b
f a
a) 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 = forall (m :: * -> *) a. Monad m => m (ListT m a) -> ListT m a
runMListT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall a. m a -> m' a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
runListT ListT m a
xs) (forall (m :: * -> *) a. Monad m => a -> m a
return forall (m :: * -> *) a. Monad m => ListT m a
nilListT) forall a b. (a -> b) -> a -> b
$
    \(a
x,ListT m a
xs) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> ListT m a -> ListT m a
consListT a
x forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT (forall (m :: * -> *) a (n :: * -> *) b.
(ListT m a -> ListT n b)
-> m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
unmapListT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> ListT m a -> ListT m a
consListT) (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        = forall (m :: * -> *) a. Monad m => ListT m a
nilListT
#if !(MIN_VERSION_base(4,11,0))
  mappend = (<>)
#endif

instance (Functor m, Applicative m, Monad m) => Alternative (ListT m) where
  empty :: forall a. ListT m a
empty = forall a. Monoid a => a
mempty
  <|> :: forall 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 = forall a. Monoid a => a
mempty
  mplus :: forall a. ListT m a -> ListT m a -> ListT m a
mplus = 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  = forall (m :: * -> *) a. Monad m => a -> ListT m a
sgListT
  <*> :: forall a 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  = 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 = forall (m :: * -> *) a. Monad m => ListT m (ListT m a) -> ListT m a
concatListT forall a b. (a -> b) -> a -> b
$ a -> ListT m b
k 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 = 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 = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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     = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall r (m :: * -> *). MonadReader r m => m r
ask
  local :: forall a. (r -> r) -> ListT m a -> ListT m a
local   = forall (m :: * -> *) a (n :: * -> *) b.
(m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b)))
-> ListT m a -> ListT n b
mapListT forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall s (m :: * -> *). MonadState s m => m s
get
  put :: s -> ListT m ()
put = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
_ = forall (f :: * -> *) a. Alternative f => f a
empty