(* Copyright (c) 2011, Thorsten Altenkirch *)
(** %\chapter{%## #Compiling expressions%}%#

# *)
Section Expr.
(** We are going to use the standard library for lists. *)
Require Import Coq.Lists.List.
Set Implicit Arguments.
(** * Evaluating expressions. *)
(**
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).
(** * A stack machine *)
(**
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 :
*)
Inductive Op : Set :=
| Push : nat -> Op
(* pushes a constant on the stack *)
| PlusC : Op.
(* addition, repalces the top two elements of the stack by their
sum. *)
(* Machine code is a list of operations: *)
Definition Code := list Op.
(* A stack is a list of natural numbers: *)
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:
*)
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 *)
(**
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.
*)
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.