### 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
*/
RuleY ---> 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*`.
*/
RuleY ---> 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`.
*/
RuleX ---> 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.
*/
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`.
*/
Ruleif-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)`.
*/
Ruleinterleave(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`.
*/
Ruleyield-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.
*/
RuleX --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)`.
*/
RuleX --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′)
/*`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.