Module demo

Compilation of arithmetic expressions to stack machine code


Require Import List ZArith.
Open Scope Z_scope.

The source language: arithmetic expressions.


Abstract syntax

Parameter var: Type.

Inductive expr: Type :=
  | Const (n: Z) (* an integer constant *)
  | Var (v: var) (* a variable *)
  | Sum (e1: expr) (e2: expr) (* e1 + e2 *)
  | Diff (e1: expr) (e2: expr) (* e1 - e2 *)
  | Prod (e1: expr) (e2: expr). (* e1 * e2 *)

Denotational semantics -- just an evaluation function, in fact. Parameterized by an environment associating values to variables.

Definition environment := var -> Z.

Fixpoint eval (env: environment) (e: expr) : Z :=
  match e with
  | Const n => n
  | Var v => env v
  | Sum e1 e2 => eval env e1 + eval env e2
  | Diff e1 e2 => eval env e1 - eval env e2
  | Prod e1 e2 => eval env e1 * eval env e2
  end.

The target language: a stack machine in the style of HP calculators


Instruction set

Inductive instruction: Type :=
  | PushConst (n: Z)
  | PushVar (v: var)
  | Add
  | Opp
  | Mul.

Definition code := list instruction.

Operational semantics

Definition stack := list Z.
Definition state := (code * environment * stack)%type.

Execution of the first instruction of the code sequence. Presented as a transition relation between "machine state before" and "machine state after".

Inductive transition: state -> state -> Prop :=
  | trans_pushconst: forall n c env stk,
      transition (PushConst n :: c, env, stk)
                 (c, env, n :: stk)
  | trans_pushvar: forall v c env stk,
      transition (PushVar v :: c, env, stk)
                 (c, env, env v :: stk)
  | trans_add: forall c env n1 n2 stk,
      transition (Add :: c, env, n2 :: n1 :: stk)
                 (c, env, (n1 + n2) :: stk)
  | trans_opp: forall c env n stk,
      transition (Opp :: c, env, n :: stk)
                 (c, env, (-n):: stk)
  | trans_mul: forall c env n1 n2 stk,
      transition (Mul :: c, env, n2 :: n1 :: stk)
                 (c, env, (n1 * n2) :: stk).

Reflexive transitive closure of a relation R.

Inductive star {A: Type} (R: A -> A -> Prop): A -> A -> Prop :=
  | star_refl: forall x,
      star R x x
  | star_one: forall x y,
      R x y -> star R x y
  | star_trans: forall x y z,
      star R x y -> star R y z -> star R x z.

star transition represents zero, one or several successive machine transitions. We use it to define what it means for the machine to halt safely after having executed the given code c.

Definition machine_run (c: code) (env: environment) (result: Z) : Prop :=
  star transition (c, env, nil) (nil, env, result :: nil).

Compilation


Compilation of arithmetic expressions to machine code. This is the familiar translation to "Reverse Polish Notation".

Fixpoint compile_expr (e: expr) : code :=
  match e with
  | Const n => PushConst n :: nil
  | Var v => PushVar v :: nil
  | Sum e1 e2 => compile_expr e1 ++ compile_expr e2 ++ Add :: nil
  | Diff e1 e2 => compile_expr e1 ++ compile_expr e2 ++ Opp :: Add :: nil
  | Prod e1 e2 => compile_expr e1 ++ compile_expr e2 ++ Mul :: nil
  end.

Such function definitions are executable, both within Coq...

Parameter vx: var.

Compute (compile_expr (Prod (Var vx) (Sum (Var vx) (Const 1)))).

... and by generation of OCaml, Haskell or Scheme programs.

Recursive Extraction compile_expr.

This is the statement of correctness for our compiler.

Theorem compile_program_correct:
  forall e env,
  machine_run (compile_expr e) env (eval env e).
Proof.
Abort.

To prove it, we need to do an induction over the expression e, and to strengthen the statement.

Lemma compile_expr_correct:
  forall e c env stk,
  star transition (compile_expr e ++ c, env, stk)
                  (c, env, eval env e :: stk).
Proof.
  induction e; intros; simpl.
Case e = Const n
  apply star_one. apply trans_pushconst.
Case e = Var v
  apply star_one. apply trans_pushvar.
Case e = Plus e1 e2
  rewrite !app_ass. simpl.
  eapply star_trans. apply IHe1.
  eapply star_trans. apply IHe2.
  apply star_one. apply trans_add.
Case e = Diff e1 e2
  rewrite !app_ass. simpl.
  eapply star_trans. apply IHe1.
  eapply star_trans. apply IHe2.
  eapply star_trans. apply star_one. apply trans_opp.
  replace (eval env e1 - eval env e2)
     with (eval env e1 + - (eval env e2))
       by omega.
  apply star_one. apply trans_add.
Case e = Prod e1 e2
  rewrite !app_ass. simpl.
  eapply star_trans. apply IHe1.
  eapply star_trans. apply IHe2.
  apply star_one. apply trans_mul.
Qed.

The original correctness statement is then a corollary.

Theorem compile_program_correct:
  forall e env,
  machine_run (compile_expr e) env (eval env e).
Proof.
  intros. red.
  replace (compile_expr e) with (compile_expr e ++ nil)
       by apply app_nil_r.
  apply compile_expr_correct.
Qed.

A more automated proof

Hint Constructors transition star.

Lemma compile_expr_correct':
  forall e c env stk,
  star transition (compile_expr e ++ c, env, stk)
                  (c, env, eval env e :: stk).
Proof.
  induction e; intros; simpl; rewrite ?app_ass; simpl; eauto.
Case e = Diff e1 e2
  replace (eval env e1 - eval env e2)
     with (eval env e1 + - (eval env e2))
       by omega.
  eauto 6.
Qed.

Generated by coq2html