<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
(* ** 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! *)