(* ** In this exercise we will implement a "certified compiler" of a
simple arithmetic language onto a stack machine.
The purpose of this exercise is to show that you can go a long way
along using only some simple features of Coq.
*)
(** * Arithmetic Expressions Over Natural Numbers *)
(** * The source language *)
(** An expression is either a natural number or the application of a
binary operator, and is defined by the BNF below. The only
binary operators we consider are addition and multiplication.
*)
Inductive exp : Set :=
| Const : nat -> exp
| Plus : exp -> exp -> exp
| Mult : exp -> exp -> exp.
(* Examples of valid expressions are
- 42
- plus 2 2
- mult (plus 2 2) 3
We can use the keyword [Check] to ask Coq to verify that a term is
well-formed.
*)
Check (Const 42).
Check (Plus (Const 2) (Const 2)).
Check (Mult (Plus (Const 2) (Const 2)) (Const 3)).
(** What does an expression mean? Intuitively:
- the expression "42" denotes the natural number 42
- the expression "plus 2 2" denotes the natural number 4
- the expression "mult (plus 2 2) 3" denotes the natural number 12
We write an interpreter that can be thought of as a trivial
denotational semantics. If the term "denotational semantics" sounds
unfriendly to you, no need to worry: we will stick to "common sense"
constructions.
*)
Fixpoint meaning (e:exp) : nat :=
match e with
| Const n => n
| Plus e1 e2 => (meaning e1) + (meaning e2)
| Mult e1 e2 => (meaning e1) * (meaning e2)
end.
(* Examples *)
Eval simpl in meaning (Const 42).
Eval simpl in meaning (Plus (Const 2) (Const 2)).
Eval simpl in meaning (Mult (Plus (Const 2) (Const 7)) (Const 3)). (* (2+7)*3 *)
Eval simpl in meaning (Mult (Const 3) (Plus (Const 2) (Const 7))). (* 3*(2+7) *)
(** * The target machine *)
(** We will compile our source expressions onto a a simple stack
machine (do you remember HP calculators?). The machine is
composed by
- the stack: a stack of natural numbers
- the program: a list of instructions
where an instruction is either
- IConst nat : put nat on top of the stack
- IPlus : pops two values from the stack and pushes their sum
- IMult : pops two values from the stack and pushes their product
*)
Inductive instr : Set :=
| IConst : nat -> instr
| IPlus : instr
| IMult : instr.
Require Import List.
Definition prog := list instr.
Definition stack := list nat.
(* Given an instruction and a stack, the [execute_instr] executes the
instruction and returns the modified stack.
*)
Definition execute_instr (i : instr) (s : stack) : stack :=
match i with
| IConst n => (n :: s)
| IPlus =>
match s with
| arg1 :: arg2 :: s' => (arg1 + arg2 :: s')
| _ => nil
end
| IMult =>
match s with
| arg1 :: arg2 :: s' => (arg1 * arg2 :: s')
| _ => nil
end
end.
(* The function [run] iterates application of [execute_instr] through
a whole program.
*)
Fixpoint run (p : prog) (s : stack) {struct p} : stack :=
match p with
| nil => s
| i :: p' => run p' (execute_instr i s)
end.
(** * Translation *)
(** The compiler takes an expression and generate code that puts
the value of the expression on the top of the stack. So:
- a constant expression [Const n] is translated into the
instruction that puts n on top of the stack [IConst n]
- an expression [Plus e1 e2] should generate code that sums the
values of the expressions e1 and e2. So we build a program that
when executed:
1- evaluates e2 and pushes the value of e2 onto the stack;
this code can be generated by recursively calling "compile"
on e2
2- evaluates e1 and pushes the value of e1 onto the stack;
this code can be generated by recursively calling "compile"
on e1
3- call IPlus to sum the two values on the top of the stack
- similarly for [Mult e1 e2].
*)
Fixpoint compile (e : exp) : prog :=
match e with
| Const n => IConst n :: nil
| Plus e1 e2 => compile e2 ++ compile e1 ++ IPlus :: nil
| Mult e1 e2 => compile e2 ++ compile e1 ++ IMult :: nil
end.
(** Before we set about proving that this compiler is correct, we can
try a few test runs, using our sample programs from earlier. *)
Eval simpl in compile (Const 42).
Eval simpl in compile (Plus (Const 2) (Const 2)).
Eval simpl in compile (Mult (Plus (Const 2) (Const 7)) (Const 3)).
Eval simpl in compile (Mult (Const 3) (Plus (Const 2) (Const 7))).
(* Observe that compiling (2+7)*3 and 3*(2+7) resulted in quite
different programs. Do we really trust our compiler? *)
(** Can you prove the theorem below? *)
Theorem compile_correct_firsttry:
forall e, run (compile e) nil = meaning e :: nil.
Proof.
Admitted.
(* Maybe you attempted
intros e. induction e. simpl; reflexivity. simpl.
and it was very unclear how to go on from there. The problem is that
the induction hypothesis IHe1 and IHe2 suppose that:
- the programs obtained by compiling e1 and e2 are executed starting
from an empty stack;
- the programs only contain the instructions of the compilation of
e1 or e2.
These induction hypothesis are too weak to help us.
Maybe you can prove a stronger theorem... can you?
*)
Lemma compile_correct':
forall e p s, run (compile e ++ p) s = run p (meaning e :: s).
Proof.
Admitted.
(* We can finally prove the compiler correctness theorem!
Yes, we can... fill in the proof below.
*)
Theorem compile_correct:
forall e, run (compile e) nil = meaning e :: nil.
Proof.
Admitted.
(** * We can now extract OCaml code that implements our stack machine *)
Recursive Extraction run.
(* and we can extract our certified compiler. *)
Recursive Extraction compile.
(** * WOW! *)
(* Can you extend the source language of our compiler to include
subtraction (denoted [-] in Coq)?
- Redefine the source grammar [exp] and the [meaning] function.
- Extend the stack machine with the new [Isub] instruction.
- Extend appropriately the compiler. Be careful: subtraction
is not commutative, and the order in which you place the
operands on the stack is important!
- Prove the correctness of the extended compiler.
*)