Commit ee3a734b authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

td6

parent 8f97eb66
TD6 : Manipulation d'expressions, extraction
============================================
**M2 LMFI**
On considère le type suivant des expressions arithmétiques `expr` défini en Coq par:
```coq
Inductive expr :
| Num : nat -> expr (* Constante numérique: n *)
| Plus : expr -> expr -> expr (* Expression somme: e1 + e2 *)
| Mult : expr -> expr -> expr. (* Expression produit: e1 * e2 *)
```
#### Exercice 1 : Evaluation directe
Définir en Coq une fonction récursive `eval : expr -> nat` calculant la valeur d'une expression.
#### Exercice 2 : Machine à pile
On considère un langage à pile (dans le style de Forth/PostScript) basé sur le jeu d'instructions suivant:
- `PUSH(n)` : Place l'entier `n` au sommet de la pile
- `ADD` : Retire les deux premiers entiers au sommet de la pile, les additionne, et place le résultat de l'addition au sommet de la pile
- `MUL` : Idem pour la multiplication
Définir en Coq:
1. un type inductif `inst` permettant de représenter ce jeu d'instructions.
2. un type `prog` représentant un *programme*, c'est-à-dire une suite finie d'instructions.
3. un type `stack` représentant une pile de notre machine, à savoir une séquence finie d'entiers facilement manipulable d'un côté.
#### Exercice 3 : Exécution
Écrire en Coq une fonction `exec_inst : inst -> stack -> stack` qui prend en argument une instruction, une pile, et retourne la nouvelle pile résultant de l'exécution de l'instruction sur la pile d'origine. Quel choix d'implémentation faites-vous pour traiter le cas où la pile de départ ne comporte pas assez d'éléments pour que l'instruction puisse s'exécuter correctement ?
Écrire en Coq une fonction `exec_prog : prog -> stack -> stack` qui effectue le même travail que la fonction précédente, mais cette fois-ci avec un programme plutôt qu'avec une instruction.
#### Exercice 4 : Compilation
Proposez une fonction `compile : expr -> prog` permettant de *compiler* une expression arithmétique en un programme de la machine à pile précédente.
A l'aide des fonctions `eval` et `exec_prog`, donner un invariant satisfait par cette fonction `compile`, et tester cet invariant sur quelques exemples d'expressions. Optionnel: on pourra essayer d'exprimer cet invariant indépendemment de la pile initiale de notre machine. NB: un tel invariant généralisé est en fait indispensable si on souhaite le *prouver* ensuite (par récurrence).
#### Exercice 5 : Extraction et programme autonome
Sur les versions récentes de Coq, commencer par charger l'extraction: `Require Extraction`.
Utiliser l'extraction pour obtenir une version OCaml de tous les types et fonctions précédents.
Exécuter ensuite le code obtenu:
- Tout d'abord dans un *toplevel* OCaml
- Ensuite en fabriquant un programme autonome (cf. `ocamlopt`), du style:
```sh
~# ./coqcalc
expr? 1+2*(3+4)
value: 15
```
Quel code OCaml faut-il ajouter pour pouvoir interagir avec le code issu de Coq ? En particulier, utiliser `ocamllex` et `menhir` (qui succède à `ocamlyacc`) pour réaliser un lecteur d'expressions arithmétiques (*parseur* en bon franglais). Voir par exemple [ce cours](http://www.dicosmo.org/CourseNotes/Compilation/9900/Cours06/) pour plus de détails.
Note: pour utiliser `menhir` sur les machines de la 2004, taper ceci dans votre terminal avant de compiler:
```sh
export PATH=~pletouze/bin:$PATH
```
#### Optionel : analyse syntaxique en Coq
Coq fournit un type `string` (après `Require Import Ascii String`). Il n'est donc pas impossible de réaliser directement en Coq un analyseur syntaxique `parse: string -> option expr`, tel que `parse "1+2*(3+4)"` donne `Some (Plus (Num 1) (Mult (Num 2) (Plus (Num 3) (Num 4)))))`.
Au fait, comment peut-on spécifier une telle fonction `parse` ?
Obtenir de nouveau une petite calculatrice par extraction. Attention lors de l'extraction à faire le pont entre les `string` OCaml et les `string` Coq.
Autre piste possible: pour la partie analyseur grammatical, les dernières version de `menhir` semblent pouvoir directement produire du code Coq...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment