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

Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Update

Synopsis

Documentation

data Change a Source #

The Change monad.

Instances

Monad Change Source # 

Methods

(>>=) :: Change a -> (a -> Change b) -> Change b #

(>>) :: Change a -> Change b -> Change b #

return :: a -> Change a #

fail :: String -> Change a #

Functor Change Source # 

Methods

fmap :: (a -> b) -> Change a -> Change b #

(<$) :: a -> Change b -> Change a #

Applicative Change Source # 

Methods

pure :: a -> Change a #

(<*>) :: Change (a -> b) -> Change a -> Change b #

(*>) :: Change a -> Change b -> Change b #

(<*) :: Change a -> Change b -> Change a #

MonadChange Change Source # 

class Monad m => MonadChange m where Source #

The class of change monads.

Minimal complete definition

tellDirty, listenDirty

Methods

tellDirty :: m () Source #

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

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.

Methods

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

updates1 :: Updater a -> Updater (f a) Source #

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

Instances

Updater1 [] Source # 

Methods

updater1 :: Updater a -> Updater [a] Source #

updates1 :: Updater a -> Updater [a] Source #

update1 :: Updater a -> EndoFun [a] Source #

Updater1 Maybe Source # 

Methods

updater1 :: Updater a -> Updater (Maybe a) Source #

updates1 :: Updater a -> Updater (Maybe a) Source #

update1 :: Updater a -> EndoFun (Maybe 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 #

Instances

Updater2 Either Source # 

Methods

updater2 :: Updater a -> Updater b -> Updater (Either a b) Source #

updates2 :: Updater a -> Updater b -> Updater (Either a b) Source #

update2 :: Updater a -> Updater b -> EndoFun (Either a b) Source #

Updater2 (,) Source # 

Methods

updater2 :: Updater a -> Updater b -> Updater (a, b) Source #

updates2 :: Updater a -> Updater b -> Updater (a, b) Source #

update2 :: Updater a -> Updater b -> EndoFun (a, b) Source #