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.

Keywords

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.

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

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

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

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

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

4.4  Types

4.5  Constants

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.

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

4.8  Expressions

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

4.8.1  Simple expressions

Constants

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

Variables

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

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:

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

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 expr₁ -> expr₂ 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₁, after which the nth value of the result is the nth value of expr₂.

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 expr₁ then expr₂ else expr₃ is the pointwise conditional: expr₁ must be a boolean stream and expr₂ and expr₃ must be two streams of the same type. The type of the result is the type of expr₂.

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₂ if the value of expr₁ is true and the value of expr₃ 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 pat₁ -> expr₁ | …| pat_n -> expr_n end is a short-cut for the expression:

provided that o is a fresh name.

Modular Reset over Expressions

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

Automata

The expression automaton state₁ -> expr₁ trans₁ | …| state_n -> expr_n trans_n end is a short-cut for the expression:

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

provided that o is a fresh name.

Testing Presence

The expression present spat₁ -> expr₁ | …| spat_n -> expr_n end is a short-cut for the expression:

provided that o is a fresh name.

4.9  Definitions

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:

with

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.

Alternative Syntax for Local Definitions

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

has the meaning of:

Equation

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

The construct match expr with pattern₁ -> action₁ | ... | 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.

Reinitialization

The construct reset definition₁ 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₁,..., definition_n restart with their initial values every time the current value of expr is true. In particular, automata appearing in definition₁,..., definition_n restart in their initial states.

Hierarchical Automata

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

or the form

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:

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:

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:

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:

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:

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:

where a handler has the form:

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

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.

4.11  Module implementation

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:

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.