Génération

La génération d'extended code (abrégé EC dans la suite) n'est pas documenté par l'implémentation officielle. Cette page cherche donc à fournir une documentation expliquant comment générer un tel code à partir d'un fichier Lustre écrit par un⋅e utilisateurice. Elle se base sur le code de l'implémentation officielle et l'observation de ses sorties.

Types

Seuls les types de base (int/bool/real) sont conservés. Les types « anonymes » sont également conservés.

Pour les variables de type tableau, on remplace chaque élément du tableau par une variable unique.

const x : int^3 = [1, 2, 3];

-- devient

const x_0 : int = 1;
const x_1 : int = 2;
const x_2 : int = 3;

Les énumérations sont remplacées par un type anonyme et un ensemble de constante externes.

type e = enum { A, B };

const e_value : e = A;

-- devient

type e;
const A : e;
const B : e;

const e_value : e = A;

Les structures sont remplacées par des variables individuelles pour chacun de leur champs.

type s = { x : int; y : real };
const s_value : s = s { x = 42; y = 3.1415 };

-- devient

const s_value_x = 42;
const s_value_y = 3.1415;

Nœuds

Les expressions sont séparées pour obtenir un seul opérateur par équation/assertion.

assert x and y and z;
z = x or y and (a < 12);

-- devient

assert_1 = x and y;
assert_2 = assert_1 and z;
assert assert_2;

a_lt_12 = a < 12;
x_or_y = x or y;
z = x_or_y and a_lt_12;

Les opérateurs suivants sont étendus : map, fill, red, fillred, boolred, condact, diese, merge, nor.

Packages

À faire plus tard…

Prise de note

Quand on compile un programme Lustre avec lv6 -ec, plusieurs options sont en réalité activées¹ :

les options pour générer du code LV4 sont activées
- les itérateurs sont inlinés (???) (global_opt.inline_iterator <- true;)
- when_on_ident <- true
- les arrays sont étendues (opt.expand_arrays <- true)
les énumérations sont transformées en constantes
on élimine les when not (no_when_not)
on supprime les préfixes (no_prefix)
on étend les nœuds (opt.expand_nodes <- true)