Safe Haskell	None
Language	Haskell2010

Agda.Utils.StrictWriter

Description

This is a very strict Writer monad, as a wrapper on Agda.Utils.StrictState.

Synopsis

class (Monoid w, Monad m) => MonadWriter w (m :: Type -> Type) | m -> w where
- writer :: (a, w) -> m a
- tell :: w -> m ()
- listen :: m a -> m (a, w)
- pass :: m (a, w -> w) -> m a
censor :: MonadWriter w m => (w -> w) -> m a -> m a
execWriter :: Monoid w => Writer w a -> w
execWriterT :: (Monoid w, Monad m) => WriterT w m a -> m w
runWriter :: Monoid w => Writer w a -> (a, w)
runWriterT :: (Monoid w, Monad m) => WriterT w m a -> m (a, w)
newtype Writer w a = Writer {
- unWriter :: State w a
}
newtype WriterT w (m :: Type -> Type) a = WriterT {
- unWriterT :: StateT w m a
}

Documentation

class (Monoid w, Monad m) => MonadWriter w (m :: Type -> Type) | m -> w where #

Minimal complete definition

(writer | tell), listen, pass

Methods

writer :: (a, w) -> m a #

writer (a,w) embeds a simple writer action.

tell :: w -> m () #

tell w is an action that produces the output w.

listen :: m a -> m (a, w) #

listen m is an action that executes the action m and adds its output to the value of the computation.

pass :: m (a, w -> w) -> m a #

pass m is an action that executes the action m, which returns a value and a function, and returns the value, applying the function to the output.

Instances

Instances details

