module Agda.Utils.Function where

-- | 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)@.
trampoline :: (a -> (Bool, a)) -> a -> a
trampoline f = loop where
  loop a = if again then loop a' else a'
    where (again, a') = f a

-- | Monadic version of 'trampoline'.
trampolineM :: (Monad m) => (a -> m (Bool, a)) -> a -> m a
trampolineM f = loop where
  loop a = do
    (again, a') <- f a
    if again then loop a' else return 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