Chapter 1 Typage d'un mini-ML
Un compilateur ML se décompose de manière classique en :
-
une analyse lexicale puis syntaxique du texte source en entrée qui construit un arbre de syntaxe;
- un vérificateur de types qui infère les types des expressions et détecte donc les erreurs
de typage;
- un producteur de code assembleur, souvent d'une machine abstraite;
- et d'une phase d'assemblage pour exécuter ce code sur un processeur existant.
On se propose dans cette section de définir la syntaxe abstraite d'un langage appelé mini-ML,
qui est un sous-ensemble de Caml-light et de montrer son mécanisme de typage, qui à des simplifications
près est celui de Caml-light. Mini-ML correspond au noyau fonctionnel de Caml-light sans
le filtrage. Il ne contient ni exceptions ni traits impératifs. Cette dernière restriction
simplifie le vérificateur de types sans en changer la nature profonde. L'algorithme d'unification
est assez différent de celui déjà vu pour le typage du l-calcul car il appliquera
directement, en faisant une modification physiques sur les types, les substitutions de variables de type.
Le programme de vérification de types s'inspire des deux exemples de Michel Mauny que l'on peut lire dans
la présentation d'une ``spécification CAML d'un sous-ensemble de CAML'' et du langage ASL de la documentation Caml-light (voir bibliographie).
Chapter 2 Typage des traits impératifs
Ce document a été traduit de LATEX par
HEVEA et HACHA.