Mercurial > cpdt > repo

changeset 3:9fea5674367c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pretty LaTeX generation
author Adam Chlipala <adamc@hcoop.net>
date Fri, 29 Aug 2008 14:24:38 -0400
parents b3f7de74d38f
children f913d32a49e4
files .hgignore book/Makefile book/StackMachine.v book/Tactics.v book/src/StackMachine.v book/src/Tactics.v
diffstat 6 files changed, 172 insertions(+), 147 deletions(-) [+]
line wrap: on
line diff
--- a/.hgignore	Fri Aug 29 13:42:37 2008 -0400
+++ b/.hgignore	Fri Aug 29 14:24:38 2008 -0400
@@ -6,3 +6,8 @@
 *.vo
 */Makefile.coq
 */.coq_globals
+
+*/coqdoc.sty
+*/cpdt.*
+*/*.log
+
--- a/book/Makefile	Fri Aug 29 13:42:37 2008 -0400
+++ b/book/Makefile	Fri Aug 29 14:24:38 2008 -0400
@@ -1,17 +1,31 @@
-MODULES    := Tactics StackMachine
-VS         := $(MODULES:%=%.v)
-GLOBALS    := .coq_globals
+MODULES_NODOC := Tactics
+MODULES_DOC   := StackMachine
+MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
+VS            := $(MODULES:%=src/%.v)
+VS_DOC        := $(MODULES_DOC:%=%.v)
+GLOBALS       := .coq_globals
 
-.PHONY: coq clean
+.PHONY: coq clean doc
 
 coq: Makefile.coq
 	make -f Makefile.coq
 
 Makefile.coq: Makefile $(VS)
 	coq_makefile $(VS) \
-		COQC = "coqc -impredicative-set -dump-glob $(GLOBALS)" \
+		COQC = "coqc -I src -impredicative-set \
+			-dump-glob $(GLOBALS)" \
 		-o Makefile.coq
 
 clean:: Makefile.coq
 	make -f Makefile.coq clean
-	rm -f Makefile.coq .depend
+	rm -f Makefile.coq .depend $(GLOBALS) \
+		latex/*.sty latex/cpdt.*
+
+doc: latex/cpdt.dvi
+
+latex/cpdt.tex: $(VS)
+	cd src ; coqdoc --latex $(VS_DOC) \
+		-o ../latex/cpdt.tex
+
+latex/cpdt.dvi: latex/cpdt.tex
+	cd latex ; latex cpdt
--- a/book/StackMachine.v	Fri Aug 29 13:42:37 2008 -0400
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,115 +0,0 @@
-(* 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.
--- a/book/Tactics.v	Fri Aug 29 13:42:37 2008 -0400
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(* 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.
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/book/src/StackMachine.v	Fri Aug 29 14:24:38 2008 -0400
@@ -0,0 +1,121 @@
+(* 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 *)
+
+(* begin hide *)
+Module Nat.
+(* end hide *)
+  (** ** 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.
+
+(* begin hide *)
+End Nat.
+(* end hide *)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/book/src/Tactics.v	Fri Aug 29 14:24:38 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.