Programmation Fonctionnelle, projet

Version & licenses
Creative Commons License

Programmation Fonctionnelle, projet : un interprèteur fonctionnel

Guyslain Naves

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 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 :

  1. ocamlbuild read_and_write
  2. ./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 :

  1. expression :=
  2. | 'fun' variable '->' expression
  3. | 'let' variable ':=' expression 'in' expression
  4. | 'let' 'rec' variable ':=' expression 'in' expression
  5. | 'if' expression 'then' expression 'else' expression
  6. | '(' expression ')'
  7. | expression binary_operator expression
  8. | unary_operator expression
  9. | variable
  10. | literal

  12. literal := int | 'true' | 'false'
  13. int := '0' | '1' | ...

  15. variable := [a-z]+ (* sauf mot-clés *)

  17. binary_operator := (* par priorité croissante *)
  18. | '&&' | '||'
  19. | '=' | '<' | '>'
  20. | '+' | '-'
  21. | '*' | '/' | '%'

  23. 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 :

  1. type operator =
  2. | Plus | Minus | Prod | Div | Mod
  3. | Or | And | Equal | Greater | Less
  4. | Neg

  6. type literal =
  7. | Integer of int
  8. | Boolean of bool

  10. type variable = string

  12. type 'label term =
  13. | FixPoint of 'label t
  14. | Abstraction of variable * 'label t
  15. | Application of 'label t * 'label t
  16. | Conditional of 'label t * 'label t * 'label t
  17. | Variable of variable
  18. | Literal of literal
  19. | Operator of 'label t * operator * 'label t
  20. | Un_Operator of operator * 'label t

  22. and 'label t =
  23. { label : 'label;
  24. term : 'label term
  25. }

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.


  2. (** [build_binary_operator label left_hand_side operation right_hand_side] *)
  3. val build_binary_operator : 'label -> 'label t -> operator -> 'label t -> 'label t

  5. val build_unary_operator : 'label -> operator -> 'label t -> 'label t

  7. val build_literal_of_int : 'label -> int -> 'label t
  8. val build_literal_of_bool : 'label -> bool -> 'label t

  10. (** [build label variable_name] *)
  11. val build_variable : 'label -> string -> 'label t

  13. (** [build_application label funct_term argument_term] *)
  14. val build_application : 'label -> 'label t -> 'label t -> 'label t

  16. (** [build_abstraction label variable_name image_term *)
  17. val build_abstraction : 'label -> string -> 'label t -> 'label t

  19. (** [build_conditional label condition_term if_yes_term if_no_term] *)
  20. val build_conditional : 'label -> 'label t -> 'label t -> 'label t -> 'label t

  22. (** [build_fixpoint label term] *)
  23. 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é).

  1. 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 $\text{Fix}~e$, on utilise la règle suivante :

$$ \text{Fix}~e \longrightarrow e~(\text{Fix}~e)$$

Donc $\text{Fix}~e$ se réduit en l'application de $e$ à $\text{Fix}~e$.

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 $\text{Fix}$. La règle est la suivante :

  1. let rec f = expr_var in expr
  2. <==>
  3. (fun f -> expr) (Fix (fun f -> expr_var))

Rappelons à cette occasion le codage de la liaison (let) :

  1. let var = expr_var in expr
  2. <==>
  3. (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 $\text{Fix}$). 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 :

  1. type :=
  2. | bool
  3. | int
  4. | type -> type

On utilisera le type suivant pour coder nos types :

  1. type term_type =
  2. | Int
  3. | Bool
  4. | 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 :

  • Var 2 = Var 3 -> Var 1

En examinant le sous-terme fun y -> y + 2 avec y : Var 4 et y + 2 : Var 5, on obtient en plus :

  • Var 2 = Var 4 -> Var 5

