module Agda.Utils.Function where
iterWhile :: (b -> Bool) -> (a -> (b, a)) -> a -> [(b,a)]
iterWhile :: (b -> Bool) -> (a -> (b, a)) -> a -> [(b, a)]
iterWhile cond :: b -> Bool
cond f :: a -> (b, a)
f = a -> [(b, a)]
loop where
loop :: a -> [(b, a)]
loop a :: a
a = (b, a)
r (b, a) -> [(b, a)] -> [(b, a)]
forall a. a -> [a] -> [a]
: if b -> Bool
cond b
b then a -> [(b, a)]
loop a
a' else []
where r :: (b, a)
r@(b :: b
b, a' :: a
a') = a -> (b, a)
f a
a
repeatWhile :: (a -> (Bool, a)) -> a -> a
repeatWhile :: (a -> (Bool, a)) -> a -> a
repeatWhile f :: a -> (Bool, a)
f = a -> a
loop where
loop :: a -> a
loop a :: a
a = if Bool
again then a -> a
loop a
a' else a
a'
where (again :: Bool
again, a' :: a
a') = a -> (Bool, a)
f a
a
repeatWhileM :: (Monad m) => (a -> m (Bool, a)) -> a -> m a
repeatWhileM :: (a -> m (Bool, a)) -> a -> m a
repeatWhileM f :: a -> m (Bool, a)
f = a -> m a
loop where
loop :: a -> m a
loop a :: a
a = do
(again :: Bool
again, a' :: a
a') <- a -> m (Bool, a)
f a
a
if Bool
again then a -> m a
loop a
a' else a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a'
trampolineWhile :: (a -> (Bool, a)) -> a -> a
trampolineWhile :: (a -> (Bool, a)) -> a -> a
trampolineWhile f :: a -> (Bool, a)
f = (a -> (Bool, a)) -> a -> a
forall a. (a -> (Bool, a)) -> a -> a
repeatWhile ((a -> (Bool, a)) -> a -> a) -> (a -> (Bool, a)) -> a -> a
forall a b. (a -> b) -> a -> b
$ \ a :: a
a ->
let (again :: Bool
again, a' :: a
a') = a -> (Bool, a)
f a
a
in (Bool
again,) (a -> (Bool, a)) -> a -> (Bool, a)
forall a b. (a -> b) -> a -> b
$ if Bool
again then a
a' else a
a
trampolineWhileM :: (Monad m) => (a -> m (Bool, a)) -> a -> m a
trampolineWhileM :: (a -> m (Bool, a)) -> a -> m a
trampolineWhileM f :: a -> m (Bool, a)
f = (a -> m (Bool, a)) -> a -> m a
forall (m :: * -> *) a. Monad m => (a -> m (Bool, a)) -> a -> m a
repeatWhileM ((a -> m (Bool, a)) -> a -> m a) -> (a -> m (Bool, a)) -> a -> m a
forall a b. (a -> b) -> a -> b
$ \ a :: a
a -> do
(again :: Bool
again, a' :: a
a') <- a -> m (Bool, a)
f a
a
(Bool, a) -> m (Bool, a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool, a) -> m (Bool, a)) -> (Bool, a) -> m (Bool, a)
forall a b. (a -> b) -> a -> b
$ (Bool
again,) (a -> (Bool, a)) -> a -> (Bool, a)
forall a b. (a -> b) -> a -> b
$ if Bool
again then a
a' else a
a
trampoline :: (a -> Either b a) -> a -> b
trampoline :: (a -> Either b a) -> a -> b
trampoline f :: a -> Either b a
f = a -> b
loop where
loop :: a -> b
loop a :: a
a = (b -> b) -> (a -> b) -> Either b a -> b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> b
forall a. a -> a
id a -> b
loop (Either b a -> b) -> Either b a -> b
forall a b. (a -> b) -> a -> b
$ a -> Either b a
f a
a
trampolineM :: Monad m => (a -> m (Either b a)) -> a -> m b
trampolineM :: (a -> m (Either b a)) -> a -> m b
trampolineM f :: a -> m (Either b a)
f = a -> m b
loop where
loop :: a -> m b
loop a :: a
a = (b -> m b) -> (a -> m b) -> Either b a -> m b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return a -> m b
loop (Either b a -> m b) -> m (Either b a) -> m b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< a -> m (Either b a)
f a
a
iterateUntil :: (a -> a -> Bool) -> (a -> a) -> a -> a
iterateUntil :: (a -> a -> Bool) -> (a -> a) -> a -> a
iterateUntil r :: a -> a -> Bool
r f :: a -> a
f = a -> a
loop where
loop :: a -> a
loop a :: a
a = if a -> a -> Bool
r a
a' a
a then a
a' else a -> a
loop a
a'
where a' :: a
a' = a -> a
f a
a
iterateUntilM :: Monad m => (a -> a -> Bool) -> (a -> m a) -> a -> m a
iterateUntilM :: (a -> a -> Bool) -> (a -> m a) -> a -> m a
iterateUntilM r :: a -> a -> Bool
r f :: a -> m a
f = a -> m a
loop where
loop :: a -> m a
loop a :: a
a = do
a
a' <- a -> m a
f a
a
if a -> a -> Bool
r a
a' a
a then a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a' else a -> m a
loop a
a'
iterate' :: Integral i => i -> (a -> a) -> a -> a
iterate' :: i -> (a -> a) -> a -> a
iterate' 0 _ x :: a
x = a
x
iterate' n :: i
n f :: a -> a
f x :: a
x | i
n i -> i -> Bool
forall a. Ord a => a -> a -> Bool
> 0 = i -> (a -> a) -> a -> a
forall i a. Integral i => i -> (a -> a) -> a -> a
iterate' (i
n i -> i -> i
forall a. Num a => a -> a -> a
- 1) a -> a
f (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$! a -> a
f a
x
| Bool
otherwise = [Char] -> a
forall a. HasCallStack => [Char] -> a
error "iterate': Negative input."
applyWhen :: Bool -> (a -> a) -> a -> a
applyWhen :: Bool -> (a -> a) -> a -> a
applyWhen b :: Bool
b f :: a -> a
f = if Bool
b then a -> a
f else a -> a
forall a. a -> a
id
applyUnless :: Bool -> (a -> a) -> a -> a
applyUnless :: Bool -> (a -> a) -> a -> a
applyUnless b :: Bool
b f :: a -> a
f = if Bool
b then a -> a
forall a. a -> a
id else a -> a
f
applyWhenM :: (Monad m) => m Bool -> (m a -> m a) -> m a -> m a
applyWhenM :: m Bool -> (m a -> m a) -> m a -> m a
applyWhenM mb :: m Bool
mb f :: m a -> m a
f x :: m a
x = m Bool
mb m Bool -> (Bool -> m a) -> m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ b :: Bool
b -> Bool -> (m a -> m a) -> m a -> m a
forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
b m a -> m a
f m a
x
applyUnlessM :: (Monad m) => m Bool -> (m a -> m a) -> m a -> m a
applyUnlessM :: m Bool -> (m a -> m a) -> m a -> m a
applyUnlessM mb :: m Bool
mb f :: m a -> m a
f x :: m a
x = m Bool
mb m Bool -> (Bool -> m a) -> m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ b :: Bool
b -> Bool -> (m a -> m a) -> m a -> m a
forall a. Bool -> (a -> a) -> a -> a
applyUnless Bool
b m a -> m a
f m a
x