Update from HH
[Flyspeck/.git] / development / thales / chaff / general / template_def.ml
1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
3 (*                                                                            *)
4 (* Author: Thomas C. Hales                                                    *)
5 (* Date: Feb 7, 2010                                                          *)
6 (* ========================================================================== *)
7
8
9 (*
10 Outputs to a file 
11 a formatted HOL Light identifier, as a module with signature.
12 The author and date information are added as comments.
13
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.
17 *)
18
19
20 module type Template_hol_type = sig
21
22   type data =
23       {
24         identifier : string;
25         chapter : string;
26         author: string;
27         date:string;
28         code:string;
29         comments:string list;
30         needlist:string list;
31       }
32
33   val output_template_def : data -> unit 
34
35   val output_template_lemma : data -> unit
36
37   val set_root_dir : string-> unit  (* default is "/tmp" *)
38
39 end;;
40
41 (* 
42 Example:  The following code creates a template identifier file 
43    "/tmp/Trigonometry/azim_def.hl",
44 populated with the code from def1
45 *)
46
47 (*
48
49 open Template_hol;;
50 let example1() = 
51   let def1 = 
52     {identifier="azim";
53      chapter="Trigonometry";
54      author="Thomas C. Hales";
55      date="Feb 7, 2010";
56      code="<Insert HOL-Light code for theorem here>";
57      comments=["This is just a test!"];
58      needlist=["Multivariate/flyspeck.ml"];
59     } in
60  let _ = set_root_dir "/tmp" in
61    output_template_def def1;;
62 example1();;
63
64 *)
65
66 module Template_hol : Template_hol_type = 
67 struct
68
69   type data =
70       {
71         identifier : string;
72         chapter : string;
73         author: string;
74         date:string;
75         code:string;
76         comments: string list;
77         needlist:string list;
78       };;
79
80   (* Comments and Line Formatting *)
81
82   let sep= "/";;
83   let pad='=';;
84   let space=' ';;
85   let emptystring="";;
86
87   let unsplit d f = function
88     | (x::xs) ->  List.fold_left (fun s t -> s^d^(f t)) (f x) xs
89     | [] -> "";;
90
91   let join_lines  = unsplit "\n" (fun x-> x);;
92   let width = 80 - 6;;
93
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;;
97
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 "";;
101
102   (* Content *)
103
104   let header t dat = 
105     let p = Printf.sprintf in
106       unsplit "\n" c_enclose [
107         pad_line;
108         p"FLYSPECK - BOOK FORMALIZATION";
109         space_line;
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;
114         pad_line;
115       ];;
116
117   let more_comments dat = 
118    if (dat.comments =[]) then emptystring else
119    "(*\n"^(join_lines dat.comments)^"\n*)\n\n\n";;
120
121   let neededfiles dat = 
122        if (dat.needlist =[]) then emptystring else
123       (unsplit "\n" (fun s -> "flyspeck_needs \""^s^"\";;") dat.needlist)^"\n\n\n";;
124
125   let body dat = 
126     let p = Printf.sprintf in
127     let uc = String.capitalize (String.lowercase dat.identifier) in (* HOL Light parsing: cap first char only *)
128       join_lines [
129         p"module type %s_def_type = sig" uc;
130         p"  val %s : thm" dat.identifier;
131         "end;;\n\n";
132         neededfiles dat;
133         p"module %s : %s_def_type = struct\n" uc uc;
134         p" let %s = " dat.identifier;
135         dat.code;
136         "\nend;;\n";
137       ];;
138
139   (* Output *)
140
141   let rootdir =ref "/tmp";;
142   let set_root_dir s = (rootdir := s);;
143
144   let filename  t dat = (!rootdir)^sep^(String.lowercase dat.chapter)^sep^dat.identifier^(ext t)^".hl";;
145
146   let save_stringarray filename xs = 
147     let oc = open_out filename in
148       for i=0 to List.length xs -1
149       do
150         Pervasives.output_string oc (List.nth xs i ^ "\n");
151       done;
152       close_out oc;;
153
154   let output_template t dat = save_stringarray (filename t dat) 
155       [header t dat;"\n\n\n";more_comments dat;
156        body dat];;
157
158   let output_template_def dat = output_template Def dat;;
159   let output_template_lemma dat = output_template Lemma dat;;
160
161 end;;
162
163