Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.ListT

Contents

- List operations
- Monadic list operations.

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

- newtype ListT (m :: Type -> Type) a = ListT {
  - runListT :: m (Maybe (a, ListT m a))
  }
- mapListT :: (m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))) -> ListT m a -> ListT n b
- unmapListT :: (ListT m a -> ListT n b) -> m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
- nilListT :: forall (m :: Type -> Type) a. Monad m => ListT m a
- consListT :: forall (m :: Type -> Type) a. Monad m => a -> ListT m a -> ListT m a
- sgListT :: forall (m :: Type -> Type) a. Monad m => a -> ListT m a
- caseListT :: Monad m => ListT m a -> m b -> (a -> ListT m a -> m b) -> m b
- foldListT :: Monad m => (a -> m b -> m b) -> m b -> ListT m a -> m b
- anyListT :: Monad m => ListT m a -> (a -> m Bool) -> m Bool
- allListT :: Monad m => ListT m a -> (a -> m Bool) -> m Bool
- sequenceListT :: Monad m => ListT m a -> m [a]
- concatListT :: forall (m :: Type -> Type) a. Monad m => ListT m (ListT m a) -> ListT m a
- runMListT :: Monad m => m (ListT m a) -> ListT m a
- consMListT :: Monad m => m a -> ListT m a -> ListT m a
- sgMListT :: Monad m => m a -> ListT m a
- mapMListT :: Monad m => (a -> m b) -> ListT m a -> ListT m b
- mapMListT_alt :: Monad m => (a -> m b) -> ListT m a -> ListT m b
- liftListT :: (Monad m, Monad m') => (forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a

# Documentation

newtype ListT (m :: Type -> Type) a Source #

Lazy monadic computation of a list of results.

Constructors

ListT |

Fields

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

#### Instances

Instances details

MonadTrans ListT Source # |
Instance details Defined in Agda.Utils.ListT Methods lift :: Monad m => m a -> ListT m a Source #
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 Source # local :: (r -> r) -> ListT m a -> ListT m a Source # reader :: (r -> a) -> ListT m a Source #
(Applicative m, MonadState s m) => MonadState s (ListT m) Source # |
Instance details Defined in Agda.Utils.ListT Methods get :: ListT m s Source # put :: s -> ListT m () Source # state :: (s -> (a, s)) -> ListT m a Source #
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 #

(Applicative m, MonadIO m) => MonadIO (ListT m) Source # |
Instance details Defined in Agda.Utils.ListT Methods liftIO :: IO a -> ListT m a Source #
(Functor m, Applicative m, Monad m) => Alternative (ListT m) Source # |
Instance details Defined in Agda.Utils.ListT Methods empty :: ListT m a Source # (<|>) :: ListT m a -> ListT m a -> ListT m a Source # some :: ListT m a -> ListT m [a] Source # many :: ListT m a -> ListT m [a] Source #
(Functor m, Applicative m, Monad m) => Applicative (ListT m) Source # |
Instance details Defined in Agda.Utils.ListT Methods pure :: a -> ListT m a Source # (<*>) :: ListT m (a -> b) -> ListT m a -> ListT m b Source # liftA2 :: (a -> b -> c) -> ListT m a -> ListT m b -> ListT m c Source # (*>) :: ListT m a -> ListT m b -> ListT m b Source # (<*) :: ListT m a -> ListT m b -> ListT m a Source #
Functor m => Functor (ListT m) Source # |
Instance details Defined in Agda.Utils.ListT Methods fmap :: (a -> b) -> ListT m a -> ListT m b Source # (<$) :: a -> ListT m b -> ListT m a Source #
(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 Source # (>>) :: ListT m a -> ListT m b -> ListT m b Source # return :: a -> ListT m a Source #
(Functor m, Applicative m, Monad m) => MonadPlus (ListT m) Source # |
Instance details Defined in Agda.Utils.ListT Methods mzero :: ListT m a Source # mplus :: ListT m a -> ListT m a -> ListT m a Source #
Monad m => MonadFail (ListT m) Source # |
Instance details Defined in Agda.Utils.ListT Methods fail :: String -> ListT m a Source #
Monad m => Monoid (ListT m a) Source # |
Instance details Defined in Agda.Utils.ListT Methods mempty :: ListT m a Source # mappend :: ListT m a -> ListT m a -> ListT m a Source # mconcat :: [ListT m a] -> ListT m a Source #
Monad m => Semigroup (ListT m a) Source # |
Instance details Defined in Agda.Utils.ListT Methods (<>) :: ListT m a -> ListT m a -> ListT m a Source # sconcat :: NonEmpty (ListT m a) -> ListT m a Source # stimes :: Integral b => b -> ListT m a -> ListT m a Source #
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