Université Paris 6 Licence d'informatique Maîtrise de Sciences et Techniques (Experts en Systèmes Informatiques)	Module de Programmation Année 1999-2000

Travaux pratiques n° 2: synthèse de types pour Micro-Caml

Le but du TP est d'implanter un algorithme de synthèse des types pour un petit langage fonctionnel dont la syntaxe est très proche de celle de Caml Light.

Cet algorithme sera construit pas à pas en considérant des formes d'expressions de plus en plus complexes. On considèrera dans un premier temps que les expressions n'ont pas de type polymorphe: on traitera donc d'abord le cas des constantes, des expressions arithmétiques, des expressions conditionnelles, puis les applications, les fonctions et enfin les récursions.

On traitera ensuite le cas général d'expressions ayant des types polymorphes en suivant encore la même progression.

1 Définition syntaxique du langage

Un programme est une suite de déclarations de la forme:

 <decl> :: = let <nom> = <expr>;;

où <expr> désigne n'importe quelle expression. Un <nom> est une séquence ininterrompue de lettres de l'alphabet. Les expressions sont définies par la grammaire suivante au format BNF (Bachus Naur Form):

 <expr> ::= if <expr> then <expr> else <expr>          
         |  let <nom> = <expr> in <expr>               
         |  function <nom> -> <expr>
         |  rec <nom> <nom> = <expr>
         |  <expr> <expr>                  
         | ( <expr> ) 
         | <expr>,<expr>
         | fst <expr>
         | snd <expr>                            
         | <nom>
         | i
         | true | false
         | <expr> <op> <expr>
         | <infix> <expr>
 <op>   ::= + | - | * | / | < | > | <= | >= | != | =
 <infix>::= -

Une expression peut être une expression conditionnelle (if), une déclaration locale (let), une fonction, une fonction récursive, une application de fonction, une expression entre parenthèses, une paire de deux expressions, un accès à la première composante d'une paire (fst), un accès à la deuxième (snd), une variable (nom), une constante entière (i), un booléen (true et false), une expression arithmétique infixe ou une expression arithmétique préfixe.

Exemple 1

Les expressions suivantes sont des expressions valides du langage:


  let f =
    function x -> function y -> if y = x then let x = 2 in x+y else 3;;

  let resultat = f 2 3;;

  let rec fact x = if x = 0 then 1 else x * (fact (x-1));;

  let app f g x = f (g x);;

2 Principes généraux

Le typage d'une expression consiste en la succession de plusieurs étapes:

Une première étape d'analyse syntaxique qui construit une structure représentant la déclaration donnée en entrée.
Une étape de typage associant un type à chaque déclaration. Ici, ce typage utilisera un environnement de typage associant des types aux identificateurs du programme.
Une étape d'affichage du résultat et de mise à jour de l'environnement global. Un message d'erreur approprié sera émis en cas d'erreur durant le typage.

Une partie de ces phases successives vous est donnée. Certaines sont à compléter ou à réaliser. L'organisation est détaillée ci-dessous.

2.1 Représentation abstraite des expressions et des types

Les expressions du langage et les types sont définis dans le module:

Module syntaxe_abstraite

Déclare les types de données suivants:

  type decl = ...
  and expr = ...
  and immediat = ..
  and localisation = ...
 
  and typ = ...
  and var_type = ...
  and schema_de_type = ...

Cette partie définit les déclarations, les expressions, les valeurs dites immédiates (entiers, booléens), une information donnant la position de l'expression analysée dans le fichier source, les types du langage, les variables de type et les schémas de type. Ce module vous est donné.

Un module global déclarant l'environnement de typage global ainsi qu'une exception qui sera levée lorsqu'une erreur est survenue lors de l'analyse du programme (erreur de syntaxe ou erreur de typage).

Module global

Déclare les valeurs suivantes:

  exception Erreur;;
  value env_global : (string * schema_de_type) list ref;;
  value ajout_global : (string * schema_de_type) list -> unit;;
  value env_global : unit -> (string * schema_de_type) list;;

Ce module vous est donné.

2.2 Analyse syntaxique

Module syntaxe

Déclare les fonctions d'analyse syntaxique permettant de construire une déclaration et une expression à partir d'une chaîne de caractères. La troisième fonction d'analyse lit le contenu d'une chaîne de caractères stockée dans un buffer dit buffer lexical. Ce buffer devra avoir été crée au préalable. Cette création est expliquée dans le module lexing du manuel de référence de Caml Light (page 151).

  lire_decl_chaine : string -> decl
  lire_expr_chaine : string -> expr
  lire_decl : lexing__lexbuf -> decl

Cette partie vous est donnée.

2.3 Typage

L'algorithme de synthèse des types est basé sur l'algorithme d'unification que vous avez vu en td. On en rappelle ici brièvement le principe:

Unifier deux types t et t' consiste à trouver comment remplacer les variables de ces types par des types, de telle sorte qu'après remplacement, les deux types obtenus soient égaux. Autrement dit, il s'agit de trouver une substitution (une liste d'association) [a₁ \ t₁,...,a_n \ t_n] telle que:

