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

Agda.Utils.Function

Contents

Synopsis

Documentation

iterWhile :: (b -> Bool) -> (a -> (b, a)) -> a -> [(b, a)] Source

Repeat a state transition `f :: a -> (b, a)` with output `b` while condition `cond` on the output is true. Return all intermediate results and the final result where `cond` is `False`.

Postconditions (when it terminates): `fst (last (iterWhile cond f a)) == False`. `all fst (init (interWhile cond f a))`.

repeatWhile :: (a -> (Bool, a)) -> a -> a Source

Repeat something while a condition on some state is true. Return the last state (including the changes of the last transition, even if the condition became false then).

repeatWhileM :: Monad m => (a -> m (Bool, a)) -> a -> m a Source

Monadic version of `repeatWhile`.

trampolineWhile :: (a -> (Bool, a)) -> a -> a Source

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 = trampolineWhile \$ a -> maybe (False,a) (True,) (f a)`.

`trampolineWhile` is very similar to `repeatWhile`, only that it discards the state on which the condition went `False`, and returns the last state on which the condition was `True`.

trampolineWhileM :: Monad m => (a -> m (Bool, a)) -> a -> m a Source

Monadic version of `trampolineWhile`.

trampoline :: (a -> Either b a) -> a -> b Source

More general trampoline, which allows some final computation from iteration state `a` into result type `b`.

trampolineM :: Monad m => (a -> m (Either b a)) -> a -> m b Source

Monadic version of `trampoline`.

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

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 Source

Monadic version of `iterateUntil`.

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

`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 Source

`applyWhen b f a` applies `f` to `a` when `b`.

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

`applyUnless b f a` applies `f` to `a` unless `b`.

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

Monadic version of `applyWhen`

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

Monadic version of `applyUnless`