← 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/Monad.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/Monad.hs
1
 
{-# LANGUAGE CPP #-}
 
1
{-# LANGUAGE CPP              #-}
2
2
{-# LANGUAGE FlexibleContexts #-}
3
3
 
4
4
module Agda.Utils.Monad
9
9
    )
10
10
    where
11
11
 
12
 
import Prelude             hiding (concat)
 
12
import Prelude             hiding (concat)
13
13
import Control.Monad       hiding (mapM, forM)
14
 
import Control.Monad.Error
15
14
import Control.Monad.State
16
15
import Control.Monad.Writer
17
16
import Control.Applicative
19
18
import Data.Foldable as Fold
20
19
import Data.Maybe
21
20
 
 
21
import Agda.Utils.Except
 
22
  ( Error(noMsg, strMsg)
 
23
  , MonadError(catchError, throwError)
 
24
  )
 
25
 
22
26
import Agda.Utils.List
23
27
 
24
 
#include "../undefined.h"
 
28
#include "undefined.h"
25
29
import Agda.Utils.Impossible
26
30
 
27
31
-- Conditionals and monads ------------------------------------------------
28
32
 
29
33
-- | @when_@ is just @Control.Monad.when@ with a more general type.
30
34
when_ :: Monad m => Bool -> m a -> m ()
31
 
when_ b m = when b $ do m >> return ()
 
35
when_ b m = when b $ m >> return ()
32
36
 
33
37
-- | @unless_@ is just @Control.Monad.unless@ with a more general type.
34
38
unless_ :: Monad m => Bool -> m a -> m ()
35
 
unless_ b m = unless b $ do m >> return ()
 
39
unless_ b m = unless b $ m >> return ()
36
40
 
37
41
whenM :: Monad m => m Bool -> m a -> m ()
38
42
whenM c m = c >>= (`when_` m)
45
49
-- | Monadic if-then-else.
46
50
ifM :: Monad m => m Bool -> m a -> m a -> m a
47
51
ifM c m m' =
48
 
    do  b <- c
49
 
        if b then m else m'
 
52
    do  b <- c
 
53
        if b then m else m'
50
54
 
51
55
-- | @ifNotM mc = ifM (not <$> mc)@
52
56
ifNotM :: Monad m => m Bool -> m a -> m a -> m a
113
117
mapMaybeM f xs = catMaybes <$> Trav.mapM f xs
114
118
 
115
119
-- | A monadic version of @'dropWhile' :: (a -> Bool) -> [a] -> [a]@.
116
 
dropWhileM :: (Monad m) => (a -> m Bool) -> [a] -> m [a]
 
120
dropWhileM :: Monad m => (a -> m Bool) -> [a] -> m [a]
117
121
dropWhileM p []       = return []
118
122
dropWhileM p (x : xs) = ifM (p x) (dropWhileM p xs) (return (x : xs))
119
123
 
120
124
-- Error monad ------------------------------------------------------------
121
125
 
 
126
-- | To simulate @MaybeT@ by @ExceptT@.
122
127
instance Error () where
123
128
  noMsg = ()
124
129
 
134
138
    Left e  -> throwError e
135
139
    Right r -> return r
136
140
 
137
 
 
138
 
bracket :: (Error e, MonadError e m)
139
 
        => m a         -- ^ Acquires resource. Run first.
140
 
        -> (a -> m c)  -- ^ Releases resource. Run last.
141
 
        -> (a -> m b)  -- ^ Computes result. Run in-between.
142
 
        -> m b
143
 
bracket acquire release compute = do
144
 
  resource <- acquire
145
 
  compute resource `finally` release resource
146
 
 
147
141
-- State monad ------------------------------------------------------------
148
142
 
149
143
-- | Bracket without failure.  Typically used to preserve state.
150
 
bracket_ :: (Monad m)
 
144
bracket_ :: Monad m
151
145
         => m a         -- ^ Acquires resource. Run first.
152
146
         -> (a -> m c)  -- ^ Releases resource. Run last.
153
147
         -> m b         -- ^ Computes result. Run in-between.
160
153
  return result
161
154
 
162
155
-- | Restore state after computation.
163
 
localState :: (MonadState s m) => m a -> m a
 
156
localState :: MonadState s m => m a -> m a
164
157
localState = bracket_ get put
165
158
 
166
159
-- Read -------------------------------------------------------------------
167
160
 
168
161
readM :: (Error e, MonadError e m, Read a) => String -> m a
169
162
readM s = case reads s of
170
 
            [(x,"")]    -> return x
171
 
            _           ->
 
163
            [(x,"")]    -> return x
 
164
            _           ->
172
165
              throwError $ strMsg $ "readM: parse error string " ++ s
173
166
 
174
167
 
175
 
 
176
 
 
177
168
-- RETIRED STUFF ----------------------------------------------------------
178
169
 
 
170
{- RETIRED, ASR, 09 September 2014. Not used.
 
171
-- | Bracket for the 'Error' class.
 
172
 
 
173
-- bracket :: (Error e, MonadError e m)
 
174
--         => m a         -- ^ Acquires resource. Run first.
 
175
--         -> (a -> m c)  -- ^ Releases resource. Run last.
 
176
--         -> (a -> m b)  -- ^ Computes result. Run in-between.
 
177
--         -> m b
 
178
-- bracket acquire release compute = do
 
179
--   resource <- acquire
 
180
--   compute resource `finally` release resource
 
181
-}
 
182
 
179
183
{- RETIRED, Andreas, 2012-04-30. Not used.
180
184
concatMapM :: Applicative m => (a -> m [b]) -> [a] -> m [b]
181
185
concatMapM f xs = concat <$> traverse f xs
184
188
--   the force to be effective. For the 'IO' monad you do.
185
189
forceM :: Monad m => [a] -> m ()
186
190
forceM xs = do () <- length xs `seq` return ()
187
 
               return ()
 
191
               return ()
188
192
 
189
193
commuteM :: (Traversable f, Applicative m) => f (m a) -> m (f a)
190
194
commuteM = traverse id