0 | ||| Various utility combinators.
  1 | |||
  2 | ||| A note on arrow operators: Arrow operators in this module are
  3 | ||| of the form `i>o`, where `i` is either `>`, `^`, `!`, or `?`.
  4 | ||| and `o` is either `>`, `^`, `!`, or `-`. Each of these symbols
  5 | ||| describe a different type of arrow-like function at the
  6 | ||| corresponding end of the operator:
  7 | |||
  8 | ||| The following table lists the meaning of symbols
  9 | |||
 10 | ||| | Symbol      | Meaning                  | Example                    |
 11 | ||| |-------------|--------------------------|----------------------------|
 12 | ||| | `>`         | An MSF                   | arr (*2) >>> arrM printLn  |
 13 | ||| | `^`         | a pure function          | (*2) ^>> printLn           |
 14 | ||| | `!`         | an effectful computation | arr (*2) >>! printLn       |
 15 | |||
 16 | ||| In addition, symbol `?` corresponds to an event stream input, and
 17 | ||| symbol `-` describes fanning out to a list of sinks:
 18 | |||
 19 | ||| ```idris example
 20 | ||| when (> 10) ?>- [ arrM printLn, put ]
 21 | ||| ```
 22 | module Data.MSF.Util
 23 |
 24 | import Data.List
 25 | import Data.MSF.Core
 26 |
 27 | --------------------------------------------------------------------------------
 28 | --          Sequencing Utilities
 29 | --------------------------------------------------------------------------------
 30 |
 31 | export infixr 1 ^>>, >>^, >>!, !>>, ?>>, >>-, ^>-, !>-, ?>-
 32 |
 33 | ||| Sequencing of an MSF and a pure function
 34 | export %inline
 35 | (>>^) : MSF m i o -> (o -> o2) -> MSF m i o2
 36 | sf >>^ f = sf >>> arr f
 37 |
 38 | ||| Sequencing of a pure function and an MSF
 39 | export %inline
 40 | (^>>) : (i -> i2) -> MSF m i2 o -> MSF m i o
 41 | f ^>> sf = arr f >>> sf
 42 |
 43 | ||| Sequencing of an MSF and an effectful computation
 44 | export %inline
 45 | (>>!) : MSF m i o -> (o -> m o2) -> MSF m i o2
 46 | sf >>! f = sf >>> arrM f
 47 |
 48 | ||| Sequencing of an effectful computation and an MSF
 49 | export %inline
 50 | (!>>) : (i -> m i2) -> MSF m i2 o -> MSF m i o
 51 | f !>> sf = arrM f >>> sf
 52 |
 53 | --------------------------------------------------------------------------------
 54 | --          Paralellising Utilities
 55 | --------------------------------------------------------------------------------
 56 |
 57 | ||| Like `fan` but discards the results.
 58 | ||| This is mainly useful for broadcasting to data sinks
 59 | ||| (streaming functions that do not produce any interesting
 60 | ||| output).
 61 | |||
 62 | ||| TODO: Should we require a proof here that `os` is a list
 63 | |||       of `Unit`?
 64 | export %inline
 65 | fan_ : FanList m i os -> MSF m i ()
 66 | fan_ sfs = Fan sfs >>> Const ()
 67 |
 68 | ||| Broadcasting an MSF to a list of sinks
 69 | export %inline
 70 | (>>-) : MSF m i x -> FanList m x os -> MSF m i ()
 71 | sf >>- sfs = sf >>> fan_ sfs
 72 |
 73 | ||| Broadcasting a pure function to a list of sinks
 74 | export %inline
 75 | (^>-) : (i -> x) -> FanList m x os -> MSF m i ()
 76 | f ^>- sfs = arr f >>> fan_ sfs
 77 |
 78 | ||| Broadcasting an effectful computation to a list of sinks
 79 | export %inline
 80 | (!>-) : (i -> m x) -> FanList m x os -> MSF m i ()
 81 | f !>- sfs = arrM f >>> fan_ sfs
 82 |
 83 | ||| Extract the first argument from an MSF taking a pair
 84 | ||| of input values.
 85 | export
 86 | firstArg : MSF m (HList [x,i]) o -> x -> MSF m i o
 87 | firstArg sf vx = fan [const vx, id] >>> sf
 88 |
 89 | ||| Extract the second argument from an MSF taking a pair
 90 | ||| of input values.
 91 | export
 92 | secondArg : MSF m (HList [i,x]) o -> x -> MSF m i o
 93 | secondArg sf vx = fan [id, const vx] >>> sf
 94 |
 95 | ||| Extract the first value of an n-ary product
 96 | export
 97 | hd : MSF m (HList (i :: t)) i
 98 | hd = arr $ \(h::_) => h
 99 |