Monoid w => MonadWriter w (Writer w) Source #
Instance details Defined in Agda.Utils.StrictWriter Methods writer :: (a, w) -> Writer w a # tell :: w -> Writer w () # listen :: Writer w a -> Writer w (a, w) # pass :: Writer w (a, w -> w) -> Writer w a #
MonadWriter w m => MonadWriter w (CatchT m) #
Instance details Defined in Control.Monad.Catch.Pure Methods writer :: (a, w) -> CatchT m a # tell :: w -> CatchT m () # listen :: CatchT m a -> CatchT m (a, w) # pass :: CatchT m (a, w -> w) -> CatchT m a #
MonadWriter w m => MonadWriter w (MaybeT m) #
Instance details Defined in Control.Monad.Writer.Class Methods writer :: (a, w) -> MaybeT m a # tell :: w -> MaybeT m () # listen :: MaybeT m a -> MaybeT m (a, w) # pass :: MaybeT m (a, w -> w) -> MaybeT m a #
Monoid w => MonadWriter w ((,) w) #	Since: mtl-2.2.2
Instance details Defined in Control.Monad.Writer.Class Methods writer :: (a, w) -> (w, a) # tell :: w -> (w, ()) # listen :: (w, a) -> (w, (a, w)) # pass :: (w, (a, w -> w)) -> (w, a) #
MonadWriter w m => MonadWriter w (ReaderT r m) Source #
Instance details Defined in Agda.Utils.StrictReader Methods writer :: (a, w) -> ReaderT r m a # tell :: w -> ReaderT r m () # listen :: ReaderT r m a -> ReaderT r m (a, w) # pass :: ReaderT r m (a, w -> w) -> ReaderT r m a #
MonadWriter w m => MonadWriter w (StateT s m) Source #
Instance details Defined in Agda.Utils.StrictState Methods writer :: (a, w) -> StateT s m a # tell :: w -> StateT s m () # listen :: StateT s m a -> StateT s m (a, w) # pass :: StateT s m (a, w -> w) -> StateT s m a #
(Monoid w, Monad m) => MonadWriter w (WriterT w m) Source #
Instance details Defined in Agda.Utils.StrictWriter Methods writer :: (a, w) -> WriterT w m a # tell :: w -> WriterT w m () # listen :: WriterT w m a -> WriterT w m (a, w) # pass :: WriterT w m (a, w -> w) -> WriterT w m a #
(Monoid w', MonadWriter w m) => MonadWriter w (AccumT w' m) #	There are two valid instances for `AccumT`. It could either: Lift the operations to the inner `MonadWriter` Handle the operations itself, à la a `WriterT`. This instance chooses (1), reflecting that the intent of `AccumT` as a type is different than that of `WriterT`. Since: mtl-2.3
Instance details Defined in Control.Monad.Writer.Class Methods writer :: (a, w) -> AccumT w' m a # tell :: w -> AccumT w' m () # listen :: AccumT w' m a -> AccumT w' m (a, w) # pass :: AccumT w' m (a, w -> w) -> AccumT w' m a #
MonadWriter w m => MonadWriter w (ExceptT e m) #	Since: mtl-2.2
Instance details Defined in Control.Monad.Writer.Class Methods writer :: (a, w) -> ExceptT e m a # tell :: w -> ExceptT e m () # listen :: ExceptT e m a -> ExceptT e m (a, w) # pass :: ExceptT e m (a, w -> w) -> ExceptT e m a #
MonadWriter w m => MonadWriter w (IdentityT m) #
Instance details Defined in Control.Monad.Writer.Class Methods writer :: (a, w) -> IdentityT m a # tell :: w -> IdentityT m () # listen :: IdentityT m a -> IdentityT m (a, w) # pass :: IdentityT m (a, w -> w) -> IdentityT m a #
MonadWriter w m => MonadWriter w (ReaderT r m) #
Instance details Defined in Control.Monad.Writer.Class Methods writer :: (a, w) -> ReaderT r m a # tell :: w -> ReaderT r m () # listen :: ReaderT r m a -> ReaderT r m (a, w) # pass :: ReaderT r m (a, w -> w) -> ReaderT r m a #
MonadWriter w m => MonadWriter w (StateT s m) #
Instance details Defined in Control.Monad.Writer.Class Methods writer :: (a, w) -> StateT s m a # tell :: w -> StateT s m () # listen :: StateT s m a -> StateT s m (a, w) # pass :: StateT s m (a, w -> w) -> StateT s m a #
MonadWriter w m => MonadWriter w (StateT s m) #
Instance details Defined in Control.Monad.Writer.Class Methods writer :: (a, w) -> StateT s m a # tell :: w -> StateT s m () # listen :: StateT s m a -> StateT s m (a, w) # pass :: StateT s m (a, w -> w) -> StateT s m a #
(Monoid w, Monad m) => MonadWriter w (WriterT w m) #	Since: mtl-2.3
Instance details Defined in Control.Monad.Writer.Class Methods writer :: (a, w) -> WriterT w m a # tell :: w -> WriterT w m () # listen :: WriterT w m a -> WriterT w m (a, w) # pass :: WriterT w m (a, w -> w) -> WriterT w m a #
(Monoid w, Monad m) => MonadWriter w (WriterT w m) #
Instance details Defined in Control.Monad.Writer.Class Methods writer :: (a, w) -> WriterT w m a # tell :: w -> WriterT w m () # listen :: WriterT w m a -> WriterT w m (a, w) # pass :: WriterT w m (a, w -> w) -> WriterT w m a #
(Monoid w, Monad m) => MonadWriter w (WriterT w m) #
Instance details Defined in Control.Monad.Writer.Class Methods writer :: (a, w) -> WriterT w m a # tell :: w -> WriterT w m () # listen :: WriterT w m a -> WriterT w m (a, w) # pass :: WriterT w m (a, w -> w) -> WriterT w m a #
MonadWriter w m => MonadWriter w (EquivT s c v m) #
Instance details Defined in Data.Equivalence.Monad Methods writer :: (a, w) -> EquivT s c v m a # tell :: w -> EquivT s c v m () # listen :: EquivT s c v m a -> EquivT s c v m (a, w) # pass :: EquivT s c v m (a, w -> w) -> EquivT s c v m a #
(Monoid w, Monad m) => MonadWriter w (RWST r w s m) #	Since: mtl-2.3
Instance details Defined in Control.Monad.Writer.Class Methods writer :: (a, w) -> RWST r w s m a # tell :: w -> RWST r w s m () # listen :: RWST r w s m a -> RWST r w s m (a, w) # pass :: RWST r w s m (a, w -> w) -> RWST r w s m a #
(Monoid w, Monad m) => MonadWriter w (RWST r w s m) #
Instance details Defined in Control.Monad.Writer.Class Methods writer :: (a, w) -> RWST r w s m a # tell :: w -> RWST r w s m () # listen :: RWST r w s m a -> RWST r w s m (a, w) # pass :: RWST r w s m (a, w -> w) -> RWST r w s m a #
(Monoid w, Monad m) => MonadWriter w (RWST r w s m) #
Instance details Defined in Control.Monad.Writer.Class Methods writer :: (a, w) -> RWST r w s m a # tell :: w -> RWST r w s m () # listen :: RWST r w s m a -> RWST r w s m (a, w) # pass :: RWST r w s m (a, w -> w) -> RWST r w s m a #

