0 | module Control.RIO.App
 1 |
 2 | import public Data.List.Quantifiers.Extra
 3 | import public Control.RIO
 4 | import System
 5 |
 6 | %default total
 7 |
 8 | --------------------------------------------------------------------------------
 9 | --          App : A RIO with several possible error types
10 | --------------------------------------------------------------------------------
11 |
12 | ||| A `RIO` computation, which can fail with one of several errors.
13 | public export
14 | 0 App : (xs : List Type) -> (a : Type) -> Type
15 | App xs a = RIO (HSum xs) a
16 |
17 | --------------------------------------------------------------------------------
18 | --          Throwing and injection computations that can fail
19 | --------------------------------------------------------------------------------
20 |
21 | ||| Throw an exception to be caught in the `App` monad.
22 | |||
23 | ||| The error type has to be in the list of accepted errors.
24 | export
25 | throw : Has x xs => (err : x) -> App xs a
26 | throw err = fail (inject err)
27 |
28 | ||| Inject a `RIO` computation into one dealing with several
29 | ||| possible errors.
30 | export
31 | injectRIO : Has x xs => RIO x a -> App xs a
32 | injectRIO = mapFst inject
33 |
34 | ||| Inject an `Either x a` computation into a `RIO` monad dealing
35 | ||| with several possible errors.
36 | export
37 | injectEither : Has x xs => Either x a -> App xs a
38 | injectEither (Left v)  = throw v
39 | injectEither (Right v) = pure v
40 |
41 | ||| Inject an `IO (Either x a)` computation into a `RIO` monad dealing
42 | ||| with several possible errors.
43 | export
44 | injectIO : Has x xs => IO (Either x a) -> App xs a
45 | injectIO = injectRIO . liftEitherIO
46 |
47 | --------------------------------------------------------------------------------
48 | --          Error handling
49 | --------------------------------------------------------------------------------
50 |
51 | ||| An error handler.
52 | public export
53 | 0 Handler : (a,x : Type) -> Type
54 | Handler a x = x -> RIO Void a
55 |
56 | ||| Handle a single error type in an application.
57 | |||
58 | ||| This removes the error type from the list of possible errors
59 | ||| in the resulting `App` type.
60 | export
61 | handle : (prf : Has x xs) => Handler a x -> App xs a -> App (xs - x) a
62 | handle f =
63 |   catch $ \u =>
64 |     case map f (decomp @{prf} u) of
65 |       Left y  => fail y
66 |       Right y => lift y
67 |
68 | hall : (prf : All (Handler a) ts) => HSum ts -> RIO Void a
69 | hall @{h :: t} (Here v)  = h v
70 | hall @{h :: t} (There v) = hall v
71 | hall @{[]}     x         = absurd x
72 |
73 | ||| Handle all errors, converting the computation to one that cannot fail.
74 | export
75 | handleAll : (prf : All (Handler a) xs) => App xs a -> RIO Void a
76 | handleAll = catch $ \u => hall u
77 |
78 | ||| Handle all errors, converting the computation to one that cannot fail.
79 | |||
80 | ||| This yields the provided default value in case of an error.
81 | export
82 | handleAllDflt : (prf : All (Handler ()) xs) => a -> App xs a -> RIO Void a
83 | handleAllDflt v = handleAll @{mapProperty (($> v) .) prf}
84 |
85 | ||| Run an application handling all errors. This can be invoked
86 | ||| directly from  an applcation's `main` function. It invokes
87 | ||| `exitFailure` in case of an error.
88 | export
89 | runApp : All (Handler ()) xs -> App xs () -> IO ()
90 | runApp hs app = do
91 |   True <- run $ catch (\u => hall @{hs} u $> False) (app $> True)
92 |     | False => exitFailure
93 |   exitSuccess
94 |