git.iko.soy/Idris-dev
on master help sign in
Simplify some expressions in IOExcept.

Use ioe_fail helper method where appropriate in Catchable and Exception Effect.

commit076c2d63f02b6a320dbcb94c60c6b4b66d2f6c03 authorLeif Warner <abimelech@gmail.com> dateWed 28 Oct 2015, 22:59 (11 years ago) parent7b30b6d
3 files changed+7−13
compare with master
unifiedsplit
libs/base/Control/Catchable.idr+2−2 libs/base/Control/IOExcept.idr+4−10 libs/effects/Effect/Exception.idr+1−1
libs/base/Control/Catchable.idr+2−2
@@ -16,14 +16,14 @@ instance Catchable (Either a) a where
1616 catch (Left err) h = h err
1717 catch (Right x) h = (Right x)
1818
19− throw x = Left x
19+ throw = Left
2020
2121instance Catchable (IOExcept err) err where
2222 catch (IOM prog) h = IOM (do p' <- prog
2323 case p' of
2424 Left e => let IOM he = h e in he
2525 Right val => return (Right val))
26− throw x = IOM (return (Left x))
26+ throw = ioe_fail
2727
2828instance Catchable List () where
2929 catch [] h = h ()
libs/base/Control/IOExcept.idr+4−10
@@ -10,8 +10,7 @@ instance Functor (IOExcept e) where
1010
1111instance Applicative (IOExcept e) where
1212 pure x = IOM (pure (pure x))
13− (IOM f) <*> (IOM a) = IOM (do f' <- f; a' <- a
14− return (f' <*> a'))
13+ (IOM f) <*> (IOM a) = IOM [| f <*> a |]
1514
1615instance Monad (IOExcept e) where
1716 (IOM x) >>= k = IOM (do x' <- x;
@@ -21,15 +20,10 @@ instance Monad (IOExcept e) where
2120 Left err => return (Left err))
2221
2322ioe_lift : IO a -> IOExcept err a
24−ioe_lift op = IOM (do op' <- op
25− return (Right op'))
23+ioe_lift op = IOM $ map Right op
2624
2725ioe_fail : err -> IOExcept err a
28−ioe_fail e = IOM (return (Left e))
26+ioe_fail e = IOM $ pure (Left e)
2927
3028ioe_run : IOExcept err a -> (err -> IO b) -> (a -> IO b) -> IO b
31−ioe_run (IOM act) err ok = do act' <- act
32− case act' of
33− Left e => err e
34− Right v => ok v
35−
29+ioe_run (IOM act) err ok = either err ok !act
libs/effects/Effect/Exception.idr+1−1
@@ -18,7 +18,7 @@ instance Show a => Handler (Exception a) IO where
1818 believe_me (exit 1)
1919
2020instance Handler (Exception a) (IOExcept a) where
21− handle _ (Raise e) k = IOM (return (Left e))
21+ handle _ (Raise e) k = ioe_fail e
2222
2323instance Handler (Exception a) (Either a) where
2424 handle _ (Raise e) k = Left e