1.4  Data-types, Pattern matching

1.4.1  Type definitions

Sum types, product types, and record types may be defined in the same way as in Objective Caml. The syntax is the one of Objective Caml. See the Objective Caml documentation for details and the present reference manual for syntactic considerations.

The first example defines a sum type number, with both integers and floating point numbers. The second one defines a type circle, representing a circle as a record containing a center, given by its coordinates, and a radius.

type number = Int of int | Float of float

type circle = { center: float * float; radius: float }

1.4.2  Pattern matching

The language provides means for doing pattern matching over streams with a match/with construction à la Objective Caml. This construction is a generalized form of the merge and thus, follows the same clocking rules.

Consider the example of a colored wheel rotating on an axis and for which we want to compute the rotation direction. This wheel is composed of three sections with colors blue (Blue), red (Red) and green (Green). A sensor observes the successive colors on the wheel and has to decide if the wheel is immobile or determine the rotation direction.

We consider that the direction is direct (Direct) when there is a succession of Red, Green, Blue, Red..., the opposite direction being indirect (Indirect). There are some instants where the direction is undetermined (Undetermined) or that the wheel is immobile (Immobile).

We program the controler in the following way. First, we introduce two sum types. The function direction then compares three successive values of the input stream i.

type color = Blue | Red | Green
type dir = Direct | Indirect | Undetermined | Immobile

let node direction i = d where
  rec pi = i fby i
  and ppi = i fby pi
  and match ppi, pi, i with
    (Red, Red, Red) | (Blue, Blue, Blue) | (Green, Green, Green) ->
         do d = Immobile done
  | (_, Blue, Red) | (_, Red, Green) | (_, Green, Blue) -> 
         do d = Direct done
  | (_, Red, Blue) | (_, Blue, Green) | (_, Green, Red) -> 
         do d = Indirect done
  | _ -> do d = Undetermined done
  end

val direction :  color => dir
val direction :: ’a -> ’a

The handler of a pattern-matching construct is made of a set of equations defining shared variables (here the variable d). At each instant, the match/with statement selects the first pattern (from top to bottom) which matches the actual value of the triple pii, pi, i and executes the corresponding branch. During a reaction, only one branch is executed.

Because only one branch is executed during a reactin, one must be careful when programming with such control structures, in particular in the presence of delay operators. This can be illustrated on the following program. This program is made of two modes: in the Up mode, the variable o increases by step 1 whereas in the mode Down, it decreases by step -1.

type modes = Up | Down

let node two m i = o where
  rec last o = i
  and match m with
        Up -> do o = last o + 1 done
      | Down -> do o = last o - 1 done
      end

The equation last o = i defines a shared memory last o which is initialized with the first value of i. o is called a shared variable because it is defined by several equations. When m equals Up, o equals last o + 1. When m equals Down, o equals last o - 1. The communication between the two modes is done through a shared memory last o. last o contains the previous value of o, the last time o has been defined. The execution diagram for some execution is given below.

This program is equivalent to the following one:

type modes = Up | Down

let node two m i = o where
  rec last_o = i -> pre o
  and match m with
        Up -> do o = last_o + 1 done
      | Down -> do o = last_o - 1 done
      end

making clear that last o stands for the previous defined value of o.

Warning: Whereas last o may seem to be just another way to refer to the previous value of a stream like pre o does, there is a fundamental difference between the two. This difference is a matter or instant of observation.

• In data-flow systems (e.g., block diagram design à la Simulink or Scade/Lustre), pre e stands for a local memory, that is, pre denotes the last value of its argument, the last time it was computed. If pre e appear in a block structure which is executed from time to time — say on some clock ck — it means that the argument e is only computed when ck is true.
• last o denotes the previous value of the variable o on the instant where the variable o is defined. last o is only valid when o stands for a variable and not an expression. last o is useful to communicate values between modes and this is why we call it a shared memory.

We illustrate the difference between the two on the following example. We now compute two other streams c1 and c2 returning respectively the number of instants each mode is active.

let node two m i = (o, c1, c2) where
  rec last o = i
  and last c1 = 0
  and last c2 = 0
  and match m with
        Up -> do o = last o + 1
              and c1 = 1 -> pre c1 + 1
              done
       | Down -> do o = last o - 1
                 and c2 = 1 -> pre c2 + 1
                 done
    end

The equation c1 = 1 -> pre c1 + 1 is only active in the Up mode whereas equation c2 = 1 -> pre c2 + 1 is active in mode Down. The execution diagram is given below.

A pattern matching composes several complementary sub-streams, that is, streams on complementary clocks. The above pattern matching has two branches. Every branch defines its own clock, one denoting the instants where m = Up and the other denoting the instant where m = Down.

1.4.3  Local Definitions

It is possible to define variables which stay local to a branch. For example:

let node two m i = o where
  match m with
    Up -> let rec c = 0 -> pre c + 1 in
          do o = c done
  | Down -> do o = 0 done
  end

1.4.4  Implicit Definition of Shared Variables

Finally, note that the branches of a pattern-matching constraint do not have to contain a definition for all the shared variables. Shared variables are implicitely completed by adding an equation of the form x = last xin branches which they are not defined. Nonetheless, the compiler rejects program for which it cannot guaranty that the last value is defined. Thus, the following program is statically rejected.

let node two m i = o where
  rec match m with
        Up -> do o = last o + 1 done
      | Down -> do o = last o - 1 done
      end
File "test.ls", line 9, characters 21-31:
>        Up -> do o = last o + 1 done
>                     ^^^^^^^^^^
This expression may not be initialised.