Prof de TP : gabriel.scherer@irif.fr

Programmation synchrone

Système réactif

Heptagon installé : heptc

Ce qu’on a appris jusqu’ici

• Programmation (langages)
  • OCaml, C, C++, Python
• Algorithmique
  • Modèle et Spécification, tris, graphe
• Programmation transformationnels (par opposition à réactif) (merci Zohar Manna et Amir Pnueli)
  • aka lis une entrée, calcule et produis une sortie
  • Exemple transformationnel : sort (UNIX), gcc

Programmation réactive

Exemple réactif

• Pilote automatique
  • Depuis les années 80 : il y a une assistance automatique en permanence pendant un vol d’avion, même lorsqu’on est en mode manuel (fly-by-wire).
• Modem
• Four sophistiqué
• ABS

Caractéristiques essentielles des systèmes réactifs

• Criticité
  • Coût démesuré (vies humaines)
  • Exemple : Vol 501 d’Ariane V (coût : centaine de millions d’euros)
    • L’institut INRIA a participé aux réunions concernant cet événement.
  • Exemple : Machine Therac-25 : 6 irradiations massives, trois mortels
  • En général :
    • Aéronautique (fly-by-wire)
    • Médical (radiothérapie) : pompes à insuline, pacemaker…
    • Militaire (guidage des missiles…)

Dans le logiciel critique, il faut faire “ceinture et bretelle”.

• Temps-réel : réagir dans un intervalle de temps fixé
  • Exemple : TCAS-II

Correction temporelle $\leftrightarrow$ correction fonctionnelle $\RA$ il y a des cas où ça va ensemble

• Mathématiques dédiées
  • Systèmes dynamiques
  • Automatique (+ appliquée que les systèmes dynamiques) $\RA$ Control Theory // sous-texte du cours

Mathématiques nées avec la révolution industrielle

Exemple : Régulateur à boules de Watt

• Contraintes de ressources
  • Matériel informatique dédié embarqué : contraintes de performances, de batterie (énergie), en espace (mémoire), de temps (lié à l’aspect algorithmique)
  • Lié à la compilation, au système d’exploitation, etc.

Langages synchrones

Langages spécialisés pour la programmation des systèmes réactifs

Objectifs

• Aider la programmation à un haut niveau de sûreté
• Faciliter le respect des contraintes temps réel
• Proche des mathématiques dédiées (proche du concept de l’automatique)

$\RA$ Idée sous-jacente : Notion de temps logique, discret et global

Langages conçus en France : à Grenoble (notamment), Nice, Rennes et Paris.

Schéma-bloc

Utilisés pour palier les besoins des ingénieurs avec un background “automatique” vers le code C

• On programmait directement avec les dessins, un fil = une suite infinis de données
• SCADE 6 était un programme pour ça, c’était un peu comme un compilateur en somme

Heptagon : la programmation synchrone a flots de données

Cf. Dossier de code

Exécution cyclique à 3 phases :

• Lecture (capteurs/état)
• Calcul
• Écriture (actionnaires/état)

A la fin de développement : vérification des contraintes temporelles.

On programme dans un langage avec un temps logique et un temps discret.

On considère qu’entre le début et la fin du cycle, aucun temps ne s’est écoulé, afin que l’environnement n’ait pas le temps de changer.

D’un certain point de vue, on peut représenter un programme synchrone comme une machine à état / un automate (à mémoire) finie et déterministe. Notre automate, en plus d’avoir des entrées, possède des sorties, c’est un transducteur.

Pour prouver si deux automates sont égaux, on peut faire une bisimulation.

Une bisimulation est une relation $R \subseteq S \times S$ tel que $\forall (s_{1}, s_{2}) \in R$, on a :

1. $s_{1}$ final $\Leftrightarrow$ $s_{2}$ est final
2. Si $s_{1} \xrightarrow{a} s_{1}'$, il existe $s_{2}'$ tel que $s_{2} \xrightarrow{s_{2}'}$ et $(s_{1}', s_{2}') \in R$
   
3. si $s_{2} \xrightarrow{a} s_{2}'$, il existe $s_{1}'$ tel que $s_{1} \xrightarrow{a} s_{1}'$ et $(s_{1}', s_{2}') \in R$

Théorème : deux états finaux $s_{1}$ et $s_{2}$ reconnaissent le même langage ssi il existe une bisimulation $R$ telle que $(s_{1}, s_{2}) \in R$

Exemple :
Bisimulation : $R = \{ (x, u)_{x}, (y, v)_{x}, (y, w)_{x}, (z, w)_{x}, (z, v)_{x} \}$

Exemple transducteur :

Heptagon

Langage fonctionnel à flux de données

$\RA$ produits des automates

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

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
 
Copier

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é *)
Copier

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
 
