git.iko.soy/Idris-dev
on master help sign in
Add Catchable and IOExcept modules
commit4187c577a51b8bf6429970dd4f11a2e425589df6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 25 Feb 2013, 14:05 (14 years ago) parentf8e41c5
3 files changed+76−2
compare with master
unifiedsplit
lib/Control/Catchable.idr+35 lib/Control/IOExcept.idr+38 lib/base.ipkg+3−2
lib/Control/Catchable.idrnew file+35
@@ -0,0 +1,35 @@
1+module Prelude.Catchable
2+
3+import Prelude.List
4+import Prelude.Maybe
5+import Prelude.Either
6+import Control.IOExcept
7+
8+class Catchable (m : Type -> Type) t where
9+ throw : t -> m a
10+ catch : m a -> (t -> m a) -> m a
11+
12+instance Catchable Maybe () where
13+ catch Nothing h = h ()
14+ catch (Just x) h = Just x
15+
16+ throw () = Nothing
17+
18+instance Catchable (Either a) a where
19+ catch (Left err) h = h err
20+ catch (Right x) h = (Right x)
21+
22+ throw x = Left x
23+
24+instance Catchable (IOExcept err) err where
25+ catch (ioM prog) h = ioM (do p' <- prog
26+ case p' of
27+ Left e => let ioM he = h e in he
28+ Right val => return (Right val))
29+ throw x = ioM (return (Left x))
30+
31+instance Catchable List () where
32+ catch [] h = h ()
33+ catch xs h = xs
34+
35+ throw () = []
lib/Control/IOExcept.idrnew file+38
@@ -0,0 +1,38 @@
1+module Control.IOExcept
2+
3+import Prelude
4+
5+-- An IO monad with exception handling
6+
7+data IOExcept : Type -> Type -> Type where
8+ ioM : IO (Either err a) -> IOExcept err a
9+
10+instance Functor (IOExcept e) where
11+ fmap f (ioM fn) = ioM (fmap (fmap f) fn)
12+
13+instance Applicative (IOExcept e) where
14+ pure x = ioM (pure (pure x))
15+ (ioM f) <$> (ioM a) = ioM (do f' <- f; a' <- a
16+ return (f' <$> a'))
17+
18+instance Monad (IOExcept e) where
19+ return = pure
20+ (ioM x) >>= k = ioM (do x' <- x;
21+ case x' of
22+ Right a => let (ioM ka) = k a in
23+ ka
24+ Left err => return (Left err))
25+
26+ioe_lift : IO a -> IOExcept err a
27+ioe_lift op = ioM (do op' <- op
28+ return (Right op'))
29+
30+ioe_fail : err -> IOExcept err a
31+ioe_fail e = ioM (return (Left e))
32+
33+ioe_run : IOExcept err a -> (err -> IO b) -> (a -> IO b) -> IO b
34+ioe_run (ioM act) err ok = do act' <- act
35+ case act' of
36+ Left e => err e
37+ Right v => ok v
38+
lib/base.ipkg+3−2
@@ -6,7 +6,7 @@ modules = Builtins, Prelude, IO, System,
66 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
77 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
88 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
9− Prelude.Heap, Prelude.Complex, Prelude.Functor,
9+ Prelude.Heap, Prelude.Complex, Prelude.Functor,
1010
1111 Network.Cgi,
1212 Debug.Trace,
@@ -18,4 +18,5 @@ modules = Builtins, Prelude, IO, System,
1818 Data.Morphisms, Data.Bits, Data.Mod2,
1919
2020 Control.Monad.Identity, Control.Monad.State, Control.Category,
21− Control.Arrow
21+ Control.Arrow,
22+ Control.Catchable, Control.IOExcept