<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 product
*)

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? *)

(** Can you prove the theorem below? *)

Theorem compile_correct_firsttry: 
  forall e, run (compile e) nil = meaning e :: nil.
Proof.
Admitted.

  (* Maybe you attempted 
 
  intros e. induction e. simpl; reflexivity. simpl.

  and it was very unclear how to go on from there.  The problem is that
  the induction hypothesis IHe1 and IHe2 suppose that:

  - the programs obtained by compiling e1 and e2 are executed starting
    from an empty stack;

  - the programs only contain the instructions of the compilation of
    e1 or e2.

  These induction hypothesis are too weak to help us.  

  Maybe you can prove a stronger theorem...  can you?
*)

Lemma compile_correct': 
  forall e p s, run (compile e ++ p) s = run p (meaning e :: s).
Proof.
Admitted.

(* 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.
Admitted.

(** * 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! *)

(* Can you extend the source language of our compiler to include 
   subtraction (denoted [-] in Coq)?

   - Redefine the source grammar [exp] and the [meaning] function.

   - Extend the stack machine with the new [Isub] instruction.

   - Extend appropriately the compiler.  Be careful: subtraction
     is not commutative, and the order in which you place the
     operands on the stack is important!

   - Prove the correctness of the extended compiler.
*)