Copier

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
 
Copier

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

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
 
Copier

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
Copier

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

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

$$\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
 
Copier

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
 
Copier

Réinitisalisation (modulaire)

Bloc = Soit une liste de blocs, soit une liste d’équations soit la réinitialisation d’un bloc (entre let et tel)
Exemple de bloc de réinitialisation : reset bloc every expression

node nat_reset() returns (o : int)
var c : bool;
let
  reset o = 0 fby (o + 1) every c;
  c = true fby false fby false fby c;
tel
 
(* qui est équivalent à *)
node nat_reset2() returns (o : int)
var c : bool;
let
  o = if c then 0 else (0 fby (0 + 1));
  c = true fby false fby false fby c;
tel
 
Copier

(* exemple avec une fonction externe *)
node nat() returns (o : int)
let
  o = 0 fby (o + 1);
tel
 
node nat_reset() returns (o : int)
var c : bool;
let
  (* fonctionne avec une fonctionne *)
  reset o = nat() every c;
  c = true fby false fby false fby c;
tel
 
(* ça, ça ne fonctionne pas *)
node nat_reset2() returns (o : int)
var c : bool;
let
  o = if c then 0 else nat();
  c = true fby false fby false fby c;
tel
 
Copier

Reset = réinitialisation modulaire, passe à travers les abstractions
Utile, mais rend le programme rapidement incompréhensible.

Types structurés et énumérés

Types structurés

type cpl = { re : float; im : float }
 
node add(x, y: cpl) returns (o: cpl)
let
  o = { re = x.re +. y.re
      ; im = x.im +. y.im };
tel
 
node conj(x: cpl) returns (o: cpl)
let
  o = { re = x.re
      ; im = -.x.im };
tel
 
Copier

Mot-clé fun permet de définir une node qui ne dépend pas du temps (pas d’état). Donc, par exemple, fby est rejeté des fun.

type cpl = { re : float; im : float }
 
fun add(x, y: cpl) returns (o: cpl)
let
  o = { re = x.re +. y.re
      ; im = x.im +. y.im };
tel
 
fun conj(x: cpl) returns (o: cpl)
let
  o = { re = x.re
      ; im = -.x.im };
tel
 
Copier

Types énumérés

type alpha = A | B | C (* commence par une majuscule, alpha est soit A, B, ou C *)
type etats = X | Y | Z | Mort
 
node automate(l : alpha) returns (accept : bool)
var etat_courant, etat_precedent : etats;
let
  etat_courant =      if (etat_precedent, l) = (X, A) then Y
                 else if (etat_precedent, l) = (Y, B) then Z
                 else if (etat_precedent, l) = (Y, C) then Y
                 else if (etat_precedent, l) = (Z, A) then Y
                 else Mort;
  etat_precedent = X fby etat_courant;
  accept = (etat_courant = Z);
tel
 
Copier

Horloges

Exercice : Définir une suite $o : int$ telle que $o_{2k} = k$ $o_{2k+1}=0$

$o = 0, 0, 1, 0, 2, 0, 3, 0, 4, 0, \dots$

node k() returns (o: int)
var p: bool; v: int;
let
  o = if p then v else 0;
  v = 0 fby if p then v else (v + 1);
  p = true fby not p;
tel
 
Copier

On remarque que $o$ c’est la suite naturelle séparée de $0$.
On peut donc mélanger/entrelacés la suite des entiers naturels et la suite des 0.

Opérateur d’entrelacement merge

node nat() returns (o : int)
let
  o = 0 fby (o + 1);
tel
 
node k() returns (o: int)
var p: bool; v: int;
let
  o = merge p v 0;
  v = nat();
  p = true fby not p;
tel
 
Copier

