module Agda.Utils.Function where
-- | 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))@.
iterWhile :: (b -> Bool) -> (a -> (b, a)) -> a -> [(b,a)]
iterWhile cond f = loop where
loop a = r : if cond b then loop a' else []
where r@(b, a') = f a
-- | 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).
repeatWhile :: (a -> (Bool, a)) -> a -> a
repeatWhile f = loop where
loop a = if again then loop a' else a'
where (again, a') = f a
-- | Monadic version of 'repeatWhile'.
repeatWhileM :: (Monad m) => (a -> m (Bool, a)) -> a -> m a
repeatWhileM f = loop where
loop a = do
(again, a') <- f a
if again then loop a' else return 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 = 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@.
trampolineWhile :: (a -> (Bool, a)) -> a -> a
trampolineWhile f = repeatWhile $ \ a ->
let (again, a') = f a
in (again,) $ if again then a' else a
-- | Monadic version of 'trampolineWhile'.
trampolineWhileM :: (Monad m) => (a -> m (Bool, a)) -> a -> m a
trampolineWhileM f = repeatWhileM $ \ a -> do
(again, a') <- f a
return $ (again,) $ if again then a' else a
-- | More general trampoline, which allows some final computation
-- from iteration state @a@ into result type @b@.
trampoline :: (a -> Either b a) -> a -> b
trampoline f = loop where
loop a = either id loop $ f a
-- | Monadic version of 'trampoline'.
trampolineM :: Monad m => (a -> m (Either b a)) -> a -> m b
trampolineM f = loop where
loop a = either return loop =<< f 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.
iterateUntil :: (a -> a -> Bool) -> (a -> a) -> a -> a
iterateUntil r f = loop where
loop a = if r a' a then a' else loop a'
where a' = f a
-- | Monadic version of 'iterateUntil'.
iterateUntilM :: Monad m => (a -> a -> Bool) -> (a -> m a) -> a -> m a
iterateUntilM r f = loop where
loop a = do
a' <- f a
if r a' a then return a' else loop a'
-- | @'iterate'' n f x@ applies @f@ to @x@ @n@ times and returns the
-- result.
--
-- The applications are calculated strictly.
iterate' :: Integral i => i -> (a -> a) -> a -> a
iterate' 0 f x = x
iterate' n f x | n > 0 = iterate' (n - 1) f $! f x
| otherwise = error "iterate': Negative input."
-- * Iteration over Booleans.
-- | @applyWhen b f a@ applies @f@ to @a@ when @b@.
applyWhen :: Bool -> (a -> a) -> a -> a
applyWhen b f = if b then f else id
-- | @applyUnless b f a@ applies @f@ to @a@ unless @b@.
applyUnless :: Bool -> (a -> a) -> a -> a
applyUnless b f = if b then id else f
-- | Monadic version of @applyWhen@
applyWhenM :: (Monad m) => m Bool -> (m a -> m a) -> m a -> m a
applyWhenM mb f x = mb >>= \ b -> applyWhen b f x
-- | Monadic version of @applyUnless@
applyUnlessM :: (Monad m) => m Bool -> (m a -> m a) -> m a -> m a
applyUnlessM mb f x = mb >>= \ b -> applyUnless b f x