# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1220031757 14400
# Node ID b3f7de74d38f1be6897f11b8e9dfcf4251b34c2a
# Parent  0ba25681a11beb3c71e9a3db13bf67ab52346056
Start of stack machine example

diff -r 0ba25681a11b -r b3f7de74d38f .hgignore
--- a/.hgignore	Wed Aug 20 11:23:02 2008 -0400
+++ b/.hgignore	Fri Aug 29 13:42:37 2008 -0400
@@ -5,3 +5,4 @@
 *.depend
 *.vo
 */Makefile.coq
+*/.coq_globals
diff -r 0ba25681a11b -r b3f7de74d38f book/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/book/Makefile	Fri Aug 29 13:42:37 2008 -0400
@@ -0,0 +1,17 @@
+MODULES    := Tactics StackMachine
+VS         := $(MODULES:%=%.v)
+GLOBALS    := .coq_globals
+
+.PHONY: coq clean
+
+coq: Makefile.coq
+	make -f Makefile.coq
+
+Makefile.coq: Makefile $(VS)
+	coq_makefile $(VS) \
+		COQC = "coqc -impredicative-set -dump-glob $(GLOBALS)" \
+		-o Makefile.coq
+
+clean:: Makefile.coq
+	make -f Makefile.coq clean
+	rm -f Makefile.coq .depend
diff -r 0ba25681a11b -r b3f7de74d38f book/StackMachine.v
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/book/StackMachine.v	Fri Aug 29 13:42:37 2008 -0400
@@ -0,0 +1,115 @@
+(* 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/
+ *)
+
+Require Import List.
+
+Require Import Tactics.
+
+
+(** * Arithmetic expressions over natural numbers *)
+
+Module Nat.
+  (** ** 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.
+
+End Nat.
diff -r 0ba25681a11b -r b3f7de74d38f book/Tactics.v
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/book/Tactics.v	Fri Aug 29 13:42:37 2008 -0400
@@ -0,0 +1,26 @@
+(* 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/
+ *)
+
+Require Import List.
+
+
+Ltac rewriteHyp :=
+  match goal with
+    | [ H : _ |- _ ] => rewrite H
+  end.
+
+Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *).
+
+Ltac rewriter := autorewrite with cpdt in *; rewriterP.
+
+Hint Rewrite app_ass : cpdt.
+
+Ltac sintuition := simpl; intuition.
+
+Ltac crush := sintuition; rewriter; sintuition.