Up Next

1.1  The core language

1.1.1  Point-wise Operations

The language is a functional language, with a syntax close to Objective Caml. As in Lustre, every ground type or any scalar value imported from the host language, Objective Caml, is implicitly lifted to streams. Thus:

Program executions can be represented as chronograms, showing the sequence of values taken by streams during the execution. The example below shows five streams, one per line. The first line shows the value of a stream c, which has the value t (true) at the first instant, f (false) at the second one, and t at the third. The notation …indicates that the stream has more values (it is infinite), not represented here. Similarly, the following lines define x and y. The fourth line define a stream obtained by adding x and y, addition is done point-wisely.

ctft
xx0x1x2
yy0y1y2
x+yx0+y0x1+y1x2+y2
if c then x else yx0y1x2

1.1.2  Delays

fby is a delay operator. The expression x fby y, which can be read as “x followed by y” takes the first value of x at the first instant, then takes the previous value of y. In other words, it delays y by one instant, and is initialized by x.

xx0x1x2
yy0y1y2
x fby yx0y0y1

It is often needed to separate the delay from the initialization. This is done using the delay operator pre, and the initialization operator ->. pre x delays its argument x, and has an unspecified value (denoted here by nil) at the first instant. x -> y takes the first value of x at the first instant, then the current value of y. The expression x -> (pre y) is equivalent to x fby y.

xx0x1x2
yy0y1y2
pre xnilx0x1
x -> yx0y1y2

The initialization check made by the compiler checks that the behavior of a program never depends on the value nil. See section 1.1.10 for details.

Warning: A common error with the initialization operator is to use it for defining the first two values of a stream. This does not work, since x -> y -> z = x -> z. One should instead write x fby y fby z or, x -> pre (y -> pre z).

1.1.3  Global declarations

A program is made of a sequence of declarations of global values. let defines non recursive global values whereas let rec define recursive global values. These global values may be (infinite) constant streams or functions. For example:

let dt = 0.001
let g = 9.81

These declarations define two infinite constant streams dt and g. The type and clock of each expression are infered, the compiler can display them by using the option -i:

$ lucyc -i tutorial.ls
val dt :  float
val dt :: static
val g :  float
val g :: static

For each declaration, we get the inferred type and clock. Clocks will be explained further in a later part.

Only constant values can be defined globally, thus rejecting the following program:

let init = true -> false

Trying to compile this program, we get the following answer:

$ lucyc tutorial.ls
File "tutorial.ls", line 1, characters 11-24:
>let init = true -> false
>           ^^^^^^^^^^^^^
This expression should be combinatorial.

The right part of a global let declaration cannot contain any delay operations. Definitions containing delays are sequential and introduced by the notation node (see 1.1.5).

1.1.4  Combinatorial Functions

Stream functions are separated into combinatorial and sequential functions. A function is combinatorial when its output at instant n depends only on its input at the same instant n.

The definition of combinatorial function uses the let notation seen previously. Consider, for example, the function computing the average of its two inputs. We directly give its type and clock signatures as computed by the compiler.

let average (x,y) = (x + y) / 2

val average :  int * int -> int
val average :: ’a * ’a -> ’a

This function get the type signature int * int -> int stating that it takes two integer streams and returns an integer stream. Its clock signature states that it is a length preserving function, that is, it returns a value for every input.

Function definition can contain local declarations, introduced using either the where, or the let notation (see 1.1.7). For example the average function can be written:

let average (x,y) = o where
  o = (x + y) / 2

let average (x,y) =
  let o = (x + y) / 2 in
  o

As another example of combinatorial program, we end with the classical description of a one-bit adder. A full adder takes three bits (a, b and a carry bit c) and it returns the result c and the new carry co.

let xor (a, b) = (a & not(b)) or (not a & b)

let full_add(a, b, c) = (s, co) where
       s = xor (xor (a, b), c)
   and co = (a & b) or (b & c) or (a & c)

val xor :  bool * bool -> bool
val xor :: ’a * ’a -> ’a
val full_add :  bool * bool * bool -> bool * bool
val full_add :: ’a * ’a * ’a -> ’a * ’a

    
Figure 1.1: A half-adder and a full-adder 

