## 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:

• `int` stands for the type of streams of integers,
• `1` stands for the constant stream of values 1,
• `+` adds point-wisely its two input streams. It can be seen as an adder circuit, in the same way, `&` can be seen as an “and” gate.

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.

 c t f t … x x0 x1 x2 … y y0 y1 y2 … x+y x0+y0 x1+y1 x2+y2 … if c then x else y x0 y1 x2 …

### 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.

 x x0 x1 x2 … y y0 y1 y2 … x fby y x0 y0 y1 …

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.

 x x0 x1 x2 … y y0 y1 y2 … pre x nil x0 x1 … x -> y x0 y1 y2 …

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
```

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

where
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:

 m 0 0 0 0 0 0 … 1 1 1 1 1 1 1 … pre nat nil 0 1 2 3 4 … pre nat + 1 nil 1 2 3 4 5 … m -> pre nat + 1 0 1 2 3 4 5 … from m 0 1 2 3 4 5 …

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)
```
 c f f t t f t … false f f f f f f … false fby c f f f t t f … not (false fby c) t t t f f t … edge c f f t f f t …

`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.