1structure holindex :> holindex = 2struct 3 4open Lib Feedback HolKernel Parse boolLib mungeTools holindexData 5 6(******************************************************************************) 7(* Some datastructures to store all the necessary information in *) 8(******************************************************************************) 9 10val default_linewidth_ref = ref 80; 11val use_occ_sort_ref = ref false; 12 13(******************************************************************************) 14(* Parse the input file *) 15(******************************************************************************) 16 17 18(* 19 val file = "/home/tt291/Documents/thesis/holmunge/test.hix"; 20 val ds = new_data_store (); 21 val l = Portable.input_line fh; 22*) 23 24val error_found = ref false; 25fun report_error e = (print e;print"\n";error_found := true); 26fun report_warning e = (print e;print"\n"); 27 28local 29 fun is_not_space c = not (Char.isSpace c) 30 fun is_lbrace c = c = #"{" 31 fun is_not_rbrace c = not (c = #"}") 32 33 fun space_trim ls = 34 Substring.dropr Char.isSpace (Substring.dropl Char.isSpace ls) 35 36 val tokenfun_space = Substring.splitl is_not_space 37 fun tokenfun_brace ls = 38 let 39 val (ls1, ls2) = Substring.splitl is_not_rbrace ls; 40 val ls1' = Substring.triml 1 ls1 41 val ls2' = Substring.triml 1 ls2 42 in 43 (ls1', ls2') 44 end; 45 fun tokenfun ls = if is_lbrace (valOf(Substring.first ls)) then 46 tokenfun_brace ls else tokenfun_space ls 47 48 fun parse_substring ls = 49 if Substring.isEmpty ls then [] else 50 let 51 val (ls1, ls2) = tokenfun ls 52 val ls1' = space_trim ls1 53 val ls2' = space_trim ls2 54 in 55 ls1'::(parse_substring ls2') 56 end; 57 58in 59 60fun tokenise_hix_line l = 61let 62 val sl = Substring.full l; 63 val sll = parse_substring sl; 64 val ll = List.map Substring.string sll 65in 66 ll 67end; 68 69end; 70 71 72 73fun process_hix_line basedir ds l = 74let 75 val ll = tokenise_hix_line l; 76in 77 case ll of 78 ["Definition", ty_arg, id_arg, label_arg, content_arg] => 79 update_data_store (true, report_error) 80 ds ty_arg id_arg 81 (fn ent => data_entry___update_label (SOME label_arg) 82 (data_entry___update_content (SOME content_arg) ent)) 83 | ["Printed", ty_arg, id_arg, page_arg] => 84 update_data_store (false, report_error) ds ty_arg id_arg 85 ((data_entry___add_page page_arg) o 86 (data_entry___update_printed true)) 87 | ["Reference", ty_arg, id_arg, page_arg] => 88 update_data_store (false, report_error) ds ty_arg id_arg 89 ((data_entry___add_page page_arg) o 90 (data_entry___update_in_index true)) 91 | ["ForceIndex", ty_arg, id_arg] => 92 update_data_store (false, report_error) ds ty_arg id_arg 93 (data_entry___update_in_index true) 94 | ["FullIndex", ty_arg, id_arg, f_arg] => 95 update_data_store (false, report_error) ds ty_arg id_arg 96 (data_entry___update_full_index (f_arg = "true")) 97 | ["FormatOptions", ty_arg, id_arg, options_arg] => 98 update_data_store (false, report_error) ds ty_arg id_arg 99 (data_entry___update_options options_arg) 100 | ["Comment", ty_arg, id_arg, comment_arg] => 101 update_data_store (false, report_error) ds ty_arg id_arg 102 (data_entry___update_comment (SOME comment_arg)) 103 | ["Overrides", file] => 104 (mungeTools.user_overrides := mungeTools.read_overrides file; 105 ds) 106 | ["UseOccurenceSort"] => 107 let 108 val _ = use_occ_sort_ref := true; 109 in 110 ds 111 end 112 | ["Linewidth", length_arg] => 113 let 114 val n_opt = Int.fromString length_arg 115 val _ = if isSome n_opt then (default_linewidth_ref := valOf n_opt) else (); 116 in 117 ds 118 end 119 | ["UseFile", filename] => 120 (let 121 val file = if Path.isAbsolute filename then filename else 122 Path.concat (basedir, filename) 123 val entryL = AssembleHolindexParser.parse_hdf_file file; 124 in 125 foldl (fn (de, ds) => parse_entry___add_to_data_store ds de) ds 126 entryL 127 end handle Interrupt => raise Interrupt 128 | _ => (report_error ("Error while parsing '"^filename^"' in '"^basedir^"'");ds)) 129 | _ => (report_error ("Error line: "^l); ds) 130end; 131 132 133 134fun cleanup_data_store (sds_thm, sds_term, sds_type) = 135let 136 fun cleanup_subdata_store sds = 137 let 138 val sdsL = Redblackmap.listItems sds 139 val sdsL' = List.filter (data_entry_is_used o snd) sdsL; 140 in 141 sdsL' 142 end; 143 fun thmmapfun (id, de:data_entry) = 144 (id, if (isSome (#content de)) then de else 145 data_entry___update_content (SOME id) de) 146in 147 (List.map thmmapfun (cleanup_subdata_store sds_thm), 148 cleanup_subdata_store sds_term, 149 cleanup_subdata_store sds_type) 150end; 151 152 153fun parse_hix file = 154let 155 val ds_ref = ref new_data_store; 156 val fh = Portable.open_in file; 157 val basedir = Path.dir file; 158 159 val _ = while (not (Portable.end_of_stream fh)) do ( 160 ds_ref := process_hix_line basedir (!ds_ref) (Portable.input_line fh) 161 ); 162 163 val _ = Portable.close_in fh 164in 165 cleanup_data_store (!ds_ref) 166end; 167 168 169 170 171 172(******************************************************************************) 173(* Output definitions *) 174(******************************************************************************) 175fun destruct_theory_thm s2 = 176 let 177 val ss2 = (Substring.full s2) 178 val (x1,x2) = Substring.splitl (fn c => not (c = #".")) ss2 179 val x2' = Substring.triml 1 x2 180 in 181 (Substring.string x1, Substring.string x2') 182 end 183 184fun command2string mungeTools.Term = "Term" 185 | command2string mungeTools.Theorem = "Theorem" 186 | command2string mungeTools.Type = "Type"; 187 188fun holmunge_format command id options content = 189let 190 val _ = if (isSome content) then () else Feedback.fail(); 191 val empty_posn = (0,0); 192 val opts = mungeTools.parseOpts empty_posn ("alltt,"^options); 193 val _ = if command = mungeTools.Theorem then 194 let 195 val (ty, tm) = destruct_theory_thm (valOf content); 196 val _ = DB.fetch ty tm 197 handle HOL_ERR e => 198 (report_error (#message e);Feedback.fail()); 199 in 200 () 201 end else (); 202 val replacement_args = 203 {argpos = empty_posn, command=command, commpos = empty_posn, 204 options = opts, argument=(valOf content)}; 205 val width_opt = mungeTools.optset_width opts; 206 val width = if isSome width_opt then valOf width_opt else (!default_linewidth_ref); 207 val fs = PP.pp_to_string width mungeTools.replacement replacement_args 208 val _ = if fs = "" then (report_error 209 ("Error while formating "^(command2string command)^" '"^id^"'!");Feedback.fail()) else (); 210in 211 UTF8.translate (fn " " => "\\ " 212 | "\n" => "\\par " 213 | s => s) fs 214end handle Interrupt => raise Interrupt 215 | _ => ""; 216 217 218(*val os = Portable.std_out*) 219fun output_holtex_def_internal (definetype,id,cs) os = 220let 221 val _ = Portable.output (os, definetype); 222 val _ = Portable.output (os, id); 223 val _ = Portable.output (os, "}{"); 224 val _ = Portable.output (os, cs); 225 val _ = Portable.output (os, "}\n"); 226in 227 () 228end handle Interrupt => raise Interrupt 229 | _ => () 230 231 232 233fun output_holtex_def command definetype os (id, 234 ({options = options, 235 content = content_opt, 236 printed = printed, 237 latex = latex_opt, 238 ...}:data_entry)) = 239let 240 val cs = if isSome latex_opt then 241 (report_error ("Notice: using user defined latex for "^(command2string command)^" '"^id^"'!");valOf latex_opt) else 242 holmunge_format command id options content_opt; 243 val _ = if (cs = "") then Feedback.fail() else (); 244 val _ = if printed then 245 output_holtex_def_internal (definetype,id,cs) os 246 else (); 247in 248 (id, cs) 249end handle Interrupt => raise Interrupt 250 | _ => (id, "") 251 252 253 254fun process_type_defs os = 255 List.map (output_holtex_def mungeTools.Type "\\defineHOLty{" os) 256 257 258fun process_term_defs os = 259 List.map (output_holtex_def mungeTools.Term "\\defineHOLtm{" os) 260 261fun process_thm_defs os = 262 List.map (output_holtex_def mungeTools.Theorem "\\defineHOLthm{" os) 263 264fun output_all_defs os (thmL, termL, typeL) = 265let 266 val typeDefL = process_type_defs os typeL; 267 val termDefL = process_term_defs os termL; 268 val thmDefL = process_thm_defs os thmL; 269 270 fun list2map l = 271 let 272 val emptyMap = Redblackmap.mkDict String.compare; 273 in 274 List.foldr (fn ((id,d),m) => Redblackmap.insert(m,id,d)) emptyMap l 275 end 276in 277 (list2map thmDefL,list2map termDefL,list2map typeDefL) 278end; 279 280 281(******************************************************************************) 282(* Output index *) 283(******************************************************************************) 284 285 286(* -------------------------------------------------------------------------- *) 287(* comparisons for sorting the index *) 288(* -------------------------------------------------------------------------- *) 289 290val string_compare = String.collate (fn (c1, c2) => 291 Char.compare (Char.toUpper c1, Char.toUpper c2)) 292 293fun entry_list_pos_compare ((id1, de1 as {pos_opt=NONE,...}:data_entry), 294 (id2, de2 as {pos_opt=NONE,...}:data_entry)) = 295 string_compare (id1, id2) 296 | entry_list_pos_compare ((id1, de1 as {pos_opt=SOME _,...}:data_entry), 297 (id2, de2 as {pos_opt=NONE,...}:data_entry)) = 298 LESS 299 | entry_list_pos_compare ((id1, de1 as {pos_opt=NONE,...}:data_entry), 300 (id2, de2 as {pos_opt=SOME _,...}:data_entry)) = 301 GREATER 302 | entry_list_pos_compare ((id1, de1 as {pos_opt=SOME pos1,...}:data_entry), 303 (id2, de2 as {pos_opt=SOME pos2,...}:data_entry)) = 304 305 let 306 val r = Int.compare(pos1,pos2) 307 in if r = EQUAL then string_compare (id1,id2) else r end; 308 309 310fun entry_list_label_compare ((id1, de1 as {label=NONE,...}:data_entry), 311 (id2, de2 as {label=NONE,...}:data_entry)) = 312 entry_list_pos_compare ((id1,de1),(id2,de2)) 313 | entry_list_label_compare ((id1, de1 as {label=SOME _,...}:data_entry), 314 (id2, de2 as {label=NONE,...}:data_entry)) = 315 GREATER 316 | entry_list_label_compare ((id1, de1 as {label=NONE,...}:data_entry), 317 (id2, de2 as {label=SOME _,...}:data_entry)) = 318 LESS 319 | entry_list_label_compare ((id1, de1 as {label=SOME l1,...}:data_entry), 320 (id2, de2 as {label=SOME l2,...}:data_entry)) = 321 let 322 val r = string_compare (l1,l2) 323 in if r = EQUAL then entry_list_pos_compare ((id1,de1),(id2,de2)) else r end 324 325 326fun entry_list_thm_compare ((id1, de1 as {content=NONE,...}:data_entry), 327 (id2, de2 as {content=NONE,...}:data_entry)) = 328 entry_list_label_compare ((id1,de1),(id2,de2)) 329 | entry_list_thm_compare ((id1, de1 as {content=SOME _,...}:data_entry), 330 (id2, de2 as {content=NONE,...}:data_entry)) = 331 GREATER 332 | entry_list_thm_compare ((id1, de1 as {content=NONE,...}:data_entry), 333 (id2, de2 as {content=SOME _,...}:data_entry)) = 334 LESS 335 | entry_list_thm_compare ((id1, de1 as {content=SOME c1,...}:data_entry), 336 (id2, de2 as {content=SOME c2,...}:data_entry)) = 337 let 338 val (theory1,thm1) = destruct_theory_thm c1; 339 val (theory2,thm2) = destruct_theory_thm c2; 340 val r = Lib.list_compare string_compare ([theory1,thm1], [theory2,thm2]) 341 in if r = EQUAL then entry_list_label_compare ((id1,de1),(id2,de2)) else r end 342 343 344(* -------------------------------------------------------------------------- *) 345(* other auxiliary defs *) 346(* -------------------------------------------------------------------------- *) 347 348 349exception nothing_to_do; 350 351fun process_index_pages pages = 352let 353 val pL = Redblackset.listItems pages 354 val pnL = List.map (fn s => (s, Int.fromString s)) pL 355 fun get_int (_, NONE) = 0 356 | get_int (_, (SOME n)) = n 357 val pnL' = Listsort.sort (fn (a,b) => Int.compare (get_int a, get_int b)) pnL; 358 val intL = List.map (fn p => (p,p)) pnL'; 359 360 fun make_intervals [] = [] 361 | make_intervals [pnp] = [pnp] 362 | make_intervals ((pn, (p, NONE))::pnL) = 363 (pn, (p, NONE))::(make_intervals pnL) 364 | make_intervals (pnp::((p, NONE), pn)::pnL) = 365 pnp::((p, NONE),pn)::(make_intervals pnL) 366 | make_intervals ((pn1, (p1,SOME n1))::((p2, SOME n2), pn2)::pnL) = 367 if (n2 = n1 + 1) then 368 make_intervals ((pn1, pn2)::pnL) 369 else 370 (pn1, (p1,SOME n1))::make_intervals(((p2, SOME n2), pn2)::pnL) 371 372 fun remove_intervals [] = [] 373 | remove_intervals (((p1:string, NONE:int option),_)::pnL) = 374 p1::remove_intervals pnL 375 | remove_intervals ((_, (p2, NONE:int option))::pnL) = 376 p2::remove_intervals pnL 377 | remove_intervals (((p1, SOME n1), (p2, SOME n2))::pnL) = 378 if (n1 = n2) then 379 p1::remove_intervals pnL 380 else (if (n2 > n1 + 1) then 381 ((String.concat [p1, "--", p2])::remove_intervals pnL) 382 else (p1::p2::remove_intervals pnL)) 383 384 val sL = remove_intervals (make_intervals intL) 385 val sL' = List.map (fn s => String.concat ["\\hyperpage{", s, "}"]) sL 386in 387 String.concat (commafy sL') 388end; 389 390 391 392fun bool2latex true = "true" 393 | bool2latex false = "false" 394 395fun boolopt2latex (SOME b) def = bool2latex b 396 | boolopt2latex NONE def = def; 397 398fun output_holtex_index d (indextype,flagtype) os (id, 399 ({label = label_opt, 400 full_index = full_index, 401 pages = pages, 402 comment = comment_opt, ...}:data_entry)) = 403let 404 val label = if isSome label_opt then valOf(label_opt) else ""; 405 val _ = Portable.output (os, indextype); 406 val _ = Portable.output (os, id); 407 val _ = Portable.output (os, "}{"); 408 val _ = Portable.output (os, label); 409 val _ = Portable.output (os, "}{"); 410 val _ = Portable.output (os, process_index_pages pages); 411 val _ = Portable.output (os, "}{"); 412 val _ = Portable.output (os, boolopt2latex full_index flagtype); 413 val _ = Portable.output (os, "}{"); 414 val _ = Portable.output (os, bool2latex (not (Redblackset.isEmpty pages))); 415 val _ = Portable.output (os, "}{"); 416 val _ = Portable.output (os, if isSome comment_opt then valOf comment_opt else ""); 417 val _ = Portable.output (os, "}{"); 418 val _ = Portable.output (os, Redblackmap.find (d,id)); 419 val _ = Portable.output (os, "}\n"); 420in 421 () 422end handle Interrupt => raise Interrupt 423 | _ => (); 424 425 426 427fun process_type_index d os typeL = 428let 429 val type_entryL = List.filter (#in_index o snd) typeL; 430 val _ = if null(type_entryL) then raise nothing_to_do else (); 431 val type_entryL' = Listsort.sort entry_list_pos_compare type_entryL; 432 433 val _ = Portable.output(os, " \\begin{HOLTypeIndex}\n"); 434 val _ = List.map (output_holtex_index d (" \\HOLTypeIndexEntry{","holIndexLongTypeFlag") os) type_entryL' 435 val _ = Portable.output(os, " \\end{HOLTypeIndex}\n"); 436in 437 () 438end handle nothing_to_do => (); 439 440 441fun process_term_index d os termL = 442let 443 val term_entryL = List.filter (#in_index o snd) termL; 444 val _ = if null(term_entryL) then raise nothing_to_do else (); 445 val term_entryL' = Listsort.sort entry_list_pos_compare term_entryL; 446 447 val _ = Portable.output(os, " \\begin{HOLTermIndex}\n"); 448 val _ = List.map (output_holtex_index d (" \\HOLTermIndexEntry{","holIndexLongTermFlag") os) term_entryL' 449 val _ = Portable.output(os, " \\end{HOLTermIndex}\n"); 450in 451 () 452end handle nothing_to_do => (); 453 454 455fun process_thm_index d os thmL = 456let 457 val thm_entryL = List.filter (#in_index o snd) thmL; 458 val _ = if null(thm_entryL) then raise nothing_to_do else (); 459 val cmp = if (!use_occ_sort_ref) then entry_list_pos_compare else 460 entry_list_thm_compare 461 val thm_entryL' = Listsort.sort cmp thm_entryL; 462 463 fun thmmapfun (id, de:data_entry) = 464 let 465 val label_opt = #label de; 466 val add_label = if (isSome label_opt) then 467 (" "^(valOf label_opt)) else ""; 468 val content_opt = (#content de); 469 val content = if isSome content_opt then valOf content_opt else id; 470 val (thy,thm) = destruct_theory_thm content; 471 val thythm = if (!use_occ_sort_ref) then 472 (thy^ "Theory."^thm) else thm 473 val new_label = SOME ("\\HOLThmName{"^thythm ^ "}"^add_label); 474 in 475 (id, thy, data_entry___update_label new_label de) 476 end; 477 val thm_entryL'' = List.map thmmapfun thm_entryL'; 478 479 val _ = Portable.output(os, "\\begin{HOLThmIndex}\n"); 480 481 fun foldfun ((id, thy, de), old_thy) = 482 let 483 val _ = if ((!use_occ_sort_ref) orelse (thy = old_thy)) then () else 484 (Portable.output(os, " \\HOLThmIndexTheory{"^thy^"}\n")) 485 val _ = output_holtex_index d (" \\HOLThmIndexEntry{","holIndexLongThmFlag") os (id, de); 486 in 487 thy 488 end; 489 val _ = List.foldl foldfun "" thm_entryL''; 490 val _ = Portable.output(os, "\\end{HOLThmIndex}\n"); 491 492in 493 () 494end handle nothing_to_do => (); 495 496 497 498fun output_all_index os (thmD,termD,typeD) (thmL, termL, typeL) = 499let 500 val _ = process_type_index typeD os typeL; 501 val _ = process_term_index termD os termL; 502 val _ = process_thm_index thmD os thmL; 503 val _ = Portable.output (os, " \n"); 504in 505 () 506end; 507 508 509 510 511 512 513(******************************************************************************) 514(* Put everything together *) 515(******************************************************************************) 516 517(* 518 val basename = Globals.HOLDIR ^ "/src/TeX/holindex-demo"; 519 val file = (basename ^ ".hix") 520 val (thmL, termL, typeL) = parse_hix file 521*) 522 523fun holindex basename = 524let 525 val _ = error_found := false; 526 val ds = parse_hix (basename ^ ".hix") 527 val os = Portable.open_out (basename ^ ".tde") 528 val dd = output_all_defs os ds 529 val _ = Portable.close_out os; 530 val os = Portable.open_out (basename ^ ".tid") 531 val _ = output_all_index os dd ds; 532 val _ = Portable.close_out os; 533 val _ = if (!error_found) then (Process.exit Process.failure) else () 534in 535 () 536end; 537 538end 539