Chapter 4  The language

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.

4.1  Lexical conventions

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

The following character sequences are also keywords.

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

4.2  Values

4.2.1  Basic values

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

4.2.2  Tuples, records, sum types

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.

4.3  Global names

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.

4.3.1  Naming values

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

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.

4.3.2  Referring to named values

    | module-name . value-name
    | module-name . capitalized-ident
    | module-name . typeconstr

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

4.4  Types

type::= ident
    | ( type )
    | type {* type}
    | type typeconstr
    | ( type {, type }) typeconstr
    | typeconstr
ftype::=type -> type

4.5  Constants

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

4.6  Patterns

Patterns allow binding identifiers to the components of data structures.

    | ( pattern )
    | pattern as ident
    | _
    | pattern , pattern { , pattern }
    | ()
    | immediate
    | constructor
    | { label = pattern { ; label = pattern } }

4.7  Signal Patterns

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

    | simple-expression pattern
    | signal-pattern on simple-expr
    | signal-pattern & signal-pattern
    | signal-pattern || signal-pattern

4.8  Expressions

    | constructor
    | immediate
    | ( expr )
    | { label = expr { ; label = expr } }
    | simple-expr . label
pattern-list::=pattern { pattern }
    | 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:

function application-
... let,...-

4.8.1  Simple expressions


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.

Parenthesized expressions

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

Local definitions

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

let definition1 and ... and definitionn 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 definition1 and ... and definitionn in expr

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

4.8.2  Operators

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.

Unit Delays

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 expr1 fby expr2 is the first value of expr1. The nth value is the n−1th value of expr2.

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.

Initialization Operation

The expression expr1 -> expr2 initializes a stream. The expri must be streams of the same type. The first value of the result is the first value of expr1, after which the nth value of the result is the nth value of expr2.

The initialization operator must be activated on a discrete clock.

Access to a Shared State Variable

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.

Point-wise conditional

The expression if expr1 then expr2 else expr3 is the pointwise conditional: expr1 must be a boolean stream and expr2 and expr3 must be two streams of the same type. The type of the result is the type of expr2.

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 expr2 if the value of expr1 is true and the value of expr3 otherwise.

Function application

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

4.8.3  Control Structures

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.

Pattern Matching over Expressions

The expression match expr with pat1 -> expr1 || patn -> exprn end is a short-cut for the expression:

let match expr with
| pat1 -> do o = expr1 done
| patn -> do o = exprn done
end in

provided that o is a fresh name.

Modular Reset over Expressions

The expression reset expr1 every expr2 is a short-cut for let reset o = expr1 every expr2 in o, provided that o is a fresh name.


The expression automaton state1 -> expr1 trans1 || staten -> exprn transn end is a short-cut for the expression:

let automaton
| state1 -> do o = expr1 trans1
| staten -> do o = exprn transn
end in

provided that o is a fresh name.

Testing Presence

The expression present spat1 -> expr1 || spatn -> exprn end is a short-cut for the expression:

let present
| spat1 -> do o = expr1 done
| spatn -> do o = exprn done
end in

provided that o is a fresh name.

4.9  Definitions

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 }

Global Value Definition

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.

Global Function Definition

A global function definition is of the form:

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


function-kind::=fun  |  node  |  hybrid


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

Alternative Syntax for Local Definitions

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

expr where [ rec ] definition1 and ... and definitionn

has the meaning of:

let [ rec ] definition1 and ... and definitionn in expr


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

Initialization of a State Variable

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

Signal Emission

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.

Pattern Matching

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

The construct match expr with pattern1 -> action1 | ... | patternn -> actionn 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 patterni .

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 definition1 and ... and definitionn 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 definition1,..., definitionn restart with their initial values every time the current value of expr is true. In particular, automata appearing in definition1,..., definitionn restart in their initial states.

Hierarchical Automata

def-automaton-handlers::=[ | ] def-automaton-handler { | def-automaton-handler }
def-automaton-handler::=constructor [ pattern ] -> automaton-definition
automaton-definition::=local-definitions do definition-list transitions
    | 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
    | 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:

  1. The transition then state is shorthand for until true then state
  2. 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.

Testing the Presence of a Signal

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.

4.10  Type definition

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 }
record-type-def::={ label-type { ; label-type } }
label-type::=ident : type
type-params::= ident
    | ( ident { , ident } )

4.11  Module implementation

implementation::={ impl-phrase [ ;; ] }
    | 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.

4.12  Importing 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 [ ;; ] }
    | 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.