t[a₁ \ t₁,...,a_n \ t_n] = t'[a₁ \ t₁,...,a_n \ t_n]

Cette substitution est désignée subst_type dans la suite du texte. Par exemple, les deux types:

int ® (a₁ ® bool * a₂) et a₃ ® (int ® bool * (int * bool) )

sont unifiables en utilisant la substitution:

[a₃ \ int, a₁ \ int, a₂ \ (int * bool)]

L'unification est réalisée par le module suivant:

Module unification

Définit les types de données et les valeurs suivantes:

exception Unification;;

value reinit_var_de_type : unit -> unit;;
value gen_var_type : unit -> var_type;;

value vars : var_type list -> var_type list -> typ -> var_type list;;
value var_libres : typ -> var_type list;;
value var_libres_env : (string * schema_de_type) list -> var_type list;;

value substituer : (var_type * typ) list -> typ -> typ;;
value unifier : (var_type * typ) list -> typ -> typ -> (var_type * typ) list;;

value generaliser : 
  (string * schema_de_type) list -> typ * (var_type * typ) list -> schema_de_type;;
value instancier : schema_de_type -> typ;;

La fonction gen_var_type rend une nouvelle variable de type et reinit_var_de_type permet d'initialiser cette fonction.

substituer subst_type t où subst_type est une substitution de type (associant des types à des variables de type) et t, un type, rend un type t' déduit de t en remplaçant les variables de t figurant dans subst_type par les types qui leur sont associés.

unifier subst_type t1 t2, où subst_type est une substitution de type, t1 et t2 sont des types, rend une nouvelle substitution subst_type' telle que substituer subst_type' t1 = substituer subst_type' t2. Lorsque les deux types ne sont pas unifiables, l'exception Unification est levée.

Ce module vous est donné. Il est recommandé cependant de l'examiner en détail et d'essayer plusieurs exemples avant de s'attaquer au typage des programmes.

Module typer

Définit les types de données et les valeurs suivantes:

value unifier_exp : 
  (var_type * typ) list -> expr -> typ -> typ -> (var_type * typ) list;;
value typer : 
  (string * schema_de_type) list -> (var_type * typ) list 
                                 -> expr -> typ * (var_type * typ) list;;
value typer_decl : decl -> unit;;

