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@2:   (** ** Source language *)
adamc@2: 
adamc@4: Inductive binop : Set := Plus | Times.
adamc@2: 
adamc@4: Inductive exp : Set :=
adamc@4: | Const : nat -> exp
adamc@4: | Binop : binop -> exp -> exp -> exp.
adamc@2: 
adamc@4: Definition binopDenote (b : binop) : nat -> nat -> nat :=
adamc@4:   match b with
adamc@4:     | Plus => plus
adamc@4:     | Times => mult
adamc@4:   end.
adamc@2: 
adamc@4: Fixpoint expDenote (e : exp) : nat :=
adamc@4:   match e with
adamc@4:     | Const n => n
adamc@4:     | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2)
adamc@4:   end.
adamc@2: 
adamc@2: 
adamc@2:   (** ** Target language *)
adamc@2: 
adamc@4: Inductive instr : Set :=
adamc@4: | IConst : nat -> instr
adamc@4: | IBinop : binop -> instr.
adamc@2: 
adamc@4: Definition prog := list instr.
adamc@4: Definition stack := list nat.
adamc@2: 
adamc@4: Definition instrDenote (i : instr) (s : stack) : option stack :=
adamc@4:   match i with
adamc@4:     | IConst n => Some (n :: s)
adamc@4:     | IBinop b =>
adamc@4:       match s with
adamc@4:         | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s')
adamc@4:         | _ => None
adamc@4:       end
adamc@4:   end.
adamc@2: 
adamc@4: Fixpoint progDenote (p : prog) (s : stack) {struct p} : option stack :=
adamc@4:   match p with
adamc@4:     | nil => Some s
adamc@4:     | i :: p' =>
adamc@4:       match instrDenote i s with
adamc@4:         | None => None
adamc@4:         | Some s' => progDenote p' s'
adamc@4:       end
adamc@4:   end.
adamc@2: 
adamc@2: 
adamc@2:   (** ** Translation *)
adamc@2: 
adamc@4: Fixpoint compile (e : exp) : prog :=
adamc@4:   match e with
adamc@4:     | Const n => IConst n :: nil
adamc@4:     | Binop b e1 e2 => compile e2 ++ compile e1 ++ IBinop b :: nil
adamc@4:   end.
adamc@2: 
adamc@2: 
adamc@2:   (** ** Translation correctness *)
adamc@2: 
adamc@4: Lemma compileCorrect' : forall e s p, progDenote (compile e ++ p) s =
adamc@4:   progDenote p (expDenote e :: s).
adamc@4:   induction e.
adamc@2: 
adamc@4:   intros.
adamc@4:   unfold compile.
adamc@4:   unfold expDenote.
adamc@4:   simpl.
adamc@4:   reflexivity.
adamc@2: 
adamc@4:   intros.
adamc@4:   unfold compile.
adamc@4:   fold compile.
adamc@4:   unfold expDenote.
adamc@4:   fold expDenote.
adamc@4:   rewrite app_ass.
adamc@4:   rewrite IHe2.
adamc@4:   rewrite app_ass.
adamc@4:   rewrite IHe1.
adamc@4:   simpl.
adamc@4:   reflexivity.
adamc@4: Abort.
adamc@2: 
adamc@4: Lemma compileCorrect' : forall e s p, progDenote (compile e ++ p) s =
adamc@4:   progDenote p (expDenote e :: s).
adamc@4:   induction e; crush.
adamc@4: Qed.
adamc@2: 
adamc@4: Theorem compileCorrect : forall e, progDenote (compile e) nil = Some (expDenote e :: nil).
adamc@4:   intro.
adamc@4:   rewrite (app_nil_end (compile e)).
adamc@4:   rewrite compileCorrect'.
adamc@4:   reflexivity.
adamc@4: Qed.