0 | module FS.Concurrent.Util
 1 |
 2 | import Data.Linear.Deferred
 3 | import FS.Pull
 4 | import IO.Async
 5 |
 6 | %default total
 7 |
 8 | ||| Awaits the completion of a `Deferred`, wrapping the
 9 | ||| result with the potential of failure.
10 | export %inline
11 | awaitRes : Deferred World (Result es a) -> Async e es a
12 | awaitRes def = await def >>= fromResult
13 |
14 | ||| Finalizes a deferred in case of an `Error` outcome.
15 | export
16 | putErr : Deferred World (Result es ()) -> Outcome es () -> Async e [] ()
17 | putErr def (Error x) = putDeferred def (Left x)
18 | putErr def _         = pure ()
19 |
20 | ||| Concurrently runs the given stream until it either terminates or
21 | ||| is interrupted by `check`.
22 | |||
23 | ||| This is a low-level utility used to implement the combinators in this
24 | ||| module. It is exported, because it might be useful when
25 | ||| implementing other combinators,
26 | export
27 | parrunCase :
28 |      (check   : Deferred World a)
29 |   -> (finally : Outcome fs () -> Async e [] ())
30 |   -> EmptyStream (Async e) fs
31 |   -> Async e es (Fiber [] ())
32 | parrunCase check finally p =
33 |   assert_total $ start $ ignore $
34 |     guaranteeCase (raceOutcome {es = []} (await check) (pull p)) $ \case
35 |       -- Succeeded res => finally res
36 |       -- Canceled      => finally Canceled
37 |       -- Error err impossible
38 |       Succeeded (Left _) => finally Canceled
39 |       Succeeded (Right $ Succeeded o) => finally o
40 |       Succeeded (Right x) => finally Canceled
41 |       Canceled  => finally Canceled
42 |       Error _ impossible
43 |
44 | ||| Concurrently runs the given stream until it either terminates or
45 | ||| is interrupted by `check`.
46 | |||
47 | ||| This is a low-level utility used to implement the combinators in this
48 | ||| module. It is exported, because it might be useful when
49 | ||| implementing other combinators,
50 | export %inline
51 | parrun :
52 |      (check   : Deferred World a)
53 |   -> (finally : Async e [] ())
54 |   -> EmptyStream (Async e) fs
55 |   -> Async e es (Fiber [] ())
56 | parrun check = parrunCase check . const
57 |