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