Template generation

.hgignore

@@ -13,3 +13,5 @@ Makefile.coq
 
 html/coqdoc.css
 html/*.html
+
+templates/*.v

Makefile

 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 @@ Makefile.coq: Makefile $(VS)
 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 @@ html: Makefile $(VS)
 
 dvi:
 	xdvi latex/cpdt
+
+templates: $(TEMPLATES)
+
+templates/%.v: src/%.v
+	ocaml tools/make_template.ml <$< >$@

src/StackMachine.v

@@ -198,6 +198,7 @@ Theorem compileCorrect : forall e, progDenote (compile e) nil = Some (expDenote
 (* 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 @@ We are almost done.  The lefthand and righthand sides can be seen to match by si
 
   reflexivity.
 Qed.
+(* end thide *)
 
 
 (** * Typed Expressions *)
@@ -793,6 +795,7 @@ Theorem tcompileCorrect : forall t (e : texp t), tprogDenote (tcompile e nil) tt
 (* 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 @@ Hint Rewrite tcompileCorrect' : cpdt.
 Theorem tcompileCorrect : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt).
   crush.
 Qed.
+(* end thide *)

tools/make_template.ml

+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