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

Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Update

Synopsis

Documentation

data Change a #

The Change monad.

Instances

Monad Change # 

Methods

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

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

return :: a -> Change a #

fail :: String -> Change a #

Functor Change # 

Methods

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

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

Applicative Change # 

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 # 

Methods

tellDirty :: Change () #

listenDirty :: Change a -> Change (a, Bool) #

class Monad m => MonadChange m where #

The class of change monads.

Minimal complete definition

tellDirty, listenDirty

Methods

tellDirty :: m () #

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

Instances

MonadChange Identity #

A mock change monad.

MonadChange Change # 

Methods

tellDirty :: Change () #

listenDirty :: Change a -> Change (a, Bool) #

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

Run a Change computation, returning result plus change flag.

type Updater a = a -> Change a #

sharing :: Updater a -> Updater a #

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

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

Blindly run an updater.

dirty :: Updater a #

Mark a computation as dirty.

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

class Traversable f => Updater1 f 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) #

Instances

Updater1 [] # 

Methods

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

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

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

Updater1 Maybe # 

Methods

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

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

update1 :: Updater a -> EndoFun (Maybe a) #

class Updater2 f where #

Like Bifunctor, but preserving sharing.

Minimal complete definition

updater2

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) #

Instances

Updater2 Either # 

Methods

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

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

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

Updater2 (,) # 

Methods

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

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

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