Agda-2.6.1.1: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Utils.ListT

Description

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.

Synopsis

Documentation

newtype ListT m a Source #

Lazy monadic computation of a list of results.

Constructors

ListT 

Fields

Instances

Instances details
MonadTrans ListT Source # 
Instance details

Defined in Agda.Utils.ListT

Methods

lift :: Monad m => m a -> ListT m a #

(Applicative m, MonadState s m) => MonadState s (ListT m) Source # 
Instance details

Defined in Agda.Utils.ListT

Methods

get :: ListT m s #

put :: s -> ListT m () #

state :: (s -> (a, s)) -> ListT m a #

(Applicative m, MonadReader r m) => MonadReader r (ListT m) Source # 
Instance details

Defined in Agda.Utils.ListT

Methods

ask :: ListT m r #

local :: (r -> r) -> ListT m a -> ListT m a #

reader :: (r -> a) -> ListT m a #

(Functor m, Applicative m, Monad m) => Monad (ListT m) Source # 
Instance details

Defined in Agda.Utils.ListT

Methods

(>>=) :: ListT m a -> (a -> ListT m b) -> ListT m b #

(>>) :: ListT m a -> ListT m b -> ListT m b #

return :: a -> ListT m a #

Functor m => Functor (ListT m) Source # 
Instance details

Defined in Agda.Utils.ListT

Methods

fmap :: (a -> b) -> ListT m a -> ListT m b #

(<$) :: a -> ListT m b -> ListT m a #

Monad m => MonadFail (ListT m) Source # 
Instance details

Defined in Agda.Utils.ListT

Methods

fail :: String -> ListT m a #

(Functor m, Applicative m, Monad m) => Applicative (ListT m) Source # 
Instance details

Defined in Agda.Utils.ListT

Methods

pure :: a -> ListT m a #

(<*>) :: ListT m (a -> b) -> ListT m a -> ListT m b #

liftA2 :: (a -> b -> c) -> ListT m a -> ListT m b -> ListT m c #

(*>) :: ListT m a -> ListT m b -> ListT m b #

(<*) :: ListT m a -> ListT m b -> ListT m a #

(Applicative m, MonadIO m) => MonadIO (ListT m) Source # 
Instance details

Defined in Agda.Utils.ListT

Methods

liftIO :: IO a -> ListT m a #

(Functor m, Applicative m, Monad m) => Alternative (ListT m) Source # 
Instance details

Defined in Agda.Utils.ListT

Methods

empty :: ListT m a #

(<|>) :: ListT m a -> ListT m a -> ListT m a #

some :: ListT m a -> ListT m [a] #

many :: ListT m a -> ListT m [a] #

(Functor m, Applicative m, Monad m) => MonadPlus (ListT m) Source # 
Instance details

Defined in Agda.Utils.ListT

Methods

mzero :: ListT m a #

mplus :: ListT m a -> ListT m a -> ListT m a #

MonadTCM tcm => MonadTCM (ListT tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ListT tcm a Source #

MonadTCState m => MonadTCState (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadTCEnv m => MonadTCEnv (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: ListT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> ListT m a -> ListT m a Source #

MonadReduce m => MonadReduce (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ListT m a Source #

HasOptions m => HasOptions (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

ReadTCState m => ReadTCState (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: ListT m TCState Source #

locallyTCState :: Lens' a TCState -> (a -> a) -> ListT m b -> ListT m b Source #

withTCState :: (TCState -> TCState) -> ListT m a -> ListT m a Source #

MonadAddContext m => MonadAddContext (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> ListT m a -> ListT m a Source #

addLetBinding' :: Name -> Term -> Dom Type -> ListT m a -> ListT m a Source #

updateContext :: Substitution -> (Context -> Context) -> ListT m a -> ListT m a Source #

withFreshName :: Range -> ArgName -> (Name -> ListT m a) -> ListT m a Source #

HasBuiltins m => HasBuiltins (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

MonadDebug m => MonadDebug (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

HasConstInfo m => HasConstInfo (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Signature

Monad m => Semigroup (ListT m a) Source # 
Instance details

Defined in Agda.Utils.ListT

Methods

(<>) :: ListT m a -> ListT m a -> ListT m a #

sconcat :: NonEmpty (ListT m a) -> ListT m a #

stimes :: Integral b => b -> ListT m a -> ListT m a #

Monad m => Monoid (ListT m a) Source # 
Instance details

Defined in Agda.Utils.ListT

Methods

mempty :: ListT m a #

mappend :: ListT m a -> ListT m a -> ListT m a #

mconcat :: [ListT m a] -> ListT m a #

mapListT :: (m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))) -> ListT m a -> ListT n b Source #

Boilerplate function to lift MonadReader through the ListT transformer.

List operations

nilListT :: Monad m => ListT m a Source #

The empty lazy list.

consListT :: Monad m => a -> ListT m a -> ListT m a Source #

Consing a value to a lazy list.

sgListT :: Monad m => a -> ListT m a Source #

Singleton lazy list.

caseListT :: Monad m => ListT m a -> m b -> (a -> ListT m a -> m b) -> m b Source #

Case distinction over lazy list.

foldListT :: Monad m => (a -> m b -> m b) -> m b -> ListT m a -> m b Source #

Folding a lazy list, effects left-to-right.

sequenceListT :: Monad m => ListT m a -> m [a] Source #

Force all values in the lazy list, effects left-to-right

concatListT :: Monad m => ListT m (ListT m a) -> ListT m a Source #

The join operation of the ListT m monad.

Monadic list operations.

runMListT :: Monad m => m (ListT m a) -> ListT m a Source #

We can `run' a computation of a ListT as it is monadic itself.

consMListT :: Monad m => m a -> ListT m a -> ListT m a Source #

Monadic cons.

sgMListT :: Monad m => m a -> ListT m a Source #

Monadic singleton.

mapMListT :: Monad m => (a -> m b) -> ListT m a -> ListT m b Source #

Extending a monadic function to ListT.

mapMListT_alt :: Monad m => (a -> m b) -> ListT m a -> ListT m b Source #

Alternative implementation using foldListT.

liftListT :: (Monad m, Monad m') => (forall a. m a -> m' a) -> ListT m a -> ListT m' a Source #

Change from one monad to another