Heptagon

Langage fonctionnel à flux de données

\RA produits des automates

node identite(x : int) returns (o : int)
let
  o = x;
tel

Nœud = fonction de flots

Compilation

Fichier .ept \xrightarrow{hept} fichiers .c \xrightarrow{gcc} exécutable

heptc -target c -s identite test.ept

• -i : affiche les types compilés

heptc -i -target c -s identite test.ept :

val identite(x : int :: .) returns (o : int :: .)

\text{identite. } int^{\omega} \ra int^{\omega}

Monde simple, les objets définis sont utilisés.

node identite(x : int) returns (o : int)
var y : int
let
  o = x;
tel

y doit être utilisé.

Heptagon n’est pas un langage impératif, on définit des équations.
On fait des conjonctions (définitions simultanées), l’ordre n’est pas important ; tout est vrai.

Insensible à l’ordre des équations
\RA Définitions mutuellement récursives

Dans un programme Heptagon valide, on peut toujours calculer une valeur. Rejette les programmes non causaux (le compilateur fait une analyse de causalité/productivité).

y = y (* erreur de causalité *)

Programmation Flots-de-données et causalité

Opérateurs combinatoires

node f() returns (x, y : int, z : bool)
let
  x = 1;
  y = 42;
  z = false;
tel

node g() returns (o: int)
let
  (* motif *)
  (x, y, z) = f();
  o = x;
tel

Equivaut à :

e expression Heptagon
\lb e \rb sémantique de e (une suite)
\lb l \rb_{n} = l avec \lb l \rb_{n} la constante littérale (42, 1, \text{False}) (n c’est l’instant n aka le temps)
\lb e_{1} + e_{2} \rb_{n} = \lb e_{1} \rb_{n} + \lb e_{2} \rb_{n}
\lb e_{1} - e_{2} \rb_{n} = \lb e_{1} \rb_{n} - \lb e_{2} \rb_{n}
…
\lb e_{1} \text{ op } e_{2} \rb_{n} = \lb e_{1} \rb_{n} \text{ op } \lb e_{2} \rb_{n} avec \text{op} un opérateur quelconque

\lb\text{if }e_{1}\text{ then }e_{2}\text{ else }e_{3}\rb_{n} = \begin{cases} \lb e_{2} \rb_{n} & \text{ si } \lb e_{1} \rb_{n} = \text{ True} \\\\ \lb e_{3} \rb_{n} & \text{ si } \lb e_{1} \rb_{n} = \text{ False} \end{cases}

Opérateurs séquentiels

• Opérateur Fby (Followed by) : décalage
  \lb e_{1}\text{ fby }e_{2}\rb_{n} = \begin{cases} \lb e_{1} \rb_{0} & \text{ si } n = 0 \\\\ \lb e_{2} \rb_{n-1} & \text{ si } n > 0 \end{cases}

Comportement temporel, il y a un état.

Exercice

(* Définir un noeud half dont la sortie o est un
   flot booléen qui alterne entre les valeurs
   true et false, en commençant par true. *)
node half() returns (o : bool)
let
  o = true fby not o;
tel

(* on peut aussi faire *)
node half() returns (o : bool)
let
  o = true fby false fby o;
tel

Chronogramme associé :

o = true fby not o
  = true fby not (true fby not o)
  = true fby (not true) fby not (not o)
  = true fby false fby o (* c'est notre solution 2 !!*)
  = true fby false fby true fby false fby ...

Notes

e1 fby e2 fby e3 = e1 fby (e2 fby e3) ce qui est la conséquence de chaîner plusieurs fby.
\RA associatif à droite

Exercice

(* o1 est comme la fonction half(), o2 est l'inverse en gros *)
node halves() returns (o1, o2 : bool)
let
  o1 = true fby o2;
  o2 = false fby o1; (* on peut aussi faire o2 = not o1 *)
tel

Exercice

Disgression : positif, c’est >= 0, positivee (anglais) c’est > 0

node j() returns (nat, pos : int)
let
  nat = 0 fby pos; (* suite des naturels *)
  pos = nat + 1;   (* suite des naturels *strictement positifs* *)
tel

En faisant une équation :

nat = 0 fby pos
    = 0 fby (nat + 1)
    = 0 fby ((0 fby (nat + 1)) + 1)
    = 0 fby 1 fby (nat + 2)
    = 0 fby 1 fby ((0 fby (nat + 1)) + 2)
    = 0 fby 1 fby 2 fby (nat + 3) 

• Opérateur pre
  \lb \text{pre } e \rb_{n} = \begin{cases} \text{nil} & \text{ si } n = 0 \\\\ \lb e \rb_{n-1} & \text{ si } n > 0 \end{cases}

• Opérateur -> appelé “init”
  \lb e_{1} \ra e_{2} \rb_{n} = \begin{cases} \lb e_{1} \rb_{0} & \text{ si } n = 0 \\\\ \lb e_{2} \rb_{n} & \text{ si } n > 0 \end{cases}

Exemple

node j4() returns (x : int)
let
  x = 0 -> (pre x + 1);
tel

\lb e_{1} e_{1} \text{ fby } e_{2} \rb_{n} = \lb e_{1} \ra \text{pre } e_{2} \rb_{n} = \begin{cases} \lb e_{1} \rb_{0} & \text{ si } n = 0 \\\\ \lb \text{pre } e_{2} \rb_{n} = \lb e_{2} \rb_{n-1} & \text{ si } n > 0 \end{cases}

Analyses statiques

Typage, causalité, initialisation, horloges…

Causalité

```ocaml
node j() returns (nat, pos : int)
let
  nat = 0 -> pos; 
  pos = nat + 1;
tel

Mémo lecture erreur
|| = en parallèle
^qqch = je dois lire qqch
^pos < nat = je dois lire pos avant nat

$ hept -s j -t test.ept 
File "test.ept", line 1-5, characters 0-3:
>node j() returns (nat, pos : int)
>let
>  nat = 0 -> pos;
>  pos = nat + 1;
>tel
Causality error: the following constraint is not causal.
^pos < nat
 || ^nat < pos