Library Expr
Compiling expressions
Section Expr.
We are going to use the standard library for lists.
Require Import Coq.Lists.List.
Set Implicit Arguments.
We define a simple language of expressions over natural numbers: only containing numeric constants and addition. This is already a useful abstraction over the one-dimensional view of a program as a sequence of symbols, i.e. we don't care about precedence or balanced bracktes.
However, this means that at some point we'd have to implement a parser and verify it.
Inductive Expr : Set :=
| Const : nat -> Expr
| Plus : Expr -> Expr -> Expr.
The expression "(3 + 5) + 2" is represented by the following tree:
Definition e1 : Expr := Plus (Plus (Const 3) (Const 5)) (Const 2).
We give a "denotational" semantics to our expressions by
recursively assigning a value (their denotation). This process is
called evaluation - hence the function is called eval. It is
defined by structural recursion over the structure of the
expression tree.
Fixpoint eval (e:Expr) {struct e} : nat :=
match e with
| Const n => n
| Plus e1 e2 => (eval e1) + (eval e2)
end.
Let's evaluate our example expression:
Eval compute in (eval e1).
We are going to describe how to calculate the value of an
expression on a simple stack machine - thus giving rise to an
"operational semantics".
First we specify the operation of our machine, there are only two operations :
First we specify the operation of our machine, there are only two operations :
Inductive Op : Set :=
| Push : nat -> Op
| PlusC : Op.
Definition Code := list Op.
Definition Stack := list nat.
We define recursively how to execute code wrt any given stack. This
function proceeds by linear recursion over the stack and could be
easily implemented as a "machine".
Fixpoint runAux (st:Stack)(p:Code) {struct p} : nat := match p with
| nil => match st with
| nil => 0
| n :: st' => n
end
| op :: p' =>
match op with
| Push n => runAux (n :: st) p'
| PlusC => match st with
| nil => 0
| n :: nil => 0
| n1 :: n2 :: st' =>
runAux ((n1 + n2) :: st') p'
end
end
end.
We run a piece of code by starting with the empty stack.
Definition run (p:Code) : nat := runAux nil p.
Definition c1 : Code
:= Push 2 :: Push 3 :: PlusC :: nil.
Eval compute in (run c1).
A simple compiler
We implement a simple compiler which translates an expression into
code for the stack machine.
A naive implementation looks like this:
A naive implementation looks like this:
Fixpoint compile_naive (e:Expr) {struct e} : list Op :=
match e with
| Const n => (Push n) :: nil
| Plus e1 e2 => (compile_naive e2)++
(compile_naive e1)++
(PlusC::nil)
Why do we need to do this in this order?
end.
A better alternative both in terms of efficiency and verification is a "continuation based" compiler. We compile an expression e wrt a continuation p, some code which is going to be run after it.
Fixpoint compileAux (e:Expr) (p:Code) {struct e} : Code := match e with
| Const n => Push n :: p
| Plus e1 e2 => compileAux e2
(compileAux e1 (PlusC :: p))
end.
The top level compiler just uses the empty continuation.
Definition compile (e:Expr) : Code := compileAux e nil.
Test the compiler
Eval compute in compile e1.
And run the compiled code:
Eval compute in run (compile e1).
Compiler correctness means that the operational semantics of the
compiled code agrees with its denotational semantics.
forall e:Expr, run (compile e) = eval e.
However, to prove this we have to show a more general lemma about the auxilliary functions.
forall e:Expr, run (compile e) = eval e.
However, to prove this we have to show a more general lemma about the auxilliary functions.
Lemma compileLem : forall (e:Expr)(p:Code)(st:Stack),
runAux st (compileAux e p) = runAux ((eval e)::st) p.
induction e.
intros p st.
simpl.
reflexivity.
simpl.
intros.
rewrite IHe2.
rewrite IHe1.
simpl.
reflexivity.
Qed.
The main theorem is a simple application of the previous lemma:
Theorem compileOk : forall e:Expr,
run (compile e) = eval e.
intro e.
unfold run.
unfold compile.
rewrite compileLem.
simpl.
reflexivity.
Qed.
End Expr.