Agda.Utils.Monad.Undo

Synopsis

class (Functor m, MonadState s m) => MonadUndo s m | m -> s where

undo :: m ()

setUndo :: m ()

getUndoStack :: m [s]

putUndoStack :: [s] -> m ()

newtype UndoT s m a = UndoT {

unUndoT :: StateT [s] m a

}

runUndoT :: Monad m => UndoT s m a -> m a

mapUndoT :: (m (a, [s]) -> n (b, [s])) -> UndoT s m a -> UndoT s n b

getUndoStateNumber :: MonadUndo s m => m Int

clearUndoHistory :: MonadUndo s m => m ()

Documentation

class (Functor m, MonadState s m) => MonadUndo s m | m -> s where

Source

An undo monad is a state monad with backtracking.

Methods

undo :: m ()

Source

setUndo :: m ()

Source

getUndoStack :: m [s]

Source

putUndoStack :: [s] -> m ()

Source

Instances

MonadIO m => MonadUndo TCState (TCMT m)

(MonadState s m, Monad m) => MonadUndo s (UndoT s m)

newtype UndoT s m a

Source

The undo monad transformer turns any state monad into an undo monad.

Constructors

UndoT

unUndoT :: StateT [s] m a

Instances

MonadError e m => MonadError e (UndoT s m)

MonadReader e m => MonadReader e (UndoT s m)

MonadState s m => MonadState s (UndoT s' m)

(MonadState s m, Monad m) => MonadUndo s (UndoT s m)

MonadTrans (UndoT s)

Monad m => Monad (UndoT s m)

Monad m => Functor (UndoT s m)

MonadIO m => MonadIO (UndoT s m)

runUndoT :: Monad m => UndoT s m a -> m a

Source

mapUndoT :: (m (a, [s]) -> n (b, [s])) -> UndoT s m a -> UndoT s n b

Source

getUndoStateNumber :: MonadUndo s m => m Int

Source

clearUndoHistory :: MonadUndo s m => m ()

Source

Produced by Haddock version 2.4.2