← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda/raring-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/Monad/Exception.hs

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2009-07-20 19:49:41 UTC
  • Revision ID: james.westby@ubuntu.com-20090720194941-hcjy91vrn16csh7d
Tags: upstream-2.2.4+dfsg
Import upstream version 2.2.4+dfsg

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/TypeChecking/Monad/Exception.hs
 
1
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}
 
2
 
 
3
-- | Basically a copy of the ErrorT monad transformer. It's handy to slap
 
4
--   onto TCM and still be a MonadTCM (which isn't possible with ErrorT).
 
5
 
 
6
module Agda.TypeChecking.Monad.Exception where
 
7
 
 
8
import Control.Applicative
 
9
import Control.Monad.Error
 
10
import Control.Monad.State
 
11
import Control.Monad.Reader
 
12
import Agda.TypeChecking.Monad.Base
 
13
 
 
14
newtype ExceptionT err m a = ExceptionT { runExceptionT :: m (Either err a) }
 
15
 
 
16
class Error err => MonadException err m | m -> err where
 
17
  throwException :: err -> m a
 
18
  catchException :: m a -> (err -> m a) -> m a
 
19
 
 
20
instance (Monad m, Error err) => Monad (ExceptionT err m) where
 
21
  return = ExceptionT . return . Right
 
22
  ExceptionT m >>= k = ExceptionT $ do
 
23
    r <- m
 
24
    case r of
 
25
      Left err -> return $ Left err
 
26
      Right x  -> runExceptionT $ k x
 
27
  fail = ExceptionT . return . Left . strMsg
 
28
 
 
29
instance (Monad m, Error err) => MonadException err (ExceptionT err m) where
 
30
  throwException = ExceptionT . return . Left
 
31
  catchException m h = ExceptionT $ do
 
32
    r <- runExceptionT m
 
33
    case r of
 
34
      Left err  -> runExceptionT $ h err
 
35
      Right x   -> return $ Right x
 
36
 
 
37
instance MonadTrans (ExceptionT err) where
 
38
  lift = ExceptionT . liftM Right
 
39
 
 
40
instance Functor f => Functor (ExceptionT err f) where
 
41
  fmap f = ExceptionT . fmap (either Left (Right . f)) . runExceptionT
 
42
 
 
43
instance (Error err, Applicative m, Monad m) => Applicative (ExceptionT err m) where
 
44
  pure  = return
 
45
  (<*>) = ap
 
46
 
 
47
instance (Error err, MonadState s m) => MonadState s (ExceptionT err m) where
 
48
  get   = ExceptionT $ Right `liftM` get
 
49
  put x = ExceptionT $ Right `liftM` put x
 
50
 
 
51
instance (Error err, MonadReader r m) => MonadReader r (ExceptionT err m) where
 
52
  ask     = ExceptionT $ Right `liftM` ask
 
53
  local f = ExceptionT . local f . runExceptionT
 
54
 
 
55
instance (Error err, MonadError err' m) => MonadError err' (ExceptionT err m) where
 
56
  throwError err = ExceptionT $ Right `liftM` throwError err
 
57
  catchError m h = ExceptionT $ runExceptionT m `catchError` (runExceptionT . h)
 
58
 
 
59
instance (Error err, MonadIO m) => MonadIO (ExceptionT err m) where
 
60
  liftIO m = ExceptionT $ Right `liftM` liftIO m
 
61
 
 
62
instance (Error err, MonadTCM tcm) => MonadTCM (ExceptionT err tcm) where
 
63
  liftTCM m = ExceptionT $ Right `liftM` liftTCM m
 
64