1.3  Valued Signals

Zélus provides valued signals that are built and accessed, respectively, through the constructions emit and present. At every instant, a valued signal is a pair comprising (1) a boolean c indicating when the signal is present and (2) a value that is present when c is true.3

1.3.1  Signal Emission

Unlike shared variables, signal values are not necessarily defined at every instant, nor do they implicitly keep their previous value when not updated. Consider this program, for instance:

let node within (min, max, x) = o where
  rec c = (min <= x) & (x <= max)
  and present c -> do emit o = () done
val within : 'a * 'a * 'a -D-> unit signal

It computes a condition c based on the input x. The signal o is present with value () every time c is true. There is no need to give an initial value for o. When c is false, o is simply absent. Removing the emit gives a program that the compiler rejects:

let node within (min, max, x) = o where
  rec c = (min <= x) & (x <= max)
  and present c -> do o = () done
File "tutorial.zls", line 3-4, characters 6-34: >......present c -> do o = () done >..... Type error: o has type unit, but is expected to be a signal.

The output o is not declared as a shared variable (with init) nor is it defined as a signal (with emit).

1.3.2  Signal Presence and Values

The presence of a signal expression e can be tested by the boolean expression ?e. The following program, for example, counts the number of instants where x is emitted.

let node count x = cpt where
  rec cpt = if ?x then 1 -> pre cpt + 1 else 0 -> pre cpt
val count : 'a signal -D-> int

There is also a more general mechanism to test signal presence that treats multiple signals simultaneously and allows access to their values. It resembles the pattern-matching construct of ML and it only allows signal values to be accessed at instants of emission.4

The program below has two input signals, x and y, and returns the sum of their values when both are emitted, the value of x when it alone is emitted, the value of y when it alone is emitted, and 0 otherwise.

let node sum (x, y) = o where
  present
  | x(v) & y(w) -> do o = v + w done
  | x(v) -> do o = v done
  | y(w) -> do o = w done
  else do o = 0 done
  end
val sum : int signal * int signal -D-> int

A present statement comprises several signal patterns and handlers. The patterns are tested sequentially from top to bottom. The signal condition x(v) & y(w) matches when both x and y are present. The condition x(v) means “x is present and has some value v”. When x is present, the variable v is bound to its value in the corresponding handler.

In the signal pattern x(v) & y(w), x and y are expressions that evaluate to signal values and v and w are patterns. Writing x(42) & y(w) means “detect the presence of signal x with value 42 and the simultaneous presence of y”.

The output of the preceding function is a regular stream since the test is exhaustive thanks to the else clause. Omitting this default case results in an error.

let node sum (x, y) = o where
  present
  | x(v) & y(w) -> do o = v + w done
  | x(v1) -> do o = v1 done
  | y(v2) -> do o = v2 done
  end
File "tutorial.zls", line 2-6, characters 2-108: >..present > | x(v) & y(w) -> do o = v + w done > | x(v1) -> do o = v1 done > | y(v2) -> do o = v2 done > end Type error: o has type int, but is expected to be a signal.

This error is easily eliminated by giving a last value to o—for example, by adding the equation init o = 0 outside the present statement. The default case is then implicitly completed with o = last o. Another way is to state that o is a signal and thus only partially defined.

let node sum (x, y) = o where
  present
  | x(v) & y(w) -> do emit o = v + w done
  | x(v1) -> do emit o = v1 done
  | y(v2) -> do emit o = v2 done
  end
val sum : int signal * int signal -D-> int signal

Signal patterns may also contain boolean expressions. The following program adds the values of the two signals x and y if they are emitted at the same time and if z >= 0.

let node sum (x, y, z) = o where
  present
    x(v) & y(w) & (z >= 0) -> do o = v + w done
  else do o = 0 done
  end


Remark: Signals make it possible to mimic the default construction of the language Signal [4]. Signal’s default x y takes the value of x when x is present and the value of y when x is absent and y is present. The signal pattern x(v) | y(v) tests the presence of “x or y”.

let node signal_default (x, y) = o where
  present
    x(v) | y(v) -> do emit o = v done
  end

This is only a simulation of Signal’s behavior since all information about the instants where x and y are present—the so-called clock calculus of Signal [4]—is hidden at run-time and not exploited by the compiler. In particular, and unlike in the clock calculus of Signal, the Zélus compiler cannot determine that o is emitted only when x or y are present.

Unlike Lustre, Lucid Synchrone and Signal, Zélus does not currently have a clock calculus.


3
For OCaml programmers: signals are like streams of an option type.
4
Unlike in Esterel where signal values are maintained implicitly and can be accessed even in instants where they are not emitted. The approach of Zélus is slightly more cumbersome, but it is safer and avoids initialization issues and the allocation of a state variable.