Définir un type typ
des types en mini-ML.
Définir un type prog
des programmes mini-ML avec
annotations de type (en particulier, les arguments des fonctions
sont typés).
Définir une fonction infer
de type
string * typ) list -> prog -> typ (
qui prend un environnement de typage et un programme et infère le
type du programme. Dans le cas où le programme n’est pas typable, on
lèvera une exception Not_typable
préalablement déclarée. Il
pourra être utile d’utiliser la fonction List.assoc
pour trouver le type d’une variable dans un environnement.
Définir (en utilisant infer
) une fonction
check
de type
bool prog -> typ ->
qui détermine si un programme admet un type donné. L’utiliser pour vérifier que
(3 + 2, true)
a le type int * bool
(fun (x : int) → x + 1) 2
a le type
int
Définir une fonction typable
de type
prog -> bool
qui détermine si un terme est typable.
L’utiliser pour vérifier que les fonctions suivantes ne sont pas
typables :
(fun (x : int) → x) true
true 5
fst 3
(fun (x : int) → y)
(fun (f : int → int) → f false)
Définir une fonction fresh
de type
unit -> string
qui renvoie un nouveau nom de variable à
chaque appel : "x0"
, puis "x1"
, puis
"x2"
, etc. On considérera que ces noms sont frais
dans la suite, c’est-à-dire qu’ils n’apparaissent pas dans les
programmes considérés.
Définir une fonction sub
de type
string -> prog -> prog prog ->
telle que sub t x u
renvoie t
dans lequel
toutes les occurrences libres de x
ont été remplacées par
u
(c’est-à-dire t[x↦u]
). Vérifier que
le résultat de
(x , y)[x ↦ 5]
est
(5 , y)
le résultat de
(fun (x : int) → x)[x ↦ 5]
est
(fun (x : int) → x)
(à α-conversion près)
le résultat de
(fun (x : int) → x + y)[y ↦ x + 1]
n’est pas
(fun (x : int) → x + (x + 1))
Définir une fonction eval
de type
prog -> prog
qui évalue un programme en une valeur. On
lèvera une exception Cannot_evaluate
lorsque l’on ne peut
pas évaluer le programme. Vérifier que
(fun (x : int) → x + x) 5
s’évalue en 10
.
On cherche à étendre le langage afin d’implémenter la fonction factorielle. À titre d’exercice, nous allons d’abord l’implémenter en OCaml.
Définir un opérateur de point fixe par
let rec fix f x = f (fix f) x
Définir la fonction factorielle de façon récursive. Vérifier que 5! = 120.
Modifier votre implémentation de la factorielle de sorte à ne pas
utiliser rec
(mais vous pouvez utiliser fix
).
Vérifier que 5! = 120.
On cherche maintenant à étendre notre mini-ML de sorte à pouvoir y réaliser une définition similaire.
Ajouter au langage des opérations de
Ajouter un opérateur de point fixe.
Implémenter la fonction factorielle et vérifier que 5! = 120.
Implémenter la division euclidienne (qui calcule le quotient et le reste d’une division). Vérifier que pour a = 279 et b = 15 le quotient est 18 et le reste est 9.
Implémenter l’algorithme d’Euclide qui calcule le pgcd de deux entiers. Vérifier que le pgcd de 1071 et 462 est 21.
L’opération de substitution est assez coûteuse en pratique. Plutôt que d’effectuer les substitutions lors d’une application, il est plus efficace de propager un environnement d’évaluation qui est une liste de paires (xi, vi) constituées d’une variable et d’une valeur indiquant que au moment où on utilisera la variable xi, il faudra la remplacer par sa valeur vi.
Réimplémenter la fonction d’évaluation eval
de
type
string * prog) list -> prog -> prog (
sans utiliser la substitution, le premier argument étant l’environnement d’évaluation. Vérifier que
(fun (x : int) → x + x) 5
s’évalue en 10
.