1structure Hol_pp :> Hol_pp = 2struct 3 4open HolKernel DB Parse; 5 6(*--------------------------------------------------------------------------* 7 * Prettyprint a theory for the user * 8 *--------------------------------------------------------------------------*) 9 10val CONSISTENT = Portable.CONSISTENT 11val INCONSISTENT = Portable.INCONSISTENT; 12 13fun print s = !Feedback.MESG_outstream s 14 15fun pp_theory (THEORY(name, {parents, types, consts, 16 axioms,definitions,theorems})) = 17let 18 open smpp 19 val pp_thm = lift pp_thm 20 val pp_type = lift pp_type 21 val nl2 = add_newline >> add_newline 22 fun vspace l = if null l then nothing else nl2 23 fun vblock(header, ob_pr, obs) = 24 if null obs then nothing 25 else 26 block CONSISTENT 4 ( 27 add_string (header^":") >> 28 add_newline >> 29 pr_list ob_pr add_newline obs 30 ) 31 fun pr_thm (heading, ths) = 32 vblock(heading, 33 (fn (s,th) => block CONSISTENT 0 ( 34 add_string s >> add_newline >> 35 add_string " " >> 36 pp_thm th 37 ) 38 ), 39 Listsort.sort (inv_img_cmp #1 String.compare) ths) 40 val longest_const_size = 41 List.foldl (fn ((s,_),i) => Int.max(size s, i)) 0 42 consts 43 val m = 44 block CONSISTENT 0 ( 45 add_string ("Theory: "^name) >> nl2 >> 46 vblock ("Parents", add_string, Listsort.sort String.compare parents) >> 47 nl2 >> 48 vblock ("Type constants", 49 (fn (name,arity) => 50 (add_string name >> 51 add_string (" "^Lib.int_to_string arity))), 52 types) >> 53 vspace types >> 54 vblock ("Term constants", 55 (fn (name,htype) => 56 block CONSISTENT 0 ( 57 add_string name >> 58 add_string ( 59 CharVector.tabulate(longest_const_size + 3 - size name, 60 K #" ")) >> 61 pp_type htype 62 ) 63 ), 64 consts) >> 65 vspace consts >> 66 67 pr_thm ("Axioms", axioms) >> vspace axioms >> 68 pr_thm ("Definitions", definitions) >> vspace definitions >> 69 pr_thm ("Theorems", theorems) 70 ) 71in 72 Parse.mlower m 73end; 74 75(*--------------------------------------------------------------------------- 76 Support for print_theory 77 ---------------------------------------------------------------------------*) 78 79fun print_theory0 pfn thy = 80 HOLPP.prettyPrint(pfn, 80) (pp_theory (dest_theory thy)) 81fun print_theory_to_outstream thy ostrm = 82 print_theory0 (fn s => TextIO.output(ostrm, s)) thy 83 84val print_theory = print_theory0 print 85 86fun print_theory_to_file thy file = 87 let open TextIO 88 val ostrm = openOut file 89 in print_theory_to_outstream thy ostrm 90 ; closeOut ostrm 91 end 92 handle e => raise wrap_exn "DB" "print_theory_to_file" e; 93 94 95(*--------------------------------------------------------------------------- 96 Print a theory as HTML 97 ---------------------------------------------------------------------------*) 98 99fun pp_theory_as_html theory_name = let 100 open Portable PP smpp 101 val THEORY(_,{parents,types, consts, 102 axioms, definitions, theorems}) = dest_theory theory_name 103 fun colour thing col = 104 String.concat["<font color=\"",col,"\">",thing,"</font>"]; 105 fun strong s = 106 add_string"<span class=\"strong\">" >> add_string s >> 107 add_string"</span>" 108 fun STRONG s = 109 add_string"<span class=\"vstrong\">" >> 110 add_string s >> 111 add_string"</span>" 112 fun title s = add_string(String.concat ["<h1>",s,"</h1>"]); 113 fun link (l,s) = 114 add_string("<a href = "^Lib.quote l^">") >> 115 strong s >> 116 add_string"</a>" 117 val HR = add_newline >> add_string"<hr>" >> add_newline 118 119 fun pblock(ob_pr, obs) = 120 block CONSISTENT 4 ( 121 STRONG "Parents" >> 122 add_string " " >> 123 add_break (1,0) >> 124 pr_list ob_pr (add_string " " >> add_break (1,0)) obs 125 ) >> add_newline >> add_newline 126 127 fun sig_block(ob_pr1, obs1, ob_pr2,obs2) = 128 if null types andalso null consts then nothing 129 else 130 title "Signature" >> add_newline >> 131 block CONSISTENT 4 ( 132 block CONSISTENT 0 ( 133 add_string "<center>" >> add_newline >> 134 add_string "<table BORDER=4 CELLPADDING=10 CELLSPACING=1>" >> 135 add_newline 136 ) >> add_newline >> 137 (if null types then nothing 138 else 139 block CONSISTENT 0 ( 140 add_string "<tr>" >> add_break (1,0) >> 141 add_string "<th>" >> add_break (1,0) >> 142 add_string "Type" >> add_break (1,0) >> 143 add_string "<th>" >> add_break (1,0) >> 144 add_string "Arity" 145 ) >> 146 pr_list (fn x => add_string"<tr>" >> ob_pr1 x) add_newline obs1 >> 147 add_newline) >> 148 (if null consts then nothing 149 else 150 block CONSISTENT 0 ( 151 add_string "<tr>" >> add_break (1,0) >> 152 add_string "<th>" >> add_break (1,0) >> 153 add_string "Constant" >> add_break (1,0) >> 154 add_string "<th>" >> add_break (1,0) >> 155 add_string "Type" 156 ) >> 157 pr_list (fn x => (add_string"<tr>" >> ob_pr2 x)) 158 add_newline obs2 >> 159 add_newline) 160 ) >> add_newline >> 161 block CONSISTENT 0 ( 162 add_string "</table>" >> add_newline >> 163 add_string "</center>" >> add_newline 164 ) >> add_newline 165 166 fun dl_block(header, ob_pr, obs0 : (string * 'a) list) = 167 let 168 val obs = Listsort.sort (inv_img_cmp #1 String.compare) obs0 169 in 170 block CONSISTENT 0 ( 171 title header >> 172 add_newline >> 173 add_string"<DL>" >> add_newline >> 174 pr_list 175 (fn (x,ob) => 176 block CONSISTENT 0 ( 177 add_string"<DT>" >> strong x >> add_newline >> 178 add_string"<DD>" >> add_newline >> 179 ob_pr ob 180 ) 181 ) 182 add_newline obs >> 183 add_newline >> 184 add_string"</DL>" 185 ) >> add_newline >> add_newline 186 end 187 188 fun pr_thm (heading, ths) = 189 dl_block(heading, 190 (fn th => block CONSISTENT 0 ( 191 add_string"<pre>" >> 192 add_newline >> 193 lift pp_thm th >> 194 add_newline >> 195 add_string"</pre>" >> 196 add_newline 197 )), 198 ths) 199 val NL = smpp.add_newline 200in 201 block CONSISTENT 0 ( 202 add_string "<!DOCTYPE html PUBLIC \"-//W3C//DTD HTML 4.01//EN\">" >> 203 add_newline >> 204 205 add_string "<html>" >> add_newline >> 206 add_string("<head><title>Theory: "^theory_name^"</title>") >> 207 add_string("<meta http-equiv=\"content-type\"\ 208 \ content=\"text/html;charset=UTF-8\">") >> 209 add_newline >> 210 add_string("<style type=\"text/css\">") >> NL >> 211 add_string "<!--\n\ 212 \ body {background: #faf0e6; color: #191970; }\n\ 213 \ span.freevar { color: blue}\n\ 214 \ span.boundvar { color: green}\n\ 215 \ span.typevar { color: purple}\n\ 216 \ span.type { color: teal}\n\ 217 \ span.strong { color: black; font-weight: bold}\n\ 218 \ span.vstrong { color: black; \n\ 219 \ font-weight: bold;\n\ 220 \ font-size: larger}\n\ 221 \ h1 {color: black}\n\ 222 \ th {color: crimson}\n\ 223 \-->" >> 224 NL >> add_string "</style>" >> NL >> 225 add_string("</head>") >> 226 add_newline >> 227 add_string "<body>" >> 228 add_newline >> 229 title ("Theory \""^theory_name^"\"") >> 230 add_newline >> 231 232 (if null parents then nothing 233 else pblock ((fn n => link(n^"Theory.html",n)), parents)) >> 234 sig_block((fn (Name,Arity) => 235 block CONSISTENT 0 ( 236 add_string"<td>" >> add_break(1,0) >> strong Name >> 237 add_break(1,0) >> 238 add_string"<td>" >> add_break(1,0) >> 239 add_string (Lib.int_to_string Arity) 240 )), 241 types, 242 (fn (Name,Ty) => 243 block CONSISTENT 0 ( 244 add_string"<td>" >> add_break(1,0) >> strong Name >> 245 add_break(1,0) >> 246 add_string"<td>" >> add_break(1,0) >> lift pp_type Ty 247 )), 248 consts) >> 249 (if null axioms then nothing else pr_thm ("Axioms", axioms)) >> 250 (if null definitions then nothing 251 else (if null axioms then nothing else (HR >> HR)) >> 252 pr_thm ("Definitions", definitions)) >> 253 (if null theorems then nothing 254 else (if null axioms andalso null definitions then nothing 255 else HR >> HR) >> 256 pr_thm ("Theorems", theorems)) >> 257 add_newline >> 258 HR >> 259 add_string "</body>" >> add_newline >> 260 add_string "</html>" >> add_newline 261 ) 262end; 263 264val pp_theory_as_html = Parse.mlower o pp_theory_as_html 265 266fun print_theory_as_html s path = let 267 val name = (case s of "-" => current_theory() | other => s) 268 val ostrm = TextIO.openOut path 269 val oldbackend = !Parse.current_backend 270 val _ = Parse.current_backend := PPBackEnd.raw_terminal 271 (* would like this to be html_terminal, but it causes 272 occasional exceptions *) 273 fun finalise() = (Parse.current_backend := oldbackend; TextIO.closeOut ostrm) 274 fun out s = TextIO.output(ostrm, s) 275in 276 PP.prettyPrint(out, 78) (pp_theory_as_html name) 277 handle e => (finalise(); raise e); 278 finalise() 279end; 280 281fun html_theory s = print_theory_as_html s (s^"Theory.html"); 282 283(*--------------------------------------------------------------------------- 284 Refugee from Parse structure 285 ---------------------------------------------------------------------------*) 286 287fun export_theory_as_docfiles dirname = 288 Parse.export_theorems_as_docfiles dirname 289 (axioms "-" @ definitions "-" @ 290 theorems "-"); 291 292 293 294 295 296fun data_to_string (((th,name),(thm,cl)):data) = 297let 298 open PPBackEnd Parse 299 val cl_s = if cl = Thm then "THEOREM" else 300 if cl = Axm then "AXIOM" else 301 "DEFINITION"; 302 val name_style = add_style_to_string [Bold] name 303 304 val s = th^"Theory."^name^" ("^cl_s^")\n"; 305 val s_style = (th^"Theory.")^name_style^" ("^cl_s^")\n"; 306 val size = String.size s 307 fun line 0 l = l 308 | line n l = line (n-1) ("-"^l) 309 val s = s_style^(line (size-1) "\n")^ppstring pp_thm thm^"\n"; 310in 311 s 312end; 313 314 315val data_list_to_string = (foldl (fn (d, s) => s^(data_to_string d)^"\n\n") "\n\n\n"); 316 317val print_apropos = print o data_list_to_string o apropos; 318val print_find = print o data_list_to_string o find; 319fun print_match x1 x2 = print (data_list_to_string (match x1 x2)); 320 321end 322