unifier_exp subst_type e typ_obtenu typ_attendu unifie le type typ_obtenu pour l'expression e avec le type typ_attendu. Si l'unification a échoué (l'exception Unification a été levée), cette fonction devra émettre un message d'erreur approprié.

typer env_de_type subst_type e rend le type obtenu pour l'expression e ainsi qu'une nouvelle substitution de type (on peut en effet supposer que le typage de e a fait apparaitre de nouvelles contraintes de type). Elle est paramétrée par un environnement de type env_type (associant des schémas de type aux variables du programme) et subst_type.

typer_decl s'occupe du typage des déclarations: cette fonction type une déclaration, modifie l'environnement global et affiche le type obtenu.

Ce module est à écrire.

2.4 Affichage et traitement des erreurs

Une fois le type obtenu, celui-ci doit être affiché et en cas d'erreur, il est nécessaire de pouvoir indiquer à l'utilisateur l'endroit exact de l'erreur.

Module localisation

Ce module permet d'afficher une partie du code source où une erreur a été trouvée. Ce module exporte les deux fonctions suivantes:

  initialiser_localisation : string -> in_channel -> lexing__lexbuf -> unit
  afficher_source : syntaxe_abstraite__localisation -> unit

initialiser_localisation fichier ic lexbuf permet d'initialiser les fonctions du module: fichier est le nom du fichier dans lequel se trouvent les déclarations, ic est son descripteur de fichier (voir page 126 du manuel Caml Light), lexbuf est un buffer lexical. Cette fonction doit impérativement être exécutée avant d'utiliser la fonction afficher_source sur un programme écrit dans un fichier.

afficher_source loc permet d'afficher une partie du code source autour de la localisation loc.

Ce module vous est donné.

Module erreur

Définit divers types d'erreurs. Il exporte les fonctions:

  value erreur_de_syntaxe : localisation -> unit;;
  value erreur_identificateur : localisation -> string -> unit;;
  value erreur_de_type : 
    localisation -> typ -> typ -> unit;;

erreur_de_syntaxe loc traite des erreurs de syntaxe. erreur_identificateur loc x indique que x n'est pas déclaré en montrant la ligne concernée. erreur_de_type loc ty_obtenu ty_attendu indique que le type obtenu n'est pas unifiable avec le type attendu.

Ce module vous est donné.

Module main

Il devra exporter les fonctions suivantes:

  main_decl : unit -> unit
  main_string : string -> unit

Ce module est à écrire.

La fonction main_decl lance l'analyse syntaxique et le typage de la suite des déclarations apparaissant dans un fichier. Les déclarations sont analysées les unes après les autres. L'analyse d'un fichier s'arrête dès que l'analyse d'une déclaration échoue.

La construction de la fonction de synthèse des types sera faite pas à pas en construisant ou en augmentant les modules typer et main. Dans un premier temps, vous considèrerez que les expressions ne sont pas polymorphes (elles ne contiennent pas de variables de type). Vous traiterez ensuite le cas général. Pour cela, vous devrez développer votre implantation à l'aide d'un Makefile et de manière interactive en vérifiant qu'à chaque étape, la succession des étapes élémentaires est correcte.

3 Types monomorphes

3.1 Les constantes, les expressions arithmétiques et les conditionnelles

Question 1

Ecrire la fonction de typage lorsque les expressions sont réduites à des constantes entières ou booléennes. Lorsque l'expression à typer n'est pas définie, l'exception Non_implante pourra être levée.

Question 2

Enrichissez la fonction de typage pour qu'elle traite les expressions arithmétiques et les comparaisons. On rappelle ici qu'une expression arithmétique 1 + 3 est vue comme une double application de la variable + à la constante 1 puis à la constante 3.

Indication: Pour s'en convaincre, vous pouvez tester le résultat de l'analyse syntaxique sur des expressions arithmétiques.

Vous supposerez dans un premier temps que les comparaisons sont toujours appliquées à des entiers.

En cas d'erreur de type, vous afficherez un message approprié.

Question 3

Enrichissez la fonction de typage pour qu'elle traite également les conditionnelles. On rappelle ici qu'une expression conditionnelle if c then e1 else e2 est bien typée si c est un booléen et si e1 et e2 sont de même type.

3.2 Les variables et les définitions locales

Le typage d'une expression contenant une variable nécessite la définition d'un environnement permettant d'associer des types à des noms. Un environnement est une liste d'association (nom, schéma de type), donc une valeur de type:

  (string * schema_de_type) list

Question 4

Définir la fonction de typage des variables et des définitions locales. On fait l'hypothèse ici que les types ne sont pas polymorphes. Il n'y a donc pas de règle d'instanciation ni de règle de généralisation.

3.3 Les applications, les fonctions et les récursions

Etendre le typage pour qu'il traite des applications, les fonctions puis les fonctions récursives.

3.4 Les déclarations globales

Un programme est une suite de déclarations qui sont évaluées dans un environnement global.

Question 5

Définir la fonction de typage des déclarations globales dans le module typer et la fonction principale dans le module main. Il faudra pour cela ouvrir le fichier en lecture, lancer l'analyse syntaxique puis le typage et enfin, mettre à jour l'environnement de type global.

4 Types polymorphes

Modifiez la fonction de typage typer pour qu'elle traite les expressions ayant des types polymorphes.

Question 6

Cette extension sera faite pas à pas.

Ajoutez un traitement des fonctions fst et snd dont le type est polymorphe.
Définisser la nouvelle règle de typage des variables. La règle de typage des variables dans un environnement de type env_type est:
si env_type(x) = " a₁,...,a_n.ty alors x: instancier (" a₁,...,a.ty)
où la fonction instancier remplace les variables a₁,...,a_n par des variables de type neuves.
Définissez la nouvelle règle de typage des déclarations locales et globales. On rappelle qu'une fois que le type d'une déclaration a été obtenu, celui-ci doit être généralisé. On a:
generaliser env_type (ty) = " a₁,...,a_n.ty
où les a_i n'appartiennent pas à var_libre_env env_type.
Simplifiez alors le traitement des fonctions d'accès fst et snd ainsi que le traitement des expressions arithmétiques en remarquant qu'il suffit, pour les typer, de charger un environnement initial donnant le schéma de type associé à chaque opérateur arithmétique. Par exemple:
```
  + : Tpour_tout([],Tfleche(int,Tfleche(int,int)))
```
Indication: L'ensemble de ces déclarations pourra être rassemblé dans un module d'initialisation.

5 Compte rendu de TP

Le compte rendu doit être rédigé de manière concise et précise, en soignant la présentation.

Vous rendrez le code source de la version traitant le cas des types polymorphes. Vous expliquerez votre implantation du typage des variables, des conditionnelles, des applications, des fonctions et des récursions.

Indication: la fonction typer complète peut être écrite en moins de 100 lignes.
Donner un jeu d'exemples significatifs pour tester la fonction d'évaluation des expressions et des déclarations.

6 Documents fournis

Tous les fichiers nécessaires pour le TP se trouvent dans le catalogue /Infos/caml-ens/99-00/tp2. Vous y trouverez un fichier LISEZMOI qui décrit les différents fichiers ainsi qu'un Makefile donnant l'architecture générale de l'évaluateur. Ce fichier est à modifier suivant vos besoin. Enfin, le fichier exemples.txt vous donne quelques exemples de programmes du langage et le résultat rendu par le typage.

Vous disposer de l'exécutable typer qui prend en entrée un fichier fichier.mml et qui affiche sur la sortie standard le résultat du typage.

Ce document a été traduit de L^AT_EX par H^EV^EA.