Agda.Utils.ListT

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.

Documentation

newtype ListT m a

Lazy monadic computation of a list of results.

Constructors

ListT

Fields

• runListT :: m (Maybe (a, ListT m a))

Instances

MonadTrans ListT

Defined in Agda.Utils.ListT

Methods

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

MonadFresh i m => MonadFresh i (ListT m)

Defined in Agda.TypeChecking.Monad.Base

Methods

fresh :: ListT m i

(Applicative m, MonadReader r m) => MonadReader r (ListT m)

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

(Applicative m, MonadState s m) => MonadState s (ListT m)

Defined in Agda.Utils.ListT

Methods

get :: ListT m s

put :: s -> ListT m ()

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

HasOptions m => HasOptions (ListT m)

Defined in Agda.Interaction.Options.HasOptions

Methods

pragmaOptions :: ListT m PragmaOptions

commandLineOptions :: ListT m CommandLineOptions

MonadReduce m => MonadReduce (ListT m)

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ListT m a

MonadTCEnv m => MonadTCEnv (ListT m)

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: ListT m TCEnv

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

MonadTCM tcm => MonadTCM (ListT tcm)

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ListT tcm a

MonadTCState m => MonadTCState (ListT m)

Defined in Agda.TypeChecking.Monad.Base

Methods

getTC :: ListT m TCState

putTC :: TCState -> ListT m ()

modifyTC :: (TCState -> TCState) -> ListT m ()

ReadTCState m => ReadTCState (ListT m)

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: ListT m TCState

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

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

HasBuiltins m => HasBuiltins (ListT m)

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> ListT m (Maybe (Builtin PrimFun))

MonadAddContext m => MonadAddContext (ListT m)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

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

MonadDebug m => MonadDebug (ListT m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ListT m String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> ListT m a -> ListT m a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> ListT m a -> ListT m a

getVerbosity :: ListT m Verbosity

getProfileOptions :: ListT m ProfileOptions

isDebugPrinting :: ListT m Bool

nowDebugPrinting :: ListT m a -> ListT m a

PureTCM m => PureTCM (ListT m)

Defined in Agda.TypeChecking.Monad.Pure

HasConstInfo m => HasConstInfo (ListT m)

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> ListT m Definition

getConstInfo' :: QName -> ListT m (Either SigError Definition)

getRewriteRulesFor :: QName -> ListT m RewriteRules

MonadBench m => MonadBench (ListT m)

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (ListT m)

Methods

getBenchmark :: ListT m (Benchmark (BenchPhase (ListT m)))

putBenchmark :: Benchmark (BenchPhase (ListT m)) -> ListT m ()

modifyBenchmark :: (Benchmark (BenchPhase (ListT m)) -> Benchmark (BenchPhase (ListT m))) -> ListT m ()

finally :: ListT m b -> ListT m c -> ListT m b

Monad m => MonadFail (ListT m)

Defined in Agda.Utils.ListT

Methods

fail :: String -> ListT m a

(Applicative m, MonadIO m) => MonadIO (ListT m)

Defined in Agda.Utils.ListT

Methods

liftIO :: IO a -> ListT m a

(Functor m, Applicative m, Monad m) => Alternative (ListT m)

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) => Applicative (ListT m)

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

Functor m => Functor (ListT m)

Defined in Agda.Utils.ListT

Methods

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

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

(Functor m, Applicative m, Monad m) => Monad (ListT m)

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, Applicative m, Monad m) => MonadPlus (ListT m)

Defined in Agda.Utils.ListT

Methods

mzero :: ListT m a

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

Monad m => Monoid (ListT m a)

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

Monad m => Semigroup (ListT m a)

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

type BenchPhase (ListT m)

Defined in Agda.Utils.Benchmark

type BenchPhase (ListT m) = BenchPhase m

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

Boilerplate function to lift MonadReader through the ListT transformer.

unmapListT :: (ListT m a -> ListT n b) -> m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))

Inverse to mapListT.

List operations

nilListT :: Monad m => ListT m a

The empty lazy list.

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

Consing a value to a lazy list.

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

Singleton lazy list.

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

Case distinction over lazy list.

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

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

anyListT :: Monad m => ListT m a -> (a -> m Bool) -> m Bool

Lazy monadic disjunction of lazy monadic list, effects left-to-right

allListT :: Monad m => ListT m a -> (a -> m Bool) -> m Bool

Lazy monadic conjunction of lazy monadic list, effects left-to-right

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

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

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

The join operation of the ListT m monad.

Monadic list operations.

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

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

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

Monadic cons.

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

Monadic singleton.

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

Extending a monadic function to ListT.

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

Alternative implementation using foldListT.

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

Change from one monad to another