A full adder can be described more efficiently as a composition of two half adders. The graphical description is given in figure 1.1 and it corresponds to the following code:

let half_add(a,b) = (s, co)
   where 
       s = xor (a, b)
   and co = a & b

val half_add :  bool * bool -> bool * bool
val half_add :: ’a * ’a -> ’a * ’a

let full_add(a,b,c) = (s, co)
  where
  rec (s1, c1) = half_add(a,b)
  and (s, c2) = half_add(c, s1)
  and co = c1 or c2

val full_add :  bool * bool * bool -> bool * bool
val full_add :: ’a * ’a * ’a -> ’a * ’a * ’a

1.1.5  Sequential Functions

Sequential functions (or state functions) are such that their output at instant n may depend on the history of their inputs, that is, input values of instants k (kn).

To generalise, an expression is called sequential if it may produce a time evolving value when its free variables are kept constant. Otherwise, we call it combinatorial. A sufficient condition to be a combinatorial expression is not to contain any delay, initialization operator, nor state machine. This is verified by type checking.

Sequential functions are introduced by the keyword node. They receive a different type signature than the one given to combinatorial functions. The type signature int => int states that from is a stream function from an integer stream to an integer stream and that its output may depend on the history of its input.

The following function computes the sequence of integers starting at some initial value given by parameter m:

let node from m = nat where
  rec nat = m -> pre nat + 1

val from :  int => int
val from :: ’a -> ’a

Applying this function to the constant stream 0 yields the following execution:

m000000
1111111
pre natnil01234
pre nat + 1nil12345
m -> pre nat + 1012345
from m012345

Combinatorial functions are checked to be combinatorial at compile time, thus forgetting the keyword node leads to an error:

let from n = nat where
  rec nat = n -> pre nat + 1

and we get:

$ lucyc tutorial.ls
File "tutorial.ls", line 16, characters 12-28:
>  rec nat = n -> pre nat + 1
>            ^^^^^^^^^^^^^^^^
This expression should be combinatorial.


We can define an edge detector in the following way:

let node edge c = c & not (false fby c)
cffttft
falseffffff
false fby cfffttf
not (false fby c)tttfft
edge cfftfft

edge is a global function from boolean streams to boolean streams.


An integrator is defined by:

let dt = 0.01

let node integr x0 dx = x where
  rec x = x0 -> pre x +. dx *. dt

val integr :  float -> float => float
val integr :: ’a -> ’a -> ’a

integr is a global function returning a stream x defined recursively. The operators +., *. stand for the addition and multiplication over floating point numbers. Sequential functions may be composed as any other functions. For example:

let node double_integr x0 dx0 d2x = x where
  rec x = integr x0 dx
  and dx = integr dx0 d2x

It is possible to build functions from other functions by applying the later only partially. For example:

let integr0 = integr 0.0

Which is equivalent to:

  let node integr0 dx = integr 0.0 dx

1.1.6  Anonymous Functions

Functions can be defined in an anonymous way and can be used as values. Anonymous combinatorial functions are introduced using a single arrow (->), anonymous sequential ones using a double arrow (=>). For example, the expression fun x y -> x + y is the sum function and has type int -> int -> int). The expression fun x y => x fby x fby y defines a double delay and has the type 'a -> 'a => 'a.

The functions average and from can be defined as:

let average = fun (x,y) -> (x + y) / 2
let from = fun n => nat where rec nat = n -> pre nat + 1

1.1.7  Local definitions and Mutually Recursive Definition

Variables may be defined locally with a let/in or let rec/in and there is no special restriction on the expressions appearing on the right of a definition. The following program, computes the Euclidean distance between two points:

let distance (x0,y0) (x1,y1) =
  let d0 = x1 -. x0 in
  let d1 = y1 -. x1 in
  sqrt (d0 *. d0 +. d1 *. d1)

Notice that because d0 and d1 denote infinite sequences, the computations of x1 -. x0 and y1 -. x1 are (virtually) executed in parallel. Nonetheless, when writing sequences of definitions let/in such as above, the sequential order is preserved for each reaction of the system, that is, the current value of d0 is always computed before the current value of d1. This sequential order may be of importance if side-effects are present.

