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

Safe HaskellNone
LanguageHaskell98

Agda.Utils.Update

Synopsis

Documentation

class Monad m => MonadChange m where Source

The class of change monads.

Methods

tellDirty Source

Arguments

:: m ()

Mark computation as having changed something.

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

Instances

runChange :: Change a -> (a, Bool) Source

Run a Change computation, returning result plus change flag.

type Updater a = a -> Change a Source

sharing :: Updater a -> Updater a Source

Replace result of updating with original input if nothing has changed.

runUpdater :: Updater a -> a -> (a, Bool) Source

Blindly run an updater.

dirty :: Updater a Source

Mark a computation as dirty.

ifDirty :: MonadChange m => m a -> (a -> m b) -> (a -> m b) -> m b Source

class Traversable f => Updater1 f where Source

Like Functor, but preserving sharing.

Minimal complete definition

Nothing

Methods

updater1 :: Updater a -> Updater (f a) Source

updates1 Source

Arguments

:: Updater a 
-> Updater (f a)
= sharing . updater1

update1 :: Updater a -> EndoFun (f a) Source

class Updater2 f where Source

Like Bifunctor, but preserving sharing.

Minimal complete definition

updater2

Methods

updater2 :: Updater a -> Updater b -> Updater (f a b) Source

updates2 :: Updater a -> Updater b -> Updater (f a b) Source

update2 :: Updater a -> Updater b -> EndoFun (f a b) Source