1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Author: Thomas C. Hales *)
5 (* Date: Feb 7, 2010 *)
6 (* ========================================================================== *)
11 a formatted HOL Light identifier, as a module with signature.
12 The author and date information are added as comments.
14 The file pathname is derived from the root directory, which can be set by the user,
15 the lowercase of chapter string must match a subdirectory name precisely,
16 and the identifier is used to create the file name.
20 module type Template_hol_type = sig
33 val output_template_def : data -> unit
35 val output_template_lemma : data -> unit
37 val set_root_dir : string-> unit (* default is "/tmp" *)
42 Example: The following code creates a template identifier file
43 "/tmp/Trigonometry/azim_def.hl",
44 populated with the code from def1
53 chapter="Trigonometry";
54 author="Thomas C. Hales";
56 code="<Insert HOL-Light code for theorem here>";
57 comments=["This is just a test!"];
58 needlist=["Multivariate/flyspeck.ml"];
60 let _ = set_root_dir "/tmp" in
61 output_template_def def1;;
66 module Template_hol : Template_hol_type =
76 comments: string list;
80 (* Comments and Line Formatting *)
87 let unsplit d f = function
88 | (x::xs) -> List.fold_left (fun s t -> s^d^(f t)) (f x) xs
91 let join_lines = unsplit "\n" (fun x-> x);;
94 let c_enclose s = "(* "^s^String.make (width - String.length s) space^" *)";;
95 let pad_line = (String.make width pad);;
96 let space_line = String.make width space;;
98 type opt = Def | Lemma;;
99 let label t = if t=Def then "Definition" else "Lemma";;
100 let ext t = if t=Def then "_def" else "";;
105 let p = Printf.sprintf in
106 unsplit "\n" c_enclose [
108 p"FLYSPECK - BOOK FORMALIZATION";
110 p"%s: %s" (label t) dat.identifier;
111 p"Chapter: %s" dat.chapter;
112 p"Author: %s" dat.author;
113 p"Date: %s" dat.date;
117 let more_comments dat =
118 if (dat.comments =[]) then emptystring else
119 "(*\n"^(join_lines dat.comments)^"\n*)\n\n\n";;
121 let neededfiles dat =
122 if (dat.needlist =[]) then emptystring else
123 (unsplit "\n" (fun s -> "flyspeck_needs \""^s^"\";;") dat.needlist)^"\n\n\n";;
126 let p = Printf.sprintf in
127 let uc = String.capitalize (String.lowercase dat.identifier) in (* HOL Light parsing: cap first char only *)
129 p"module type %s_def_type = sig" uc;
130 p" val %s : thm" dat.identifier;
133 p"module %s : %s_def_type = struct\n" uc uc;
134 p" let %s = " dat.identifier;
141 let rootdir =ref "/tmp";;
142 let set_root_dir s = (rootdir := s);;
144 let filename t dat = (!rootdir)^sep^(String.lowercase dat.chapter)^sep^dat.identifier^(ext t)^".hl";;
146 let save_stringarray filename xs =
147 let oc = open_out filename in
148 for i=0 to List.length xs -1
150 Pervasives.output_string oc (List.nth xs i ^ "\n");
154 let output_template t dat = save_stringarray (filename t dat)
155 [header t dat;"\n\n\n";more_comments dat;
158 let output_template_def dat = output_template Def dat;;
159 let output_template_lemma dat = output_template Lemma dat;;