Start of Intro

.hgignore

@@ -11,3 +11,5 @@ syntax: glob
 */cpdt.*
 */*.log
 
+book/html/coqdoc.css
+book/html/*.html

book/Makefile

 MODULES_NODOC := Tactics
-MODULES_DOC   := StackMachine
+MODULES_DOC   := Intro StackMachine
 MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
 VS            := $(MODULES:%=src/%.v)
 VS_DOC        := $(MODULES_DOC:%=%.v)
 GLOBALS       := .coq_globals
 
-.PHONY: coq clean doc
+.PHONY: coq clean doc dvi html
 
 coq: Makefile.coq
 	make -f Makefile.coq
@@ -21,11 +21,20 @@ clean:: Makefile.coq
 	rm -f Makefile.coq .depend $(GLOBALS) \
 		latex/*.sty latex/cpdt.*
 
-doc: latex/cpdt.dvi
+doc: latex/cpdt.dvi html
 
 latex/cpdt.tex: $(VS)
 	cd src ; coqdoc --latex $(VS_DOC) \
+		-p "\usepackage{url}" \
 		-o ../latex/cpdt.tex
 
 latex/cpdt.dvi: latex/cpdt.tex
 	cd latex ; latex cpdt
+
+html: $(VS)
+	cd src ; coqdoc $(VS_DOC) \
+		--glob-from ../$(GLOBALS) \
+		-d ../html
+
+dvi:
+	xdvi latex/cpdt

book/src/StackMachine.v

@@ -16,106 +16,99 @@ Require Import Tactics.
 
 (** * Arithmetic expressions over natural numbers *)
 
-(* begin hide *)
-Module Nat.
-(* end hide *)
   (** ** Source language *)
 
-  Inductive binop : Set := Plus | Times.
+Inductive binop : Set := Plus | Times.
 
-  Inductive exp : Set :=
-  | Const : nat -> exp
-  | Binop : binop -> exp -> exp -> exp.
+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.
+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.
+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.
+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.
+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 *)
+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.