ModuleAgda-2.7.0.1Haskell2010

Agda.Utils.Update

4 types
3 classes
8 values

PackageAgda-2.7.0.1
Exports15
LanguageHaskell2010
LicenceMIT
SourceUpdate.hs

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

The ChangeT monad transformer.

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

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

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

Run a ChangeT computation, returning result plus change flag.

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

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)

Blindly run an updater.

typetype Change a = ChangeT Identity a

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

The class of change monads.

Methods

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

Instances3MonadChange

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

valuerunChange :: Change a -> (a, Bool)

Run a Change computation, returning result plus change flag.

typetype Updater a = UpdaterT Identity a

valuerunUpdater :: Updater a -> a -> (a, Bool)

Blindly run an updater.

valuedirty :: Monad m => UpdaterT m a

Mark a computation as dirty.

valueifDirty

:: (Monad m, MonadChange m)
=> m a
-> a -> m b
-> a -> m b
-> m b

classclass Traversable f => Updater1 (f :: Type -> Type) where

Like Functor, but preserving sharing.

Methods

updater1 :: Updater a -> Updater (f a)
updates1 :: Updater a -> Updater (f a)
update1 :: Updater a -> EndoFun (f a)

Instances2Updater1

Updater1 MaybeDefined in Agda-2.7.0.1 · Agda.Utils.Update
Updater1 []Defined in Agda-2.7.0.1 · Agda.Utils.Update

classclass Updater2 (f :: Type -> Type -> Type) where

Like Bifunctor, but preserving sharing.

Methods

updater2 :: Updater a -> Updater b -> Updater (f a b)
updates2 :: Updater a -> Updater b -> Updater (f a b)
update2 :: Updater a -> Updater b -> EndoFun (f a b)

Instances2Updater2

Updater2 EitherDefined in Agda-2.7.0.1 · Agda.Utils.Update
Updater2 Tuple2Defined in Agda-2.7.0.1 · Agda.Utils.Update