| Safe Haskell | Safe-Inferred |
|---|
Agda.Utils.Function
Contents
- trampoline :: (a -> (Bool, a)) -> a -> a
- trampolineM :: Monad m => (a -> m (Bool, a)) -> a -> m a
- iterateUntil :: (a -> a -> Bool) -> (a -> a) -> a -> a
- iterateUntilM :: Monad m => (a -> a -> Bool) -> (a -> m a) -> a -> m a
- iterate' :: Integral i => i -> (a -> a) -> a -> a
- applyWhen :: Bool -> (a -> a) -> a -> a
- applyUnless :: Bool -> (a -> a) -> a -> a
Documentation
trampoline :: (a -> (Bool, a)) -> a -> aSource
A version of the trampoline function.
The usual function iterates f :: a -> Maybe a as long
as Just{} is returned, and returns the last value of a
upon Nothing.
usualTrampoline f = trampoline $ a -> maybe (False,a) (True,) (f a).
trampolineM :: Monad m => (a -> m (Bool, a)) -> a -> m aSource
Monadic version of trampoline.
iterateUntil :: (a -> a -> Bool) -> (a -> a) -> a -> aSource
Iteration to fixed-point.
iterateUntil r f a0 iterates endofunction f, starting with a0,
until r relates its result to its input, i.e., f a .
r a
This is the generic pattern behind saturation algorithms.
If f is monotone with regard to r,
meaning a implies r bf a ,
and r f bf-chains starting with a0 are finite
then iteration is guaranteed to terminate.
A typical instance will work on sets, and r could be set inclusion,
and a0 the empty set, and f the step function of a saturation algorithm.
iterateUntilM :: Monad m => (a -> a -> Bool) -> (a -> m a) -> a -> m aSource
Monadic version of iterateUntil.
iterate' :: Integral i => i -> (a -> a) -> a -> aSource
iterate' n f xf to x n times and returns the
result.
The applications are calculated strictly.
Iteration over Booleans.
applyUnless :: Bool -> (a -> a) -> a -> aSource
applyUnless b f a applies f to a unless b.