Safe Haskell	None
Language	Haskell2010

Agda.Utils.Update

Synopsis

data Change a
class Monad m => MonadChange m where
runChange :: Change a -> (a, Bool)
type Updater a = a -> Change a
sharing :: Updater a -> Updater a
runUpdater :: Updater a -> a -> (a, Bool)
dirty :: Updater a
ifDirty :: MonadChange m => m a -> (a -> m b) -> (a -> m b) -> m b
class Traversable f => Updater1 f where
class Updater2 f where

Documentation

data Change a Source #

The Change monad.

Instances

Monad Change Source #
Instance details Defined in Agda.Utils.Update 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 #
Instance details Defined in Agda.Utils.Update Methods fmap :: (a -> b) -> Change a -> Change b # (<$) :: a -> Change b -> Change a #
Applicative Change Source #
Instance details Defined in Agda.Utils.Update Methods pure :: a -> Change a # (<>) :: Change (a -> b) -> Change a -> Change b # liftA2 :: (a -> b -> c) -> Change a -> Change b -> Change c # (>) :: Change a -> Change b -> Change b # (<*) :: Change a -> Change b -> Change a #
MonadChange Change Source #
Instance details Defined in Agda.Utils.Update Methods tellDirty :: Change () Source # listenDirty :: Change a -> Change (a, Bool) Source #

class Monad m => MonadChange m where Source #

The class of change monads.

Minimal complete definition

tellDirty, listenDirty

Methods

tellDirty Source #

Arguments

:: m ()

Mark computation as having changed something.

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

Instances

MonadChange Identity Source #	A mock change monad.
Instance details Defined in Agda.Utils.Update Methods tellDirty :: Identity () Source # listenDirty :: Identity a -> Identity (a, Bool) Source #
MonadChange Change Source #
Instance details Defined in Agda.Utils.Update Methods tellDirty :: Change () Source # listenDirty :: Change a -> Change (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 Source #

Arguments

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

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

Instances

Updater1 [] Source #
Instance details Defined in Agda.Utils.Update Methods updater1 :: Updater a -> Updater [a] Source # updates1 :: Updater a -> Updater [a] Source # update1 :: Updater a -> EndoFun [a] Source #
Updater1 Maybe Source #
Instance details Defined in Agda.Utils.Update 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 #
Instance details Defined in Agda.Utils.Update 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 #
Instance details Defined in Agda.Utils.Update 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 #