100 | ||| Extract the tail of an n-ary product
101 | export
102 | tl : MSF m (HList (i :: t)) (HList t)
103 | tl = arr $ \(_::t) => t
104 |
105 | ||| Extract the second value of an n-ary product
106 | export
107 | snd : MSF m (HList (i :: i2 :: t)) i2
108 | snd = arr $ \(_ :: v :: _) => v
109 |
110 | ||| Swaps a pair of input values
111 | export
112 | swap : MSF m (HList [a,b]) (HList [b,a])
113 | swap = arr $ \[va,vb] => [vb,va]
114 |
115 | --------------------------------------------------------------------------------
116 | --          Selecting Utilities
117 | --------------------------------------------------------------------------------
118 |
119 | ||| Convert an `Either` input to a binary sum, which
120 | ||| can then be sequenced with a call to `choice` or `collect`.
121 | export
122 | either : MSF m (Either i1 i2) (HSum [i1,i2])
123 | either = arr $ either Here (There . Here)
124 |
125 | ||| Run the given MSF only if the input is a `Left`.
126 | export
127 | ifLeft : Monoid o => MSF m i o -> MSF m (Either i a) o
128 | ifLeft sf = either >>> collect [sf, neutral]
129 |
130 | ||| Run the given MSF only if the input is a `Right`.
131 | export
132 | ifRight : Monoid o => MSF m i o -> MSF m (Either a i) o
133 | ifRight sf = either >>> collect [neutral, sf]
134 |
135 | ||| Convert an `Maybe` input to a binary sum, which
136 | ||| can then be sequenced with a call to `choice` or `collect`.
137 | export
138 | maybe :  MSF m (Maybe i) (HSum [i,()])
139 | maybe = arr $ maybe (There $ Here ()) Here
140 |
141 | ||| Run the given MSF only if the input is a `Just`.
142 | export
143 | ifJust : Monoid o => MSF m i o -> MSF m (Maybe i) o
144 | ifJust sf = maybe >>> collect [sf, neutral]
145 |
146 | ||| Run the given MSF only if the input is a `Nothing`.
147 | export
148 | ifNothing : Monoid o => MSF m () o -> MSF m (Maybe i) o
149 | ifNothing sf = maybe >>> collect [neutral, sf]
150 |
151 | ||| Convert an input to a binary sum, depending on whether
152 | ||| the given predicate returns `True` or `False`. The result
153 | ||| can then be sequenced with a call to `choice` or `collect`.
154 | export
155 | bool : (f : i -> Bool) -> MSF m i (HSum [i,i])
156 | bool f = arr $ \vi => if f vi then Here vi else (There $ Here vi)
157 |
158 | ||| Run the given MSF only if the predicate holds for the input.
159 | export
160 | ifTrue : Monoid o => (f : i -> Bool) -> MSF m i o -> MSF m i o
161 | ifTrue f sf = bool f >>> collect [sf, neutral]
162 |
163 | ||| Run the given MSF only if the predicate does not hold for the input.
164 | export
165 | ifFalse : Monoid o => (f : i -> Bool) -> MSF m i o -> MSF m i o
166 | ifFalse f sf = bool f >>> collect [neutral, sf]
167 |
168 | ||| Run the given MSF only if the input equlas the given value
169 | export
170 | ifIs : Eq i => Monoid o => (v : i) -> MSF m i o -> MSF m i o
171 | ifIs v = ifTrue (v ==)
172 |
173 | ||| Run the given MSF only if the input does not equal the given value
174 | export
175 | ifIsNot : Eq i => Monoid o => (v : i) -> MSF m i o -> MSF m i o
176 | ifIsNot v = ifFalse (v ==)
177 |
178 | --------------------------------------------------------------------------------
179 | --          Looping Utilities
180 | --------------------------------------------------------------------------------
181 |
182 | ||| Uses the given value as a seed for feeding back output
183 | ||| of the MSF back to its input.
184 | export
185 | feedback_ : s -> MSF m (HList [s,i]) s -> MSF m i ()
186 | feedback_ v sf = feedback v $ sf >>^ (:: [()])
187 |
188 | ||| Delay a stream by one sample.
189 | export %inline
190 | iPre : o -> MSF m o o
191 | iPre v = feedback v swap
192 |
193 | ||| Applies a function to the input and an accumulator,
194 | ||| outputting the updated accumulator.
195 | export
196 | accumulateWith : (i -> o -> o) -> o -> MSF m i o
197 | accumulateWith f ini = feedback ini (arr g)
198 |
199 |   where
200 |     g : HList [o,i] -> HList [o,o]
201 |     g [acc,inp] = let acc' = f inp acc in [acc',acc']
202 |
203 | ||| Counts the number of scans of the signal function.
204 | export
205 | count : Num n => MSF m i n
206 | count = const 1 >>> accumulateWith (+) 0
207 |
208 | ||| Accumulate the inputs, starting from an initial value.
209 | export
210 | appendFrom : Semigroup v => v -> MSF m v v
211 | appendFrom = accumulateWith (<+>)
212 |
213 | ||| Accumulate the inputs, starting from `neutral`
214 | export
215 | append : Monoid n => MSF m n n
216 | append = appendFrom neutral
217 |
218 | ||| Applies a transfer function to the input and an accumulator,
219 | ||| returning the updated accumulator and output.
220 | export
221 | mealy : (i -> s -> HList [s,o]) -> s -> MSF m i o
222 | mealy f s0 = feedback s0 (arr $ \[s,i] => f i s)
223 |
224 | ||| Unfolds a function over an initial state
225 | ||| value.
226 | export
227 | unfold : (s -> HList [s,o]) -> s -> MSF m i o
228 | unfold f ini = feedback ini (arr $ \(h::_) => f h)
229 |
230 | ||| Generates output using a step-wise generation function and an initial
231 | ||| value. Version of 'unfold' in which the output and the new accumulator
232 | ||| are the same.
233 | export
234 | repeatedly : (o -> o) -> o -> MSF m i o
235 | repeatedly f = unfold $ \vo => let vo2 = f vo in [vo2,vo2]
236 |
237 | ||| Cycles through the given non-empty list of values.
238 | export
239 | cycle : (vs : List o) -> {auto 0 prf : NonEmpty vs} -> MSF m i o
240 | cycle (h :: t) = unfold next (h :: t)
241 |
242 |   where
243 |     next : List o -> HList [List o, o]
244 |     next Nil        = [t,h]
245 |     next (h' :: t') = [t',h']
246 |
247 | --------------------------------------------------------------------------------
248 | --          Observing Streaming Functions
249 | --------------------------------------------------------------------------------
250 |
251 | ||| Observe input values through the given sink.
252 | export
253 | observeWith : MSF m i () -> MSF m i i
254 | observeWith sf = fan [id,sf] >>> hd
255 |
256 | ||| Run the given effectful computation on each input.
257 | export %inline
258 | withEffect : (i -> m ()) -> MSF m i i
259 | withEffect = observeWith . arrM
260 |
261 | ||| Run the given monadic action on each input.
262 | export %inline
263 | runEffect : m () -> MSF m i i
264 | runEffect = withEffect . const
265 |
266 | --------------------------------------------------------------------------------
267 | --          Event Streams
268 | --------------------------------------------------------------------------------
269 |
270 | ||| The empty event stream that never fires an event
271 | export
272 | never : MSF m i (Event o)
273 | never = const NoEv
274 |
275 | ||| Convert an event stream to a streaming function
276 | ||| holding the value of the last event fired starting
277 | ||| from the given initial value.
278 | export
279 | hold : o -> MSF m (Event o) o
280 | hold = accumulateWith (\ev,v => fromEvent v ev)
281 |
282 | ||| Fire the given event `n` times.
283 | export
284 | ntimes : Nat -> o -> MSF m i (Event o)
285 | ntimes n vo = Switch (feedback n $ arr next) (const never)
286 |
287 |   where
288 |     next : HList [Nat,i] -> HList [Nat,Either () (Event o)]
289 |     next [0,_]   = [0, Left ()]
290 |     next [S k,_] = [k, Right $ Ev vo]
291 |
292 | ||| Fire the given event exactly once on the first
293 | ||| evaluation step.
294 | export
295 | once : o -> MSF m i (Event o)
296 | once = ntimes 1
297 |
298 | ||| Fire an event whenever the given predicate holds.
299 | export
300 | when : (i -> Bool) -> MSF m i (Event i)
301 | when f = arr $ \vi => toEvent (f vi) vi
302 |
303 | ||| Like `when` but discard the input.
304 | export
305 | when_ : (i -> Bool) -> MSF m i (Event ())
306 | when_ f = arr $ \vi => toEvent (f vi) ()
307 |
308 | ||| Fire an event whenever the input equals the given value.
309 | export
310 | is : Eq i => i -> MSF m i (Event i)
311 | is v = when (v ==)
312 |
313 | ||| Fire an event whenever the input does not equal the given value.
314 | export
315 | isNot : Eq i => i -> MSF m i (Event i)
316 | isNot v = when (v /=)
317 |
318 | ||| Fire an event if the input is a `Left`.
319 | export
320 | whenLeft : MSF m (Either a b) (Event a)
321 | whenLeft = arr $ either Ev (const NoEv)
322 |
323 | ||| Fire an event if the input is a `Right`.
324 | export
325 | whenRight : MSF m (Either a b) (Event b)
326 | whenRight = arr $ either (const NoEv) Ev
327 |
328 | ||| Fire an event if the input is a `Just`.
329 | export
330 | whenJust : MSF m (Maybe a) (Event a)
331 | whenJust = arr maybeToEvent
332 |
333 | ||| Fire an event if the input is a `Nothing`.
334 | export
335 | whenNothing : MSF m (Maybe a) (Event ())
336 | whenNothing = arr $ maybe (Ev ()) (const NoEv)
337 |
338 | ||| Convert an `Event` input to a binary sum, which
339 | ||| can then be sequenced with a call to `choice` or `collect`.
340 | export
341 | event :  MSF m (Event i) (HSum [i,()])
342 | event = arr $ event (There $ Here ()) Here
343 |
344 | ||| Run the given MSF only if the input fired an event.
345 | export
346 | ifEvent : Monoid o => MSF m i o -> MSF m (Event i) o
347 | ifEvent sf = event >>> collect [sf, const neutral]
348 |
349 | ||| Broadcast an event to a list of sinks.
350 | export %inline
351 | (?>-) : MSF m i (Event x) -> FanList m x os -> MSF m i ()
352 | ef ?>- sfs = ef >>> ifEvent (fan_ sfs)
353 |
354 | ||| Run the given MSF if the input stream fires and event.
355 | export %inline
356 | (?>>) : Monoid o => MSF m i (Event x) -> MSF m x o -> MSF m i o
357 | ef ?>> sf = ef >>> ifEvent sf
358 |
359 | ||| Run the given MSF only if the input fired no event.
360 | export
361 | ifNoEvent : Monoid o => MSF m () o -> MSF m (Event i) o
362 | ifNoEvent sf = event >>> collect [const neutral, sf]
363 |
364 | ||| Fire an event whenever the input value changed.
365 | ||| Always fires on first input.
366 | export
367 | onChange : Eq i => MSF m i (Event i)
368 | onChange = mealy accum  NoEv
369 |
370 |   where
371 |     accum : i -> Event i -> HList [Event i, Event i]
372 |     accum v old =
373 |       let ev = Ev v
374 |        in if ev == old then [ev,NoEv] else [ev,ev]
375 |
376 | ||| Fires the first input as an event whenever the
377 | ||| second input fires.
378 | export
379 | onEvent : MSF m (HList [a, Event e]) (Event a)
380 | onEvent = arr $ \case [va,e] => e $> va
381 |
382 | ||| Combines the first input with the event fired by the
383 | ||| second input.
384 | export
385 | onEventWith : (a -> e -> b) -> MSF m (HList [a, Event e]) (Event b)
386 | onEventWith f = arr $ \case [va,e] => f va <$> e
387 |
388 | ||| Combines an input event stream with a stream function
389 | ||| holding an `Either` trying to extract a `Left` whenever
390 | ||| an event is fired.
391 | export
392 | leftOnEvent : MSF m (HList [Either a b, Event e]) (Event a)
393 | leftOnEvent = arr $ \case [Left va,e] => e $> va
394 |                           _           => NoEv
395 |
396 | ||| Combines an input event stream with a stream function
397 | ||| holding an `Either` trying to extract a `Right` whenever
398 | ||| an event is fired.
399 | export
400 | rightOnEvent : MSF m (HList [Either a b, Event e]) (Event b)
401 | rightOnEvent = arr $ \case [Right vb,e] => e $> vb
402 |                            _            => NoEv
403 |
404 | ||| Combines an input event stream with a stream function
405 | ||| holding a `Maybe` trying to extract the value from a `Just` whenever
406 | ||| an event is fired.
407 | export
408 | justOnEvent : MSF m (HList [Maybe a, Event e]) (Event a)
409 | justOnEvent = arr $ \case [Just va,e] => e $> va
410 |                           _           => NoEv
411 |
412 | --------------------------------------------------------------------------------
413 | --          Merging Event Streams
414 | --------------------------------------------------------------------------------
415 |
416 | ||| Fires an event whenever one of the two given
417 | ||| event streams fire. Uses the given function
418 | ||| to combine simultaneously occuring events.
419 | export
420 | unionWith :
421 |      (o -> o -> o)
422 |   -> MSF m i (Event o)
423 |   -> MSF m i (Event o)
424 |   -> MSF m i (Event o)
425 | unionWith = elementwise2 . unionWith
426 |
427 | ||| Left-biased union of event streams.
428 | ||| In case of simultaneously occuring events, the
429 | ||| event from the first event stream is fired.
430 | |||
431 | ||| This is the same behavior as `(<|>)` from
432 | ||| the MSFs `Alternative` implementation
433 | export
434 | unionL : MSF m i (Event o) -> MSF m i (Event o) -> MSF m i (Event o)
435 | unionL = elementwise2 unionL
436 |
437 | ||| Right-biased union of event streams.
438 | ||| In case of simultaneously occuring events, the
439 | ||| event from the second event stream is fired.
440 | export
441 | unionR : MSF m i (Event o) -> MSF m i (Event o) -> MSF m i (Event o)
442 | unionR = elementwise2 unionR
443 |
444 | ||| Union of event streams using a `Semigroup` to
445 | ||| merge values in case of simultaneously occuring events.
446 | |||
447 | ||| This is an alias for `(<+>)`.
448 | export %inline
449 | union :
450 |      {auto _ : Semigroup o}
451 |   -> MSF m i (Event o)
452 |   -> MSF m i (Event o)
453 |   -> MSF m i (Event o)
454 | union = (<+>)
455 |
456 | export
457 | (<|>) : Alternative f => MSF m i (f o) -> MSF m i (f o) -> MSF m i (f o)
458 | x <|> y = fan [x,y] >>> arr (\[vx,vy] => vx <|> vy)
459 |
460 | --------------------------------------------------------------------------------
461 | --          Filtering Event Streams
462 | --------------------------------------------------------------------------------
463 |
464 | ||| Filters an event stream, letting pass only values,
465 | ||| fow which the given predicate holds.
466 | export
467 | filter : (o -> Bool) -> MSF m (Event o) (Event o)
468 | filter = arr . filter
469 |
470 | ||| Filters an event stream, letting pass only values,
471 | ||| fow which the given function returns a `Just`.
472 | export
473 | mapMaybe : (i -> Maybe o) -> MSF m (Event i) (Event o)
474 | mapMaybe = arr . mapMaybe
475 |
476 | ||| Sum projection: Fires an event if a value of the given type can
477 | ||| be extracted from the input sum.
478 | export
479 | proj : (0 t : k) -> {auto prf : Elem t ks} -> MSF m (Any f ks) (Event $ f t)
480 | proj t = arr (project t)
481 |
482 | --------------------------------------------------------------------------------
483 | --          Observing Event Streams
484 | --------------------------------------------------------------------------------
485 |
486 | ||| Observe an event throught the given sink.
487 | export %inline
488 | observeEvent : MSF m i () -> MSF m (Event i) (Event i)
489 | observeEvent = observeWith . ifEvent
490 |
491 | --------------------------------------------------------------------------------
492 | --          Accumulating Events
493 | --------------------------------------------------------------------------------
494 |
495 | ||| Applies a function to the input and an accumulator,
496 | ||| outputting the updated accumulator whenever an
497 | ||| event is fire.
498 | export
499 | accumulateWithE : (i -> o -> o) -> o -> MSF m (Event i) (Event o)
500 | accumulateWithE f ini = feedback ini (arr g)
501 |
502 |   where
503 |     g : HList [o,Event i] -> HList [o,Event o]
504 |     g [acc,NoEv]  = [acc,NoEv]
505 |     g [acc,Ev vi] = let acc' = f vi acc in [acc',Ev acc']
506 |
507 | ||| Count the number of occurences of an event
508 | export
509 | countE : MSF m (Event i) (Event Nat)
510 | countE = accumulateWithE (\_,n => n + 1) 0
511 |
512 | --------------------------------------------------------------------------------
513 | --          Handling with n-ary Products
514 | --------------------------------------------------------------------------------
515 |
516 | ||| N-ary function type calculated from a list of n types.
517 | public export
518 | 0 Fun : List Type -> Type -> Type
519 | Fun [] r        = r
520 | Fun (t :: ts) r = t -> Fun ts r
521 |
522 | ||| Converts an n-ary function to one taking an n-ary
523 | ||| product as input.
524 | export
525 | uncurryNP : {0 is : _} -> Fun is o -> HList is -> o
526 | uncurryNP r []        = r
527 | uncurryNP f (v :: vs) = uncurryNP (f v) vs
528 |
529 | ||| Alias for `arr . uncurryNP`.
530 | export
531 | np : {0 is : _} -> Fun is o -> MSF m (HList is) o
532 | np = arr . uncurryNP
533 |