these-jcb/ch-tom.tex

% vim:spell spelllang=fr
\chapter{Un langage basé sur la réécriture : Tom}
\label{ch:tom}
%15p

\index{\tom|(}
%\ttodo{Autres points à voir :
%  \begin{itemize}
    %\item autres : notation implicite vs explicite (parenthèses vs crochets
    %  dans filtrage, dans backquote) ; alias -> sous-partie notations diverses,
    %  ou à diluer dans le reste ?
    %\item théories (utile ici ?)
    %\item règles de normalisation (module rule utile ici ?)
    %\item intro DSL ?, topo fonctionnement global de {\tom}, schéma compilateur
    %  {\tom} pour expliquer, phases ?
    %\item exemple simple : Peano ? toujours le même mais connu ; Nat tout le
    %  temps ou implém' directement par des int ? (mappings)
%\end{itemize}}

Dans ce chapitre, nous abordons les notions élémentaires utiles à la lecture de
ce document. Nous présentons d'abord la réécriture de termes, puis nous
décrivons le langage {\tom}~\cite{Moreau2003,Balland2007} et nous terminons par
les ancrages formels. 

%\ttodo{ref bibtex d'un ouvrage de référence pour les déf}

%nous présentons le langage {\tom} ainsi que les notions
%élémentaires utiles à la lecture de ce tapuscrit. 
%\ttodo{tom == adjonction catégorique}

\section{Réécriture}

\subsection{Signature algébrique et termes}

Cette section traite des notions de base concernant les algèbres de termes du
premier ordre.

\begin{definition}[Signature]
Une signature \caF est un ensemble fini d'opérateurs (ou symboles de fonction),
dont chacun est associé à un entier naturel par la fonction d'arité, $ar : \caF
\rightarrow \nat$. $\caF_n$ désigne le sous-ensemble de symboles d'arité n,
c'est-à-dire $\caF_n = \{ f \in \caF \mid ar(f) = n\}$.
L'ensemble des constantes est désigné par $\caF_0$.
\end{definition}


%\ttodo{Signature algébrique multi-sortée à définir comme j'en parle plus tard +
%sorte aussi donc, juste ici ; sorte = type de type, définition ci-après suffit
%?}
On classifie parfois les termes selon leur type dans des \emph{sortes}. On
parle alors de signature multi-sortée.

\begin{definition}[Signature algébrique multi-sortée]
Une signature multi-sortée est un couple \SF où \caS est un ensemble de sortes
et \caF est un ensemble d'opérateurs sortés défini par $\caF = \bigcup
 \limits_{S_1,\ldots,S_n, S \in \caS} \caF_{S_1,\ldots,S_n,S}$. Le rang d'un
symbole de fonction $f \in \caF_{S_1,\ldots,S_n,S}$ noté $rank(f)$ est défini
par le tuple ($S_1$,\ldots,$S_n$,S) que l'on note souvent $f : S_1 \times
\ldots \times S_n \rightarrow S$
\end{definition}

\begin{definition}[Terme]
Étant donné un ensemble infini dénombrable de variables \caX et une signature
\caF, on définit l'ensemble des termes \TFX comme le plus petit ensemble tel
que :
\begin{itemize}
\item \caX $\subseteq$ \TFX : toute variable de \caX est un terme de \TFX ;
\item pour tous $t_1,\ldots,t_n$ éléments de \TFX et pour tout opérateur $f \in
  \caF$ d'arité n, le terme $f(t_1,\ldots,t_n)$ est un élément de \TFX.
\end{itemize}
\end{definition}
%\ttodo{donc définir ce qu'est une variable}
Pour tout terme $t$ de la forme $f(t_1,\ldots,t_n)$, le symbole de tête de $t$,
noté $symb(t)$ est, par définition, l'opérateur $f$.\\
Un symbole de fonction dont l'arité est variable est appelé \emph{opérateur
variadique}, c'est-à-dire qu'il prend un nombre arbitraire d'arguments.



\begin{definition}[Variables d'un terme]
L'ensemble \var{t} des variables d'un terme t est défini inductivement comme
suit :
\begin{itemize}
  \item \var{t} = $\emptyset$, pour t $\in \caF_0$ ;
  \item \var{t} = \{t\}, pour t $\in \caX$ ;
  %\item \var{t} = $\bigcup \limits_{i=1}^n \var{t_i}$, pour $t = f(t_1, \ldots, t_n)$.
  \item \var{t} = $\bigcup_{i=1}^n \var{t_i}$, pour $t = f(t_1, \ldots, t_n)$.
\end{itemize}
\end{definition}

On note souvent $a,b,c,\ldots$ les constantes et $x,y,z,\ldots$ les
variables.\\
On représente les termes sous forme arborescente. Par exemple, 
%la figure~\ref{fig:ex_terme} illustre la représentation du terme $f(x,g(a))$ : 
on peut
représenter le terme $f(x,g(a))$ comme dans la figure~\ref{fig:ex_terme} :
\begin{figure}[H]
  \begin{center}
  \input{figures/ex_terme}
    \caption{Exemple de représentation arborescente d'un terme.}
    \label{fig:ex_terme}
  \end{center}
\end{figure}

%\ttodo{donc définir aussi la position}

\begin{definition}[Terme clos]
Un terme t est dit clos s'il ne contient aucune variable, c'est-à-dire si $\var{t} = \emptyset$. On note \TF l'ensemble des termes clos.
\end{definition}

Chaque nœud d'un arbre peut être identifié de manière unique par sa position.

\begin{definition}[Position]
Une position dans un terme t est représentée par une séquence $\omega$
d'entiers naturels, décrivant le chemin de la racine du terme jusqu'à un nœud
$t_{|\omega}$ du terme. Un terme $u$ a une occurrence dans $t$ si $u =
t_{|\omega}$ pour une position $\omega$ dans $t$.
\end{definition}
On notera ${\caP}os(t)$ l'ensemble des positions d'un terme $t$ et
$t[t']_{\omega}$ le remplacement du sous-terme de $t$ à la position $\omega$
par $t'$.

Par exemple, la figure~\ref{fig:ex_positions} illustre la notation des
positions pour le terme $t = f(x,g(a))$. On obtient l'ensemble des positions
${\caP}os(t)$ = $\{\epsilon, 1, 2, 21\}$ ce qui correspond respectivement aux
sous-termes $t_{|\epsilon} = f(x,g(a))$, $t_{|1} = x$, $t_{|2} = g(a)$ et
$t_{|21} = a$.

\begin{figure}[H]
  \begin{center}
  \input{figures/ex_positions}
    \caption{Notation des positions dans un terme.}
    \label{fig:ex_positions}
  \end{center}
\end{figure}



%\textbf{Notations :}
%\begin{itemize}
%  \item ${\caP}os(t)$ est l'ensemble des positions d'un terme $t$ ; 
%  \item $t[t']_{\omega}$ indique le remplacement du sous-terme de $t$ à la
%    position $\omega$ par $t'$ 
%  \item $t[\omega \hookleftarrow \sigma(r)]$ signifie que le sous-terme de $t$
%    à la position $\omega$ a été remplacé par $\sigma(r)$.
%\end{itemize}


\subsection{Filtrage}
\label{subsec:filtrage}

%FIXME\ttodo{ajouter une phrase de liant}
Une substitution est une opération de remplacement, uniquement définie par une
fonction des variables vers les termes clos.

\begin{definition}[Substitution]
Une substitution $\sigma$ est une fonction de \caX vers \TF, notée lorsque son
domaine $\dom{\sigma}$ est fini, $\sigma = \{x_1 \mapsto t_1, \ldots, x_k
\mapsto t_k\}$. Cette fonction s'étend de manière unique en un endomorphisme
$\sigma' : \TFX \rightarrow \TFX$ sur l'algèbre des termes, qui est défini
inductivement par : 
\begin{itemize}
\item $\sigma'(x) = \left\{
			\begin{array}{l}
				\sigma(x) \text{ si } x \in \dom{\sigma}\\
				x \text{ sinon}\\
			\end{array} \right.$
\item $\sigma'(f(t_1,\ldots,t_n)) = f(\sigma'(t_1),\ldots,\sigma'(t_n))$ pour
tout symbole de fonction $f \in \caF_n$.
\end{itemize}
\end{definition}
%\ttodo{donc définir aussi algèbre de termes T(S,F,V) ?}

\begin{definition}[Filtrage]
Étant donnés un motif p $\in$ \TFX et un terme clos t $\in$ \TF, p filtre t,
noté $p \match t$, si et seulement s'il existe une substitution $\sigma$ telle que
$\sigma(p) = t$ :
	$$ p \match t \Leftrightarrow \exists \sigma, \sigma(p) = t $$
\end{definition}

%\ttodo{remarques de PEM : algo de filtrage, existe ?, décidabilité ?\\ filtrage
%unitaire, filtrage syntaxique}
%
%\ttodo{oui, il existe des algos de filtrage :\\
%filtrage syntaxique $\Rightarrow$ algo récursif, solution unique si existe,
%thèse de Gérard Huet~\cite{Huet1976}}

On parle de \emph{filtrage unitaire} lorsqu'il existe une unique solution à
l'équation de filtrage. Si plusieurs solutions existent, le filtrage est
\emph{non unitaire}.

%Le filtrage peut aussi être \emph{syntaxique} ou \emph{modulo une théorie
%équationnelle}. Dans ce second cas, cela signifie que l'on a associé une
Le filtrage peut aussi être \emph{modulo une théorie équationnelle}. Cela
signifie que l'on a associé une théorie équationnelle au problème de filtrage.

\begin{definition}[Filtrage modulo une théorie équationnelle]
  Étant donnés une théorie équationnelle \caE, un motif $p$ $\in$ \TFX et un
  terme clos $t$ $\in$ \TF, $p$ filtre $t$ modulo \caE,
noté $p \match_{\caE} t$, si et seulement s'il existe une substitution $\sigma$ telle que
$\sigma(p) =_{\caE} t$, avec $=_{\caE}$ l'égalité modulo $\caE$ :
	$$ p \match_{\caE} t \Leftrightarrow \exists \sigma, \sigma(p) =_{\caE} t $$
\end{definition}

Dans la suite de cette section, nous allons expliquer ce concept, donner des
exemples de théories équationnelles et illustrer notre propos.
%\subsection{Théorie équationnelle}

Une paire de termes $(l,r)$ est appelée \emph{égalité}, \emph{axiome
équationnel} ou \emph{équation} selon le contexte, et est notée $(l=r)$. Une
théorie équationnelle peut être définie par un ensemble d'égalités. Elle
définit une classe d'équivalence entre les termes.
Dans la pratique, les théories équationnelles les plus communes sont
l'associativité, la commutativité et l'élément neutre (ainsi que leurs
combinaisons).

\begin{definition}[Opérateur associatif]
Un opérateur binaire $f$ est associatif si $\forall x,y,z \in \TFX, f(f(x,y),z) =
f(x,f(y,z))$.
\end{definition}

Par exemple, l'addition et la multiplication sont associatives sur l'ensemble
des réels $\mathbb{R}$ : $((x+y)+z) = (x+(y+z))$ et $((x\times y)\times z)) =
(x\times (y\times z))$. En revanche, la soustraction sur $\mathbb{R}$ n'est pas
associative : $((x-y)-z) \neq (x-(y-z))$.

\begin{definition}[Opérateur commutatif]
  Un opérateur binaire $f$ est commutatif si $\forall x,y \in \TFX f(x,y) =
  f(y,x)$.
\end{definition}

Par exemple, l'addition et la multiplication sont commutatives sur
$\mathbb{R}$, ainsi $x+y = y+x$ et $x\times y = y\times x$. Ce qui n'est pas le
cas de la soustraction sur $\mathbb{R}$, en effet $x-y \neq y-x$.

\begin{definition}[Élément neutre]
Soit un opérateur binaire $f$ et $x \in \TFX$, la constante $e \in \TF$ est :
\begin{itemize}
  \item neutre à gauche pour $f$ si $f(e,x) = x$ ;
  \item neutre à droite pour $f$ si $f(x,e) = x$ ;
  \item neutre si elle est neutre à gauche et neutre à droite pour $f$.
\end{itemize} 
\end{definition}
%Pour illustrer la notion d'élément neutre
%Ainsi, 0 est neutre pour l'addition sur $\mathbb{R}$ car : $0+x = x$ et $x+0 = x$.
Pour illustrer cette notion d'élément neutre, examinons la constante 0 avec
l'addition sur l'ensemble des réels $\mathbb{R}$ :
\begin{itemize}
  \item $0+x = x$, 0 est donc neutre à gauche pour l'addition ; 
  \item $x+0 = x$, 0 est donc neutre à droite pour l'addition ;
  \item on en déduit que 0 est neutre pour l'addition sur $\mathbb{R}$.
\end{itemize}

On note généralement $A$, $U$ et $C$ les théories équationnelles engendrées
respectivement par l'équation d'associativité, l'équation de neutralité et
celle de commutativité. On note $AU$ la théorie engendrée par les équations
d'associativité et de neutralité.

La théorie associative est associée aux opérateurs binaires. Pour des raisons
techniques, elle est souvent associée à une syntaxe variadiques dans les
langages de programmation fondés sur la réécriture. Par exemple, l'opérateur
variadique $list$ est simulé par l'opérateur $nil$ d'arité nulle, ainsi que par
l'opérateur binaire $cons$. Cela permet d'écrire que le terme $list(a,b,c)$ est
équivalent au terme $list(list(a,b),c)$, et qu'ils peuvent être représentés par
$cons(a,cons(b,cons(c,nil)))$.

On peut alors définir des opérations modulo une théorie équationnelle : on
parlera de \emph{filtrage équationnel} lorsque le filtrage sera associé à une
telle théorie. Pour illustrer cette notion, prenons deux exemples simples de
filtrage.

\paragraph{Exemple 1 :} Le filtrage associatif avec élément neutre ($AU$)
---~aussi appelé filtrage de liste~--- est un problème bien connu en
réécriture. Il permet d'exprimer facilement des algorithmes manipulant des
listes. En considérent $X1*$ et $X2*$ comme ides variables représentant 0 ou
plusieurs éléments d'une liste, le problème de filtrage $list(X1*,x,X2*) \ll
list(a,b,c)$ admet trois solutions : $\sigma_1 = \{ x\rightarrow a\}$,
$\sigma_2 = \{ x\rightarrow b\}$ et $\sigma_3 = \{ x\rightarrow c\}$.

%\paragraph{Exemple 1 :} Le filtrage associatif avec élément neutre ($AU$)
%---~aussi appelé filtrage de liste~--- est un problème bien connu en
%réécriture. Il permet d'exprimer facilement des algorithmes manipulant des
%listes. Considérons l'opérateur associatif $list$ avec élément neutre noté $e$.
%Le problème de filtrage $list(x,y,z) \ll list(a,b)$ admet trois solutions :
%$\sigma_1 = \{ x\rightarrow a, y\rightarrow b, z\rightarrow e\}$, $\sigma_2 =
%\{ x\rightarrow a, y\rightarrow e, z\rightarrow b\}$ et $\sigma_3 = \{
%x\rightarrow e, y\rightarrow a, z\rightarrow b\}$.


\paragraph{Exemple 2 :} Illustrons le filtrage associatif-commutatif ($AC$) et
l'addition, dont les axiomes d'associativité et commutativité sont les suivants
:
%Pour illustrer cette notion, prenons l'exemple du filtrage
%associatif-commutatif ($AC$) et de l'addition, dont les axiomes d'associativité
%et commutativité sont les suivants :
\begin{itemize}
  \item $\forall x,y,~ plus(x,y) = plus(y,x)$ ;
  \item $\forall x,y,~ plus(x,plus(y,z))=plus(plus(x,y),z)$.
\end{itemize}
Le problème de filtrage $plus(x,y) \ll plus(a,b)$ présente deux solutions
distinctes modulo AC : $\sigma_1 = \{ x\rightarrow a,y\rightarrow b\}$ et
$\sigma_2=\{ x\rightarrow b, y\rightarrow a\}$.

%Prenons l'exemple du filtrage associatif-commutatif ($AC$) permettant de
%modéliser le calcul dans les groupes et dans d'autres structures algébriques
%dotées de lois commutatives et associatives, notamment l'addition sur les
%entiers. $plus$ est associatif-commutatif et les axiomes d'associativité et
%commutativité sont les suivants :
%$$\forall x,y ; plus(x,y) = plus(y,x)$$
%$$\forall x,y ; plus(x,plus(y,z))=plus(plus(x,y),z)$$
%\begin{itemize}
%  \item le problème de filtrage $plus(a,b) \ll plus(x,y)$ possède deux solutions
%    distinctes modulo $AC$ : $\sigma_1 = \{ x\rightarrow a,y\rightarrow b\}$ et
%    $\sigma_2=\{ x\rightarrow b, y\rightarrow a\}$
%
%  \item le problème de filtrage $plus(x,y) \ll plus(plus(plus(a,b),c)$ possède
%    six solutions modulo $AC$ : 
%\end{itemize}


\subsection{Réécriture}

En réécriture, on oriente des égalités que l'on appelle des \emph{règles de
réécriture} et qui définissent un calcul.

\begin{definition}[Règle de réécriture]
Une règle de réécriture est un couple (l,r) de termes dans \TFX, notée l
$\rightarrow$ r. l est appelé membre gauche de la règle, et r membre droit.
\end{definition}

Un exemple de règle de réécriture est l'addition de n'importe quel entier $x$
avec $0$ : $$x+0~\rightarrow~x$$
Un autre exemple un peu plus complexe de règle de réécriture est la
distributivité de la multiplication par rapport à l'addition dans un anneau,
comme illustré par la figure~\ref{fig:ex_rwRule_distrib}. %ci-dessous :
%\todo{[x*(y+z) -> (x*y)+(x*z)]}
\begin{figure}[!h]
  \begin{center}
    \input{figures/ex_rwRule_distrib}
    \caption{Exemple de règle de réécriture : distributivité de la
    multiplication par rapport à l'addition dans un anneau, à savoir $x\times(y+z)
  \rightarrow (x\times y)+(x\times z)$.}
    \label{fig:ex_rwRule_distrib}
  \end{center}
\end{figure}

\begin{definition}[Système de réécriture]
Un système de réécriture sur les termes est un ensemble de règles de réécriture
(l,r) tel que :
\begin{itemize}
  \item les variables du membre droit de la règle font partie  des variables du
  membre gauche ($\var{r} \subseteq \var{l}$) ;
  \item le membre gauche d'une règle n'est pas une variable ($l \notin \caX$).
\end{itemize}
%\todo{À voir : plus « formel » (à la Cláudia) ou alors cette définition est
%suffisante ?}
\end{definition}


\begin{definition}[Réécriture]
Un terme $t \in \TFX$ se réécrit en $t'$ dans un système de réécriture \caR, ce
que l'on note $t \rarrow t'$, s'il existe :
\begin{itemize}
  \item une règle $l \rightarrow r \in \caR$ ;
  \item une position $\omega$ dans $t$ ;
  \item une substitution $\sigma$ telle que $t_{|\omega} = \sigma(l)$ et $t' =
    t[\sigma(r)]_{\omega}$. %t[\omega \hookleftarrow \sigma(r)]
\end{itemize}
\end{definition}

On appelle \emph{radical} le sous-terme $t_{|\omega}$.

Pour une relation binaire $\rightarrow$, on note $\refltransclo$ sa fermeture
transitive et réflexive. La fermeture transitive, réflexive et symétrique de
$\rightarrow$ ---~qui est alors une relation d'équivalence~--- est notée
$\symrefltransclo$.


\begin{definition}[Forme normale]
Soit $\rightarrow$ une relation binaire sur un ensemble T.
%\begin{itemize}
%\item un élément $t \in T$ est une forme normale s'il n'existe pas
%  d'élément $t' \in T $ tel que $t \rightarrow t'$. On dit alors que t est
%  irréductible ;
%\item $t \in T$ a une forme normale si $t \refltransclo t'$ pour une forme
%  normale $t'$ notée $t\downarrow$.
%\end{itemize}
Un élément t $\in$ T est réductible par $\rightarrow$ s'il existe $t' \in T$
tel que $t \rightarrow t'$. Dans le cas contraire, on dit qu'il est
irréductible. On appelle forme normale de $t$ tout élément $t'$ irréductible de
T tel que $t \refltransclo t'$. Cette forme est unique.
\end{definition}

Deux propriétés importantes d'un système de réécriture sont la
\emph{confluence} et la \emph{terminaison}. Lorsque l'on souhaite savoir si
deux termes sont équivalents, on cherche à calculer leurs formes normales et à
vérifier si elles sont égales. Cela n'est possible que si la forme normale
existe et qu'elle est unique. Une forme normale existe si $\rightarrow$
\emph{termine}, et son unicité est alors assurée si $\rightarrow$ est
\emph{confluente}, ou si elle vérifie la \emph{propriété de Church-Rosser}, qui
est équivalente.

\begin{definition}[Terminaison]
Une relation binaire $\rightarrow$ sur un ensemble T est dite terminante s'il
n'existe pas de suite infinie $(t_i)_{i\ge 1}$ d'éléments de T telle que $t_1
\rightarrow t_2 \rightarrow~\cdotp\cdotp\cdotp$.
\end{definition}

\begin{definition}[Confluence]
Soit une relation binaire $\rightarrow$ sur un ensemble T. %$\rightarrow$ est
%confluente si et seulement si : $$\forall t,t_1,t_2 (t \refltransclo t_1~et~t
%\refltransclo t_2) \Rightarrow \exists t', (t_1 \refltransclo t'~et~t_2 \refltransclo
%t')$$
\begin{itemize}
  \item[(a)] $\rightarrow$ est \emph{confluente} si et seulement si :
    $$\forall t,u,v ~(t \refltransclo u~et~t \refltransclo v) \Rightarrow
    \exists w, (u \refltransclo w~et~v \refltransclo w)$$
  \item[(b)] $\rightarrow$ vérifie la \emph{propriété de Church-Rosser} si et seulement si :
    $$\forall u,v,~u \symrefltransclo v \Rightarrow
    \exists w, (u \refltransclo w~et~v \refltransclo w)$$
\item[(c)] $\rightarrow$ est \emph{localement confluente} si et seulement si :
    $$\forall t,u,v ~(t \rightarrow u~et~t \rightarrow v) \Rightarrow
    \exists w, (u \refltransclo w~et~v \refltransclo w)$$
\end{itemize}
\end{definition}

%La figure~\ref{fig:confluence} illustre cette propriété de confluence.
%\begin{figure}[H]
%  \begin{center}
%  \input{figures/confluence}
%    \caption{Propriété de confluence.}
%    \label{fig:confluence}
%  \end{center}
%\end{figure}

La figure~\ref{fig:proprietes_binRel} illustre ces propriétés.
\begin{figure}[H]
  \begin{center}
  \input{figures/proprietes_binRel}
    \caption{Propriétés sur les relations binaires.}
    \label{fig:proprietes_binRel}
  \end{center}
\end{figure}


\subsection{Stratégies de réécriture}
%\ttodo{1. intuition 2. définitions formelles : Stratégie et réécriture sous
%stratégie ; évaluation en lambda calcul ; stratégie abstraite -> ARS ; }

En réécriture, on applique habituellement de manière exhaustive toutes les
règles sur le terme pour calculer sa forme normale, c'est-à-dire que l'on
applique toutes les règles jusqu'à ce qu'aucune règle ne puisse plus être
appliquée. Il est cependant courant d'écrire des systèmes de réécriture ne
terminant pas ou n'étant pas confluents. La méthode d'application des règles
adoptée prend donc de l'importance, car elle a, dans ce cas, un effet sur le
résultat. Il est par conséquent important d'avoir un contrôle sur l'application
des règles du système de réécriture. C'est l'objet du concept de
\emph{stratégie} que nous allons décrire dans cette section.
%On va donc définir des \emph{stratégies} pour spécifier le parcours à suivre
%dans l'arbre des dérivations.

Illustrons ce problème par un exemple où l'on considère le système de
réécriture suivant avec la signature $\{a,f\}$, $a$ étant d'arité 0 et $f$
d'arité 1 :\\
%ex confluent non-terminant extrait du manuscrit de Antoine -> permet de donner
%une bonne intuition
$\left\{\begin{array}{lclr}
  f(x) & \rightarrow & f(f(x)) & (r1)\\
  f(a) & \rightarrow & a & (r2)\\
  \end{array} \right. $\\
Sans aucune précision sur la manière d'appliquer les règles, nous remarquons
qu'il existe une suite infinie de pas de réécriture partant de $f(a)$ si l'on
applique toujours la règle $r1$ :\\
$f(a) \overset{r1}{\longrightarrow} f(f(a)) \overset{r1}{\longrightarrow}
f(f(f(a))) \overset{r1}{\longrightarrow} \cdots $\\
Le calcul ne termine pas. Si l'on applique les règles de réécriture $r1$ et $r2$
différemment, nous constatons que $f(a)$ se réduit en $a$ :\\
%$f(a) \overset{r1}{\longrightarrow} f(f(a)) \overset{r2}{\longrightarrow} f(f(a))$
$\begin{array}{lllllll}
  f(a) & \overset{r1}{\longrightarrow} & f(f(a)) &
  \overset{r2}{\longrightarrow} & f(a) & \overset{r2}{\longrightarrow}& a\\
  \downarrow {\vspace{-1.0em}\footnotesize ^{r2}} &&&&&&\\
  a&&&&&&\\
\end{array}$\\
Cet exemple illustre clairement le fait que les résultats du calcul ne sont pas
les mêmes selon la méthode d'application des règles. Pour avoir des calculs qui
terminent, on pourrait alors adopter une \emph{stratégie} d'application des
règles donnant la priorité à la règle $r2 : f(a) \rightarrow a$ par rapport à
la règle $r1 : f(x) \rightarrow f(f(x))$.

%On constate qu'il est confluent et non-terminant : il existe une suite infinie
%de pas de réécriture partant de $f(a)$ ou $g(a)$, mais ils se réduisent
%cependant tous deux en $a$. Pour avoir des calculs qui terminent, on pourrait
%adopter une stratégie d'application des règles donnant la priorité aux deux
%règles $f(a) \rightarrow a$ et $g(a) \rightarrow a$ par rapport aux deux
%premières règles.

%~\cite{Kirchner1996}

Après cette intuition de ce qu'est une stratégie, nous pouvons donner des
définitions plus formelles des concepts liés. La notion de système abstrait de
réduction (\emph{Abstract Reduction System} -- ARS)~\cite{Bezem2003} est une
manière abstraite de modéliser les calculs par transformations pas à pas
d'objets, indépendamment de la nature des objets qui sont réécrits. Un ARS peut
se définir comme un couple $(\caT,\rightarrow)$, où $\rightarrow$ est une
relation binaire sur l'ensemble \caT. De là,~\cite{Kirchner2008} donne une
représentation des ARS sous forme de graphe et introduit le concept de
stratégie abstraite.

%définitions formelles -> obligé de les mettre ? -> oui, cf cohérence avec le
%reste + déf ARS et dérivation nécessaires en cascade car déf de stratégie
%abstraite. Trouver une définition un peu plus light ?

%\begin{definition}[Système abstrait de réduction]%\cite{Bezem2003}
%  Un système abstrait de réduction (ARS) est un couple $(\caT,\rightarrow)$ où
%  $\rightarrow$ est une relation binaire sur l'ensemble \caT
%\end{definition}
\begin{definition}[Système abstrait de réduction]%\cite{Kirchner2008}
  Un système abstrait de réduction (ARS) est un graphe orienté étiqueté
  $(\caO, \caS)$. Les nœuds \caO sont appelés objets, les arêtes orientées \caS
  sont appelées pas.\\
\end{definition}

Pour un ensemble de termes \TFX, le graphe (\TFX, \caS) est l'ARS correspondant
à un système de réécriture \caR. Les arêtes correspondent à des pas de
réécriture de \caR et sont étiquetées par le nom des règles de \caR. 

\begin{definition}[Dérivation]
  Soit un ARS \caA :
  \begin{itemize}

    \item[1.] un \emph{pas de réduction} est une arête étiquetée $\phi$ complétée de sa
      source a et de sa destination b. On note un pas de réduction
      $a \aphiarrow{} b$, ou simplement $a \phiarrow{} b$ lorsqu'il n'y a pas
      d'ambiguïté ;

    \item[2.] une \emph{\caA-dérivation} (ou \emph{séquence de
      \caT-réductions}) est un chemin $\pi$ dans le graphe \caA ;

    \item[3.] lorsque cette dérivation est finie, $\pi$ peut s'écrire $a_0
      \phiarrow{0} a_1 \phiarrow{1} a_2 \cdots \phiarrow{n-1} a_n$ et on dit
      que $a_0$ se réduit en $a_n$ par la dérivation $\pi =
      \phi_0\phi_1\ldots\phi_{n-1}$ ; notée aussi $a_0
      \rightarrow^{\phi_0\phi_1\ldots\phi_{n-1}} a_n$ ou simplement $a_0
      \piarrow a_n$. n est la \emph{longueur} de $\pi$ ;
      \begin{itemize}
        \item[(a)] la source de $\pi$ est le singleton \{$a_0$\}, notée
          $dom(\pi)$ ;
        \item[(b)] la destination de $\pi$ est le singleton $\{a_n\}$, 
          notée $\pi[a_0]$.
      \end{itemize}
    \item[4.] une dérivation est vide si elle n'est formée d'aucun pas de
      réduction. La dérivation vide de source a est notée $id_a$.

  \end{itemize}
\end{definition}

\begin{definition}[Stratégie abstraite]%definition de \cite{Kirchner2008}, p5-6
  Soit un ARS \caA :
  \begin{itemize}
    \item[1.] une stratégie abstraite  est un sous-ensemble de toutes les
      dérivations de \caA ;

    \item[2.] appliquer la stratégie $\zeta$ sur un objet a, noté par $\zeta[a]$, est
      l'ensemble de tous les objets atteignables depuis a en utilisant une
      dérivation dans $\zeta$ :
      $\zeta[a] = \{\pi[a]~|~\pi \in \zeta\}$. Lorsqu'aucune dérivation dans
      $\zeta$ n'a pour source a, on dit que l'application sur $a$ de la
      stratégie a échoué ;

    \item[3.] appliquer la stratégie $\zeta$ sur un ensemble d'objets consiste
      à appliquer $\zeta$ à chaque élément $a$ de l'ensemble. Le résultat est
      l'union de $\zeta[a]$ pour tous les $a$ de l'ensemble d'objets ;

    \item[4.] le \emph{domaine} d'une stratégie est l'ensemble des objets qui
      sont la source d'une dérivation dans $\zeta$ : $dom(\zeta) =
      \bigcup \limits_{\delta \in \zeta} dom(\delta)$ ;

    \item[5.] la stratégie qui contient toutes les dérivations vides est $Id = \{
      id_a ~|~ a \in \caO\}$.
  \end{itemize}
\end{definition}

%\ttodo{transition section suivante : lien vers le langage}

Concrètement, on peut exprimer ces stratégies de manière déclarative grâce aux
langages de stratégies que proposent la plupart des langages à base de règles
tels que {\elan}~\cite{Vittek1994,Borovansky1998,Borovansky1996},
{\stratego}~\cite{Visser1998,Visser01},
{\maude}~\cite{Clavel1996a,Clavel2002,Clavel2011} et {\tom}, que
nous allons présenter dans la section suivante.

\paragraph{{\elan}.} {\elan} propose deux types de règles : les
règles anonymes systématiquement appliquées (servant à la normalisation de
termes) et les règles étiquetées pouvant être déclenchées à la demande
sous contrôle d'une stratégie.  Le résultat de l'application d'une telle règle
sur un terme est un multi-ensemble de termes, ce qui permet de gérer le
non-déterminisme. {\elan} a introduit la notion de stratégie en proposant un
langage de combinateurs permettant de composer les stratégies et de contrôler
leur application. Parmi ces combinateurs, on retiendra notamment l'opérateur de
séquence, des opérateurs de choix non-déterministes et des opérateurs de
répétition.

\paragraph{{\stratego}.} S'inspirant d'{\elan}, {\stratego} se concentre sur un
nombre restreint de combinateurs élémentaires, ainsi que sur leur combinaison.
À ces combinateurs (séquence, identité, échec, test, négation, choix
déterministe et non-déterministe) sont ajoutés un opérateur de récursion
($\mu$) et des opérateurs permettant d'appliquer la stratégie : sur le
$i^{\text{\textit{ème}}}$ fils du sujet (\emph{i(s)}), sur tous les sous-termes
du sujet (\emph{All(s)}), sur le premier fils du sujet sans échec
(\emph{One(s)}), sur tous les sous-termes du sujet sans échec (\emph{Some(s)}).
Grâce à ces opérateurs, il est possible d'élaborer des stratégies de haut
niveau telles que \emph{TopDown} et \emph{BottomUp}.

\paragraph{{\maude}.} L'approche de {\maude} est un peu différente : le
contrôle sur l'application des règles s'opère grâce à la réflexivité du
système~\cite{Clavel1996,Clavel2002a}. Les objets du langage {\maude} ayant une
représentation \emph{meta}, il est possible d'utiliser un opérateur
(\texttt{meta-apply}) pour appliquer les règles. Cet opérateur évalue les
équations, normalise le terme, et retourne la \emph{meta-représentation} du
terme résultant de l'évaluation. On peut contrôler l'application des règles de
réécriture par un autre programme défini par réécriture. Pour des raisons
pratiques, des travaux ont été menés plus
récemment~\cite{MartiOliet2005,Eker2007} pour offrir un langage de stratégies
plus proche de ce que {\elan}, {\stratego} et {\tom} proposent.


\paragraph{{\tom}.} À partir du concept de stratégie et en s'inspirant de ces
langages, {\tom} implémente lui aussi un langage de
stratégies~\cite{BallandMR08,Balland2012}. Il est fondé sur des stratégies
élémentaires (\emph{Identity} et \emph{Fail}), sur des combinateurs de
composition (\emph{Sequence}, \emph{Recursion} ---$\mu$---, \emph{Choice},
\emph{Not}, \emph{IfThenElse}) et de traversée (\emph{All}, \emph{One},
\emph{Up} et \emph{Omega}). De ces combinateurs, à l'image de {\stratego}, des
stratégies composées peuvent être élaborées (\emph{Try}, \emph{Repeat},
\emph{Innermost}, etc.). Nous reviendrons sur les stratégies de {\tom} dans la
section suivante, en particulier sur leur utilisation concrète au sein du
langage.



\section{Le langage Tom}


{\tom}~\cite{Moreau2003,Balland2007} est un langage conçu pour enrichir des
langages généralistes de fonctionnalités issues de la réécriture et de la
programmation fonctionnelle. Il ne s'agit pas d'un langage \emph{stand-alone} :
il est l'implémentation du concept des \og îlots formels \fg (\emph{formal
islands})~\cite{Balland2006} qui sont ajoutés au sein de programmes écrits dans
un langage hôte. Les constructions {\tom} sont transformées et compilées vers
le langage hôte. Parmi les fonctionnalités apportées par {\tom}, on compte le
filtrage de motif (\emph{pattern-matching}), les règles de réécriture, les
stratégies, ainsi que les ancrages algébriques (\emph{mappings}). 

%Le compilateur {\tom} est lui-même écrit en {\tom} (\emph{bootstrap}). 

%\ttodo{Fonctionnement de {\tom} : faire le schéma chaîne de compilation, ou
%alors tout à la fin ? Plutôt à la fin vu qu'il faut faire apparaître les
%mappings, etc.}

Dans la suite de cette section, nous décrirons le langage {\tom} en illustrant
ses fonctionnalités et constructions par des exemples simples. Sauf indication
contraire, les extraits de code hôte seront en {\java}. Pour une documentation
complète et détaillée, le lecteur intéressé pourra se référer au manuel
disponible en téléchargement~\cite{Bach2009} ou directement en
ligne~\cite{TomManual-2.10}. Les outils sont tous accessibles {\via} le site
officiel du projet {\tom}\footnote{Voir \url{http://tom.loria.fr/}.}.


\subsection{Signature algébrique}
\label{subsec:signalg}\index{signature algébrique}
{\tom} permet à l'utilisateur de spécifier des signatures algébriques
multi-sortées {\via} l'outil {\gom}~\cite{Reilles2007}. Le langage
{\gom}\index{\gom} permet de décrire une structure de données et d'en générer
l'implémentation typée en {\java}. Le listing~\ref{code:gomPeanoSimple}
illustre une définition de signature {\gom} :

\input{code/gomPeanoSimple}

Un module {\gom} est composé d'un préambule comportant un nom
---~\texttt{Peano} dans cet exemple~--- précédé du mot-clef \texttt{module}
(ligne 1). Le début de la signature est annoncé par le mot-clef
\texttt{abstract syntax} (ligne 2). Cet exemple étant extrêmement simple, le
préambule est composé uniquement de ces deux lignes. Pour un module plus
complexe qui utiliserait des types définis dans une autre signature, la clause
\texttt{imports} suivie des signatures à importer peut être intercalée entre
les deux clauses précédentes. Le projet {\tom} fournit notamment une
bibliothèque de signatures pour les types primitifs (types \emph{builtin}) tels
que les \emph{entiers} (\texttt{int}), les \emph{caractères} (\texttt{char}),
les \emph{flottants} (\texttt{float}) et les \emph{chaînes de caractères}
(\texttt{String}). La signature en elle-même est composée d'un ensemble de
sortes ---~\texttt{Nat} dans notre exemple~--- ayant des constructeurs
---~\texttt{zero} et \texttt{suc} ici.

Ce générateur propose un typage fort au niveau de la structure de données
{\java} générée, ce qui garantit que les objets créés sont conformes à la
signature multi-sortée. Un second aspect intéressant de cet outil est le fait
qu'il offre le partage maximal~\cite{Appel1993}, rendant les structures
générées très efficaces en temps (tests d'égalité en temps constant) et en
espace. Les classes générées peuvent être modifiées par l'intermédiaire de la
fonctionnalité de \emph{hooks}. Ce mécanisme permet d'ajouter des blocs de code
{\java} aux classes générées (par exemple, intégration d'attributs invisibles
au niveau algébrique, mais manipulables par la partie {\java} de l'application)
ou d'associer une théorie équationnelle telle que A, AC, ACU à certains
opérateurs. Il est même possible de spécifier cette théorie équationnelle par
des règles de normalisation. Les termes construits sont ainsi toujours en forme
normale.

La signature est compilée en une implémentation {\java} ainsi qu'un ancrage
permettant l'utilisation de cette structure dans les programmes {\tom}. Dans un
premier temps, pour présenter les constructions du langage {\tom}, nous ne nous
préoccuperons pas de ces ancrages ni de l'implémentation concrète {\java}.

\subsection{Construction \emph{backquote} « ` »}
\index{\tom!backquote, \lex{`}|(}
La construction \lex{`} (\emph{backquote}) permet de créer la structure de
données représentant un terme algébrique en allouant et initialisant les objets
en mémoire. Elle permet à la fois de construire un terme et de récupérer la
valeur d'une variable instanciée par le filtrage de motif.  Ainsi, on peut
construire des termes de type \texttt{Nat} de l'exemple précédent avec des
instructions \emph{backquote}. L'instruction {\tomjava} \og\texttt{Nat un =
`suc(zero());}\fg déclare une variable \texttt{un} dont le type est \texttt{Nat},
ayant pour valeur le représentant algébrique \emph{suc(zero())}.

Un terme \emph{backquote} peut aussi contenir des variables du langage hôte,
ainsi que des appels de fonctions. Ainsi, l'instruction \texttt{Nat deux =
`suc(un);} permet de créer le terme \texttt{deux} à partir de \texttt{un} créé
précédemment. Le compilateur {\tom} n'analysant pas du tout le code hôte,
notons que nous supposons que la partie hôte ---~\texttt{un} dans l'exemple~---
est conforme à la signature algébrique et que le terme est donc bien formé.
L'utilisation du \emph{backquote} permet à l'utilisateur %de ne pas se soucier
%de l'implémentation concrète du type du langage hôte et de ne manipuler que sa
%vue algébrique.
de créer un terme et de manipuler sa vue algébrique sans se soucier de
son implémentation concrète dans le langage hôte.
\index{\tom!backquote, \lex{`}|)}



\subsection{Filtrage de motif}
\label{subsec:matching}\index{Filtrage|(}\index{Pattern-matching|(}

Dans la plupart des langages généralistes tels que {\C} ou {\java}, on ne
trouve pas les notions de type algébrique et de terme, mais uniquement celle de
types de données composées (structures {\C} et objets {\java}). De même, la
notion de filtrage de motif (\emph{pattern-matching}) que l'on retrouve dans
les langages fonctionnels tels que {\caml} ou {\haskell} n'existe généralement
pas dans la plupart des langages impératifs classiques. Le filtrage permet de
tester la présence de motifs (\emph{pattern}) dans une structure de données et
d'instancier des variables en fonction du résultat de l'opération de filtrage.

Ces constructions sont apportées par {\tom} dans des langages généralistes. Il
devient donc possible de filtrer des motifs dans {\java}. En outre, les
constructions de filtrage de {\tom} étant plus expressives que dans {\caml}
(notamment le filtrage équationnel et le filtrage non linéaire), il
est possible de les employer aussi en son sein pour utiliser le filtrage
équationnel.


Le lexème \lex{\%match}\index{\tom!\lex{\%match}} introduit la construction de
filtrage de {\tom}. Celle-ci peut être vue comme une généralisation de la
construction habituelle \emph{switch-case} que l'on retrouve dans beaucoup de
langages généralistes.  Cependant, plutôt que de filtrer uniquement sur des
entiers, des caractères, voire des chaînes de caractères, {\tom} filtre sur des
\emph{termes}. Les motifs permettent de discriminer et de récupérer
l'information contenue dans la structure de données algébrique sur laquelle on
filtre.

Dans le listing~\ref{code:matchPeanoPlus} suivant, nous reprenons l'exemple des
entiers de Peano pour lesquels nous encodons l'addition avec {\tom} et {\java}.
Pour ce premier exemple où les deux langages apparaissent en même temps, nous
adoptons un marquage visuel pour désigner {\java} (noir) et {\tom} (gris). Cela
permet de visualiser le tissage étroit entre le langage {\tom} et le langage
hôte dans lequel il est intégré. Par la suite, le principe étant compris, nous
n'adopterons plus ce code visuel.
 %\ttodo{voir quelle version garder : JNat, ou la simple avec Nat ?}
\input{code/matchPeanoPlus}
 
Dans cet exemple, la fonction \texttt{peanoPlus} prend en arguments deux termes
\texttt{t1} et \texttt{t2} de type \texttt{Nat}
représentant deux entiers de Peano, et retourne la
somme des deux. 
%\todo{[Ou alors je passe la phrase suivante sous silence, et j'en reparle dans les mappings] }
%\texttt{t1} et \texttt{t2} sont du type {\tom} \texttt{Nat}, implémenté par le type {\java} \texttt{JNat}. 
Le calcul est opéré par filtrage en utilisant la construction \lex{\%match} :
\begin{itemize}
  \item elle prend un ou plusieurs arguments ---~deux dans notre exemple~---
    entre parenthèses ;
  \item elle est composée d'un ensemble de \emph{règles} de la forme
    \texttt{membre gauche -> \{membre droit\}} ;
  \item le membre gauche est composé du ou des motifs séparés les uns des autres
    par une virgule ;
  \item le membre droit est un bloc de code mixte (hôte + \textsf{Tom}).
\end{itemize}
Dans notre exemple, le calcul de filtrage est le suivant : 
\begin{itemize}
%  \item si \texttt{x} filtre \texttt{t1}, alors \texttt{zero()} et
%    \texttt{succ(y)} peuvent éventuellement filtrer \texttt{t2} ;
  \item si \texttt{zero()} filtre \texttt{t2}, alors le résultat de
    l'évaluation de la fonction \texttt{peanoPlus} est \texttt{x}, instancié par
    \texttt{t1} par filtrage ;
  \item si \texttt{suc(y)} filtre \texttt{t2}, alors le symbole de tête du
    terme \texttt{t2} est \emph{suc}. Le sous-terme \texttt{y} est ajouté à
    \texttt{x} et le résultat de l'évaluation de \texttt{peanoPlus} est donc
    \texttt{suc(peanoPlus(x,y))}.
\end{itemize}
%Bien que l'expression de la fonction \texttt{peanoPlus} soit donnée de manière
%fonctionnelle, elle définit bien une fonction {\java} qui peut être utilisée
%comme toute autre fonction {\java} dans le programme. 
L'expression de la fonction \texttt{peanoPlus} est donnée par filtrage et
définit une fonction {\java} qui peut être utilisée comme toute autre fonction
{\java} dans le programme.
Notons cette
particularité qu'a le langage {\tom} de complètement s'intégrer au langage hôte
sans pour autant être intrusif. Ainsi, le compilateur {\tom} n'analyse que le
code {\tom} (parties grisées dans le listing~\ref{code:matchPeanoPlus}), les
instructions hôtes n'étant pas examinées et ne fournissant aucune information
au compilateur. Les instructions {\tom} sont traduites vers le langage hôte
et remplacées en lieu et place, sans modification du code hôte existant.

Une deuxième particularité des constructions de filtrage du langage {\tom} est
liée à la composition des membres droits des règles : plutôt qu'être de simples
termes, il s'agit en fait d'instructions du langage hôte qui sont exécutées
lorsqu'un filtre est trouvé. Si aucune instruction du langage hôte ne rompt le
flot de contrôle, toutes les règles peuvent potentiellement être exécutées.
Pour interrompre ce flot lorsqu'un filtre est trouvé, il faut utiliser les
instructions {\adhoc} du langage hôte, telles que \texttt{break} ou
\texttt{return}, comme dans le listing~\ref{code:matchPeanoPlus}.

%\ttodo{match alternatif ?~\ref{code:matchAltPeanoPlus} :
%\input{code/matchPeanoPlus}}


\index{Filtrage!associatif|(}

\paragraph{Filtrage associatif.} Dans le cas d'un filtrage non unitaire
(filtrage pour lequel il existe plusieurs solutions,
voir~\ref{subsec:filtrage}), l'action est exécutée pour chaque filtre
solution. Le filtrage syntaxique étant unitaire, il n'est pas possible
d'exprimer ce comportement. Le langage {\tom} dispose de la possibilité
d'opérer du \emph{filtrage associatif avec élément neutre} (ou \emph{filtrage
de liste}, noté $AU$ dans la section~\ref{subsec:filtrage}) qui n'est pas
unitaire et qui permet d'exprimer aisément des algorithmes opérant du filtrage
sur des listes. Il est ainsi possible de définir des opérateurs variadiques
(opérateurs d'arité variable, par exemple les opérateurs de listes), comme nous
l'avons vu dans la section précédente (\ref{subsec:filtrage}). Dans le
listing~\ref{code:gomPeano} suivant, nous reprenons notre exemple des entiers
de Peano que nous augmentons d'un nouveau constructeur, \texttt{concNat} de
sorte \texttt{NatList} et dont les sous-termes sont de type \texttt{Nat}.
%\pagebreak

\input{code/gomPeano}

L'opérateur \texttt{concNat} peut être vu comme un opérateur de concaténation
de listes de \texttt{Nat} : \texttt{concNat()} représente la liste vide
d'entiers naturels, \texttt{concNat(zero())} la liste ne contenant que
\texttt{zero()} et \texttt{concNat(zero(),suc(zero()),suc(suc(zero())))} la
liste contenant trois entiers naturels : 0, 1 et 2. La liste vide est
l'élément neutre.
{\tom} distingue syntaxiquement les variables de filtrage représentant un
élément ---~par exemple \texttt{x} dans le
listing~\ref{code:matchPeanoPlus}~--- et les variables représentant une
sous-liste d'une liste existante en ajoutant le caractère \texttt{*}.

Le filtrage associatif permet d'opérer une itération sur les éléments d'une
liste comme l'illustre l'exemple du
listing~\ref{code:listmatchingAfficherPeano} :

\input{code/listmatchingAfficherPeano}

Dans cet exemple, \texttt{liste} est une liste d'entiers naturels, de type
\texttt{NatList} implémenté par le type {\java} \texttt{NatList}.  Nous
souhaitons afficher ces entiers avec leur position dans la liste. L'action est
exécutée pour chaque filtre trouvé, et les variables de listes \texttt{X1*} et
\texttt{X2*} sont instanciées pour chaque sous-liste préfixe et suffixe de la
liste \texttt{liste}. \texttt{X1} correspond à un objet {\java} de type
\texttt{NatList}, la méthode \texttt{length()} retournant la longueur de la
liste peut donc être utilisée pour obtenir l'indice de l'élément \texttt{x}.
L'énumération s'opère tant que le flot d'exécution n'est pas interrompu. Dans
notre exemple, nous nous contentons d'afficher l'élément et sa position.
L'exécution de la procédure \texttt{afficher} sur l'entrée \texttt{liste =
`conc(zero(), zero(), suc(suc(zero())), zero())} donne :

\input{code/outputAfficherPeano}
\index{Filtrage!associatif|)}

\index{Filtrage!non\ linéaire|(}
Le langage {\tom} offre aussi la possibilité de procéder à du filtrage
\emph{non-linéaire} (motifs pour lesquels une même variable apparaît plusieurs
fois). Le listing~\ref{code:nonlinearlistmatchingSupprimerDoublon} ci-après
illustre ce mécanisme : dans la fonction \texttt{supprimerDoublon}, la variable
\texttt{x} apparaît à plusieurs reprises dans le motif.
\index{Filtrage!non\ linéaire|)}

\input{code/nonlinearlistmatchingSupprimerDoublon}

Parmi les notations disponibles dans le langage, certaines sont très couramment
utilisées et apparaîtront dans les extraits de code de ce document. Nous les
illustrons dans le 
%Ajoutons aussi des notations disponibles dans le langage que nous utiliserons
%couramment, que nous illustrons dans le
listing~\ref{code:aliasunderscoreAfficherPeano} dont le but est d'afficher un
sous-terme de la liste \texttt{liste} ayant la forme \texttt{suc(suc(y))},
ainsi que sa position dans la liste, s'il existe :

\input{code/aliasunderscoreAfficherPeano}

Les notations \texttt{\_} et \texttt{\_*} pour les sous-listes désignent des
variables dites anonymes : c'est-à-dire que leur valeur ne peut être utilisée
dans le bloc action de la règle.  La notation \texttt{@} permet de créer des
alias : ainsi, on peut nommer des sous-termes obtenus par filtrage. L'alias
permet de vérifier qu'un motif filtre ---~\texttt{suc(suc(\_))} dans notre
exemple~--- tout en instanciant une variable ---~\texttt{x}~--- avec la valeur
de ce sous-terme. Si on applique la procédure \texttt{chercher} à l'entrée
précédente définie comme \texttt{liste = `conc(zero(), zero(),
suc(suc(zero())), zero())}, on obtient le résultat suivant :
\begin{tomcode4}
  suc(suc(zero())) trouv#\texttt{é}#, en position 2
\end{tomcode4}

\index{Filtrage|)}\index{Pattern-matching|)}

\subsection{Notations implicite et explicite}
%\todo{notation implicite vs explicite ? ou alors au fil de l'eau plus tard ? ou
%pas trop utile ?}

Lorsque l’on écrit un \emph{pattern} dans le membre gauche d'une règle, il est
possible d'écrire l'opérateur et ses champs de deux manières. %En effet, les
%champs des opérateurs {\tom} 
Ces derniers étant nommés, plutôt qu'écrire l'opérateur avec tous ses arguments
(\emph{notation explicite}), on peut utiliser leurs noms dans le motif pour
expliciter des sous-termes particuliers et en omettre d'autres. Ces derniers
sont alors ignorés lors du filtrage. Cette notation est dite \emph{implicite}
et s'utilise {\via} les lexèmes \lex{[} et \lex{]}. Il existe également une
notation à base de contraintes qui peut rendre l'écriture implicite plus
naturelle dans certains cas.

Considérons un exemple simple pour illustrer ces deux notations : si on définit
les personnes comme des termes construits en utilisant l'opérateur
\emph{Personne}, d'arité \emph{3} et de type \emph{Personne}, ayant les
arguments nommés \emph{nom} et \emph{prenom} de type « chaîne de caractères »,
et \emph{age} de type entier, les trois fonctions suivantes du
listing~\ref{code:implicitExplicitNotations} sont équivalentes :

\input{code/implicitExplicitNotations}

Outre l'indéniable gain en lisibilité du code qu'elle apporte de par
l'utilisation des noms, la notation implicite améliore la maintenabilité du
logiciel développé. En effet, dans le cas d'une extension de la signature
(ajout d'un champ \emph{numTelephone}, par exemple), l'usage de la notation
explicite impose d'ajouter un \texttt{\_} dans toutes les règles où l'opérateur
\emph{Personne} est utilisé. Dans notre exemple, la première fonction
---~\texttt{peutConduireExplicite()}~--- devrait donc être modifiée,
contrairement aux deux autres ---~\texttt{peutConduireImplicite()} et
\texttt{peutConduireImplicite2()}. Avec cette
notation, seuls les motifs manipulant explicitement les champs ayant été
changés doivent être modifiés, d'où une plus grande robustesse au changement.\\
Dans la suite de ce manuscrit, nous utiliserons indifféremment l'une ou l'autre
des notations dans les extraits de code proposés.


\subsection{Stratégies : maîtriser l'application des règles de réécriture}
\label{subsec:strategy}\index{Stratégie|(}\index{\tom!\lex{\%strategy}}

On peut analyser la structure de termes et encoder des règles de transformation
grâce à la construction \lex{\%match}. Le contrôle de l'application de ces
règles peut alors se faire en {\java} en utilisant par exemple la récursivité.
Cependant, traitement et parcours étant entrelacés, cette solution n'est pas
robuste au changement et le code peu réutilisable. En outre, il est difficile
de raisonner sur une telle transformation. Une autre solution est d'utiliser
des \emph{stratégies}~\cite{BallandMR08,Balland2012}, qui sont un moyen
d'améliorer le contrôle qu'a l'utilisateur sur l'application des règles de
réécriture. Le principe de programmation par stratégies permet de séparer le
traitement (règles de réécriture, partie métier de l'application) du parcours
(traversée de la structure de données arborescente), et de spécifier la manière
d'appliquer les règles métier.

{\tom} fournit un puissant langage de stratégies, inspiré de
{\elan}~\cite{Borovansky1998}, {\stratego}~\cite{Visser1998},
%\cite{Kats2010}\cite{Hemel2010}
et {\jjtrav}~\cite{Visser2001}. Ce langage permet d'élaborer des stratégies
complexes en composant des combinateurs élémentaires tels que
\texttt{Sequence}, \texttt{Repeat}, \texttt{TopDown} et la récursion. Il sera
donc en mesure de contrôler finement l'application des règles de réécriture en
fonction du parcours défini. Le listing~\ref{code:strategyPeanoTransform}
illustre la construction \lex{\%strategy}, ainsi que son utilisation :
\input{code/strategyPeanoPlus}

Dans cet exemple, nous supposons que notre signature contient d'autres
opérateurs : \texttt{plus} et \texttt{one} de type \texttt{Nat}. La stratégie
\texttt{transformationPeano} réécrit les constructeurs \texttt{one} en
\texttt{suc(zero())} et les constructeurs \texttt{plus(zero(),x)} en
\texttt{x}. Ligne 1, \texttt{additionPeano} étend \texttt{Identity}, ce qui
donne le comportement par défaut de la stratégie : si aucune
règle ne s'applique, aucune transformation n'a lieu, par opposition à
\texttt{Fail} qui spécifie que la transformation échoue si la règle ne peut
être appliquée. La construction \lex{visit} (ligne 2) opère un premier filtre
sur les sortes de type \texttt{Nat} sur lesquelles les règles doivent
s'appliquer. Les règles sont quant à elles construites sur le même modèle que
les règles de la construction \lex{\%match}, décrite dans la
section~\ref{subsec:matching}. Le membre gauche est un \emph{pattern}, tandis
que le membre droit est un bloc action composé de code {\tomjava}. Ensuite, la
stratégie est composée avec une stratégie de parcours fournie par une
bibliothèque appelée \texttt{sl}. Le terme la représentant est créé, et sa
méthode \texttt{visit} est appliquée sur le nombre que nous souhaitons
transformer. Pour l'entrée donnée, le résultat affiché est le suivant (les 
couleurs ont été ajoutées pour faire apparaître clairement les sous-termes
transformés) :
\begin{tomcode4}
  plus(plus(suc(suc(#\colcode{darkgreen}{one()}#)), #\tomred{one()}#), #\javablue{plus(suc(one()),zero())}#) 
    a #\texttt{é}#t#\texttt{é}# transform#\texttt{é}# en 
  plus(plus(suc(suc(#\colcode{darkgreen}{suc(zero())}#)), #\tomred{suc(zero())}#), #\javablue{suc(suc(zero()))}#)
\end{tomcode4}

Pour des informations plus détaillées sur les stratégies {\tom} ainsi que sur
leur implémentation dans le langage, nous conseillons la lecture
de~\cite{Balland2009, BallandMR08, Balland2012} ainsi que la page dédiée du
site officiel du projet
{\tom}\footnote{Voir
  \url{http://tom.loria.fr/wiki/index.php5/Documentation:Strategies/}.}.

%\ttodo{est-il nécessaire de lister les stratégies disponibles ? Est-il
%nécessaire d'écrire ce que sont chacune d'entre elles ?}
%\ttodo{ ?? mettre une explication formelle : fonction, composition, énumération
%  de positions, etc. ; ? -> oui, certainement}

\index{Stratégie|)}

\section{Ancrages formels}
\label{subsec:mapping}\index{Ancrages algébriques|(}\index{Mappings|(}

Précédemment, nous avons vu que nous pouvons ajouter des constructions de
filtrage au sein de langages hôtes et que nous sommes en mesure de filtrer des
termes. %objets arbitraires. 

Les constructions de filtrage sont compilées indépendamment des implémentations
concrètes des termes. Ainsi, dans les exemples, nous filtrons sur des termes
de type \texttt{Nat} et \texttt{NatList}, définis dans la signature {\gom}.
Cependant, les fonctions {\java} prennent des paramètres d'un type donné que
le compilateur {\java} est censé comprendre, et nous n'avons pas détaillé la
manière dont le lien entre les types {\tom} et les types {\java} est assuré.
%Cependant, les fonctions {\java} prenaient des paramètres de type
%\texttt{JNat} et \texttt{JNatList}. 
À la compilation, les instructions sur les
termes algébriques sont traduites en instructions sur le type de données
concret représentant ces termes algébriques. Le mécanisme permettant d'établir
cette relation entre les structures de données algébriques et concrètes
s'appelle le mécanisme d'\emph{ancrage}, ou \emph{mapping}. Il permet de donner une
vue algébrique d'une structure de données quelconque afin de pouvoir la
manipuler à l'aide des constructions {\tom}, sans modifier l'implémentation
concrète.

On spécifie les \emph{mappings} à l'aide des constructions {\tom}
\lex{\%typeterm}\index{\tom!\lex{\%typeterm}},
\lex{\%op}\index{\tom!\lex{\%op}} et \lex{\%oplist}\index{\tom!\lex{\%oplist}}
pour décrire respectivement les sortes, les opérateurs algébriques et les
opérateurs variadiques. Dans la section~\ref{subsec:signalg}, nous avons défini
une signature algébrique, et l'outil {\gom} génère une
implémentation concrète ainsi que les ancrages. Cela nous permet de rendre
ce mécanisme complètement transparent pour l'utilisateur. Pour expliquer les
constructions constituant les \emph{mappings}, nous allons les expliciter 
sans passer par la génération de {\gom}. Pour la suite de cette section, nous
prenons l'exemple du type \texttt{Individu} et de l'opérateur
\texttt{personne}, qui prend trois arguments : un nom et un prénom, de type
\texttt{String}, et un âge de type \texttt{int}. Nous adoptons aussi une
notation pour lever toute ambiguïté sur les types : nous préfixons les types
{\java} de la lettre \texttt{J}, et nous utiliserons l'implémentation qui suit.
%Nous utiliserons l'implémentation
%{\java} suivante des entiers de Peano.
%%Avant d'expliquer ces constructions, le
%%listing~\ref{code:implementationJPeano} donne l'implémentation concrète des
%%entiers de Peano que nous utilisons pour ces exemples :
%%\input{code/implementationJPeano}
%Avant d'expliquer ces constructions, donnons l'implémentation concrète des
%entiers de Peano que nous utilisons pour ces exemples.
Nous considérons les classes {\java} \texttt{JIndividu} et \texttt{JIndividuList}
suivantes qui implémentent respectivement les types algébriques
\texttt{Individu} et \texttt{IndividuList}.
%\lstinputlisting[name=expeano,numberstyle=\tiny,numbers=left,numberblanklines=false,frame=tb,firstnumber=1,firstline=6,lastline=7]{code/ExamplePeano.t}%style=codesource,
\lstinputlisting[name=exhumain,numberstyle=\tiny,numbers=left,numberblanklines=false,frame=tb,firstnumber=1,firstline=6,lastline=7]{code/ExempleHumain.t}%style=codesource,



%Nous considérons ensuite les classes {\java} \texttt{Jzero}, \texttt{Jsuc} et
Nous considérons ensuite les classes {\java} \texttt{Jpersonne} et
\texttt{JconcJIndividu} suivantes qui implémentent les opérateurs algébriques :
%\lstinputlisting[name=expeano,numberstyle=\tiny,numbers=left,numberblanklines=false,frame=tb,firstnumber=auto,linerange={9-10,11-22,30-30,48-59,72-72}]{code/ExamplePeano.t}%style=codesource,
\lstinputlisting[name=exhumain,numberstyle=\tiny,numbers=left,numberblanklines=true,frame=tb,firstnumber=auto,linerange={19-22,24-28,235-256}]{code/ExempleHumain.t}%style=codesource, %9-17
%avec head et tail
%\lstinputlisting[name=exhumain,numberstyle=\tiny,numbers=left,numberblanklines=true,frame=tb,firstnumber=auto,linerange={19-22, 24-28,40-51,64-64}]{code/ExempleHumain.t}%style=codesource, %9-17


Les sortes \texttt{Individu} et \texttt{IndividuList} sont exprimées {\via} le lexème
\lex{\%typeterm} comme le montre le listing~\ref{code:typetermIndividu} suivant :
%\input{code/typetermNat}
\input{code/typetermIndividu}

La construction \lex{\%typeterm} permet d'établir la relation entre le type
algébrique \texttt{Individu} et le type concret {\java} \texttt{JIndividu}.
Deux sous-constructions la composent :
\begin{itemize}
  \item \lex{implement} donne l'implémentation effective du langage hôte
    à lier au type algébrique ; 
  \item \lex{is\_sort} est utilisée en interne par le compilateur pour tester le
    type d'un élément (optionnel) ;
%  \item \lex{equals} définit comment comparer deux termes (optionnel).
\end{itemize}

La sorte \texttt{Individu} étant définie, il est nécessaire de spécifier à
{\tom} comment \emph{construire} et comment \emph{détruire} (décomposer) les
termes de ce type. Pour cela, nous utilisons la construction \lex{\%op}, comme
illustré par le listing~\ref{code:opIndividu} où l'opérateur \texttt{personne}
est défini :

%\input{code/opNat}
\input{code/opIndividu}

La définition d'opérateurs passe par une construction composée de quatre
sous-cons\-tructions :
\begin{itemize}
  \item \lex{is\_fsym} spécifie la manière de tester si un objet donné
    représente bien un terme dont le symbole de tête est l'opérateur ;
  \item \lex{make} spécifie la manière de créer un terme ;
  \item \lex{get\_slot} (optionnel) spécifie la manière de récupérer la valeur
    d'un champ du terme ;
  \item \lex{get\_default} (optionnel) donne la valeur par défaut de l'attribut.
\end{itemize}
%\todo{[utile ?]}
Notons que {\tom} ne permet pas la surcharge d'opérateurs, c'est-à-dire
qu'il n'est pas possible de définir plusieurs opérateurs ayant le même nom, mais
des champs différents.

La construction \lex{\%oplist} est le pendant de \lex{\%op} pour les opérateurs
variadiques. Ainsi, dans le listing~\ref{code:opIndividuList}, nous pouvons
définir un opérateur de liste d'individus \texttt{concIndividu}, de type
\texttt{IndividuList}, et acceptant un nombre variable de paramètres de type
\texttt{Individu}.
%\input{code/typetermNatList} %inutile
%\input{code/opNatList}
\clearpage %pour éviter une coupure
\input{code/opIndividuList}

Les sous-constructions suivantes la composent :
\begin{itemize}
  \item \lex{is\_fsym} spécifie la manière de tester si un objet donné
    représente bien un terme dont le symbole de tête est l'opérateur ;
  \item \lex{make\_empty} spécifie la manière de créer un terme vide;
  \item \lex{make\_insert} spécifie la manière d'ajouter un fils en
    première position à la liste ;
  \item \lex{get\_head} spécifie la manière de récupérer le premier élément de
    la liste;
  \item \lex{get\_tail} spécifie la manière de récupérer la queue de la liste
    (sous-liste constituée de la liste privée du premier élément) ;
  \item \lex{is\_empty} spécifie la manière de tester si une liste est vide.
\end{itemize}


Notons que le langage {\tom} supporte aussi le
sous-typage~\cite{tavares09,Tavares2012}. Il est donc possible de spécifier un
type comme sous-type d'un autre type déjà exprimé. Cette relation de
sous-typage exprimée dans les types {\tom} doit évidemment être cohérente avec
celle exprimée dans l'implémentation concrète en {\java}. Reprenons l'exemple
précédent des \emph{individus} et considérons différents sens possibles :
\emph{être vivant} (sens couramment utilisé, d'où le constructeur
\texttt{personne}), \emph{spécimen vivant d'origine animale ou végétale} (en
biologie) et \emph{élément constituant un ensemble} (en statistiques). Le type
\emph{Individu} pouvant être ambigu, nous décidons de le préciser en intégrant
des sous-types. Pour cela, il existe une construction {\tom} permettant de
spécifier un sous-type dans un ancrage algébrique : \lex{extends}, qui complète
la construction \lex{\%typeterm}.

\input{code/subtype.tex}

Dans le listing~\ref{code:subtypeIndividu}, nous déclarons donc un nouveau
type, \texttt{IndividuBiologie}, sous-type de \texttt{Individu} (lignes 1 à 5).
Il est implémenté par le type {\java} \texttt{JIndividuBiologie} dont la
relation de sous-typage avec \texttt{JIndividu} est exprimée par la
construction {\java} consacrée à l'héritage : \lex{extends} (ligne 7). Il est
ensuite possible de définir de manière classique des opérateurs de type
\texttt{IndividuBiologie} comme l'illustre le listing~\ref{code:opSubtype}.

\input{code/opSubtype}

\index{Ancrages algébriques|)}\index{Mappings|)}

\section{Domaines d'applications}

{\tom} est particulièrement utile pour parcourir et transformer les structures
arborescentes comme {\xml} par exemple. Il est donc tout à fait indiqué pour
écrire des compilateurs ou interpréteurs, et plus généralement des outils de
transformation de programmes ou de requêtes. Outre son utilisation pour écrire
le compilateur {\tom} lui-même, nous noterons son usage dans les cadres
académiques et industriels suivants :
\begin{itemize}

  \item implémentation d'un mécanisme défini par Guillaume Burel dans sa
    thèse~\cite{burel09} pour une méthode des tableaux particulière appelée
    {\tamed}~\cite{bonichon04} ;
    
  \item prototypage de langages tels que {\miniml} dont la compilation a été
    décrite par Paul Brauner dans sa thèse~\cite{brauner10} ; 

  \item implémentation d'un assistant à la preuve tel que {\lemuridae}
    développé par Paul Brauner pour un calcul des séquents nommé
    {\lkms}~\cite{brauner10} ;

  \item implémentation de compilateurs ou interpréteurs, comme le
  compilateur {\pluscaltwo}
  \footnote{Voir \url{https://gforge.inria.fr/projects/pcal2-0/}.} qui traduit des
  algorithmes exprimés en {\pluscal} en {\tlaplus} pour faire du
  \emph{model-checking} ;

  \item raisonnement formel sur la plateforme
    {\rodin}~\footnote{Voir \url{http://www.event-b.org/}.}. Il s'agit d'un outil
    industriel \emph{open source} développé par
    Systerel\footnote{Voir \url{http://www.systerel.fr/}.} qui permet de formaliser,
    d'analyser et de prouver les spécifications de systèmes complexes ;

    %http://ovado.fr/

%Tom est utilisé pour la plateforme Rodin (http://www.event-b.org/), notamment
%pour faire du raisonnement formel. La plateforme Rodin est un outil industriel
%open-source qui permet de formaliser, d'analyser et de prouver les
%spécifications de systèmes complexes.

  \item outil de transformation de requêtes OLAP (\emph{OnLine Analytical
    Processing}) en requêtes {\sql} (\emph{Structured Query Language}) pour
    assurer la rétro-compatibilité entre les versions du logiciel
    {\crystalreports}\footnote{Voir \url{http://crystalreports.com/}.} développé par
    Business Object\footnote{Voir \url{http://www.businessobjects.com/}.} ;
    
  \item transformations de modèles qualifiables pour les systèmes embarqués
  temps-réel dans le projet
{\quarteft}\footnote{Site du projet : \url{http://quarteft.loria.fr/}.} porté par le LAAS-CNRS
\footnote{Laboratoire d'Analyse et d'Architecture des Systèmes :
  \url{http://www.laas.fr/}.}, l'IRIT \footnote{Institut de Recherche en
  Informatique de Toulouse : \url{http://www.irit.fr/}.}, l'ONERA-DTIM
  \footnote{Office national d'études et de recherches aérospatiales :
    \url{http://www.onera.fr/fr/dtim/}.} et Inria Nancy ainsi que nos partenaires
    industriels Airbus\footnote{Voir \url{http://www.airbus.com/}.} et Ellidiss
    Software\footnote{Voir \url{http://www.ellidiss.com/}.}. C'est dans ce cadre que
    s'inscrit cette thèse.

\end{itemize}

\index{\tom|)}



\section{Apport de la thèse au projet {\tom}}
\label{sec:contrib}
%\ttodo{contrib technique : extension \%transformation, \%resolve, \%tracelink,
%participation/évolution de {\tom}-{\emf} (prototype développé avant ma thèse),
%schéma pour que ce soit plus clair ; contribution : expression de
%transformations haut-niveau accessibles à tous ; expression de modèles EMF
%Ecore ; traçabilité}

Durant cette thèse, j'ai contribué techniquement au projet {\tom}. La
figure~\ref{fig:wholeTomProcessBeforeThesis} illustre le fonctionnement global
du système {\tom} au début de ma thèse, et sert de point de comparaison avec la
figure~\ref{fig:wholeTomProcessContrib} pour illustrer cet apport de
développement. 

\begin{figure}[h]
  \begin{center}
%    \begingroup
%    \tikzset{every picture/.style={scale=0.9}}
    \input{figures/wholeTomProcessBeforeThesis}
%    \endgroup
  \end{center}
  \caption{Fonctionnement global du projet {\tom} en début de thèse.}
  \label{fig:wholeTomProcessBeforeThesis}
\end{figure}

La contribution technique de cette thèse au projet {\tom} a consisté en
l'extension du langage {\tom} par l'ajout de constructions haut-niveau dédiées
à la transformation de modèles. Ces constructions haut niveau
(\lex{\%transformation}, \lex{\%resolve} et \lex{\%tracelink}) sont détaillées
dans le chapitre~\ref{ch:outils}. La construction \lex{\%transformation}
implémente une méthode proposée dans~\cite{Bach2012} pour transformer des
modèles {\emf} {\ecore}, tout en simplifiant l'écriture de la transformation
pour l'utilisateur. Cette méthode se déroule en deux phases :
\begin{itemize}
  \item une phase de \emph{décomposition} de la transformation en
    transformations élémentaires encodées par des stratégies {\tom} ;
  \item une phase de \emph{réconciliation} durant laquelle le résultat
    intermédiaire obtenu lors de la première phase est rendu cohérent et
    conforme au métamodèle cible.
\end{itemize}
Les constructions \lex{\%resolve} et \lex{\%tracelink} servent à la phase de
\emph{réconciliation} d'une transformation de modèle suivant la méthode
proposée. En suivant cette approche, l'utilisateur peut écrire les
transformations élémentaires de manière indépendante et sans aucune notion
d'ordre d'application des pas d'exécution de la transformation.

La construction \lex{\%tracelink} présente aussi un intérêt en termes de
traçabilité de la transformation. Nous souhaitons générer des traces
d'exécution de la transformation à la demande de l'utilisateur, ce pour quoi
\lex{\%tracelink} a été conçue.

Cela a eu pour conséquence l'ajout d'un nouveau greffon (voir la
figure~\ref{fig:tomArchi}) dans la chaîne de compilation (\emph{transformer}),
ainsi que l'adaptation de cette chaîne, du \emph{parser} au \emph{backend},
afin de prendre en compte cette extension du langage.\\
Outre l'évolution du langage {\tom} lui-même, le générateur d'ancrages
algébriques {\tomemf} a aussi évolué et est maintenant disponible en
version stable.
%\todo{[schéma bof bof ; en fait ce schéma peut apparaitre plus loin, dans la
%partie outillage avec les travaux d'implémentation, ici ce serait bien d'avoir
%un schéma plus simple, ou alors pas de schéma ?] }

%La figure~\ref{fig:wholeTomProcessContrib} permet de visualiser ces
%contributions, les pointillés mettant en avant les points essentiels d'apport
%de mon travail au projet {\tom}.

Nos contributions au projet {\tom} apparaissent en pointillés sur la
figure~\ref{fig:wholeTomProcessContrib}.

%Les
%pointillés dans la figure~\ref{fig:wholeTomProcessContrib} mettent en avant les
%points essentiels d'apport de mon travail au projet {\tom}.

\begin{figure}[h]
  \begin{center}
    \input{figures/wholeTomProcessContrib}
  \end{center}
  \caption{Fonctionnement global de {\tom} et contributions de ce travail de thèse au projet.}
  \label{fig:wholeTomProcessContrib}
\end{figure}


%La figure~\ref{fig:wholeTomProcessContrib} illustre le fonctionnement global du
%système {\tom}. Les zones en pointillés %fig:apportTheseTom}
%mettent en avant les points essentiels d'apport de cette thèse au projet {\tom}.

%\input{figures/wholeTomProcess}
%\ttodo{faire la version précédente sans le dessous, puis la même avec les pointillés $\righarrow$ c'est wholeTomProcessContrib}
%\input{figures/wholeTomProcess2}
%\input{figures/tomSystemContrib}
%\input{figures/tomEMFCompiler}

% vim:spell spelllang=fr