adamc@2: (* Copyright (c) 2008, Adam Chlipala
adamc@2:  * 
adamc@2:  * This work is licensed under a
adamc@2:  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@2:  * Unported License.
adamc@2:  * The license text is available at:
adamc@2:  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@2:  *)
adamc@2: 
adamc@3: (* begin hide *)
adamc@2: Require Import List.
adamc@2: 
adamc@2: Require Import Tactics.
adamc@3: (* end hide *)
adamc@2: 
adamc@2: 
adamc@2: (** * Arithmetic expressions over natural numbers *)
adamc@2: 
adamc@3: (* begin hide *)
adamc@2: Module Nat.
adamc@3: (* end hide *)
adamc@2:   (** ** Source language *)
adamc@2: 
adamc@2:   Inductive binop : Set := Plus | Times.
adamc@2: 
adamc@2:   Inductive exp : Set :=
adamc@2:   | Const : nat -> exp
adamc@2:   | Binop : binop -> exp -> exp -> exp.
adamc@2: 
adamc@2:   Definition binopDenote (b : binop) : nat -> nat -> nat :=
adamc@2:     match b with
adamc@2:       | Plus => plus
adamc@2:       | Times => mult
adamc@2:     end.
adamc@2: 
adamc@2:   Fixpoint expDenote (e : exp) : nat :=
adamc@2:     match e with
adamc@2:       | Const n => n
adamc@2:       | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2)
adamc@2:     end.
adamc@2: 
adamc@2: 
adamc@2:   (** ** Target language *)
adamc@2: 
adamc@2:   Inductive instr : Set :=
adamc@2:   | IConst : nat -> instr
adamc@2:   | IBinop : binop -> instr.
adamc@2: 
adamc@2:   Definition prog := list instr.
adamc@2:   Definition stack := list nat.
adamc@2: 
adamc@2:   Definition instrDenote (i : instr) (s : stack) : option stack :=
adamc@2:     match i with
adamc@2:       | IConst n => Some (n :: s)
adamc@2:       | IBinop b =>
adamc@2:         match s with
adamc@2:           | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s')
adamc@2:           | _ => None
adamc@2:         end
adamc@2:     end.
adamc@2: 
adamc@2:   Fixpoint progDenote (p : prog) (s : stack) {struct p} : option stack :=
adamc@2:     match p with
adamc@2:       | nil => Some s
adamc@2:       | i :: p' =>
adamc@2:         match instrDenote i s with
adamc@2:           | None => None
adamc@2:           | Some s' => progDenote p' s'
adamc@2:         end
adamc@2:     end.
adamc@2: 
adamc@2: 
adamc@2:   (** ** Translation *)
adamc@2: 
adamc@2:   Fixpoint compile (e : exp) : prog :=
adamc@2:     match e with
adamc@2:       | Const n => IConst n :: nil
adamc@2:       | Binop b e1 e2 => compile e2 ++ compile e1 ++ IBinop b :: nil
adamc@2:     end.
adamc@2: 
adamc@2: 
adamc@2:   (** ** Translation correctness *)
adamc@2: 
adamc@2:   Lemma compileCorrect' : forall e s p, progDenote (compile e ++ p) s =
adamc@2:     progDenote p (expDenote e :: s).
adamc@2:     induction e.
adamc@2: 
adamc@2:     intros.
adamc@2:     unfold compile.
adamc@2:     unfold expDenote.
adamc@2:     simpl.
adamc@2:     reflexivity.
adamc@2: 
adamc@2:     intros.
adamc@2:     unfold compile.
adamc@2:     fold compile.
adamc@2:     unfold expDenote.
adamc@2:     fold expDenote.
adamc@2:     rewrite app_ass.
adamc@2:     rewrite IHe2.
adamc@2:     rewrite app_ass.
adamc@2:     rewrite IHe1.
adamc@2:     simpl.
adamc@2:     reflexivity.
adamc@2:   Abort.
adamc@2: 
adamc@2:   Lemma compileCorrect' : forall e s p, progDenote (compile e ++ p) s =
adamc@2:     progDenote p (expDenote e :: s).
adamc@2:     induction e; crush.
adamc@2:   Qed.
adamc@2: 
adamc@2:   Theorem compileCorrect : forall e, progDenote (compile e) nil = Some (expDenote e :: nil).
adamc@2:     intro.
adamc@2:     rewrite (app_nil_end (compile e)).
adamc@2:     rewrite compileCorrect'.
adamc@2:     reflexivity.
adamc@2:   Qed.
adamc@2: 
adamc@3: (* begin hide *)
adamc@2: End Nat.
adamc@3: (* end hide *)