Agda-2.6.4.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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 :: Type -> Type) 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 #

MonadFresh i m => MonadFresh i (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fresh :: ListT m i Source #

(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 #

(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 #

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

Defined in Agda.Interaction.Options.HasOptions

Methods

pragmaOptions :: ListT m PragmaOptions Source #

commandLineOptions :: ListT m CommandLineOptions Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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 #

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

Methods

getTC :: ListT m TCState Source #

putTC :: TCState -> ListT m () Source #

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: ListT m TCState Source #

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

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

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

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> ListT m (Maybe (Builtin PrimFun)) 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' :: Origin -> 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 #

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

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

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

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

getVerbosity :: ListT m Verbosity Source #

getProfileOptions :: ListT m ProfileOptions Source #

isDebugPrinting :: ListT m Bool Source #

nowDebugPrinting :: ListT m a -> ListT m a Source #

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

Defined in Agda.TypeChecking.Monad.Pure

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

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> ListT m Definition Source #

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

getRewriteRulesFor :: QName -> ListT m RewriteRules Source #

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

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (ListT m) 
Instance details

Defined in Agda.Utils.Benchmark

type BenchPhase (ListT m) = BenchPhase m

Methods

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

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

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

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

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

Defined in Agda.Utils.ListT

Methods

fail :: String -> 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) => 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 #

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 #

(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, 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 #

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 #

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 #

type BenchPhase (ListT m) Source # 
Instance details

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 Source #

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)) Source #

Inverse to mapListT.

List operations

nilListT :: forall (m :: Type -> Type) a. Monad m => ListT m a Source #

The empty lazy list.

consListT :: forall (m :: Type -> Type) a. Monad m => a -> ListT m a -> ListT m a Source #

Consing a value to a lazy list.

sgListT :: forall (m :: Type -> Type) a. 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.

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

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

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

Lazy monadic conjunction of lazy monadic 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 :: forall (m :: Type -> Type) a. 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 a1. m a1 -> m' a1) -> ListT m a -> ListT m' a Source #

Change from one monad to another