← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/Utils/Function.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane, d5cf60f
  • Date: 2015-05-20 13:08:33 UTC
  • mfrom: (1.1.7)
  • Revision ID: package-import@ubuntu.com-20150520130833-cdcmhagwsouna237
Tags: 2.4.2.2-2
[d5cf60f] Depend on ${shlibs:Depends}, to get libc (& maybe other) deps

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Utils/Function.hs
 
1
{-# LANGUAGE TupleSections #-}
1
2
 
2
3
module Agda.Utils.Function where
3
4
 
 
5
-- | Repeat something while a condition on some state is true.
 
6
--   Return the last state (including the changes of the last
 
7
--   transition, even if the condition became false then).
 
8
 
 
9
repeatWhile :: (a -> (Bool, a)) -> a -> a
 
10
repeatWhile f = loop where
 
11
  loop a = if again then loop a' else a'
 
12
    where (again, a') = f a
 
13
 
 
14
-- | Monadic version of 'repeatWhile'.
 
15
repeatWhileM :: (Monad m) => (a -> m (Bool, a)) -> a -> m a
 
16
repeatWhileM f = loop where
 
17
  loop a = do
 
18
    (again, a') <- f a
 
19
    if again then loop a' else return a'
 
20
 
4
21
-- | A version of the trampoline function.
5
22
--
6
23
--   The usual function iterates @f :: a -> Maybe a@ as long
7
24
--   as @Just{}@ is returned, and returns the last value of @a@
8
25
--   upon @Nothing@.
9
26
--
10
 
trampoline :: (a -> (Bool, a)) -> a -> a
 
27
--   @usualTrampoline f = trampolineWhile $ \ a -> maybe (False,a) (True,) (f a)@.
 
28
--
 
29
--   @trampolineWhile@ is very similar to @repeatWhile@, only that
 
30
--   it discards the state on which the condition went @False@,
 
31
--   and returns the last state on which the condition was @True@.
 
32
trampolineWhile :: (a -> (Bool, a)) -> a -> a
 
33
trampolineWhile f = repeatWhile $ \ a ->
 
34
  let (again, a') = f a
 
35
  in (again,) $ if again then a' else a
 
36
 
 
37
-- | Monadic version of 'trampolineWhile'.
 
38
trampolineWhileM :: (Monad m) => (a -> m (Bool, a)) -> a -> m a
 
39
trampolineWhileM f = repeatWhileM $ \ a -> do
 
40
  (again, a') <- f a
 
41
  return $ (again,) $ if again then a' else a
 
42
 
 
43
-- | More general trampoline, which allows some final computation
 
44
--   from iteration state @a@ into result type @b@.
 
45
trampoline :: (a -> Either b a) -> a -> b
11
46
trampoline f = loop where
12
 
  loop a = if again then loop a' else a'
13
 
    where (again, a') = f a
 
47
  loop a = either id loop $ f a
14
48
 
15
49
-- | Monadic version of 'trampoline'.
16
 
trampolineM :: (Monad m) => (a -> m (Bool, a)) -> a -> m a
 
50
trampolineM :: Monad m => (a -> m (Either b a)) -> a -> m b
17
51
trampolineM f = loop where
18
 
  loop a = do
19
 
    (again, a') <- f a
20
 
    if again then loop a' else return a'
 
52
  loop a = either return loop =<< f a
21
53
 
22
54
-- | Iteration to fixed-point.
23
55
--
65
96
-- | @applyUnless b f a@ applies @f@ to @a@ unless @b@.
66
97
applyUnless :: Bool -> (a -> a) -> a -> a
67
98
applyUnless b f = if b then id else f
 
99
 
 
100
-- | Monadic version of @applyWhen@
 
101
applyWhenM :: (Monad m) => m Bool -> (m a -> m a) -> m a -> m a
 
102
applyWhenM mb f x = mb >>= \ b -> applyWhen b f x
 
103
 
 
104
-- | Monadic version of @applyUnless@
 
105
applyUnlessM :: (Monad m) => m Bool -> (m a -> m a) -> m a -> m a
 
106
applyUnlessM mb f x = mb >>= \ b -> applyUnless b f x