ReactiveML Manual

Process Definitions

  let process <id> { <pattern> } = <expr> in <expr>
  process <expr>
  proc <pattern> { <pattern> } -> <expr>

Process definitions are introduced by the process keyword. For instance let process p x1 x2 ... = e defines a process p with several arguments x1, x2, ... and a body e. The notation let process p x1 x2 ... = e is a shortcut for let p = fun x1 x2 ... -> process e and the notation (proc x1 x2 ... -> e) is a shortcut for (fun x1 x2 ... -> (process e)).

Basic statements

  nothing
  pause
  halt
  run <process>

nothing is equivalent to() (can be used only in a process).
pause suspends the execution until next instant.
halt suspends the execution forever (it is equivalent to loop pause end, see below).
run p executes the process p.

Compositions

  <expr> ; <expr>
  <expr> || <expr>
  let <pattern> = <expr> { and <pattern> = <expr> } in <expr>
  <expr> |> <expr>

In ReactiveML, expressions can be composed in sequence (p;q) or in parallel (p||q). The expression let x1 = e1 and x2 = e2 and x3 = e3 and ... in e compute expressions e1, e2, e3, ... in parallel to use the result in expresion e.

The expression e1 |> e2 executes e1 and e2 in parallel, but at each instant e1 is executed before e2 (this construct is not supported in all runtime).

Iterators

  loop <expr> end
  while <expr> do <expr> done
  for <id> = <expr> ( to  |  downto )  do <expr> done
  for <id> = <expr> ( to  |  downto ) dopar <expr> done

The construct loop/end is an infinite loop. while/do/done and for/do/done are the classical loops. They execute their body several times in sequence. Contrarily, the for/dopar/done loop executes its body several times in parallel.

Signal declaration

  signal <id> { , <id> } in <expr>
  signal <id> default <value> gather <function>  in  <expr>

The construct signal s declares a new signal. It is also possible to declare several signals at once: signal s1, s2, s3, ....

Sometimes, multiple values can be emitted on a signal during the same logical instant. This phenomenon is called Multi-emission. Hence, when a signal is declared, it is possible to define how to combine the values emitted during an instant with the signal/default/gather construct. Note that in this case, a default value is required.
For instance signal s default 0 gather (fun x y -> x + y) defines a a signal s with 0 as default value, and (+) as combination function. Thus, in case of multi-emission, the value of the signal is the sum of all emitted values. If no combination function is given, the behavior of the signal is to collect all emitted values in a list.

Signal emission

  emit <signal> [ <value> ]

Signal emissions are instantaneous broadcasting. Hence, a signal is present or absent during an instant but it cannot have both status. The notation emit s is a shortcut for emit s (), i.e., emit the value () on signal s.

Signal status

  present <signal> then <expr> else <expr>
  await  [ immediate ] <signal>
  pre <signal>

The expression present s then p else q tests the status of a signal s. If the signal is present, the then branch p is executed instantaneously, otherwise the else branch q is executed at the following instant.

The expression await s waits s to be emitted and terminates at the following instant. Whereas the expression await immediate s waits s to be emitted and terminates instantaneously.

Like in Esterel, the non-immediate version of await is the default one. Hence await s; await s waits two occurrences of s, while await immediate s; await immediate s is equivalent to await immediate s.

The expression pre s returns true if the signal s has been emitted at the preceding, and false otherwise.

Signal value

  await  <signal> (<pattern>) [ when <expr> ] in <expr>
  await [ immediate ] one <signal> (<variable>) in <expr>
  pre ?<signal>
  last ?<signal>
  default ?<signal>

The construct await s(v) in p waits the emission of a signal s. At the instant following the emission, the body p is executed in an environment where the pattern v is bind to the value of the signal (the combination of the values emitted at the preceding instant).

It is possible to match the value of a signal and keep waiting if the condition is not satisfied. For instance the expression await s(x::y::_) when (x + y > 42) in p waits for a list of at least two elements. Then, the sum of the first two elements of the list x + y must be greater than 42 to trigger the execution of p. Notice that this construct keeps waiting when the value of the signal does not match the pattern (e.g., x::y::_) or if the condition specified after the when keyword is not satisfied (e.g., x + y > 42).

The expression expression await one s (v) in p waits the emission of a signal s to bind the pattern v with one of the emitted values on signal s. In case of multiple emission during an instant, the choice of the value is not specified. Like await, the body of the expression is executed at the instant following the reception of the signal (except if there is the immediate keyword). To be causal by construction, there is no immediate version of the await/in construct.

The expression pre ?s evaluates to the value associated to s at the preceding instant. If s has not been emitted at the preceding instant, pre ?s is equal to the default value given at the declaration point of the signal. last ?s has a slight different behavior. It evaluates to the last value associated to s when it was emitted. Until the first emission of signal s, pre ?s and last ?s both evaluates to the default value of s.

The expression default s returns the default value of a signal s.

  do <expr> when <signal> done
  control <expr> with <signal> [ (<pattern>) [ when  <expr> ] ] done
  do <expr> until <signal> [ (<pattern>) [ when  <expr> ] [ ->  <expr> ] ] done
  do <expr> until <signal> (<pattern>) [ when  <expr> ] -> <expr>
              { | <signal> (<pattern>) [ when  <expr> ] -> <expr> } done

The do/when/done and control/with/done constructs allow to suspend the execution of an expression. do p when s done executes its body p only when the signal s is present. control p with s done switches between an active mode and a suspended one each time that the signal sis present.

The preemption construct do p until s done stops the execution of its body p at the end of instant when the signal s is emitted (it is not a looping construct). It is also posible to define a handler do p until s -> q done. In this case, an emission of signal s stops the execution of p and launches the execution of q at the following instant.

Besides, it is always possible to match a given pattern in the control structure. For instance the code do p until s (v) when (v > 0) -> q done stops the execution of p and launches q only if the value emitted on signal s is positive.

  present <config> then <expr> else <expr>
  await [ immediate ] <config>
  await <config-patt> [ when <expr> ] in <expr>
  do <expr> when <config> done
  control <expr> with <config-patt> [ when  <expr> ] done
  do <expr> until <config-patt> [ when  <expr> ] -> <expr>
              { | <config-patt>) [ when  <expr> ] -> <expr> } done

The behavior of these expressions is the same as before except that instead of depending on a signal, they depend on a Boolean configuration of signals. The expressions <config> and <config-patt> are defined as follows:

       <config> ::= <signal>
                  | <config> /\ <config>
                  | <config> \/ <config>
  <config-patt> ::= <signal>
                  | <signal> (<pattern>)
                  | <config-patt> /\ <config-patt>
                  | <config-patt> \/ <config-patt>

For example, the expression await (s1(x) /\ s2(y)) \/ s3(x::y::_) when (x + y > 42) in e waits for either s1 and s2 to be present simultaneously or s3 to be present if its associated value is a list of at least two elements. In both cases, the variables x and y are bound and the sum of their value must be greater than 42 to trigger the execution of e.