censor :: MonadWriter w m => (w -> w) -> m a -> m a #

censor f m is an action that executes the action m and applies the function f to its output, leaving the return value unchanged.

censor f m = pass (liftM (\x -> (x,f)) m)

execWriter :: Monoid w => Writer w a -> w Source #

execWriterT :: (Monoid w, Monad m) => WriterT w m a -> m w Source #

runWriter :: Monoid w => Writer w a -> (a, w) Source #

runWriterT :: (Monoid w, Monad m) => WriterT w m a -> m (a, w) Source #

newtype Writer w a Source #

Constructors

Writer
Fields unWriter :: State w a

Instances

Instances details

Monoid w => MonadWriter w (Writer w) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Methods

writer :: (a, w) -> Writer w a #

tell :: w -> Writer w () #

listen :: Writer w a -> Writer w (a, w) #

pass :: Writer w (a, w -> w) -> Writer w a #

Applicative (Writer w) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Methods

pure :: a -> Writer w a #

(<*>) :: Writer w (a -> b) -> Writer w a -> Writer w b #

liftA2 :: (a -> b -> c) -> Writer w a -> Writer w b -> Writer w c #

(*>) :: Writer w a -> Writer w b -> Writer w b #

(<*) :: Writer w a -> Writer w b -> Writer w a #

Functor (Writer w) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Methods

fmap :: (a -> b) -> Writer w a -> Writer w b #

(<$) :: a -> Writer w b -> Writer w a #

Monad (Writer w) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Methods

(>>=) :: Writer w a -> (a -> Writer w b) -> Writer w b #

(>>) :: Writer w a -> Writer w b -> Writer w b #

return :: a -> Writer w a #

ExpandCase (State w a) => ExpandCase (Writer w a) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Associated Types

type Result (Writer w a)
Instance details Defined in Agda.Utils.StrictWriter type Result (Writer w a) = Result (State w a)

Methods

expand :: ((Writer w a -> Result (Writer w a)) -> Result (Writer w a)) -> Writer w a Source #

type Result (Writer w a) Source #

Instance details

Defined in Agda.Utils.StrictWriter

type Result (Writer w a) = Result (State w a)

newtype WriterT w (m :: Type -> Type) a Source #

Constructors

WriterT
Fields unWriterT :: StateT w m a

Instances

Instances details

(Monad m, MonadError e (StateT w m)) => MonadError e (WriterT w m) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Methods

throwError :: e -> WriterT w m a #

catchError :: WriterT w m a -> (e -> WriterT w m a) -> WriterT w m a #

(Monad m, MonadReader r (StateT w m)) => MonadReader r (WriterT w m) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Methods

ask :: WriterT w m r #

local :: (r -> r) -> WriterT w m a -> WriterT w m a #

reader :: (r -> a) -> WriterT w m a #

(Monad m, MonadState s (StateT w m)) => MonadState s (WriterT w m) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Methods

get :: WriterT w m s #

put :: s -> WriterT w m () #

state :: (s -> (a, s)) -> WriterT w m a #

(Monoid w, Monad m) => MonadWriter w (WriterT w m) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Methods

writer :: (a, w) -> WriterT w m a #

tell :: w -> WriterT w m () #

listen :: WriterT w m a -> WriterT w m (a, w) #

pass :: WriterT w m (a, w -> w) -> WriterT w m a #

MonadTransControl (WriterT w) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Methods

liftWith :: Monad m => (Run (WriterT w) -> m a) -> WriterT w m a #

restoreT :: Monad m => m (StT (WriterT w) a) -> WriterT w m a #

MonadTrans (WriterT w) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Methods

lift :: Monad m => m a -> WriterT w m a #

(HasOptions m, Monoid w) => HasOptions (WriterT w m) Source #

Instance details

Defined in Agda.Interaction.Options.HasOptions

Methods

pragmaOptions :: WriterT w m PragmaOptions Source #

commandLineOptions :: WriterT w m CommandLineOptions Source #

(Monoid w, MonadReduce m) => MonadReduce (WriterT w m) Source #

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> WriterT w m a Source #

(Monoid w, MonadTCEnv m) => MonadTCEnv (WriterT w m) Source #

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: WriterT w m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> WriterT w m a -> WriterT w m a Source #

(Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm) Source #

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> WriterT w tcm a Source #

(Monoid w, MonadTCState m) => MonadTCState (WriterT w m) Source #

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTC :: WriterT w m TCState Source #

putTC :: TCState -> WriterT w m () Source #

modifyTC :: (TCState -> TCState) -> WriterT w m () Source #

