Les 3 dernières séances de TP, chacune durant 4h, consisteront en l'écriture d'un petit langage fonctionnel avec son parseur et son interprèteur. Le projet comporte plusieurs parties :
le module de combinateurs de parseurs (entrevu au
TP 8),
la manipulation formelles des expressions du langage (substitutions),
le typage des expressions,
le parseur d'expressions.
Les deux premiers points sont prioritaires. Le typage et le parseur sont à faire selon le temps dont vous disposez.
Le projet comptera pour 6 points dans la note finale. Il est à faire en binôme et devra être remis sous Ametice, accompagné d'un petit rapport décrivant ce que vous avez eu le temps ou pas de faire. La date limite de rendu est fixée au 11 avril.
Vous sont fournis :
une
interface pour le module de combinateur de parsing
Parse,
un
petit programme qui lit un fichier de code (donné en premier argument), le parse, et le réécrit (différement) en sortie standard.
Une fois codés les modules Term et Parse, vous pourrez compiler le programme read_and_write et l'exécuter, en tapant dans un terminal :
ocamlbuild read_and_write
./read_and_write fichier_source
avec fichier_source un fichier que vous créerez contenant du code source tel que décrit ci-dessous.
Description du langage
La grammaire du langage est donnée par :
expression :=
| 'fun' variable '->' expression
| 'let' variable ':=' expression 'in' expression
| 'let' 'rec' variable ':=' expression 'in' expression
| 'if' expression 'then' expression 'else' expression
| '(' expression ')'
| expression binary_operator expression
| unary_operator expression
| variable
| literal
literal := int | 'true' | 'false'
int := '0' | '1' | ...
variable := [a-z]+
binary_operator :=
| '&&' | '||'
| '=' | '<' | '>'
| '+' | '-'
| '*' | '/' | '%'
unary_operator := '-' | '!'
La sémantique est celle qu'on peut attendre des constructions utilisées.
Termes
Les termes du langage seront encodées en utilisant les types suivants :
type operator =
| Plus | Minus | Prod | Div | Mod
| Or | And | Equal | Greater | Less
| Neg
type literal =
| Integer of int
| Boolean of bool
type variable = string
type 'label term =
| FixPoint of 'label t
| Abstraction of variable * 'label t
| Application of 'label t * 'label t
| Conditional of 'label t * 'label t * 'label t
| Variable of variable
| Literal of literal
| Operator of 'label t * operator * 'label t
| Un_Operator of operator * 'label t
and 'label t =
{ label : 'label;
term : 'label term
}
On commence donc par déclarer des types pour les opérateurs, les litéraux et les variables. Ensuite, un terme se construit selon différentes règles (point fixe, abstraction, … ), formant un arbre. En chaque nœud, on place un label d'un type paramètré. Cela servira par exemple pour y indiquer des informations pendant les phases de parsing ou de typage.
Ces déclarations devront figurer dans un fichier term.ml et dans son interface (le type term ne sera pas masqué).
Le fichier term.mli (dont une partie est donnée plus haut) devra aussi contenir des constructeurs de termes. Chacun prend en premier argument le label qui sera placé en racine du terme construit.
val build_binary_operator : 'label -> 'label t -> operator -> 'label t -> 'label t
val build_unary_operator : 'label -> operator -> 'label t -> 'label t
val build_literal_of_int : 'label -> int -> 'label t
val build_literal_of_bool : 'label -> bool -> 'label t
val build_variable : 'label -> string -> 'label t
val build_application : 'label -> 'label t -> 'label t -> 'label t
val build_abstraction : 'label -> string -> 'label t -> 'label t
val build_conditional : 'label -> 'label t -> 'label t -> 'label t -> 'label t
val build_fixpoint : 'label -> 'label t -> 'label t
Le module Term pourra aussi contenir des prédicats ou des fonctions sur les opérateurs, au besoin.
Enfin vous donnerez une fonction pour écrire un terme sous la forme d'une chaîne de caractères. Vous essayerez autant que possible d'avoir une sortie lisible (lignes courtes, code indenté).
val lines_of_term : ?line_length:int -> ?verbose_flag:bool -> string option t -> string list -> string list
Cette fonction utilise des arguments optionnels. De plus, si un terme a pour label une chaine de caractères, et que le flag verbose_flag est à false, plutôt qu'écrire la chaîne correspondant à l'encodage du terme, on écrira seulement son label (voir les exemples en bas de page).
Évaluation des termes
L'évaluation des termes sera géré par un module qui formera un fichier eval.ml.
Comme appris pendant le cours 2 , l'évaluation des termes se fait par substitution. Ceci fonctionne pour les application dont le membre gauche est directement une abstraction.
Il faut rajouter d'autres règles pour les autres constructions : conditionnelles, opérateurs, points fixes.
Évaluation des opérateurs
Si les deux fils d'un opérateur binaire sont des litéraux, on le simplifie selon les règles pour en faire à son tour un litéral.
On procède de même pour les opérateurs unaires.
Évaluation des conditionnelles
Si la condition d'une conditionnelle est un litéral booléen, on la simplifie en gardant seulement son deuxième membre (s'il le litéral est true) ou son troisième membre (s'il est false).
On propose d'écrire une fonction prenant un terme, et calculant une simplification de ce terme telle que plus aucune simplification ne soit possible. Cette fonction sera appelée systématiquement sur le résultat d'un terme.
Point fixe
La règle de point fixe nous permettra de coder des fonctions récursives. Pour simplifier un terme de point fixe, notons-le , on utilise la règle suivante :
Donc se réduit en l'application de à .
Pour ne pas avoir de boucle infini lors de l'évaluation, il faudra évaluer les points fixes de façon paresseuse obligatoirement.
Une subtilité consiste à comprendre comment encoder le let
rec à l'aide de . La règle est la suivante :
let rec f = expr_var in expr
<==>
(fun f -> expr) (Fix (fun f -> expr_var))
Rappelons à cette occasion le codage de la liaison (let) :
let var = expr_var in expr
<==>
(fun var -> expr) expr_var
Consignes
La première étape est d'écrire une fonctin réalisant la substitution d'une variable par un terme, dans un terme.
Ensuite, il faudra écrire une fonction effectuant une seule réduction (ou une seule application de la règle de
). Afin de ne pas avoir de problème avec le nommage des variables, l'application qu'on choisit de réduire ne doit pas avoir pour ancêtre un nœud abstraction. Vous évaluerez avec une stratégie stricte : on évalue d'abord les deux membres de l'application avant de faire la réduction (avec comme exception le cas du point fixe).
Une fois écrit une fonction effectuant une étape de calcul, on la répète jusqu'à ne plus trouver de réduction.
Typages
Pour le typage des termes, nous procédons par étape.
On commence par attribuer à chaque nœud du terme une variable de type distincte.
Ensuite, pour chaque nœud, on exprime les contraintes de typage entre les variables de type de ce nœud et de ses fils. Ceci nous donne une liste de contraintes.
On résout les contraintes en utilisant l'algorithme d'unification.
Le contenu de cette section formera un fichier typing.ml, dont un prototype vous est fourni, contenant l'algorithme d'unification.
La grammaire des types de notre langage est très simple :
type :=
| bool
| int
| type -> type
On utilisera le type suivant pour coder nos types :
type term_type =
| Int
| Bool
| Arrow of term_type * term_type
Description de l'algorithme
On associe à chaque sous-terme un type de la forme Var i, avec des valeurs de i distinctes, et on forme la liste de tous les sous-termes. Si deux variables portant le même nom sont liées à la même abstraction, elle doivent avoir une même valeur pour i. Par contre deux variables portant le même nom, mais non-liées à la même abstraction doivent être distinctes. Pour cela, on peut par exemple commencer par renommer les abstractions avec des identifiants distincts.
Ensuite, une fois calculée la liste des sous-termes, on déduit des contraintes de type pour chaque terme. Une contrainte prend la forme d'une paire de types devant être identifiés. Par exemple, pour le sous-terme (fun y -> y + 2) x : Var 1, avec (fun y -> y + 2) : Var 2 et x : Var 3, on obtient la contrainte :
En examinant le sous-terme fun y -> y + 2 avec y : Var 4 et y + 2 : Var 5, on obtient en plus :
Puis, en examinant y + 2, on a :
Sur cette liste de contraintes que nous obtenons, on lance l'algorithme d'unification. S'il réussit, il suffira de chercher la substitution correspond à la variable de type du terme complet pour obtenir son type.
Parsing
Les plus avancés pourront tenter de coder eux-même un parseur. Un parseur est fourni, mais vous devez coder le module Parse pour pouvoir l'utiliser.
Exemples d'un résultat final
Voici quelques exemples :
let rec fact := fun n ->
if n = 0 then 1
else n * fact (n-1)
in fact 5
Avec un peu de travail on peut afficher chaque étape du calcul pour obtenir ceci (les accolades dénotant le point fixe d'une fonction) :
(fun fact -> fact 5)
(let rec fact := (fun n -> if n = 0 then 1 else n * fact (n - 1)) in fact)
Typed successfully :
int
Reductions:
-->
{fact} 5
-->
fact {fact} 5
-->
(fun n -> if n = 0 then 1 else n * {fact} (n - 1)) 5
-->
5 * {fact} 4
-->
5 * fact {fact} 4
-->
5 * (fun n -> if n = 0 then 1 else n * {fact} (n - 1)) 4
-->
5 * 4 * {fact} 3
-->
5 * 4 * fact {fact} 3
-->
5 * 4 * (fun n -> if n = 0 then 1 else n * {fact} (n - 1)) 3
-->
5 * 4 * 3 * {fact} 2
-->
5 * 4 * 3 * fact {fact} 2
-->
5 * 4 * 3 * (fun n -> if n = 0 then 1 else n * {fact} (n - 1)) 2
-->
5 * 4 * 3 * 2 * {fact} 1
-->
5 * 4 * 3 * 2 * fact {fact} 1
-->
5 * 4 * 3 * 2 * (fun n -> if n = 0 then 1 else n * {fact} (n - 1)) 1
-->
5 * 4 * 3 * 2 * 1 * {fact} 0
-->
5 * 4 * 3 * 2 * 1 * fact {fact} 0
-->
5 * 4 * 3 * 2 * 1 * (fun n -> if n = 0 then 1 else n * {fact} (n - 1)) 0
-->
120
Irreducible term.
La suite de Fibonacci :
let rec fib := fun n ->
if n = 0 || n = 1 then 1
else fib (n-1) + fib (n-2)
in fib 4
(fun fib -> fib 4)
(let rec fib :=
(fun n -> if n = 0 || n = 1 then 1 else fib (n - 1) + fib (n - 2)) in
fib)
Typed successfully :
int
Reductions:
-->
{fib} 4
-->
fib {fib} 4
-->
(fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 4
-->
{fib} 3 + {fib} 2
-->
fib {fib} 3 + {fib} 2
-->
(fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 3 +
{fib} 2
-->
{fib} 2 + {fib} 1 + {fib} 2
-->
fib {fib} 2 + {fib} 1 + {fib} 2
-->
(fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 2 +
{fib} 1 + {fib} 2
-->
{fib} 1 + {fib} 0 + {fib} 1 + {fib} 2
-->
fib {fib} 1 + {fib} 0 + {fib} 1 + {fib} 2
-->
(fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 1 +
{fib} 0 + {fib} 1 + {fib} 2
-->
1 + {fib} 0 + {fib} 1 + {fib} 2
-->
1 + fib {fib} 0 + {fib} 1 + {fib} 2
-->
1 + (fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 0
+ {fib} 1 + {fib} 2
-->
2 + {fib} 1 + {fib} 2
-->
2 + fib {fib} 1 + {fib} 2
-->
2 + (fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 1
+ {fib} 2
-->
3 + {fib} 2
-->
3 + fib {fib} 2
-->
3 + (fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 2
-->
3 + {fib} 1 + {fib} 0
-->
3 + fib {fib} 1 + {fib} 0
-->
3 + (fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 1
+ {fib} 0
-->
3 + 1 + {fib} 0
-->
3 + 1 + fib {fib} 0
-->
3 + 1 +
(fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 0
-->
5
Irreducible term.
Une fonction plus complexe :
let rec repeat := fun n -> fun f -> fun init ->
if n = 0 then init
else repeat (n-1) f (f init)
in repeat
(fun repeat -> repeat)
(let rec repeat :=
(fun n -> fun f -> fun init -> if n = 0 then init else repeat (
n - 1) f (f init)) in repeat)
Typed successfully :
int -> ('a -> 'a) -> 'a -> 'a
Reductions:
-->
{repeat}
-->
repeat {repeat}
-->
fun n -> fun f -> fun init -> if n = 0 then init else {repeat} (n - 1) f
(f init)
Irreducible term.
