# HG changeset patch # User Adam Chlipala # Date 1220034278 14400 # Node ID 9fea5674367cde7b8a16c2c841d16029cf13053a # Parent b3f7de74d38f1be6897f11b8e9dfcf4251b34c2a Pretty LaTeX generation diff -r b3f7de74d38f -r 9fea5674367c .hgignore --- 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 + diff -r b3f7de74d38f -r 9fea5674367c book/Makefile --- 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 diff -r b3f7de74d38f -r 9fea5674367c book/StackMachine.v --- 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. diff -r b3f7de74d38f -r 9fea5674367c book/Tactics.v --- 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. diff -r b3f7de74d38f -r 9fea5674367c book/src/StackMachine.v --- /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 *) diff -r b3f7de74d38f -r 9fea5674367c book/src/Tactics.v --- /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.