0 | ||| A `Deferred s` value, is an observable, initially empty
  1 | ||| reference that can be set exactly once. As such, it is an
  2 | ||| important synchronization primitive.
  3 | |||
  4 | ||| As with other mutable references, `Deferred` values can be safely used
  5 | ||| in pure code as long as they are used locally in state thread.
  6 | module Data.Linear.Deferred
  7 |
  8 | import public Data.Linear.Token
  9 | import Data.Linear.Ref1
 10 | import Data.Linear.Traverse1
 11 | import Data.Linear.Unique
 12 | import Data.SortedMap
 13 |
 14 | %default total
 15 |
 16 | --------------------------------------------------------------------------------
 17 | -- Once
 18 | --------------------------------------------------------------------------------
 19 |
 20 | -- internal state of a `Once` value
 21 | data ST1 : Type -> Type -> Type where
 22 |   Ini1 : ST1 s a
 23 |   Val1 : (v : a) -> ST1 s a
 24 |   Obs1 : (cb : a -> F1' s) -> ST1 s a
 25 |
 26 | ||| An atomic reference that can be set exactly once and observed
 27 | ||| by at most one observer. All operations on `Once` are thread-safe.
 28 | |||
 29 | ||| There are many occasions when it is enough to be able to register
 30 | ||| only one observer. Use `Once` for these, and use `Deferred` in
 31 | ||| case you need to register many observers.
 32 | export
 33 | record Once s a where
 34 |   constructor O
 35 |   ref : Ref s (ST1 s a)
 36 |
 37 | ||| Creates a new, empty `Once`.
 38 | export %inline
 39 | once1 : F1 s (Once s a)
 40 | once1 t = let ref # t := ref1 Ini1 t in O ref # t
 41 |
 42 | ||| Convenience alias of `once1`, which takes the type of
 43 | ||| the value stored as an explicit argument.
 44 | export %inline
 45 | onceOf1 : (0 a : _) -> F1 s (Once s a)
 46 | onceOf1 _ = once1
 47 |
 48 | ||| Returns `True` if a value has been set at the given `Once`.
 49 | export %inline
 50 | completedOnce1 : Once s a -> F1 s Bool
 51 | completedOnce1 (O r) t =
 52 |   let Val1 _ # t := read1 r t | _ # t => False # t
 53 |    in True # t
 54 |
 55 | ||| Reads the set value of a `Once`. Returns `Nothing`,
 56 | ||| if no value has been set yet.
 57 | export
 58 | peekOnce1 : Once s a -> F1 s (Maybe a)
 59 | peekOnce1 (O ref) t =
 60 |   let Val1 x # t := read1 ref t | _ # t => Nothing # t
 61 |    in Just x # t
 62 |
 63 | ||| Atomically tries to write the given value to a `Once`.
 64 | |||
 65 | ||| The value is written if and only if no other value has
 66 | ||| been set first. If an observer has been registered, it will be
 67 | ||| invoked immediately.
 68 | export
 69 | putOnce1 : Once s a -> (v : a) -> F1' s
 70 | putOnce1 (O ref) v t = assert_total $ let x # t := read1 ref t in go x x t
 71 |
 72 |   where
 73 |     go : ST1 s a -> ST1 s a -> F1' s
 74 |     go x Ini1 t =
 75 |       case caswrite1 ref x (Val1 v) t of
 76 |         True # t => () # t
 77 |         _    # t => putOnce1 (O ref) v t
 78 |     go x (Val1 _)  t = () # t
 79 |     go x (Obs1 cb) t =
 80 |       case caswrite1 ref x (Val1 v) t of
 81 |         True # t => cb v t
 82 |         _    # t => putOnce1 (O ref) v t
 83 |
 84 | unobs : Once s a -> F1' s
 85 | unobs (O ref) t =
 86 |   assert_total $ let x # t := read1 ref t in go x x t
 87 |   where
 88 |     go : ST1 s a -> ST1 s a -> F1' s
 89 |     go x (Obs1 cb) t =
 90 |       case caswrite1 ref x Ini1 t of
 91 |         True # t => () # t
 92 |         _    # t => unobs (O ref) t
 93 |     go x _ t = () # t
 94 |
 95 | ||| Observe a `Once` by installing a callback.
 96 | |||
 97 | ||| The callback is invoked immediately in case the value has
 98 | ||| already been set.
 99 | |||
100 | ||| The action that is returned by this function can be used to
101 | ||| unregister the observer.
102 | |||
103 | ||| Note: `Once` values can only be observed
104 | |||       by one observer. Use `Deferred` in case you need to install
105 | |||       many observers. In case another observer has already been set,
106 | |||       this is a no-op and the callback never invoked.
107 | export
108 | observeOnce1 : Once s a -> (a -> F1' s) -> F1 s (F1' s)
109 | observeOnce1 (O ref) cb t = assert_total $ let x # t := read1 ref t in go x x t
110 |   where
111 |     go : ST1 s a -> ST1 s a -> F1 s (F1' s)
112 |     go x (Val1 v) t = let _ # t := cb v t in unit1 # t
113 |     go x Ini1     t =
114 |       case caswrite1 ref x (Obs1 cb) t of
115 |         True # t => unobs (O ref) # t
116 |         _    # t => observeOnce1 (O ref) cb t
117 |     go x _        t = unit1 # t
118 |
119 | --------------------------------------------------------------------------------
120 | -- Deferred
121 | --------------------------------------------------------------------------------
122 |
123 | -- internal state of a `Deferred` value
124 | data ST : Type -> Type -> Type where
125 |   Val : (v : a) -> ST s a
126 |   Obs : (cbs : SortedMap (Token s) (a -> F1' s)) -> ST s a
127 |
128 | ||| An atomic reference that can be set exactly once and observed
129 | ||| by an arbitrary number of observers. Any operations on a `Deferred`
130 | ||| are thread-safe.
131 | export
132 | record Deferred s a where
133 |   constructor D
134 |   ref : Ref s (ST s a)
135 |
136 | ||| Creates a new, empty `Deferred s a`.
137 | export %inline
138 | deferred1 : F1 s (Deferred s a)
139 | deferred1 t = let ref # t := ref1 (Obs empty) t in D ref # t
140 |
141 | ||| Convenience alias of `deferred1`, which takes the type of
142 | ||| the value stored as an explicit argument.
143 | export %inline
144 | deferredOf1 : (0 a : _) -> F1 s (Deferred s a)
145 | deferredOf1 _ = deferred1
146 |
147 | ||| Returns `True` if a value has been set at the given `Deferred`.
148 | export %inline
149 | completed1 : Deferred s a -> F1 s Bool
150 | completed1 (D r) t =
151 |   let Val _ # t := read1 r t | _ # t => False # t
152 |    in True # t
153 |
154 | ||| Reads the set value of a `Deferred`. Returns `Nothing`,
155 | ||| if no value has been set yet.
156 | export
157 | peekDeferred1 : Deferred s a -> F1 s (Maybe a)
158 | peekDeferred1 (D ref) t =
159 |   let Val x # t := read1 ref t | _ # t => Nothing # t
160 |    in Just x # t
161 |
162 | ||| Atomically tries to write the given value to a `Deferred`.
163 | |||
164 | ||| The value is written if and only if no other values has
165 | ||| been set first. Any observers will be invoked immediately.
166 | export
167 | putDeferred1 : Deferred s a -> (v : a) -> F1' s
168 | putDeferred1 (D r) v t = assert_total $ let x # t := read1 r t in go x x t
169 |
170 |   where
171 |     go : ST s a -> ST s a -> F1' s
172 |     go x (Val _)   t = () # t
173 |     go x (Obs cbs) t =
174 |      let True # t := caswrite1 r x (Val v) t | _ # t => putDeferred1 (D r) v t
175 |       in traverse1_ (\cb => cb v) (Prelude.toList cbs) t
176 |
177 | unobsDef : Deferred s a -> Token s -> F1 s ()
178 | unobsDef (D r) tok t = assert_total $ let x # t := read1 r t in go x x t
179 |   where
180 |     go : ST s a -> ST s a -> F1' s
181 |     go x (Val _)   t = () # t
182 |     go x (Obs cbs) t =
183 |       case caswrite1 r x (Obs $ delete tok cbs) t of
184 |         True # t => () # t
185 |         _    # t => unobsDef (D r) tok t
186 |
187 | ||| Observe a `Deferred` by installing a callback using the given
188 | ||| token for identification.
189 | |||
190 | ||| The callback is invoked immediately in case the value has
191 | ||| already been set.
192 | |||
193 | ||| The action that is returned by this function can be used to
194 | ||| unregister the observer.
195 | export
196 | observeDeferredAs1 : Deferred s a -> Token s -> (a -> F1' s) -> F1 s (F1' s)
197 | observeDeferredAs1 (D r) tok cb t =
198 |   assert_total $ let x # t := read1 r t in go x x t
199 |   where
200 |     go : ST s a -> ST s a -> F1 s (F1' s)
201 |     go x (Val v)   t = let _ # t := cb v t in unit1 # t
202 |     go x (Obs cbs) t =
203 |      case caswrite1 r x (Obs $ insert tok cb cbs) t of
204 |        True # t => unobsDef (D r) tok # t
205 |        _    # t => observeDeferredAs1 (D r) tok cb t
206 |
207 | ||| Observe a `Deferred` by installing a callback.
208 | |||
209 | ||| The callback is invoked immediately in case the value has
210 | ||| already been set.
211 | |||
212 | ||| The action that is returned by this function can be used to
213 | ||| unregister the observer.
214 | export %inline
215 | observeDeferred1 : Deferred s a -> (a -> F1' s) -> F1 s (F1' s)
216 | observeDeferred1 def cb t =
217 |   let tok # t := token1 t
218 |    in observeDeferredAs1 def tok cb t
219 |
220 | --------------------------------------------------------------------------------
221 | -- Lift1 Utilities
222 | --------------------------------------------------------------------------------
223 |
224 | ||| Lifted version of `once1`
225 | export %inline
226 | once : Lift1 s f => f (Once s a)
227 | once = lift1 once1
228 |
229 | ||| Lifted version of `onceOf`
230 | export %inline
231 | onceOf : Lift1 s f => (0 a : _) -> f (Once s a)
232 | onceOf _ = once
233 |
234 | ||| Lifted version of `peekOnce1`
235 | export %inline
236 | peekOnce : Lift1 s f => Once s a -> f (Maybe a)
237 | peekOnce o = lift1 $ peekOnce1 o
238 |
239 | ||| Lifted version of `completedOnce1`
240 | export %inline
241 | completedOnce : Lift1 s f => Once s a -> f Bool
242 | completedOnce d = lift1 $ completedOnce1 d
243 |
244 |
245 | ||| Lifted version of `putOnce1`
246 | export %inline
247 | putOnce : Lift1 s f => Once s a -> (v : a) -> f ()
248 | putOnce o v = lift1 $ putOnce1 o v
249 |
250 | ||| Lifted version of `completed1`
251 | export %inline
252 | completed : Lift1 s f => Deferred s a -> f Bool
253 | completed d = lift1 $ completed1 d
254 |
255 | ||| Lifted version of `deferred1`
256 | export %inline
257 | deferred : Lift1 s f => f (Deferred s a)
258 | deferred = lift1 deferred1
259 |
260 | ||| Lifted version of `deferredOf1`
261 | export %inline
262 | deferredOf : Lift1 s f => (0 a : _) -> f (Deferred s a)
263 | deferredOf _ = deferred
264 |
265 | ||| Lifted version of `peekDeferred1`
266 | export %inline
267 | peekDeferred : Lift1 s f => Deferred s a -> f (Maybe a)
268 | peekDeferred d = lift1 $ peekDeferred1 d
269 |
270 | ||| Lifted version of `putDeferred1`
271 | export %inline
272 | putDeferred : Lift1 s f => Deferred s a -> (v : a) -> f ()
273 | putDeferred d v = lift1 $ putDeferred1 d v
274 |