Puis, en examinant y + 2, on a :

  • Var 4 = Int
  • Var 5 = Int
  • Int = Int (puisque le litéral 2 a le type Int).

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 :

  1. let rec fact := fun n ->
  2. if n = 0 then 1
  3. else n * fact (n-1)
  4. 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) :

  1. (fun fact -> fact 5)
  2. (let rec fact := (fun n -> if n = 0 then 1 else n * fact (n - 1)) in fact)
  3. Typed successfully :
  4. int
  5. Reductions:
  6. -->
  7. {fact} 5
  8. -->
  9. fact {fact} 5
  10. -->
  11. (fun n -> if n = 0 then 1 else n * {fact} (n - 1)) 5
  12. -->
  13. 5 * {fact} 4
  14. -->
  15. 5 * fact {fact} 4
  16. -->
  17. 5 * (fun n -> if n = 0 then 1 else n * {fact} (n - 1)) 4
  18. -->
  19. 5 * 4 * {fact} 3
  20. -->
  21. 5 * 4 * fact {fact} 3
  22. -->
  23. 5 * 4 * (fun n -> if n = 0 then 1 else n * {fact} (n - 1)) 3
  24. -->
  25. 5 * 4 * 3 * {fact} 2
  26. -->
  27. 5 * 4 * 3 * fact {fact} 2
  28. -->
  29. 5 * 4 * 3 * (fun n -> if n = 0 then 1 else n * {fact} (n - 1)) 2
  30. -->
  31. 5 * 4 * 3 * 2 * {fact} 1
  32. -->
  33. 5 * 4 * 3 * 2 * fact {fact} 1
  34. -->
  35. 5 * 4 * 3 * 2 * (fun n -> if n = 0 then 1 else n * {fact} (n - 1)) 1
  36. -->
  37. 5 * 4 * 3 * 2 * 1 * {fact} 0
  38. -->
  39. 5 * 4 * 3 * 2 * 1 * fact {fact} 0
  40. -->
  41. 5 * 4 * 3 * 2 * 1 * (fun n -> if n = 0 then 1 else n * {fact} (n - 1)) 0
  42. -->
  43. 120
  44. Irreducible term.

La suite de Fibonacci :

  1. let rec fib := fun n ->
  2. if n = 0 || n = 1 then 1
  3. else fib (n-1) + fib (n-2)
  4. in fib 4
  1. (fun fib -> fib 4)
  2. (let rec fib :=
  3. (fun n -> if n = 0 || n = 1 then 1 else fib (n - 1) + fib (n - 2)) in
  4. fib)
  5. Typed successfully :
  6. int
  7. Reductions:
  8. -->
  9. {fib} 4
  10. -->
  11. fib {fib} 4
  12. -->
  13. (fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 4
  14. -->
  15. {fib} 3 + {fib} 2
  16. -->
  17. fib {fib} 3 + {fib} 2
  18. -->
  19. (fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 3 +
  20. {fib} 2
  21. -->
  22. {fib} 2 + {fib} 1 + {fib} 2
  23. -->
  24. fib {fib} 2 + {fib} 1 + {fib} 2
  25. -->
  26. (fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 2 +
  27. {fib} 1 + {fib} 2
  28. -->
  29. {fib} 1 + {fib} 0 + {fib} 1 + {fib} 2
  30. -->
  31. fib {fib} 1 + {fib} 0 + {fib} 1 + {fib} 2
  32. -->
  33. (fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 1 +
  34. {fib} 0 + {fib} 1 + {fib} 2
  35. -->
  36. 1 + {fib} 0 + {fib} 1 + {fib} 2
  37. -->
  38. 1 + fib {fib} 0 + {fib} 1 + {fib} 2
  39. -->
  40. 1 + (fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 0
  41. + {fib} 1 + {fib} 2
  42. -->
  43. 2 + {fib} 1 + {fib} 2
  44. -->
  45. 2 + fib {fib} 1 + {fib} 2
  46. -->
  47. 2 + (fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 1
  48. + {fib} 2
  49. -->
  50. 3 + {fib} 2
  51. -->
  52. 3 + fib {fib} 2
  53. -->
  54. 3 + (fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 2
  55. -->
  56. 3 + {fib} 1 + {fib} 0
  57. -->
  58. 3 + fib {fib} 1 + {fib} 0
  59. -->
  60. 3 + (fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 1
  61. + {fib} 0
  62. -->
  63. 3 + 1 + {fib} 0
  64. -->
  65. 3 + 1 + fib {fib} 0
  66. -->
  67. 3 + 1 +
  68. (fun n -> if n = 0 || n = 1 then 1 else {fib} (n - 1) + {fib} (n - 2)) 0
  69. -->
  70. 5
  71. Irreducible term.

Une fonction plus complexe :

  1. let rec repeat := fun n -> fun f -> fun init ->
  2. if n = 0 then init
  3. else repeat (n-1) f (f init)
  4. in repeat
  1. (fun repeat -> repeat)
  2. (let rec repeat :=
  3. (fun n -> fun f -> fun init -> if n = 0 then init else repeat (
  4. n - 1) f (f init)) in repeat)
  5. Typed successfully :
  6. int -> ('a -> 'a) -> 'a -> 'a
  7. Reductions:
  8. -->
  9. {repeat}
  10. -->
  11. repeat {repeat}
  12. -->
  13. fun n -> fun f -> fun init -> if n = 0 then init else {repeat} (n - 1) f
  14. (f init)
  15. Irreducible term.