L'objectif principal de ce TP est d'étendre le système de vérification des types du langage A6000 aux nouvelles constructions introduites dans les TP 5 et 6. Un objectif secondaire consiste à étendre le langage avec des structures de données dont le type est défini par l'utilisateur.
1. Règles de typage
On reprend les définitions utilisées dans le cours d'ouverture, étendues au système complet.
1.1. Jugements
Les types τ sont définis par la grammaire suivante :
τ ::= integer
| boolean
| []τ
Le jugement de typage Γ ⊢ e : τ pour une expression e signifie que, dans l'environnement de types Γ, l'expression e est bien typée, de type τ.
Le jugement de typage Γ ⊢ i pour une instruction i signifie que, dans l'environnement de types Γ, l'instruction i est bien typée. Cette forme peut également s'appliquer à un bloc b.
1.2. Règles
Le typage des expressions e est donné par les règles d'inférence suivantes :
--------------- ------------------ -------------------
Γ ⊢ n : integer Γ ⊢ true : boolean Γ ⊢ false : boolean
Γ(id) = τ Γ ⊢ e₁ : []τ Γ ⊢ e₂ : integer
---------- ----------------------------------
Γ ⊢ id : τ Γ ⊢ e₁[e₂] : τ
Γ ⊢ e₁ : integer Γ ⊢ e₂ : integer
-------------------------------------- ( op ∈ {+, -, *} )
Γ ⊢ e₁ op e₂ : integer
Γ ⊢ e₁ : integer Γ ⊢ e₂ : integer
-------------------------------------- ( op ∈ {<, <=, ==} )
Γ ⊢ e₁ op e₂ : boolean
Γ ⊢ e₁ : boolean Γ ⊢ e₂ : boolean
-------------------------------------- ( op ∈ {&&, ||} )
Γ ⊢ e₁ op e₂ : boolean
Γ ⊢ e₁ : τ₁ ... Γ ⊢ eₙ : τₙ Γ(f) = (τ₁, ..., τₙ) -> τ
--------------------------------------------------------------
Γ ⊢ f(e₁, ..., eₙ) : τ
Γ ⊢ e : integer
---------------
Γ ⊢ [e]τ : []τ
Le typage des instructions i et blocs b est donné par les règles d'inférence suivantes :
∀i∈b. (Γ ⊢ i)
-------------
Γ ⊢ b
Γ(id) = τ Γ ⊢ e : τ
--------------------------
Γ ⊢ id := e
Γ ⊢ e : boolean Γ ⊢ b
-------------------------
Γ ⊢ while (e) (b)
Γ ⊢ e : boolean Γ ⊢ b₁ Γ ⊢ b₂
-------------------------------------
Γ ⊢ if e then b₁ else b₂
Γ ⊢ e : integer
---------------
Γ ⊢ print(e)
Γ ⊢ e₁ : τ₁ ... Γ ⊢ eₙ : τₙ Γ(f) = (τ₁, ..., τₙ) -> ∅
--------------------------------------------------------------
Γ ⊢ f(e₁, ..., eₙ)
2. Travail attendu
Étendre le vérificateur de types du langage A6000 pour qu'il couvre l'ensemble des constructions données dans cette page, en suivant les règles de typage.
3. Extension : types définis par l'utilisateur
Vous pouvez étendre le langage A6000 en donnant à l'utilisateur la possibilité de définir lui-même de nouveaux types.
3.1. Types produit
Un type produit permet de définir une structure de données constituée de plusieurs champs éventuellement mutables, à la manière des record de Caml ou des struct de C.
Une telle structure peut être représentée en mémoire comme un tableau. On a une différence au niveau du typage, car chaque champ a un type prédéfini qui peut différer d'un champ à l'autre. Une autre différence apparaît au niveau de l'accès aux champs, les champs étant désignés par leur nom dans le langage de surface. C'est au compilateur de traduire ensuite ces noms en indices, par exemple lors de la phase d'effacement des types (plus vite cette traduction est faite, plus vite on peut se reposer sur les mécanismes déjà présents).
3.2. Types somme
Un type produit permet de définir une structure de données pouvant prendre plusieurs formes, comme les types inductifs de Caml, ou les types union de C.
Une telle structure peut être représentée en mémoire comme un tableau représentant les différents champs du constructeurs, avec un champ supplémentaire identifiant le constructeur lui-même. Le nombre et le type des champs varie en fonction du constructeur. L'accès se fait ensuite via des constructions match/with, traduites au niveau du code en des tests sur la valeur du champ identifiant le constructeur.