Considérons le langage IMP vu en cours. On rappelle que sa syntaxe est constituée des

• expressions arithmétiques:
  a  : :=  n  |  x  |  a + a′  |  a − a′  |  a × a′
  
• expressions booléennes:
  b  : :=  true  |  false  |  a < a′  |  not b
  
• commandes:
  b  : :=  skip  |  x := a  |  c ; c′  |  if b then c else c′  |  while b do c
  

1 Évaluation du langage

1. On définit la notation suivante pour le type des variables :

   type var = string

   Définir chacune des catégories syntaxiques ci-dessus par des types inductifs nommés aexp, bexp et cexp.

2. On définit le type state des états (qui consistent en la valeur courante des variables) par

   type state = var -> int

   Définir l’état initial state0 (où toutes les variables ont la valeur 0) ainsi qu’une fonction state_set de type state -> var -> int -> state qui modifie la valeur d’une variable dans un état.

3. Définir des fonctions aeval, beval et eval qui donnent le résultat de l’évaluation de chacune des catégories syntaxiques dans un état donné.

2 Exemples de programmes

1. Programmez la fonction factorielle et vérifiez que l’on a bien 5! = 120 :

   let () =
     let s = state_set state0 "x" 5 in
     let s = eval s fact in
     assert (s "y" = 120)

2. Programmez une fonction qui, étant donnés deux entiers a et b, calcule le quotient et le reste de la division euclidienne de a par b (vous devriez arriver à reconstituer cet algorithme sans cours ou internet). Vérifiez que pour a = 279 et b = 15 le quotient est 18 et le reste est 9.

3. Programmez l’algorithme d’Euclide permettant de calculer le plus grand diviseur commun de deux entiers a et b (vous pourrez ajouter l’égalité d’entiers comme primitive au langage si nécessaire). Vérifier que le pgcd de 1071 et 462 est 21.

3 Réduction

Nous allons maintenant implémenter la sémantique à petits pas. La réduction d’une expression n’étant pas toujours définie, nous utiliserons des types option dans les valeurs de retour : None signifiera que la réduction n’est pas définie.

1. Définir une fonction ared de type state -> aexpr -> aexpr option qui calcule un pas de réduction d’une expression arithmétique.
2. Définir une fonction bred de type state -> bexpr -> bexpr option qui calcule un pas de réduction d’une expression booléenne.
3. Définir une fonction red de type state -> cexpr -> (state * cexpr) option qui calcule un pas de réduction d’une commande.
4. Définir à nouveau, en utilisant red, la fonction eval de type state -> cexpr -> state qui évalue une commande. Vérifier qu’elle fonctionne en testant à nouveau la factorielle (et les autres exemples de la section précédente).