3
3
module Language.Boogie.ErrorAccum where
4
4
5
5
import Control.Monad
6
+ import Control.Applicative
6
7
import Control.Monad.Trans
7
8
import Control.Monad.Trans.Error
8
9
9
- -- | Error accumulator:
10
- -- used in combination with ErrorT to store intermediate computation results,
11
- -- when errors should be accumulated rather than reported immediately
10
+ -- | Error accumulator:
11
+ -- used in combination with ErrorT to store intermediate computation results,
12
+ -- when errors should be accumulated rather than reported immediately
12
13
newtype ErrorAccumT e m a = ErrorAccumT { runErrorAccumT :: m ([e ], a ) }
13
14
14
15
instance (ErrorList e , Monad m ) => Functor (ErrorAccumT e m ) where
@@ -29,48 +30,48 @@ instance (ErrorList e, Monad m) => Monad (ErrorAccumT e m) where
29
30
(errs', res') <- runErrorAccumT $ k res
30
31
return (errs ++ errs', res')
31
32
32
-
33
+
33
34
instance ErrorList e => MonadTrans (ErrorAccumT e ) where
34
35
lift m = ErrorAccumT $ do
35
36
a <- m
36
- return ([] , a)
37
-
37
+ return ([] , a)
38
+
38
39
-- | Transform an error computation and default value into an error accumlator
39
40
accum :: (ErrorList e , Monad m ) => ErrorT [e ] m a -> a -> ErrorAccumT e m a
40
41
accum c def = ErrorAccumT (errToAccum def `liftM` runErrorT c)
41
42
where
42
43
errToAccum def (Left errs) = (errs, def)
43
44
errToAccum def (Right x) = ([] , x)
44
-
45
- -- | Transform an error accumlator back into a regular error computation
45
+
46
+ -- | Transform an error accumlator back into a regular error computation
46
47
report :: (ErrorList e , Monad m ) => ErrorAccumT e m a -> ErrorT [e ] m a
47
48
report accum = ErrorT (accumToErr `liftM` runErrorAccumT accum)
48
49
where
49
50
accumToErr ([] , x) = Right x
50
- accumToErr (es, _) = Left es
51
+ accumToErr (es, _) = Left es
51
52
52
53
-- | 'mapAccum' @f def xs@ :
53
54
-- Apply @f@ to all @xs@, accumulating errors and reporting them at the end
54
55
mapAccum :: (ErrorList e , Monad m ) => (a -> ErrorT [e ] m b ) -> b -> [a ] -> ErrorT [e ] m [b ]
55
- mapAccum f def xs = report $ mapM (acc f) xs
56
+ mapAccum f def xs = report $ mapM (acc f) xs
56
57
where
57
58
acc f x = accum (f x) def
58
-
59
+
59
60
-- | 'mapAccumA_' @f xs@ :
60
61
-- Apply @f@ to all @xs@ throwing away the result, accumulating errors
61
62
mapAccumA_ :: (ErrorList e , Monad m ) => (a -> ErrorT [e ] m () ) -> [a ] -> ErrorAccumT e m ()
62
- mapAccumA_ f xs = mapM_ (acc f) xs
63
+ mapAccumA_ f xs = mapM_ (acc f) xs
63
64
where
64
65
acc f x = accum (f x) ()
65
-
66
+
66
67
-- | Same as 'mapAccumA_', but reporting errors at the end
67
68
mapAccum_ :: (ErrorList e , Monad m ) => (a -> ErrorT [e ] m () ) -> [a ] -> ErrorT [e ] m ()
68
- mapAccum_ f xs = report $ mapAccumA_ f xs
69
+ mapAccum_ f xs = report $ mapAccumA_ f xs
69
70
70
71
-- | 'zipWithAccum_' @f xs ys@ :
71
72
-- Apply type checking @f@ to all @xs@ and @ys@ throwing away the result,
72
73
-- accumulating errors and reporting them at the end
73
74
zipWithAccum_ :: (ErrorList e , Monad m ) => (a -> b -> ErrorT [e ] m () ) -> [a ] -> [b ] -> ErrorT [e ] m ()
74
- zipWithAccum_ f xs ys = report $ zipWithM_ (acc f) xs ys
75
+ zipWithAccum_ f xs ys = report $ zipWithM_ (acc f) xs ys
75
76
where
76
77
acc f x y = accum (f x y) ()
0 commit comments