### Flowing

[
  Funcon   left-to-right   Alias l-to-r
  Funcon   right-to-left   Alias r-to-l
  Funcon   sequential      Alias seq
  Funcon   effect
  Funcon   choice
  Funcon   if-true-else    Alias if-else
  Funcon   while-true      Alias while
  Funcon   do-while-true   Alias do-while
  Funcon   interleave
  Datatype yielding
  Funcon   signal
  Funcon   yielded
  Funcon   yield
  Funcon   yield-on-value
  Funcon   yield-on-abrupt
  Funcon   atomic
]


Meta-variables
  T <: values
  T* <: values*


#### Sequencing

Funcon
  left-to-right(_:(=>(T)*)*) : =>(T)*
Alias
  l-to-r = left-to-right
/*
  `left-to-right(...)` computes its arguments sequentially, from left to right,
  and gives the resulting sequence of values, provided all terminate normally.
  For example, `integer-add(X, Y)` may interleave the computations of `X` and
  `Y`, whereas `integer-add left-to-right(X, Y)` always computes `X` before `Y`.

  When each argument of `left-to-right(...)` computes a single value, the type
  of the result is the same as that of the argument sequence. For instance,
  when `X:T` and `Y:T'`, the result of `left-to-right(X, Y)` is of type `(T, T')`.
  The only effect of wrapping an argument sequence in `left-to-right(...)` is to
  ensure that when the arguments are to be evaluated, it is done in the
  specified order.
*/
Rule
                              Y ---> Y'
  ------------------------------------------------------------
  left-to-right(V*:(T)*, Y, Z*) ---> left-to-right(V*, Y', Z*)
Rule
  left-to-right(V*:(T)*) ~> V*


Funcon
  right-to-left(_:(=>(T)*)*) : =>(T)*
Alias
  r-to-l = right-to-left
/*
  `right-to-left(...)` computes its arguments sequentially, from right to left,
  and gives the resulting sequence of values, provided all terminate normally.

  Note that `right-to-left(X*)` and `reverse left-to-right reverse(X*)` are
  not equivalent: `reverse(X*)` interleaves the evaluation of `X*`.
*/
Rule
                              Y ---> Y'
  ------------------------------------------------------------
  right-to-left(X*, Y, V*:(T)*) ---> right-to-left(X*, Y', V*)
Rule
  right-to-left(V*:(T)*) ~> V*


Funcon
  sequential(_:(=>null-type)*, _:=>T) : =>T
Alias
  seq = sequential
/*
  `sequential(X, ...)` computes its arguments in the given order. On normal
  termination, it returns the value of the last argument; the other arguments
  all compute `null-value`.

  Binary `sequential(X, Y)` is associative, with unit `null-value`.
*/
Rule
                  X ---> X'
  -----------------------------------------
  sequential(X, Y+) ---> sequential(X', Y+)
Rule
  sequential(null-value, Y+) ~> sequential(Y+)
Rule
  sequential(Y) ~> Y


Funcon
  effect(V*:T*) : =>null-type
    ~> null-value
/*
  `effect(...)` interleaves the computations of its arguments, then discards
  all the computed values.
*/


#### Choosing

Funcon
  choice(_:(=>T)+) : =>T
/*
  `choice(Y, ...)` selects one of its arguments, then computes it.
  It is associative and commutative.
*/
Rule
  choice(X*, Y, Z*) ~> Y


Funcon
  if-true-else(_:booleans, _:=>T, _:=>T) : =>T
Alias
  if-else = if-true-else
/*
  `if-true-else(B, X, Y)` evaluates `B` to a Boolean value, then reduces
  to `X` or `Y`, depending on the value of `B`.
*/
Rule
  if-true-else(true, X, Y) ~> X
Rule
  if-true-else(false, X, Y) ~> Y


#### Iterating

Funcon
  while-true(B:=>booleans, X:=>null-type) : =>null-type
    ~> if-true-else(B, sequential(X, while-true(B, X)), null-value)
Alias
  while = while-true
/*
  `while-true(B, X)` evaluates `B` to a Boolean value. Depending on the value
  of `B`, it either executes `X` and iterates, or terminates normally.

  The effect of abruptly breaking the iteration is obtained by the combination
  `handle-break(while-true(B, X))`, and that of abruptly continuing the iteration by
  `while-true(B, handle-continue(X))`.
*/

Funcon
  do-while-true(X:=>null-type, B:=>booleans) : =>null-type
    ~> sequential(X, if-true-else(B, do-while-true(X, B), null-value))
Alias
  do-while = do-while-true
/*
  `do-while-true(X, B)` is equivalent to `sequential(X, while-true(B, X))`.
*/


#### Interleaving

Funcon
  interleave(_:T*) : =>T*
/*
  `interleave(...)` computes its arguments in any order, possibly interleaved,
  and returns the resulting sequence of values, provided all terminate normally.
  Fairness of interleaving is not required, so pure left-to-right computation
  is allowed.

  `atomic(X)` prevents interleaving in `X`, except after transitions that emit
  a `yielded(signal)`.
*/
Rule
  interleave(V*:T*) ~> V*


Datatype
  yielding ::= signal


Entity
  _ --yielded(_:yielding?)-> _
/*
  `yielded(signal)` in a label on a transition allows interleaving at that point
  in the enclosing atomic computation.
  `yielded( )` indicates interleaving at that point in an atomic computation
  is not allowed.
*/


Funcon
  yield : =>null-type
   ~> yield-on-value(null-value)


Funcon
  yield-on-value(_:T) : =>T
/*
  `yield-on-value(X)` allows interleaving in an enclosing atomic computation
  on normal termination of `X`.
*/
Rule
  yield-on-value(V:T) --yielded(signal)-> V


Funcon
  yield-on-abrupt(_:=>T) : =>T
/*
  `yield-on-abrupt(X)` ensures that abrupt termination of `X` is propagated
  through an enclosing atomic computation.
*/
Rule
                   X --abrupt(V:T),yielded(_?)-> X'
  --------------------------------------------------------------------
  yield-on-abrupt(X) --abrupt(V),yielded(signal)-> yield-on-abrupt(X')
Rule
                   X --abrupt( )-> X'
  ----------------------------------------------------
  yield-on-abrupt(X) --abrupt( )-> yield-on-abrupt(X')
Rule
  yield-on-abrupt(V:T) ~> V


Funcon
  atomic(_:=>T) : =>T
/*
  `atomic(X)` computes `X`, but controls its potential interleaving with other
  computations: interleaving is only allowed following a transition of `X` that
  emits `yielded(signal)`.
*/
Rule
                   X --yielded( )->1 X'
          atomic(X') --yielded( )->2 X''
  -----------------------------------------------
  atomic(X) --yielded( )->1 ; --yielded( )->2 X''
Rule
          X --yielded( )-> V
                V : T
  ---------------------------
  atomic(X) --yielded( )-> V
Rule
  atomic(V:T) ~> V
Rule
          X --yielded(signal)-> X'
  -----------------------------------
  atomic(X) --yielded( )-> atomic(X')