The syntax of the language is presented in BNF-like notation. Terminal symbols are set in typewriter font (like this). Non-terminal symbols are set in italic font (like that). Square brackets [ ... ] denote optional components. Curly brackets { ... } denotes zero, one, or several repetitions of the enclosed components.

We adopt the lexical conventions of OCaml for blanks, comments, identifiers, integer literals, floating-point literals, character literals, string literals, and prefix and infix symbols.

The following identifiers are reserved as keywords.

as automaton atomic inline continue disc do done until unless emit present match period with end fun node hybrid discrete init in and open val local unsafe let rec where open fby next up der reset pre type every true false or on last if then else quo mod land lor lxor lsl lsr asr

The following character sequences are also keywords.

-> > < = <> >= ) & ? + - * / ;; <= ( .

Zélus provides the basic values of OCaml—that is, integer numbers, floating-point numbers, characters and character strings—and with the same conventions.

Zélus provides the tuples of OCamlwith the same conventions. It also provides records and sum types with constructors of arity 0.

Functions map values to other values.
They are separated into three main
categories: pure or *combinatorial* functions, discrete-time stateful
functions, and continuous-time stateful functions.

The naming conventions in Zélus are inherited from OCamlsubject to the restrictions detailed in this section.

Names in Zélus fall into one of three syntactic classes:

- value-name for value names,
- typeconstr-name for type constructors, and
- module-name for module names.

value-name | ::= | lowercase-ident |

| | ( operator-name ) | |

operator-name | ::= | prefix-symbol | infix-symbol | * | = | or | & | || |

constructor-name | ::= | capitalized-ident |

| | () | |

typeconstr-name | ::= | lowercase-ident |

module-name | ::= | capitalized-ident |

The syntactic class of lowercase-ident is the set of identifiers starting with a lowercase letter whereas capitalized-ident is the set of of identifiers starting with a capital letter.

value-path | ::= | value-name |

| | module-name . value-name | |

constructor | ::= | constructor-name |

| | module-name . capitalized-ident | |

typeconstr | ::= | typeconstr-name |

| | module-name . typeconstr |

A value can be referred to either by its name or by its name qualified with a module name.

type | ::= | ’ ident |

| | ( type ) | |

| | type {* type} | |

| | type typeconstr | |

| | ( type {, type }) typeconstr | |

| | typeconstr |

ftype | ::= | type -> type |

immediate | ::= | integer-literal |

| | float-literal | |

| | char-literal | |

| | string-literal | |

| | boolean-literal |

Constants are formed of literals from the base types (integers, floating-point numbers, characters, character strings, and booleans).

Patterns allow binding identifiers to the components of data structures.

pattern | ::= | ident |

| | ( pattern ) | |

| | pattern as ident | |

| | _ | |

| | pattern , pattern { , pattern } | |

| | () | |

| | immediate | |

| | constructor | |

| | { label = pattern { ; label = pattern } } |

Signal patterns allows for testing the presence of signals and for binding their values with patterns. A boolean expressions is also considered a signal pattern (in non-continuous contexts).

signal-pattern | ::= | simple-expr |

| | simple-expression pattern | |

| | signal-pattern on simple-expr | |

| | signal-pattern & signal-pattern | |

| | signal-pattern || signal-pattern |

simple-expr | ::= | value-path |

| | constructor | |

| | immediate | |

| | ( expr ) | |

| | { label = expr { ; label = expr } } | |

| | simple-expr . label | |

pattern-list | ::= | pattern { pattern } |

expr | ::= | simple-expr |

| | value-path simple-expr | |

| | let [ rec ] definition { and definition } in expr | |

| | if expr then expr else expr | |

| | prefix-op expr | |

| | expr infix-op expr | |

| | up expr | |

| | not expr | |

| | expr fby expr | |

| | pre expr | |

| | expr -> expr | |

| | last ident | |

| | match expr with match-handlers [ end ] | |

| | reset expr every expr | |

| | present present-handlers [ end ] | |

infix-op | ::= | infix-symbol | * | = | or | || | & |

match-handlers | ::= | [ | ] pattern -> expr { | pattern -> expr } |

present-handlers | ::= | [ | ] signal-pattern -> expr { | signal-pattern -> expr } |

The precedence and associativity rules of OCamlare adopted. The rules for Zélus-specific primitives are, in order from highest to lowest precedence:

last | right |

pre | - |

function application | - |

fby | left |

... let,... | - |

-> | right |

A constant expression, like 1 or false, denotes an infinite stream of that constant.

A variable evaluates to the value bound to that variable in the current evaluation environment.

The expression ( expr ) has the same value as expr.

The let and let rec constructs bind variables locally. The expression

let definition_{1} and ...
and definition_{n} in expr

defines values to be visible in expr. In a let definition, variables names appearing on the right of an equality are bound to their definition in the current environment. This environment does not contains names from the let definition itself.

Recursive definitions of variables are introduced by let rec:

let rec definition_{1} and ...
and definition_{n} in expr

In a recursive definition the current environment also contains names defined within the let construction itself.

The operators written infix-op in the grammar are applied by placing them between two expressions. The operators written prefix-op in the grammar are applied by placing them in front of an expression.

The basic operators provided by OCaml (from the Pervasives module) are imported. Scalar values imported from the host language become stream operators that are applied pointwise.

The expression pre expr denotes the delayed stream. The nth value of the result is the n−1th value of expr. The value at the first instant is undefined.

The binary operator fby is the initialized delay operator. The
first value of expr_{1} fby expr_{2} is the
first value of expr_{1}. The nth value is the n−1th
value of expr_{2}.

These two delay operators may only be activated on a *discrete clock*.
In Zélus (version 1.2) this is ensured by imposing that they appear only
in contexts of kind k = D.

The expression expr_{1} -> expr_{2}
initializes a stream.
The expr_{i} must be streams of the same type. The
first value of the result is the first value of
expr_{1}, after which the nth value of the result is the nth
value of expr_{2}.

The initialization operator must be activated on a *discrete clock*.

The expression last ident denotes the previous computed value of the variable ident.

As opposed to the unit delays, pre and fby, the
operator last only applies to variable names and it can be activated
on both *discrete* and *continuous* clocks.
Nonetheless, when last x appears in a continuous context,
Zélus (version 1.2) imposes that x be a continuous state variable; in
other words, it must be defined directly by an equation of the form
der x = e.

The expression if expr_{1} then
expr_{2} else expr_{3} is the pointwise
conditional: expr_{1} must be a boolean stream and
expr_{2} and expr_{3} must be two streams of the same
type. The type of the result is the type of expr_{2}.

Warning: this operator is strict, that is, at every step, both branches
are evaluated regardless of the value of the condition. The result at
instant n is the value of expr_{2} if the value of
expr_{1} is true and the value of expr_{3} otherwise.

The expression value-path simple-expr is the application of the function value-path to the expression simple-expr.

The constructions reset, match/with, reset, and automaton are control-structures which combine equations and thus belong to the syntactic class of definitions (see section 4.9).

A derived form belonging to the syntactic class of expressions is also provided. The derived form is useful for textual programming whereas the original one is motivated by the graphical representation of dataflow programs. The derived form is only syntactic sugar for the original form.

The expression
match expr with
pat_{1} -> expr_{1} | …| pat_{n} -> expr_{n} end
is a short-cut for the expression:

let | match expr with |

| pat_{1} ->
do o = expr_{1} done | |

… | |

| pat_{n} ->
do o = expr_{n} done | |

end in | |

o |

provided that o is a fresh name.

The expression reset expr_{1} every expr_{2}
is a short-cut for
let reset o = expr_{1}
every expr_{2} in o,
provided that o is a fresh name.

The expression
automaton state_{1} -> expr_{1}
trans_{1}
| …| state_{n} -> expr_{n}
trans_{n} end is a short-cut
for the expression:

let | automaton |

| state_{1} ->
do o = expr_{1} trans_{1} | |

… | |

| state_{n} ->
do o = expr_{n} trans_{n} | |

end in | |

o |

provided that o is a fresh name.

The expression
present
spat_{1} -> expr_{1} | …| spat_{n} -> expr_{n} end
is a short-cut for the expression:

let | present |

| spat_{1} ->
do o = expr_{1} done | |

… | |

| spat_{n} ->
do o = expr_{n} done | |

end in | |

o |

provided that o is a fresh name.

value-definition | ::= | let ident = expr |

| | [ let ] [ kind ] ident pattern = result-expr | |

function-kind | ::= | fun | node | hybrid |

result-expr | ::= | expr [ where [ rec ] definition { and definition } ] |

definition | ::= | pattern = expr |

| | init ident = expr | |

| | emit ident = expr | |

| | match expr with def-match-handlers [ end ] | |

| | reset definition { and definition } every expr | |

| | automaton def-automaton-handlers [ end ] | |

| | present def-present-handlers [ else definition ] [ end ] | |

| | [ local-definitions ] do definition-list done | |

definition-list | ::= | [ definition { and definition } ] |

local-definitions | ::= | { let [ rec ] definition { and definition } in } { local ident in } |

A global definition ident = expr defines the value of the global identifier ident to be equal to the value of expr in the current global environment. The expression expr must be combinatorial.

A global function definition is of the form:

[ let ] [ kind ] ident pattern =
result-expr

with

function-kind | ::= | fun | node | hybrid |

where

- fun is the kind of combinatorial functions—typically a function imported from the host language and applied pointwise. Its body result-expr must only contain combinatorial operations. In particular, it may not invoke stateful functions like unit delays or integrators.
- node is the kind of (possibly) stateful discrete-time functions—typically a synchronous function that must be activated on a discrete-time scale. Its body result-expr must only contain combinatorial and discrete-time stateful operations. In particular, it may not invoke continuous-time operators like integrators or zero-crossing detection.
- hybrid is the kind of (possibly) stateful continuous-time functions—typically a function that contains ODEs and/or zero-crossing detection and must be activated continuously. It may contain all kinds of operator provided that discrete-time operations are activated on discrete events.

The language provides an alternate form of local definitions for returning the results of functions. The expression:

expr where [ rec ]
definition_{1} and ... and definition_{n}

has the meaning of:

let [ rec ]
definition_{1} and ... and definition_{n}
in expr

The equation pattern = expr defines the current value of pattern to be equal to the current value of expr.

A definition init ident = expr initializes the value of last ident with the value of expr.

An equation emit ident = expr defines the signal ident to be equal to the value of expr. At every instant, a signal can be absent or present. When present, it carries a value.

def-match-handlers | ::= | [ | ] def-match-handler { | def-match-handler } |

def-match-handler | ::= | pattern -> definition |

The construct
match expr with pattern_{1} ->
action_{1} | ... | pattern_{n} ->
action_{n} end is used to combine n complementary
sub-streams. Each of these streams is on the clock defined by the
instants where the value of e has the form pattern_{i} .

Each definition can define local and shared variables. Shared variables are variables that may be defined and used across several branches and which are not bound by a local construct.

The construct reset definition_{1} and ...
and definition_{n} every expr allows
for resetting the computation defined by a set of definitions. All the
defined values and expression expr must be on the same
clock. This construction acts as a regular multi-definition except
that the streams and automata defined in
definition_{1},..., definition_{n} restart with their
initial values every time the current value of *expr* is true. In
particular, automata appearing in definition_{1},...,
definition_{n} restart in their initial states.

def-automaton-handlers | ::= | [ | ] def-automaton-handler { | def-automaton-handler } |

def-automaton-handler | ::= | constructor [ pattern ] -> automaton-definition |

automaton-definition | ::= | local-definitions do definition-list transitions |

transitions | ::= | done |

| | then state-expression | |

| | continue state-expression | |

| | unless transition { else transition } | |

| | until transition { else transition } | |

transition | | | signal-pattern then [ local-definitions do definition-list ] in state |

| | signal-pattern continue [ local-definitions do definition-list ] in state | |

state-expression | ::= | constructor |

| | constructor ( expr ) |

The construction automaton def-automaton-handler | ... | def-automaton-handler end defines an automaton. Each branch of the automaton has either the form:

constructor -> automaton-definition

or the form

constructor pattern -> automaton-definition

where constructor denotes the name of the state. This state may be parameterized by a pattern. The first branch defines the initial state and this state cannot be parameterized unless an initialization clause is given.

The action associated to a state has the form:

local-definitions do definition-list
transitions

It comprises a (possibly empty) sequence of local definitions to the state, a definition list of shared variables, and a (possibly empty) list of transitions to be tested sequentially. Transitions may have several forms. Writing:

until transition { else transition }

defines a *weak transition* which is executed within the current reaction
but at the end of it, that is, *after* definitions from the current state have
been executed. Transitions are all evaluated in the same instant but
sequentially: the first transition to succeed determines the target
state at the next reaction. Writing:

unless transition { else transition }

defines a *strong transition* which is executed *before* the
reaction starts, that is, before definitions from the current state
have been executed. Transitions are all evaluated in the same instant
but sequentially: the first transition to succeed determines the
current active state.

A transition may reset or not the history of the state being entered. Writing:

signal-pattern then
[ local-definitions do definition-list ]
in state

indicates that the target state is *entered by reset*, that is, all
streams and automata in the target state restart with their initial
values.
Writing:

signal-pattern continue
[ local-definitions do definition-list ]
in state

has the same behavior except that the target state is *entered by
history*, that is, no reset occurs. For both kinds of transition
(reset or history), the condition signal-pattern is
tested. When it is true, local-definitions do
definition-list in state are executed in
the same reaction.

The language provides two transition shorthands:

- The transition then state is shorthand for until true then state
- The transition continue state is shorthand for until true continue state.

Zélus (version 1.2) forbids the mixing of weak and strong conditions within a single automaton (not counting nested automata). This differs from Lucid Synchrone, for example, which allows for arbitrary combinations within an automaton. We made this choice to simplify code generation and allow for more efficient execution. But we may lift this restriction in a future release.

The present construct resembles the pattern-matching one. It has the form:

present def-present-handlers [ else definition ]
end

where a handler has the form:

def-present-handlers | ::= | [ | ] def-present-handler { | def-present-handler } |

def-present-handler | ::= | signal-pattern -> definition |

At every instant, signal patterns are tested sequentially and the one which first succeeds determines the action to execute. The optional handler:

else definition

defines a condition which always succeed and thus gives a default action.

Abstract types can be defined. Their syntax is inherited from OCaml and recalled here.

type-definition | ::= | type typedef { and typedef } |

typedef | ::= | [ type-params ] typeconstr-name |

| | sum-type-def | |

| | record-type-def | |

sum-type-def | ::= | [ | ] one-sum-def { | one-sum-def } |

one-sum-def | ::= | capitalized-ident |

record-type-def | ::= | { label-type { ; label-type } } |

label-type | ::= | ident : type |

type-params | ::= | ’ ident |

| | ( ’ ident { , ’ ident } ) |

implementation | ::= | { impl-phrase [ ;; ] } |

impl-phrase | ::= | value-definition |

| | type-definition | |

| | open module-name |

A module implementation comprises a sequence of implementation phrases. An implementation phrase either opens a module, declares a type, or defines a sequence of values.

- The instruction open modifies the list of opened modules by adding the module name to the head of the list of opened modules.
- The type definition defines a type from the implementation phrases following the definition.
- The value definition defines global values.

Scalar interfaces written in OCaml can be imported into Zélus. In the current implementation, a restricted subset of OCaml interfaces is considered. The syntax is the following:

scalar-interface | :: = | { scalar-interface-phrase [ ;; ] } |

scalar-interface-phrase | ::= | value-declaration |

| | type-definition | |

value-declaration | ::= | val ident : type |

When a value is imported from OCaml, it is automatically lifted to the stream level:

- A scalar value with a basic or declared type becomes an infinite stream of that type.
- A scalar functional value becomes a stream functional value applied pointwise to its argument.