Commit 5ebbe6f2 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

TD6 : english version

parent f32a3339
TD6 : arithmetical expressions, extraction
**M2 LMFI**
We consider here an inductive type `expr` of arithmetical expressions defined in Coq via :
Inductive expr :=
| Num : nat -> expr (* Numerical constant: n *)
| Plus : expr -> expr -> expr (* Sum expression: e1 + e2 *)
| Mult : expr -> expr -> expr. (* Product expression: e1 * e2 *)
#### Exercise 1 : direct evaluation
Define in Coq a recursive function `eval : expr -> nat` that computes the value of an expression.
#### Exercise 2 : stack machine
We consider a stack language (in the style of Forth/PostScript) based on the following instruction set:
- `PUSH(n)` : Place the number `n` on top of the stack
- `ADD` : Remove the first two numbers from the top of the stack and add them and put the result on top of the stack
- `MUL` : Same for multiplication
Define in Coq:
1. an inductive type `inst` allowing to represent this instruction set.
2. a type `prog` representing a *program*, i.e. a finite sequence of instructions.
3. a type `stack` representing a stack of our machine, i.e. a finite sequence of numbers with easy access on one side (called the "top" of the stack).
#### Exercise 3 : Execution
Write in Coq a function `exec_inst : inst -> stack -> stack` which takes as arguments an instruction and a stack and returns a new stack obtained by executing the instruction on the initial stack. How could you handle the situation of an initial stack without enough elements to execute correctly a `ADD` or `MUL` instruction ?
Write in Coq a fonction `exec_prog : prog -> stack -> stack` similar to the previous function, but this time works with a program instead of just a single instruction.
#### Exercise 4 : Compilation
Propose a fonction `compile : expr -> prog` allowing to *compile* an arithmetical expression into a program for our stack machine.
Thanks to `eval` and `exec_prog`, give an invariant satisfied by this `compile` function, and test this invariant on some examples of expressions. Optionnal: try to express this invariant independently from the initial stack of the machine. Note that this generalized invariant is actually mandatory if we try later to *prove* it (by induction).
#### Exercise 5 : Extraction and standalone program
Start by loading the extraction tool : `Require Extraction` (might be unnecessary on old versions of Coq).
Use the extraction to obtain an OCaml version of all the previous types and functions.
Execute this OCaml code:
- First in an OCaml *toplevel* (such as `ocaml` or online on [](
- Then by building a standalone program executable on your computer (cf. `ocamlopt`), something like:
~# ./coqcalc
expr? 1+2*(3+4)
value: 15
What OCaml code should we write to be able to interact with the extracted code from Coq ? In particular, you can use `ocamllex` and `menhir` (a modern derivative of `ocamlyacc`) to realize a reader of arithmetical exressions (a.k.a. *parser*). See [this example]( or [this course]( for more details.
#### Optionnal : parsing in Coq
Coq provides a type `string` (after `Require Import Ascii String`). It is hence not impossible to realize directly in Coq a parser of arithmetical expressions `parse: string -> option expr`, such that `parse "1+2*(3+4)"` gives `Some (Plus (Num 1) (Mult (Num 2) (Plus (Num 3) (Num 4)))))`.
By the way, how could we specify such a `parse` function ?
Through this Coq `parse` function, obtain again a little standalone calculator by extraction. Beware, after extraction, you will have to convert between the types `string` of OCaml and Coq.
Another possible approach : the recent versions of `menhir` can produce directly a grammatical analyzer in 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