0 | module IO.Async.Service
 1 |
 2 | import Data.Linear.Deferred
 3 | import IO.Async
 4 | import IO.Async.Channel
 5 |
 6 | %default total
 7 |
 8 | --------------------------------------------------------------------------------
 9 | -- Service
10 | --------------------------------------------------------------------------------
11 |
12 | ||| A `Service` describes an asynchronous, effectful convertion from
13 | ||| "requests" to (dependently typed) "responses" with the potential
14 | ||| of failing with one of the given error types.
15 | |||
16 | ||| A `Service` is a resource that should be properly released once it
17 | ||| is no longer needed.
18 | public export
19 | record Service (e : Type) (errs : List Type) (req : Type) (resp : req -> Type) where
20 |   [noHints]
21 |   constructor MkService
22 |   close : Async e [] ()
23 |   send  : (r : req) -> Async e errs (resp r)
24 |
25 | export %inline
26 | Resource (Async e) (Service e es a p) where cleanup = close
27 |
28 | record Req (errs : List Type) (a : Type) (p : a -> Type) where
29 |   constructor R
30 |   req  : a
31 |   resp : Once World (Result errs $ p req)
32 |
33 | parameters {0 a,e    : Type}
34 |            {default 100 capacity : Nat}
35 |            (0 p      : a -> Type)
36 |
37 |   ||| Sets up a stateful service that runs continuously in the background
38 |   ||| until it is finally closed.
39 |   export covering
40 |   service :
41 |        s
42 |     -> (s -> (v : a) -> Async e es (s, p v))
43 |     -> Async e fs (Service e es a p)
44 |   service ini conv = do
45 |     chnl <- channelOf (Req es a p) capacity
46 |     fbr  <- start (go ini chnl)
47 |     pure $ MkService (close chnl >> wait fbr) (snd chnl)
48 |  
49 |    where
50 |      -- loops until the channel is closed
51 |      go : s -> Channel (Req es a p) -> Async e [] ()
52 |      go st chnl = do
53 |        Just (R req o) <- receive chnl | Nothing => pure ()
54 |        attempt (conv st req) >>= \case
55 |          Left x        => putOnce o (Left x)  >> go st  chnl
56 |          Right (st2,r) => putOnce o (Right r) >> go st2 chnl
57 |
58 |      snd : Channel (Req es a p) -> (v : a) -> Async e es (p v)
59 |      snd chnl v = do
60 |        o <- onceOf (Result es $ p v)
61 |        send chnl (R v o) >>= \case
62 |          Closed => canceled >> never
63 |          _      => awaitOnce o >>= either fail pure
64 |
65 |   ||| Sets up a stateless service that runs continuously in the background
66 |   ||| until it is finally closed.
67 |   export covering
68 |   stateless : ((v : a) -> Async e es (p v)) -> Async e fs (Service e es a p)
69 |   stateless f = service () $ \_,v => ((),) <$> f v
70 |
71 |   ||| Sets up a stateful service that runs continuously in the background
72 |   ||| until it is finally closed.
73 |   export covering
74 |   stateful : s -> (s -> (v : a) -> (s, p v)) -> Async e fs (Service e es a p)
75 |   stateful ini conv = service ini $ \x,st => pure $ conv x st
76 |