ModuleAgda-2.8.0.2Haskell2010

Agda.Utils.Update

Synopsis

newtype ChangeT
value runChangeT
value mapChangeT
type UpdaterT
value runUpdaterT
type Change
class MonadChange
value runChange
type Updater
value sharing
value runUpdater
value dirty
value ifDirty
class Updater1
class Updater2

PackageAgda-2.8.0.2
Exports15
LanguageHaskell2010
LicenceMIT
SourceUpdate.hs

newtypenewtype ChangeT (m :: Type -> Type) a

Source#

The ChangeT monad transformer.

Instances20MonadTrans, MonadTransControl, Monad, Functor, MonadFail, Applicative, …

MonadTrans ChangeTDefined in Agda-2.8.0.2 · Agda.Utils.Update
MonadTransControl ChangeTDefined in Agda-2.8.0.2 · Agda.Utils.Update
Monad m => Monad (ChangeT m)Defined in Agda-2.8.0.2 · Agda.Utils.Update
Functor m => Functor (ChangeT m)Defined in Agda-2.8.0.2 · Agda.Utils.Update
MonadFail m => MonadFail (ChangeT m)Defined in Agda-2.8.0.2 · Agda.Utils.Update
Applicative m => Applicative (ChangeT m)Defined in Agda-2.8.0.2 · Agda.Utils.Update
MonadIO m => MonadIO (ChangeT m)Defined in Agda-2.8.0.2 · Agda.Utils.Update
HasOptions m => HasOptions (ChangeT m)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.HasOptions
MonadReduce m => MonadReduce (ChangeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
MonadTCEnv m => MonadTCEnv (ChangeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
MonadTCM tcm => MonadTCM (ChangeT tcm)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
MonadTCState m => MonadTCState (ChangeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
ReadTCState m => ReadTCState (ChangeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
HasBuiltins m => HasBuiltins (ChangeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
MonadAddContext m => MonadAddContext (ChangeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
MonadDebug m => MonadDebug (ChangeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Debug
PureTCM m => PureTCM (ChangeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Pure
HasConstInfo m => HasConstInfo (ChangeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Signature
Monad m => MonadChange (ChangeT m)Defined in Agda-2.8.0.2 · Agda.Utils.Update
type StT ChangeT a = (a, Any)Defined in Agda-2.8.0.2 · Agda.Utils.Update

valuerunChangeT :: Functor m => ChangeT m a -> m (a, Bool)

Source#

Run a ChangeT computation, returning result plus change flag.

valuemapChangeT :: (m (a, Any) -> n (b, Any)) -> ChangeT m a -> ChangeT n b

Source#

Map a ChangeT computation (monad transformer action).

typetype UpdaterT (m :: Type -> Type) a = a -> ChangeT m a

valuerunUpdaterT :: Functor m => UpdaterT m a -> a -> m (a, Bool)

Source#

Blindly run an updater.

typetype Change a = ChangeT Identity a

classclass Monad m => MonadChange (m :: Type -> Type) where

Source#

The class of change monads.

Methods

tellDirty :: m ()
listenDirty :: m a -> m (a, Bool)

Instances3MonadChange

MonadChange IdentityDefined in Agda-2.8.0.2 · Agda.Utils.Update
A mock change monad. Always assume change has happened.
Monad m => MonadChange (ChangeT m)Defined in Agda-2.8.0.2 · Agda.Utils.Update
Monad m => MonadChange (IdentityT m)Defined in Agda-2.8.0.2 · Agda.Utils.Update