(* ** 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 sum
*)
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? *)
(* Two useful lemmas. *)
Lemma append_nil : forall X:Set, forall l : list X,
l = l ++ nil.
Proof.
intros X l.
induction l.
simpl. reflexivity.
simpl. rewrite <- IHl. reflexivity.
Qed.
Lemma append_assoc : forall X:Set, forall l1 l2 l3 : list X,
(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
intros X l1 l2 l3.
induction l1.
simpl. reflexivity.
simpl. rewrite -> IHl1. reflexivity.
Qed.
Lemma compile_correct':
forall e p s, run (compile e ++ p) s = run p (meaning e :: s).
Proof.
intros e.
(* we do not [intros p s] because we want [p] and [s] to be
universally quantified in the induction hypothesis *)
induction e.
(* Case e = Const n *)
intros p s. simpl. reflexivity.
(* Case e = Plus e1 e2 *)
intros p s.
simpl.
(* We cannot apply directly IHe1 because the program we are
executing is of the form [ (compile e2 ++ p1) ++ p2 ] and not of
the form [ compile e2 ++ (p1 ++ p2) ]. However we proved above
that list concatenation is associative in the [append_assoc]
lemma. We can then rewrite the first in the latter.
*)
rewrite append_assoc.
(* Now we can apply the induction hypothesis IHe2. *)
rewrite IHe2.
(* Similarly, we can apply the induction hypothesis IHe1. *)
rewrite append_assoc.
rewrite IHe1.
(* And we can conclude by simplification. *)
simpl.
reflexivity.
(* Case e = Mult e1 e2
This case is similar to the Plus e1 e2 case. *)
intros.
simpl.
rewrite append_assoc.
rewrite IHe2.
rewrite append_assoc.
rewrite IHe1.
simpl.
reflexivity.
Qed.
(* 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.
intros.
(* The lemma we proved above requires the program being executed to
be of the form [compile e ++ p] for an arbitrary program [p],
while the program in our goal is just [compile e]. But we proved
above that [l = l ++ nil] for any list [l].
However we cannot just [rewrite append_nil] because the goal
contains too many lists and Coq cannot determine which one we
want to rewrite. So we specialize the [append_nil] lemma to
[compile e = compile e ++ nil] before rewriting. The underscore
stands for the type [instr], which is inferred by Coq.
*)
Check append_nil.
Check (append_nil _ (compile e)).
rewrite (append_nil _ (compile e)).
rewrite compile_correct'.
simpl.
reflexivity.
Qed.
(** * 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! *)