Streams may be defined as a set of mutually recursive equations. The function which computes the minimum and maximum of some input sequence x can be written in (at least) the three equivalent ways:

let node min_max x = (min, max) where
  rec min = x -> if x < pre min then x else pre min
  and max = x -> if x > pre max then x else pre max

let node min_max x =
  let rec min = x -> if x < pre min then x else pre min
  and max = x -> if x > pre max then x else pre max in
  (min, max)

let node min_max x = (min, max) where
  rec (min, max) = (x, x) -> if x < pre min then (x, pre max)
                             else if x > pre max then (pre min, x)
                             else (pre min, pre max)

The classical sinus and co-sinus functions can be defined like the following:

  let node sin_cos theta = (sin, cos) where
    rec sin = theta *. integr 0.0 cos
    and cos = theta *. integr 1.0 (0.0 -> -. (pre sin))

We end with the programming of a mouse controller, a very classical example. Its specification is the following:

Return the event double when two click has been received in less than four top. Emits simple if only one click has been received.

And here is a possible implementation:

(* counts the number of events from the last reset res *)
let node counter (res,event) = count where
  rec count = if res then 0 else x
  and x = 0 -> if event then pre count + 1 else pre count

let node mouse (click,top) = (single,double) where
  rec counting = click -> if click & not (pre counting) then true
                          else if res & pre counting then false
                          else pre counting
  and count = counter(res,top & counting)
  and single = ((0 fby count) = 3) & top & not click
  and double = (false fby counting) & click
  and res = single or double

1.1.8  Shared Memory and Initialization

The language provides an alternative way to the use of the delay pre in order to refer to the previous value of a stream. If o is a stream variable defined by some equation, last o refers to the last value of o. For example:

let node counter i = o where
  rec last o = i
  and o = last o + 1

The equation last o = i defines the memory last o. This memory is initialized with the first value of i and then, contains the previous value of o. The above program is thus equivalent to the following one 1:

let node counter i = o where
  rec last_o = i -> pre o
  and o = last_o + 1

The memory last o will play an important role when combined with control structures. This will be detailed later.

From a syntactical point of view, last is not an operator: last o denotes a shared memory and the argument of last is necessarily a name. Thus the following program:

let node f () = o where
  rec o = 0 -> last (o + 1)

is rejected and we get:

File "tutorial.ls", line 55, characters 21-22:
>  rec o = 0 -> last (o + 1)
>                     ^
Syntax error.

1.1.9  Causality check

Recursively defined values must not contain any instantaneous or causality loops in order to be able to compute values in a sequential way. For example, if we type:

let node from m = nat where
  rec nat = m -> nat + 1

the compiler emits the message:

File "tutorial.ls", line 35, characters 12-24:
>  rec nat = m -> nat + 1
>            ^^^^^^^^^^^^
This expression may depend instantaneously of itself.

This program cannot be computed as nat depends on nat instantaneously.

The compiler statically reject program which cannot be scheduled sequentially, that is streams whose value at instant n may depend on some value at instant n. In practice, it imposes that any loop crosses a delay pre or fby.

In the current version of the compiler, the causality analysis reject recursions which are not explicitely done through a delay. The following program (which is semantically correct) is rejected:

let node f x = 0 -> pre (x + 1)

let node wrong () =
  let rec o = f o in o

1.1.10  Initialization check

The compiler checks that every delay operator is initialized. For example:

let node from m = nat where
  rec nat = pre nat + 1

File "tutorial.ls", line 35, characters 12-23:
>  rec nat = pre nat + 1
>            ^^^^^^^^^^^
This expression may not be initialised.

The analysis is a one-bit analysis where expressions are considered to be either always defined or always defined except at the very first instant. It is precisely defined in [3]. In practice, it rejects expressions like pre (pre e), that is, un-initialized expressions cannot be used as an argument of a delay and must be first initialized using ->.


1
The construction last is eliminated during the compilation process by a similar transformation.

Up Next