Agda.Utils.Function

Documentation

trampoline :: (a -> (Bool, a)) -> a -> a

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 a

Monadic version of trampoline.

iterateUntil :: (a -> a -> Bool) -> (a -> a) -> a -> a

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 r b implies f a r f b, and f-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 a

Monadic version of iterateUntil.

iterate' :: Integral i => i -> (a -> a) -> a -> a

iterate' n f x applies f to x n times and returns the result.

The applications are calculated strictly.

Iteration over Booleans.

applyWhen :: Bool -> (a -> a) -> a -> a

applyWhen b f a applies f to a when b.

applyUnless :: Bool -> (a -> a) -> a -> a

applyUnless b f a applies f to a unless b.

applyWhenM :: Monad m => m Bool -> (m a -> m a) -> m a -> m a

Monadic version of applyWhen

applyUnlessM :: Monad m => m Bool -> (m a -> m a) -> m a -> m a

Monadic version of applyUnless