Contrairement au if qui va perdre des données, le mélange entrelace les flux alors que le if/else choisis quelle valeur garder à un instant $t$.

Dans notre cas, p est notre horloge, p permet d’alterner le calcul entre p et v.

Sémantique

$$\begin{aligned} & \lb \text{merge } c e_{1} e_{2} \rb \\ &\begin{cases} \lb e_{1} \rb_{k} & \text{si } \lb c \rb_{k} = \text{ true et } \lb e_{1} \rb \neq \text{abs}, \lb e_{2} \rb_{k} = \text{abs} \\ \lb e_{2} \rb_{k} & \text{si } \lb c \rb_{k} = \text{ false et } \lb e_{1} \rb = \text{abs}, \lb e_{2} \rb_{k} \neq \text{abs} \\ \text{abs} & \text{si } \lb c \rb_{k} = \text{ abs et } \lb e_{1} \rb = \lb e_{2} \rb_{k} = \text{abs} \end{cases} \end{aligned}$$

Opérateur de sélection (échantillonnage) e when c

Sémantique

$$\begin{aligned} & \lb e \text{ when } c \rb \\ &\begin{cases} \lb e \rb_{k} & \text{si } \lb c \rb_{k} = \text{ true et } \lb e \rb_{k} \neq \text{abs} \\ \text{abs} & \text{si } \lb c \rb_{k} = \text{ false et } \lb c \rb_{k} = \text{abs} \end{cases} \end{aligned}$$

En contraste, voici le tableau pour les additions

$\lb e_{1} \rb_{k}$	$\lb e_{2} \rb_{k}$	$\lb e_{1} + e_{2} \rb_{k}$
$\neq$ abs	$\neq$ abs	$\lb e_{1} \rb_{k} + \lb e_{2} \rb_{k}$
abs	abs	abs

Si on a une sortie avec une horloge spéciale, il faut renvoyer l’horloge

node nat() returns (o : int)
let
  o = 0 fby (o + 1);
tel
 
node h() returns (p: bool; o: int)
var x : int;
let
  x = nat();
  p = true fby not p;
  o = x when p;
tel
 
Copier

when false(p) $=$ when not p

Intégrateur

node itgr(y, delta, x0 : float :: .) returns (o : float :: .) (* :: . est inféré par le compilo *)
var area : float;
let
  area = delta *. y;
  o = (x0 fby o) +. area;
tel
 