(Monoid w, ReadTCState m) => ReadTCState (WriterT w m) Source #

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: WriterT w m TCState Source #

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

getSessionState :: WriterT w m SessionState Source #

withTCState :: (TCState -> TCState) -> WriterT w m a -> WriterT w m a Source #

(HasBuiltins m, Monoid w) => HasBuiltins (WriterT w m) Source #

Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> WriterT w m (Maybe (Builtin PrimFun)) Source #

(Monoid w, MonadAddContext m) => MonadAddContext (WriterT w m) Source #

Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> WriterT w m a -> WriterT w m a Source #

addLetBinding' :: IsAxiom -> Origin -> Name -> Term -> Dom Type -> WriterT w m a -> WriterT w m a Source #

addLocalRewrite :: RewriteRule -> WriterT w m a -> WriterT w m a Source #

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

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

(MonadDebug m, Monoid w) => MonadDebug (WriterT w m) Source #

Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> WriterT w m Doc Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> Doc -> WriterT w m a -> WriterT w m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> WriterT w m a -> WriterT w m a Source #

getVerbosity :: WriterT w m Verbosity Source #

getProfileOptions :: WriterT w m ProfileOptions Source #

isDebugPrinting :: WriterT w m Bool Source #

nowDebugPrinting :: WriterT w m a -> WriterT w m a Source #

(PureTCM m, Monoid w) => PureTCM (WriterT w m) Source #

Instance details

Defined in Agda.TypeChecking.Monad.Pure

(Monoid w, HasConstInfo m) => HasConstInfo (WriterT w m) Source #

Instance details

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> WriterT w m Definition Source #

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

getGlobalRewriteRulesFor :: QName -> WriterT w m GlobalRewriteRules Source #

getLocalRewriteRulesFor :: RewriteHead -> WriterT w m RewriteRules Source #

(MonadTrace m, Monoid w) => MonadTrace (WriterT w m) Source #

Instance details

Defined in Agda.TypeChecking.Monad.Trace

Methods

traceCall :: Call -> WriterT w m a -> WriterT w m a Source #

traceCallM :: WriterT w m Call -> WriterT w m a -> WriterT w m a Source #

traceCallCPS :: Call -> ((a -> WriterT w m b) -> WriterT w m b) -> (a -> WriterT w m b) -> WriterT w m b Source #

traceClosureCall :: Closure Call -> WriterT w m a -> WriterT w m a Source #

printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> WriterT w m () Source #

(MonadFileId m, Monoid w) => MonadFileId (WriterT w m) Source #

Instance details

Defined in Agda.Utils.FileId

Methods

fileFromId :: FileId -> WriterT w m File Source #

idFromFile :: File -> WriterT w m FileId Source #

Monad m => Applicative (WriterT w m) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Methods

pure :: a -> WriterT w m a #

(<*>) :: WriterT w m (a -> b) -> WriterT w m a -> WriterT w m b #

liftA2 :: (a -> b -> c) -> WriterT w m a -> WriterT w m b -> WriterT w m c #

(*>) :: WriterT w m a -> WriterT w m b -> WriterT w m b #

(<*) :: WriterT w m a -> WriterT w m b -> WriterT w m a #

Functor m => Functor (WriterT w m) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Methods

fmap :: (a -> b) -> WriterT w m a -> WriterT w m b #

(<$) :: a -> WriterT w m b -> WriterT w m a #

Monad m => Monad (WriterT w m) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Methods

(>>=) :: WriterT w m a -> (a -> WriterT w m b) -> WriterT w m b #

(>>) :: WriterT w m a -> WriterT w m b -> WriterT w m b #

return :: a -> WriterT w m a #

MonadIO m => MonadIO (WriterT w m) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Methods

liftIO :: IO a -> WriterT w m a #

ExpandCase (m (Pair a w)) => ExpandCase (WriterT w m a) Source #

Instance details

Defined in Agda.Utils.StrictWriter

Associated Types

type Result (WriterT w m a)
Instance details Defined in Agda.Utils.StrictWriter type Result (WriterT w m a) = Result (StateT w m a)

Methods

expand :: ((WriterT w m a -> Result (WriterT w m a)) -> Result (WriterT w m a)) -> WriterT w m a Source #

type StT (WriterT w) a Source #

Instance details

Defined in Agda.Utils.StrictWriter

type StT (WriterT w) a = StT (StateT w) a

type Result (WriterT w m a) Source #

Instance details

Defined in Agda.Utils.StrictWriter

type Result (WriterT w m a) = Result (StateT w m a)