git.iko.soy/Idris-dev
on master help sign in
Simplify some expressions in IOExcept.
076c2d6Leif Warner
libs/base/Control/Catchable.idr+2−2
compare with master
unifiedsplit
@@ -16,14 +16,14 @@ instance Catchable (Either a) a where
16 catch (Left err) h = h err
16 catch (Left err) h = h err
17 catch (Right x) h = (Right x)
17 catch (Right x) h = (Right x)
18
18
19− throw x = Left x
19+ throw = Left
20
20
21instance Catchable (IOExcept err) err where
21instance Catchable (IOExcept err) err where
22 catch (IOM prog) h = IOM (do p' <- prog
22 catch (IOM prog) h = IOM (do p' <- prog
23 case p' of
23 case p' of
24 Left e => let IOM he = h e in he
24 Left e => let IOM he = h e in he
25 Right val => return (Right val))
25 Right val => return (Right val))
26− throw x = IOM (return (Left x))
26+ throw = ioe_fail
27
27
28instance Catchable List () where
28instance Catchable List () where
29 catch [] h = h ()
29 catch [] h = h ()
libs/base/Control/IOExcept.idr+4−10
@@ -10,8 +10,7 @@ instance Functor (IOExcept e) where
10
10
11instance Applicative (IOExcept e) where
11instance Applicative (IOExcept e) where
12 pure x = IOM (pure (pure x))
12 pure x = IOM (pure (pure x))
13− (IOM f) <*> (IOM a) = IOM (do f' <- f; a' <- a
13+ (IOM f) <*> (IOM a) = IOM [| f <*> a |]
14− return (f' <*> a'))
15
14
16instance Monad (IOExcept e) where
15instance Monad (IOExcept e) where
17 (IOM x) >>= k = IOM (do x' <- x;
16 (IOM x) >>= k = IOM (do x' <- x;
@@ -21,15 +20,10 @@ instance Monad (IOExcept e) where
21 Left err => return (Left err))
20 Left err => return (Left err))
22
21
23ioe_lift : IO a -> IOExcept err a
22ioe_lift : IO a -> IOExcept err a
24−ioe_lift op = IOM (do op' <- op
23+ioe_lift op = IOM $ map Right op
25− return (Right op'))
26
24
27ioe_fail : err -> IOExcept err a
25ioe_fail : err -> IOExcept err a
28−ioe_fail e = IOM (return (Left e))
26+ioe_fail e = IOM $ pure (Left e)
29
27
30ioe_run : IOExcept err a -> (err -> IO b) -> (a -> IO b) -> IO b
28ioe_run : IOExcept err a -> (err -> IO b) -> (a -> IO b) -> IO b
31−ioe_run (IOM act) err ok = do act' <- act
29+ioe_run (IOM act) err ok = either err ok !act
32− case act' of
33− Left e => err e
34− Right v => ok v
35−
libs/effects/Effect/Exception.idr+1−1
@@ -18,7 +18,7 @@ instance Show a => Handler (Exception a) IO where
18 believe_me (exit 1)
18 believe_me (exit 1)
19
19
20instance Handler (Exception a) (IOExcept a) where
20instance Handler (Exception a) (IOExcept a) where
21− handle _ (Raise e) k = IOM (return (Left e))
21+ handle _ (Raise e) k = ioe_fail e
22
22
23instance Handler (Exception a) (Either a) where
23instance Handler (Exception a) (Either a) where
24 handle _ (Raise e) k = Left e
24 handle _ (Raise e) k = Left e