(* là on integre quand meme dans itgr donc on va garder le calcul qu'on veut pas *)
node itgr_enable_bad(y, delta, x0 : float; enable : bool) returns (o : float)
var oi : float;
let
  oi = itgr(y, delta, x0) when enable; (*= j'integre tout, tout le temps *)
  o = merge enable oi ((x0 fby o) whenot enable); (* maintenant je filtre *)
tel
 
(* on appelle l'intégrateur uniquement au besoin *)
node itgr_enable(y, delta, x0 : float; enable : bool) returns (o : float)
var oi : float;
let
  (* on faite la on décide de notre horloge de base, ici cest when enable *)
  oi = itgr(y when enable, delta when enable, x0 when enable);
  o = merge enable oi ((x0 fby o) whenot enable); (* grâce au merge on a un o propre *)
tel
 
Copier

Automates

Construction de contrôle.

Grammaire

block = eq
      | block; block
      | reset block every expression
      | automaton ... end
 
Copier

Automate : plusieurs états avec chacun un bloc d’équations, avec un état “éveillé” et les autres “dormants”.

type lettre = A | B | C
 
node p(l : lettre) returns (accept : bool)
let
  automaton
    state X (* état initial pcq c'est le premier *)
      do accept = false
      unless l = A then Y
        
    state Y
      do accept = false
      unless l = B then Y (* tester dans l'ordre d'apparition *)
           | l = C then Z
 
    state Z
      do accept = true
      unless l = A then Y
 
  end  
tel
 
Copier

Il faut rajouter l’état Dead qui gère quand on sors de l’automate

type lettre = A | B | C
 
node p(l : lettre) returns (accept : bool)
let
  automaton
    state X (* état initial pcq c'est le premier *)
      do accept = false
      unless l = A then Y
           | true  then Dead
        
    state Y
      do accept = false
      unless l = B then Y (* tester dans l'ordre d'apparition *)
           | l = C then Z
           | true  then Dead
 
    state Z
      do accept = true
      unless l = A then Y
           | true  then Dead
 
    state Dead
      do accept = false
  end  
tel
 
Copier

Transitions fortes/faibles

unless $c_{1}$ then $s_{1} | \dots | s_{n}$ then $s_{n}$

• unless est une transition fortes

node a0() returns (o : bool)
let
  automaton
    state A
      do o = true
      unless true then B
 
    state B
      do o = false
  end
tel
 
Copier

until $c_{1}$ then $s_{1} | \dots | s_{n}$ then $s_{n}$

• until est une transition faible

node a1() returns (o : bool)
let
  automaton
    state A
      do o = true
      until true then B
 
    state B
      do o = false
  end
tel
 
Copier

node a3() returns (o : int)
let
  automaton
    state A
      do o = 1
      unless true then B
 
    state B
      do o = 2
      until true then C
    state C
      do o = 3
  end
tel
 
(* seul cas avec un *cas transitoire* *)
node a4() returns (o : int)
let
  automaton
    state A
      do o = 1
      until true then B
 
    (* skipped *)
    state B
      do o = 2
      unless true then C
    state C
      do o = 3
  end
tel
 
Copier

Transitions réinitialisante/continuante

• Réinitialisante : then

node f0() returns (o : int)
let
  automaton
    state X
      do o = 0 fby (o + 1)
      until (o >= 3) then Y
 
    state Y
      do o = 42
      until true then X (* a chaque fois qu'on envoie 42, on reviens sur X *)
  end
tel
 
Copier

On réinitialise quand on arrive dans l’état.

node f0() returns (o : int)
let
  automaton
    state X
      do o = 0 fby (o + 1)
      until (o >= 3) then Y
 
    state Y
      do o = 42
      unless true then X (* on regarde le unless qui est tjrs true alors le 42 sert à rien *)
  end
tel
 
Copier

node f0() returns (o : int)
let
  automaton
    state X
      do o = 0 fby (o + 1)
      until (o >= 3) then X (* reinitialisation de l'état X, sans Y *)
  end
tel
 
Copier

• Continuante : continue

node f0() returns (o : int)
let
  automaton
    state X
      do o = 0 fby (o + 1)
      until (o >= 3) continue X (* on reviens à X sans réinitialiser, donc ça fais rien *)
  end
tel
 
Copier

node f0() returns (o : int)
let
  automaton
    state X
      do o = 0 fby (o + 1)
      until (o >= 3) continue Y (* quand on va revenir apres Y, on a pas réinitalisé
                                 * alors part direct après l'entier *)
 
    state Y
      do o = 42
      until true continue X (* a chaque fois qu'on envoie 42, on reviens sur X *)
  end
tel
 
Copier

Exemple du bouton

Ce cas illustre que la valeur précédente de o est relative à la définition de l’état, pas au o global.

node switch3bad(b : bool; s : int) returns (o : int)
let
  automaton
    state Idle
      do o = 0 -> (pre o);
      unless b continue Increment
 
    state Increment
      do o = (0 -> pre o) + s
      unless b continue Multiply
 
    state Multiply
      do o = (0 -> pre o) * s
      unless b continue Idle
  end
tel
 
Copier

On peut utiliser le mot clé last

node switch3(b : bool; s : int) returns (last o : int = 0)
let
  automaton
    state Idle
      do (* o = last o; *) (* ne sert à rien car conserve le dernier état *)
      unless b continue Increment
 
    state Increment
      do o = last o + s
      unless b continue Multiply
 
    state Multiply
      do o = last o * s
      unless b continue Idle
  end
tel
 
Copier

• Variable last est tout le temps défini.
• last ne s’applique qu’à une variable définie par last
• last conserve son état

block ::= (x1, ..., xn) = expr
        | block; block
        | automaton ... end (* automaton dans automaton possible ! *)
        | reset block every expr
        | if expr then block else block
        | present ... end
        | switch ... end
 
Copier

Exemple automaton dans automaton

node f(cmd : bool) returns (o : float)
let
  automaton
    state Init (* état d'initialisation *)
      do o = 0.0
      unless cmd then Cruise
 
    state Cruise (* état de croisière *)
      var y : float;
      do automaton
        state A
          do y = 0.0 fby (y +. 1.0)
          until y >=. 10.0 then B
 
        state B
          do y = 1.0 fby (2.0 *. y)
          until y >=. 128.0 then A
      end;
      o = y +. 10.0;
  end
tel
 
Copier

switch et present

type color = Green | Amber | Cyan
 
fun color2rgb(c : color) returns (r, g, b : float)
let
  switch c
    | Green
      do r = 0.0; g = 1.0; b = 0.0
    | Amber
      do r = 1.0; g = 0.75; b = 0.0
    | Cyan
      do r = 0.0; g = 1.0; b = 1.0
  end
tel
 
fun sign(x : float) returns (o : float)
let
  present (* le booléen doit être combinatoire (sans état) *)
    | x >. 0.0 do o =    1.0
    | x <. 0.0 do o = -. 1.0
    default    do o =    0.0
  end
tel
 
Copier

• Les tableaux en Heptagon sont persistants (non mutable)
• Taille fixée à la compilation ?

Les tableaux

• Type des tableaux d’entiers de taille 10 : int^10.
• Type des tableaux de booléens de taille 30 : bool^30.
• Type de matrice (tableau à deux dimensions) de flottants de taille 5x5 : float^5^5.
• Type des tableaux de taille $n$ dont les éléments de type $t$ : t^n avec $t$ un type et $n$ une expression statique (valeur déterminée à la compilation, exemple : une constante littérale).

node arr0() returns (o1, o2, o3 : int^3)
let
  o1 = [0, 1, 2];
  o2 = 42^3;
  o3 = o1 fby o2;
tel
 
node arr1() returns (o : int^2)
var n : int;
let
  n = 0 fby (n + 2);
  o = [n, n + 1];
tel
 
Copier

expr[expr]
     ----
     |> expression statique (* permet au compilo de rester dans les bornes du tableau *)
 
expr[> expr <]
       ----
       |> expression (* quelconque, pas besoin que ça soit statique *)
 
expr.[expr] default expr
      ----
     |> expression
 
[ expr with [ expr ] = expr ]
  ---- ----   ----     ----
  |    |      |        |> : t
  |    |      |> : int
  |    |> mot clé
  |> : t^n
 
Copier

Exemple registre à décalage

(* les constructions dynamique sont à chier parce que si on a un bug il faudra débogguer *)
(* 3 bits + 1 entier de registre utilisé *)
node shiftr3dyn(ini : bool^3) returns (o : bool)
var mem : bool^3; idx : int;
let
  mem = ini fby mem;
  idx = 0 fby ((idx + 1) % 3);
  o   = mem[> idx <];
tel
 
node shiftr3dyn_bis(ini : bool^3) returns (o : bool)
var mem : bool^3; idx : int;
let
  mem = ini fby mem;
  idx = 0 fby ((idx + 1) % 3);
  o   = mem.[idx] default false;
tel
 
(* 3 bits de registre *)
node shiftr3(ini : bool^3) returns (o : bool)
var mem : bool^3;
let
  mem = ini fby [ mem[1], mem[2], mem[0] ];
  o   = mem[0];
tel
 
Copier

$\RA$ On ne peut toujours pas itérer dans un tableau.

(* pas idéal parce que s'il y a un bug dans le code, il faudra le débogger *)
node arr2() returns(o1, o2 : float^3)
let
  o1 = [1.0, 3.0, 10.0]
  o2 = [ o1 with [ 1 ] = 42.5 ]; (* modifie à l'index 1 *)
tel
 
node arr3() returns(o1, o2 : float^3)
let
  o1 = [1.0, 3.0, 10.0]
  o2 = [ o1 with [ 37 ] = 42.5 ]; (* modification ignorée car en dehors des bornes *)
tel
 
Copier

(* concaténatio de tableau *)
expr @ expr
Copier

node concat(a : int^1; b : int^2) returns (o : int^3)
let
  o = a @ b;
tel
 
Copier

Buffer circulaire

node ring_buffer(e : int; w, r : bool) returns (o : int)
var pa, a : int^7; (* pa : précedent, a : courant*)
    w_idx, r_idx : int; (* indices écriture et lecture *)
let
  pa = (0^7) fby a;
  a = if w then [ pa with [ w_idx ] = e ] else pa;
  o = a[> r_idx <];
 
  w_idx = 0 fby (w_idx + (if w then 1 else 0) % 7);
  r_idx = 0 fby (r_idx + (if r then 1 else 0) % 7);
tel
 
Copier

(* on peut également déclarer une constante *)
const n : int = 7
 
node ring_buffer(e : int; w, r : bool) returns (o : int)
var pa, a : int^n; (* pa : précedent, a : courant*)
    w_idx, r_idx : int; (* indices écriture et lecture *)
let
  pa = (0^n) fby a;
  a = if w then [ pa with [ w_idx ] = e ] else pa;
  o = a[> r_idx <];
 
  w_idx = 0 fby (w_idx + (if w then 1 else 0) % n);
  r_idx = 0 fby (r_idx + (if r then 1 else 0) % n);
tel
 
 
Copier

(* on peut également donner en paramètre une constante *)
node ring_buffer<<n : int>>(e : int; w, r : bool) returns (o : int)
var pa, a : int^n; (* pa : précedent, a : courant*)
    w_idx, r_idx : int; (* indices écriture et lecture *)
let
  pa = (0^n) fby a;
  a = if w then [ pa with [ w_idx ] = e ] else pa;
  o = a[> r_idx <];
 
  w_idx = 0 fby (w_idx + (if w then 1 else 0) % n);
  r_idx = 0 fby (r_idx + (if r then 1 else 0) % n);
tel
 
node test_buffer() returns (o : int)
var e : int; w, r : bool;
let
   e = 0 fby (e + 1);
   w = true fby false fby w;
   r = false fby true fby r;
   o = ring_buffer<<10>>(e, w, r);
tel
 
Copier

Exercice/Problème : e devrait être d’horloge w et o devrait être d’horloge r. On pourrait aussi ajouter une sortie d’erreur qui détecte si le producteur ou le consommateur est trop rapide.

Itérateurs

map / fold / mapfold

Ainsi que mapi, foldi et mapfoldi

fun add1(a : int) returns (b : int)
let
  b = a + 1;
tel
 
const n : int = 4
 
node main (x : int^n) returns (y : int^n)
let
  (* On peut enchainée les maps *)
  y = map<<n>> add1(map<<n>> add1(x));
tel
 
Copier

Type

map

fun add1(a : int) returns (b : int)
let
  b = a + 1;
tel
 
const n : int = 4
 
node main (x : int^n) returns (y : int^n)
let
  (* On peut enchainée les maps *)
  y = map<<n>> add1(map<<n>> add1(x));
tel
 
Copier

$$\begin{aligned} (y^{1},y^{2}) = \text{map<<}n\text{>> } F(x^{1},x^{2},x^{3}) \\\\ \forall 1 \leq i \leq n, (y^{1}[i], y^{2}[i]) = F(x^{1}[i], F(x^{2}[i], F(x^{3}[i]) \end{aligned}$$

fold

y = fold<<n>> F(x, a);
Par exemple : y = F(x[2], F(x[1], F(x[0], a)))

fun add(a, b : int) returns (c : int)
let
  c = a + b;
tel
 
fun sum<<n : int>>(x : int^n) returns (s : int)
let
  s = fold<<n>> add(x, 0);
tel
 
node main() returns (s : int)
let
  s = sum<<3>>([1, 2, 3]); (* renvois 6 *)
tel
 
Copier

mapfold

(z, y) = mapfold<<n>> F(x, v);

fun f(a, acc : int) returns (b, newacc : int)
let
  b = a + acc;
  newacc = b; (* cas simple *)
tel
 
node csum_array<<n : int>>(x : int^n) returns (z : int^n)
var y : int;
let
  (z, y) = mapfold<<n>> f(x, 0 fby y);
tel
 
node main() returns (s : int^3)
let
  s = csum_array<<3>>([1, 2, 3]);
tel
 
Copier

fun add2(a, b : int) returns (c : int)
let
  c = a + b;
tel
 
fun test(x : int^3) returns (o : int^3)
var y : int^3;
let
  y = [ x with [1] = 42 ];
  o = map<<3>> add2(x, y);
tel
 
Copier

Exercices

1. Le son