# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1220647592 14400
# Node ID 91e247c68ee8b9e56d331f554c7ecab39bc81822
# Parent  00366a62bd005bc096c428ba78e59af67020f4f1
Template generation

diff -r 00366a62bd00 -r 91e247c68ee8 .hgignore
--- a/.hgignore	Wed Sep 03 16:37:51 2008 -0400
+++ b/.hgignore	Fri Sep 05 16:46:32 2008 -0400
@@ -13,3 +13,5 @@
 
 html/coqdoc.css
 html/*.html
+
+templates/*.v
diff -r 00366a62bd00 -r 91e247c68ee8 Makefile
--- a/Makefile	Wed Sep 03 16:37:51 2008 -0400
+++ b/Makefile	Fri Sep 05 16:46:32 2008 -0400
@@ -1,11 +1,14 @@
 MODULES_NODOC := Tactics
-MODULES_DOC   := Intro StackMachine
+MODULES_PROSE := StackMachine
+MODULES_CODE  := StackMachine
+MODULES_DOC   := $(MODULES_PROSE) $(MODULES_CODE)
 MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
 VS            := $(MODULES:%=src/%.v)
 VS_DOC        := $(MODULES_DOC:%=%.v)
 GLOBALS       := .coq_globals
+TEMPLATES     := $(MODULES_CODE:%=templates/%.v)
 
-.PHONY: coq clean doc dvi html
+.PHONY: coq clean doc dvi html templates
 
 coq: Makefile.coq
 	make -f Makefile.coq
@@ -19,7 +22,7 @@
 clean:: Makefile.coq
 	make -f Makefile.coq clean
 	rm -f Makefile.coq .depend $(GLOBALS) \
-		latex/*.sty latex/cpdt.*
+		latex/*.sty latex/cpdt.* templates/*.v
 
 doc: latex/cpdt.dvi latex/cpdt.pdf html
 
@@ -44,3 +47,8 @@
 
 dvi:
 	xdvi latex/cpdt
+
+templates: $(TEMPLATES)
+
+templates/%.v: src/%.v
+	ocaml tools/make_template.ml <$< >$@
diff -r 00366a62bd00 -r 91e247c68ee8 src/StackMachine.v
--- a/src/StackMachine.v	Wed Sep 03 16:37:51 2008 -0400
+++ b/src/StackMachine.v	Fri Sep 05 16:46:32 2008 -0400
@@ -198,6 +198,7 @@
 (* begin hide *)
 Abort.
 (* end hide *)
+(* begin thide *)
 
 (** Though a pencil-and-paper proof might clock out at this point, writing "by a routine induction on [e]," it turns out not to make sense to attack this proof directly.  We need to use the standard trick of %\textit{%#<i>#strengthening the induction hypothesis#</i>#%}%.  We do that by proving an auxiliary lemma:
 *)
@@ -511,6 +512,7 @@
 
   reflexivity.
 Qed.
+(* end thide *)
 
 
 (** * Typed Expressions *)
@@ -793,6 +795,7 @@
 (* begin hide *)
 Abort.
 (* end hide *)
+(* begin thide *)
 
 (** Again, we need to strengthen the theorem statement so that the induction will go through.  This time, I will develop an alternative approach to this kind of proof, stating the key lemma as: *)
 
@@ -851,3 +854,4 @@
 Theorem tcompileCorrect : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt).
   crush.
 Qed.
+(* end thide *)
diff -r 00366a62bd00 -r 91e247c68ee8 tools/make_template.ml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tools/make_template.ml	Fri Sep 05 16:46:32 2008 -0400
@@ -0,0 +1,41 @@
+let input_line () = 
+  try
+    Some (input_line stdin)
+  with End_of_file -> None
+
+let rec initial last_was_empty =
+  match input_line () with
+  | None -> ()
+  | Some "(* begin thide *)" ->	thide last_was_empty
+  | Some "" ->
+      if not (last_was_empty) then
+	print_newline ();
+      initial true
+  | Some line ->
+      if String.length line >= 2 && line.[0] = '(' && line.[1] = '*' then
+	if line.[String.length line - 2] = '*' && line.[String.length line - 1] = ')' then
+	  initial last_was_empty
+	else
+	  comment last_was_empty
+      else begin
+	print_endline line;
+	initial false
+      end
+
+and comment last_was_empty =
+  match input_line () with
+  | None -> ()
+  | Some line ->
+      if String.length line >= 2 && line.[String.length line - 2] = '*'
+	  && line.[String.length line - 1] = ')' then
+	initial last_was_empty
+      else
+	comment last_was_empty
+
+and thide last_was_empty =
+  match input_line () with
+  | None -> ()
+  | Some "(* end thide *)" -> initial last_was_empty
+  | Some _ -> thide last_was_empty
+
+let () = initial false