git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2776 from LeifW/ioexcept_golf
76b1675Edwin Brady
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+8−17
@@ -2,34 +2,25 @@ module Control.IOExcept
2
2
3-- An IO monad with exception handling
3-- An IO monad with exception handling
4
4
5−data IOExcept : Type -> Type -> Type where
5+record IOExcept err a where
6+ constructor IOM
6− IOM : IO (Either err a) -> IOExcept err a
7+ runIOExcept : IO (Either err a)
7
8
8instance Functor (IOExcept e) where
9instance Functor (IOExcept e) where
9 map f (IOM fn) = IOM (map (map f) fn)
10 map f (IOM fn) = IOM (map (map f) fn)
10
11
11instance Applicative (IOExcept e) where
12instance Applicative (IOExcept e) where
12 pure x = IOM (pure (pure x))
13 pure x = IOM (pure (pure x))
13− (IOM f) <*> (IOM a) = IOM (do f' <- f; a' <- a
14+ (IOM f) <*> (IOM a) = IOM [| f <*> a |]
14− return (f' <*> a'))
15
15
16instance Monad (IOExcept e) where
16instance Monad (IOExcept e) where
17− (IOM x) >>= k = IOM (do x' <- x;
17+ (IOM x) >>= f = IOM $ x >>= either (pure . Left) (runIOExcept . f)
18− case x' of
19− Right a => let (IOM ka) = k a in
20− ka
21− Left err => return (Left err))
22
18
23ioe_lift : IO a -> IOExcept err a
19ioe_lift : IO a -> IOExcept err a
24−ioe_lift op = IOM (do op' <- op
20+ioe_lift op = IOM $ map Right op
25− return (Right op'))
26
21
27ioe_fail : err -> IOExcept err a
22ioe_fail : err -> IOExcept err a
28−ioe_fail e = IOM (return (Left e))
23+ioe_fail e = IOM $ pure (Left e)
29
24
30ioe_run : IOExcept err a -> (err -> IO b) -> (a -> IO b) -> IO b
25ioe_run : IOExcept err a -> (err -> IO b) -> (a -> IO b) -> IO b
31−ioe_run (IOM act) err ok = do act' <- act
26+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
libs/effects/Effects.idr+5
@@ -245,6 +245,11 @@ pureM = Value
245(<*>) prog v = do fn <- prog
245(<*>) prog v = do fn <- prog
246 arg <- v
246 arg <- v
247 return (fn arg)
247 return (fn arg)
248+
249+(*>) : EffM m a xs (\v => xs) ->
250+ EffM m b xs (\v => xs) -> EffM m b xs (\v => xs)
251+a *> b = do a
252+ b
248
253
249new : Handler e' m => (e : EFFECT) -> resTy ->
254new : Handler e' m => (e : EFFECT) -> resTy ->
250 {auto prf : e = MkEff resTy e'} ->
255 {auto prf : e = MkEff resTy e'} ->