0 | module Data.Linear.Sink
 1 |
 2 | import Data.Contravariant
 3 | import Data.Linear.Deferred
 4 | import Data.Linear.Ref1
 5 | import Syntax.T1
 6 | import public Data.Linear.Token
 7 |
 8 | %default total
 9 |
10 | ||| A `Sink` is a primitive consumer of values.
11 | public export
12 | record Sink o where
13 |   [noHints]
14 |   constructor S
15 |   sink1 : o -> IO1 ()
16 |
17 | ||| A `Sink` is a contravariant functor.
18 | export %inline
19 | cmap : (b -> a) -> Sink a -> Sink b
20 | cmap f (S g) = S $ g . f
21 |
22 | export %inline
23 | Contravariant Sink where
24 |   contramap = cmap
25 |
26 | ||| Create a `Sink` that collects values in a mutable
27 | ||| reference holding a `SnocList`.
28 | |||
29 | ||| The current content of the sink can be read and cleared
30 | ||| by invoking the given linear action.
31 | |||
32 | ||| The returned sink is thread-safe: Values from multiple
33 | ||| threads can be written to it.
34 | export
35 | snocSink1 : (0 a : Type) -> IO1 (Sink a, IO1 (List a))
36 | snocSink1 a = T1.do
37 |   ref <- ref1 [<]
38 |   pure (S $ \v => casmod1 ref (:< v), readList ref)
39 |   where
40 |     readList : IORef (SnocList a) -> IO1 (List a)
41 |     readList ref = casupdate1 ref $ \sv => ([<], sv <>> [])
42 |
43 | export
44 | Semigroup (Sink a) where
45 |   S s1 <+> S s2 = S $ \v,t => let _ # t := s1 v t in s2 v t
46 |
47 | export
48 | Monoid (Sink a) where
49 |   neutral = S $ \_,t => () # t
50 |
51 | export %inline
52 | sink : HasIO io => (s : Sink a) => a -> io ()
53 | sink = runIO . s.sink1
54 |
55 | export %inline
56 | sinkAs : HasIO io => (0 a : Type) -> (s : Sink a) => a -> io ()
57 | sinkAs a = sink
58 |
59 | export %inline
60 | sinkTo : HasIO io => (s : Sink a) -> a -> io ()
61 | sinkTo s = runIO . s.sink1
62 |
63 | export %inline
64 | onceSink : Once World t -> Sink t
65 | onceSink o = S (putOnce1 o)
66 |
67 | export %inline
68 | deferredSink : Deferred World t -> Sink t
69 | deferredSink o = S (putDeferred1 o)
70 |