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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Update

Synopsis

- data Change a
- class Monad m => MonadChange m where
  - tellDirty :: m ()
  - listenDirty :: m a -> m (a, Bool)
- 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
  - updater1 :: Updater a -> Updater (f a)
  - updates1 :: Updater a -> Updater (f a)
  - update1 :: Updater a -> EndoFun (f a)
- class Updater2 f where
  - 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)

# 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 Source # (>>) :: Change a -> Change b -> Change b Source # return :: a -> Change a Source # fail :: String -> Change a Source #
Functor Change Source # |
Instance details Defined in Agda.Utils.Update Methods fmap :: (a -> b) -> Change a -> Change b Source # (<$) :: a -> Change b -> Change a Source #
Applicative Change Source # |
Instance details Defined in Agda.Utils.Update Methods pure :: a -> Change a Source # (<*>) :: Change (a -> b) -> Change a -> Change b Source # liftA2 :: (a -> b -> c) -> Change a -> Change b -> Change c Source # (*>) :: Change a -> Change b -> Change b Source # (<*) :: Change a -> Change b -> Change a Source #
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.

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.

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 #

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 #