0 | module Control.Cont.Exception
 1 |
 2 | import Control.EffectAlgebra
 3 |
 4 | import Control.Monad.Free
 5 |
 6 | public export
 7 | data EitherC : Type -> (Type -> Type) -> Type -> Type where
 8 |   Throw : e -> EitherC e m a
 9 |   Catch : forall t. m t -> (e -> m t) -> (t -> m a) -> EitherC e m a
10 |
11 | public export
12 | Functor m => Functor (EitherC e m) where
13 |   map f (Throw e) = Throw e
14 |   map f (Catch p h k) = Catch p h (map f . k)
15 |
16 | public export
17 | HFunctor (EitherC e) where
18 |   hmap t (Throw x) = Throw x
19 |   hmap t (Catch p h k) = Catch (t p) (t . h) (t . k)
20 |
21 | public export
22 | Syntax (EitherC e) where
23 |   emap f (Throw e) = Throw e
24 |   emap f (Catch p h k) = Catch p h (f . k)
25 |
26 |   weave f hdl (Throw x) = Throw x
27 |   weave f hdl (Catch p h k) =
28 |     Catch (hdl (map (const p) f))
29 |           (\e => hdl (map (const (h e)) f))
30 |           (hdl . map k)
31 |
32 | public export
33 | runEitherC : Syntax sig
34 |       => Free (EitherC e :+: sig) a
35 |       -> Free sig (Either e a)
36 | runEitherC (Return x) = Return (Right x)
37 | runEitherC (Op (Inl (Throw x))) = Return (Left x)
38 | runEitherC (Op (Inl (Catch p h k))) = do
39 |   r <- runEitherC p
40 |   case r of
41 |     Left e => do
42 |       r <- runEitherC (h e)
43 |       case r of
44 |         Left e => Return (Left e)
45 |         Right x => runEitherC (k x)
46 |     Right x => runEitherC (k x)
47 | runEitherC (Op (Inr op)) = Op (weave {s = Either e} (Right ()) hdl op) where
48 |   hdl : Handler (Either e) (Free (EitherC e :+: sig)) (Free sig)
49 |   hdl = either (Return . Left) runEitherC
50 |
51 | public export
52 | throw : (Inj (EitherC e) sig) => e -> Free sig a
53 | throw err = inject {sub = EitherC e} (Throw err)
54 |
55 | public export
56 | catch : (p : Inj (EitherC e) sig) => Free sig a -> (e -> Free sig a) -> Free sig a
57 | catch p h = inject {sub = EitherC e} (Catch p h Return)
58 |
59 | public export
60 | orThrow : Syntax sig => Inj (EitherC e) sig => Maybe a -> Free sig e -> Free sig a
61 | orThrow Nothing e  = e >>= throw
62 | orThrow (Just x) e = return x
63 |