1structure EmitTeX :> EmitTeX = 2struct 3 4open HolKernel boolLib; 5 6(* ------------------------------------------------------------------------- *) 7(* Configuration *) 8(* ------------------------------------------------------------------------- *) 9 10val texOptions = "11pt, twoside"; 11 12val texLinewidth = ref 64; 13val texPrefix = ref "HOL"; 14val emitTeXDir = ref ""; 15 16val current_theory_name = ref ""; 17val current_path = ref Path.currentArc 18 19fun tex_command_escape s = 20 String.concat (map 21 (fn c => 22 case c of 23 #"_" => "XX" 24 | #"'" => "YY" 25 | #"?" => "QQ" 26 | #"!" => "ZZ" 27 | #"0" => "Zero" 28 | #"1" => "One" 29 | #"2" => "Two" 30 | #"3" => "Three" 31 | #"4" => "Four" 32 | #"5" => "Five" 33 | #"6" => "Six" 34 | #"7" => "Seven" 35 | #"8" => "Eight" 36 | #"9" => "Nine" 37 | _ => String.str c) 38 (String.explode s)); 39 40fun index_string() = 41 "\\index{" ^ 42 (if !current_theory_name = "" then 43 "" 44 else 45 !current_theory_name ^ " Theory@\\textbf {" ^ 46 !current_theory_name ^ " Theory}"); 47 48fun prefix_escape s = !texPrefix ^ (tex_command_escape s); 49 50fun prefix_string() = prefix_escape (!current_theory_name); 51fun datatype_prefix() = prefix_string() ^ "Datatypes"; 52fun definition_prefix() = prefix_string() ^ "Definitions"; 53fun theorem_prefix() = prefix_string() ^ "Theorems"; 54fun date_prefix() = prefix_string() ^ "Date"; 55fun time_prefix() = prefix_string() ^ "Time"; 56 57(* ------------------------------------------------------------------------- *) 58(* datatype_theorems : string -> (string * thm) list *) 59(* Get a list of datatype theorems in the names theory. *) 60(* These have the form |- DATATYPE x *) 61(* *) 62(* non_type_definitions : string -> (string * thm) list *) 63(* A version of DB.definitions that filters out definitions created by *) 64(* Hol_datatype and those containing WFREC. *) 65(* *) 66(* non_type_theorems : string -> (string * thm) list *) 67(* A version of DB.theorems that filters out theorems created by *) 68(* Hol_datatype. *) 69(* ------------------------------------------------------------------------- *) 70 71local 72 fun datatype_defns s = 73 map (fn x => s ^ x) 74 ["_TY_DEF", "_repfns", "_size_def"] 75 76 fun datatype_theorems s = 77 "datatype_" ^ s :: map (fn x => s ^ x) 78 ["_11", "_Axiom", "_case_cong", "_induction", "_nchotomy"] 79 80 fun enumerate_defns s = 81 [s ^ "_BIJ", s ^ "_case", s ^ "_CASE"] 82 83 fun enumerate_thms s = 84 ["num2" ^ s ^ "_ONTO", "num2" ^ s ^ "_thm", "num2" ^ s ^ "_11", 85 s ^ "2num_ONTO", s ^ "2num_thm", s ^ "2num_11", 86 s ^ "_case_def", s ^ "_EQ_" ^ s, 87 s ^ "2num_num2" ^ s, "num2" ^ s ^ "_" ^ s ^ "2num"] 88 89 fun record_defns s flds = 90 let val (l,r) = Substring.position "brss__" (Substring.full s) 91 val big = if Substring.isPrefix "brss__" r then 92 let val n = Substring.string l ^ "brss__sf" ^ 93 Substring.string (Substring.slice (r, 6, NONE)) 94 in [n, n ^ "_fupd"] end 95 else 96 [] 97 in 98 s :: s ^ "_case_def" :: (big @ List.concat 99 (map (fn x => let val y = s ^ "_" ^ x in [y, y ^ "_fupd"] end) flds)) 100 end 101 102 fun record_thms s = 103 ["EXISTS_" ^ s, "FORALL_" ^ s] @ 104 (map (fn x => s ^ x) 105 ["_11", "_accessors", "_accfupds", "_Axiom", "_case_cong", 106 "_component_equality", "_fn_updates", "_updates_eq_literal", 107 "_fupdcanon", "_fupdcanon_comp", "_fupdfupds", "_fupdfupds_comp", 108 "_induction", "_literal_11", "_literal_nchotomy", "_nchotomy"]) 109 110 fun type_defn_names thy tyop = 111 let val tyinfo = TypeBase.read {Thy = thy, Tyop = tyop} in 112 case tyinfo of 113 NONE => [] 114 | SOME x => 115 let val defns = 116 case TypeBasePure.fields_of x of 117 [] => let val constructors = map (fst o dest_const) 118 (TypeBasePure.constructors_of x) 119 in 120 case TypeBasePure.one_one_of x of 121 NONE => enumerate_defns tyop @ constructors 122 | SOME _ => tyop ^ "_case_def" :: constructors 123 end 124 | flds => record_defns tyop (map fst flds) 125 in 126 datatype_defns tyop @ defns 127 end 128 end 129 130 fun type_thm_names thy tyop = 131 let val tyinfo = TypeBase.read {Thy = thy, Tyop = tyop} in 132 case tyinfo of 133 NONE => [] 134 | SOME x => 135 let val thms = 136 case TypeBasePure.fields_of x of 137 [] => (case TypeBasePure.one_one_of x of 138 NONE => tyop ^ "_distinct" :: enumerate_thms tyop 139 | SOME _ => [tyop ^ "_distinct"]) 140 | flds => record_thms tyop 141 in 142 datatype_theorems tyop @ thms 143 end 144 end 145 146 fun datatypes s = 147 map snd (filter (fn x => fst x = s) 148 (map TypeBasePure.ty_name_of 149 (TypeBasePure.listItems (TypeBase.theTypeBase())))) 150 151 fun type_defn_set s = 152 let val thm_names = List.concat (map (type_defn_names s) (datatypes s)) in 153 Redblackset.addList (Redblackset.empty String.compare, thm_names) 154 end 155 156 fun type_thm_set s = 157 let val thm_names = List.concat (map (type_thm_names s) (datatypes s)) in 158 Redblackset.addList (Redblackset.empty String.compare, thm_names) 159 end 160 161 val rec_thm = can (match_term 162 ``f = WFREC (a:'a -> 'a -> bool) (b:('a -> 'b) -> 'a -> 'b)``) o 163 concl o SPEC_ALL 164 165 val lc = String.map Char.toLower 166 fun thm_cmp (a,b) = String.compare (lc (fst a), lc (fst b)) 167 val thm_sort = Listsort.sort thm_cmp 168in 169 fun is_datatype_thm thm = 170 ((fst o dest_const o fst o dest_comb o concl) thm = "DATATYPE") 171 handle HOL_ERR _ => false 172 173 fun datatype_theorems s = 174 let val dtype_thms = matchp is_datatype_thm [s] 175 fun dtype_name s = String.extract(s, 9, NONE) 176 in 177 map (fn x => (dtype_name (snd (fst x)), fst (snd x))) dtype_thms 178 end 179 180 fun non_type_definitions s = 181 List.filter (fn (x,y) => not ((String.sub(x, 0) = #" ") orelse 182 Redblackset.member(type_defn_set s, x) orelse 183 rec_thm y)) 184 (thm_sort (definitions s)) 185 186 fun non_type_theorems s = 187 List.filter (fn x => not ((String.sub(fst x, 0) = #" ") orelse 188 Redblackset.member(type_thm_set s, fst x))) 189 (thm_sort (theorems s)) 190end; 191 192(* ------------------------------------------------------------------------- *) 193(* An emit TeX back end *) 194(* ------------------------------------------------------------------------- *) 195 196fun token_string s = String.concat ["\\", !texPrefix, "Token", s, "{}"]; 197val KRrecordtypes = ref true 198val _ = register_btrace ("EmitTeX: K&R record type defns", KRrecordtypes) 199 200local 201 fun greek s = "\\ensuremath{\\" ^ s ^ "}" 202 fun subn i = "\\ensuremath{\\sb{" ^ Int.toString i ^ "}}" 203 204 val dollar_parens = ref true 205 val _ = register_btrace ("EmitTeX: dollar parens", dollar_parens) 206 207 fun char_map c = 208 case c 209 of "\\" => token_string "Backslash" 210 | "{" => token_string "Leftbrace" 211 | "}" => token_string "Rightbrace" 212 | "\"" => token_string "DoubleQuote" 213 | "$" => "\\$" 214 | "��" => greek "alpha" 215 | "��" => greek "beta" 216 | "��" => greek "gamma" 217 | "��" => greek "Gamma" 218 | "��" => greek "delta" 219 | "��" => greek "Delta" 220 | "��" => greek "epsilon" 221 | "��" => greek "zeta" 222 | "��" => greek "eta" 223 | "��" => greek "theta" 224 | "��" => greek "Theta" 225 | "��" => greek "iota" 226 | "��" => greek "kappa" 227 | "��" => greek "lambda" 228 | "��" => greek "Lambda" 229 | "��" => greek "mu" 230 | "��" => greek "nu" 231 | "��" => greek "xi" 232 | "��" => greek "Xi" 233 | "��" => greek "pi" 234 | "��" => greek "Pi" 235 | "��" => greek "rho" 236 | "��" => greek "sigma" 237 | "��" => greek "varsigma" 238 | "��" => greek "Sigma" 239 | "��" => greek "tau" 240 | "��" => greek "upsilon" 241 | "��" => greek "Upsilon" 242 | "��" => greek "varphi" (* U+03C6 *) 243 | "��" => greek "phi" (* U+03D5 *) 244 | "��" => greek "Phi" (* U+03A6 *) 245 | "��" => greek "chi" 246 | "��" => greek "psi" 247 | "��" => greek "Psi" 248 | "��" => greek "omega" 249 | "��" => greek "Omega" 250 | "���" => subn 1 251 | "���" => subn 2 252 | "���" => subn 3 253 | "���" => subn 4 254 | "���" => subn 5 255 | "���" => subn 6 256 | "���" => subn 7 257 | "���" => subn 8 258 | "���" => subn 9 259 | "���" => subn 0 260 | c => c 261 262 fun string_map (s,sz) = 263 case Binarymap.peek(TexTokenMap.the_map(), s) of 264 SOME result => result 265 | NONE => (UTF8.translate char_map s,case sz of NONE => String.size s | SOME sz => sz) 266 267 fun smap overrides (s,sz) = 268 case overrides s of 269 NONE => string_map (s,sz) 270 | SOME r => r 271 fun varmunge s = 272 if String.sub(s,0) = #"_" andalso 273 CharVector.all (fn c => Char.isDigit c) (String.extract(s,1,NONE)) 274 then 275 "\\HOLTokenUnderscore{}" 276 else let 277 open Substring 278 val ss = full s 279 val (pfx,primes) = splitr (equal #"'") ss 280 val prime_str_interior = translate (fn _ => "\\prime") primes 281 val prime_str = if prime_str_interior = "" then "" 282 else "\\sp{" ^ prime_str_interior ^ "}" 283 val (core,digits) = splitr Char.isDigit pfx 284 val dsz = size digits 285 val digitstr = if 0 < dsz andalso dsz <= 2 then 286 "\\sb{\\mathrm{" ^ string digits ^ "}}" 287 else string digits 288 val core_s = UTF8.translate (fn "_" => "\\HOLTokenUnderscore{}" 289 | s => s) 290 (string core) 291 in 292 core_s ^ digitstr ^ prime_str 293 end 294 295 val stringmunge = 296 UTF8.translate (fn "\\" => "\\HOLTokenBackslash{}" 297 | "~" => "\\HOLTokenTilde{}" 298 | s => s) 299 300 fun ann_string overrides (s,sz_opt,ann) = let 301 open PPBackEnd 302 val (dollarpfx,dollarsfx,s,szdelta) = 303 if String.sub(s,0) = #"$" andalso size s > 1 then 304 if !dollar_parens then ("(", ")", String.extract(s,1,NONE),2) 305 else ("", "", String.extract(s,1,NONE),0) 306 else ("", "", s,0) 307 fun addann ty s = 308 "\\" ^ !texPrefix ^ ty ^ "{" ^ s ^ "}" 309 fun smapper s = smap overrides (s, sz_opt) 310 val unmapped_sz = case sz_opt of NONE => size s | SOME i => i 311 val (string_to_print, sz) = 312 case ann of 313 BV _ => apfst (addann "BoundVar" o varmunge) (smapper s) 314 | FV _ => apfst (addann "FreeVar" o varmunge) (smapper s) 315 | Const _ => apfst (addann "Const") (smapper s) 316 | SymConst _ => apfst (addann "SymConst") (smapper s) 317 | TyOp _ => apfst (addann "TyOp") (smapper s) 318 | Literal StringLit => (addann "StringLit" 319 (stringmunge 320 (String.substring(s, 1, size s - 2))), 321 unmapped_sz) 322 | Literal FldName => apfst (addann "FieldName") (smapper s) 323 | Literal NumLit => (addann "NumLit" s, unmapped_sz) 324 | Literal CharList => (addann "CharLit" 325 (String.substring(s, 2, size s - 3)), 326 unmapped_sz) 327 | _ => smapper s 328 in 329 smpp.add_stringsz (dollarpfx ^ string_to_print ^ dollarsfx, sz + szdelta) 330 end 331 332 fun add_string overrides (s,sz) = smpp.add_stringsz (smap overrides (s,sz)) 333 fun add_xstring overrides {s,sz,ann} = 334 if isSome ann then ann_string overrides (s,sz,valOf ann) 335 else add_string overrides (s,sz) 336in 337 fun emit_latex overrides = 338 {add_break = smpp.add_break, 339 add_string = (fn s => add_string overrides (s,NONE)), 340 add_xstring = add_xstring overrides, 341 add_newline = smpp.add_newline, 342 ublock = smpp.block, 343 ustyle = fn sty => fn p => p , 344 extras = { 345 tm_grammar_upd = (fn g => g), 346 ty_grammar_upd = (fn g => g), 347 name = "emit_latex" 348 } 349 } 350end; 351 352(* ------------------------------------------------------------------------- *) 353(* pp_datatype_theorem : ppstream -> thm -> unit *) 354(* Pretty-printer for datatype theorems *) 355(* ------------------------------------------------------------------------- *) 356 357val print_datatype_names_as_types = ref false 358val _ = register_btrace ("EmitTeX: print datatype names as types", print_datatype_names_as_types) 359 360val print_datatypes_compactly = ref false 361val _ = register_btrace ("EmitTeX: print datatypes compactly", 362 print_datatypes_compactly) 363 364fun pp_datatype_theorem backend thm = 365let open smpp 366 val {add_string,add_break,ublock,add_newline,add_xstring,...} = backend 367 val S = add_string 368 val SX = add_xstring 369 val BR = add_break 370 val BB = ublock 371 val NL = add_newline 372 val trace = Feedback.trace 373 fun PT0 tm = 374 term_pp.pp_term (Parse.term_grammar()) (Parse.type_grammar()) 375 backend tm 376 val PT = Parse.mlower o (PT0 |> trace ("types", 0)) 377 val TP0 = type_pp.pp_type (Parse.type_grammar()) backend 378 val adest_type = type_grammar.abb_dest_type (Parse.type_grammar()) 379 fun TP ty = 380 if is_vartype ty orelse null (#Args (adest_type ty)) then TP0 ty 381 else 382 S "(" >> BB PP.INCONSISTENT 1 (TP0 ty) >> S")" 383 384 fun strip_type t = 385 if is_vartype t then 386 [t] 387 else 388 case dest_type t of 389 ("fun", [a, b]) => a :: strip_type b 390 | _ => [t] 391 392 fun pp_clause t = 393 let val l = strip_type (type_of t) 394 val ll = length l 395 in 396 BB PP.CONSISTENT 0 ( 397 lift PT t >> 398 (if ll < 2 then nothing 399 else 400 S " " >> 401 BB PP.INCONSISTENT 0 ( 402 mapp (fn x => (TP x >> BR(1,0))) (List.take(l, ll - 2)) >> 403 TP (List.nth(l, ll - 2)) 404 )) 405 ) 406 end 407 408 fun enumerated_type n = 409 let val l = butlast (strip_type (type_of n)) 410 val typ = fst (dest_var n) 411 in 412 all (fn x => fst (dest_type x) = typ) l 413 end 414 415 fun pp_type_name n = 416 let val l = strip_type (type_of n) 417 in 418 TP0 (last (strip_type (hd l))) 419 end 420 421 fun pp_constructor_spec (n, l) = let 422 val PT0 = if !print_datatype_names_as_types then pp_type_name else lift PT 423 val tylen = n |> dest_var |> #1 |> size 424 in 425 if enumerated_type n then 426 BB PP.CONSISTENT 0 ( 427 PT0 n >> S " " >> 428 BB PP.INCONSISTENT (tylen + 1) ( 429 S "=" >> S " " >> 430 pr_list pp_clause (BR(1,0) >> S"|" >> S " ") l 431 ) 432 ) 433 else 434 BB (if !print_datatypes_compactly then PP.INCONSISTENT 435 else PP.CONSISTENT) 2 ( 436 PT0 n >> S " " >> S "=" >> BR(1,2) >> 437 pr_list pp_clause (BR(1,0) >> S"|" >> S " ") l 438 ) 439 end 440 441 fun pp_record_spec ty l = 442 let val ll = tl l 443 fun pp_record x = 444 let 445 val (x,ty) = dest_var x 446 val ann = SOME (PPBackEnd.Literal PPBackEnd.FldName) 447 in 448 BB PP.INCONSISTENT 2 ( 449 SX {s=x,sz=NONE,ann=ann} >> S " " >> S ":" >> BR(1,0) >> 450 TP0 ty 451 ) 452 end 453 in 454 if !KRrecordtypes then ( 455 BB PP.CONSISTENT 3 ( 456 (if !print_datatype_names_as_types then TP0 (snd(dest_var(hd l))) 457 else lift PT (hd l)) >> 458 S " = " >> 459 S "<|" >> BR(1,0) >> 460 pr_list pp_record (S ";" >> BR(1,0)) ll >> 461 BR(1,~3) >> S "|>" 462 ) 463 ) else ( 464 BB PP.CONSISTENT 0 ( 465 (if !print_datatype_names_as_types then TP0 (snd(dest_var(hd l))) 466 else lift PT (hd l)) >> 467 S " =" >> BR(1,2) >> 468 BB PP.CONSISTENT 2 ( 469 S "<|" >> BR(1,0) >> 470 pr_list pp_record (S ";" >> BR(1,0)) ll >> 471 BR(1,~2) >> 472 S "|>" 473 ) 474 ) 475 ) 476 end 477 478 fun pp_binding (n, l) = 479 let val (x,ty) = dest_var n in 480 if x = "record" then 481 pp_record_spec ty l 482 else 483 pp_constructor_spec (n, l) 484 end 485 486 val t = map strip_comb (strip_conj (snd (dest_comb (concl thm)))) 487in 488 BB PP.CONSISTENT 0 (pr_list pp_binding (S " ;" >> NL >> NL) t) 489end; 490 491val datatype_thm_to_string = 492 PP.pp_to_string (!Globals.linewidth) 493 (Parse.mlower o pp_datatype_theorem PPBackEnd.raw_terminal) 494 495fun print_datatypes s = 496 app (fn (_,x) => 497 HOLPP.prettyPrint(print,!Globals.linewidth) 498 (Parse.mlower 499 (pp_datatype_theorem PPBackEnd.raw_terminal x))) 500 (datatype_theorems s); 501 502(* ------------------------------------------------------------------------- *) 503(* Various pretty-printers *) 504(* ------------------------------------------------------------------------- *) 505 506type override_map = string -> (string * int) option 507 508fun UnicodeOff f = trace ("Unicode", 0) f 509 (* can't eta-convert because of value restriction *) 510 511fun raw_pp_term_as_tex overrides tm mdata = 512 term_pp.pp_term (Parse.term_grammar()) 513 (Parse.type_grammar()) 514 (emit_latex overrides) 515 tm 516 mdata 517 (* eta-expanded into the monad for the sake of side-effects *) 518 519fun pp_term_as_tex tm = raw_pp_term_as_tex (K NONE) tm |> UnicodeOff 520 521fun raw_pp_type_as_tex overrides ty md = 522 type_pp.pp_type (Parse.type_grammar()) (emit_latex overrides) ty md 523 524fun pp_type_as_tex ty = UnicodeOff (raw_pp_type_as_tex (K NONE) ty) 525 526val print_thm_turnstile = ref true 527val _ = register_btrace ("EmitTeX: print thm turnstiles", print_thm_turnstile) 528 529fun raw_pp_theorem_as_tex overrides thm = 530 if is_datatype_thm thm then 531 pp_datatype_theorem (emit_latex overrides) thm 532 else 533 let 534 open PP smpp 535 val (turnstrs, width) = 536 if (!print_thm_turnstile) then 537 case overrides "$Turnstile$" of 538 NONE => ([(token_string "Turnstile", 2), (" ",1)], 3) 539 | SOME p => ([p], snd p) 540 else ([], 0) 541 in 542 block INCONSISTENT width ( 543 mapp add_stringsz turnstrs >> 544 raw_pp_term_as_tex overrides (concl thm) 545 ) 546 end; 547 548fun pp_theorem_as_tex ostrm = 549 raw_pp_theorem_as_tex (K NONE) ostrm |> UnicodeOff 550 |> trace ("pp_dollar_escapes", 0) 551 552fun pprint f = PP.prettyPrint (print, !Globals.linewidth) o f 553val pp_type_as_tex = fn ty => Parse.mlower (pp_type_as_tex ty) 554val pp_term_as_tex = fn tm => Parse.mlower (pp_term_as_tex tm) 555val pp_theorem_as_tex = fn th => Parse.mlower (pp_theorem_as_tex th) 556 557val print_term_as_tex = pprint pp_term_as_tex; 558val print_type_as_tex = pprint pp_type_as_tex; 559val print_theorem_as_tex = pprint pp_theorem_as_tex; 560 561val S = PP.add_string 562val NL = PP.add_newline 563val B = PP.block PP.CONSISTENT 0 564 565fun pp_hol_as_tex_command prefix (s, thm) = 566 let 567 val es = prefix ^ tex_command_escape s 568 in 569 B [ 570 S ("\\begin{SaveVerbatim}{" ^ es ^ "}"), NL, 571 pp_theorem_as_tex thm, NL, 572 S "\\end{SaveVerbatim}", NL, 573 S ("\\newcommand{\\" ^ es ^ "}{\\UseVerbatim{" ^ es ^ "}}"), NL 574 ] 575 end; 576 577fun pp_hol_as_tex p s = PP.add_string ("\\" ^ p ^ tex_command_escape s); 578 579fun pp_hol_as_tex_with_tag (p1,p2) s = 580 let val c = p2 ^ tex_command_escape s 581 in 582 B [ 583 S ("\\" ^ p2 ^ "{" ^ !current_theory_name ^ "}" ^ "{" ^ s ^ "}"), 584 pp_hol_as_tex p1 s, NL 585 ] 586 end; 587 588(* ......................................................................... *) 589 590fun pp_newcommand c = PP.add_string ("\\newcommand{\\" ^ c ^ "}{") 591 592fun pp_datatypes_as_tex thms = 593 let val prefix = datatype_prefix() 594 in 595 if null thms then B [] 596 else 597 B ( 598 map (pp_hol_as_tex_command prefix) thms @ 599 [pp_newcommand prefix, NL] @ 600 map (pp_hol_as_tex prefix o fst) thms @ 601 [S "}", NL] 602 ) 603 end; 604 605fun pp_defnitions_as_tex thms = 606 let val prefix = definition_prefix() 607 in 608 PP.block PP.CONSISTENT 0 ( 609 if null thms then [] 610 else 611 map (pp_hol_as_tex_command prefix) thms @ 612 [pp_newcommand prefix, NL] @ 613 map (pp_hol_as_tex_with_tag (prefix, "HOLDfnTag") o fst) thms @ 614 [S "}", NL] 615 ) 616 end; 617 618fun pp_theorems_as_tex thms = 619 let val prefix = theorem_prefix() 620 in 621 B ( 622 if null thms then [] 623 else 624 map (pp_hol_as_tex_command prefix) thms @ 625 [pp_newcommand prefix, NL] @ 626 map (pp_hol_as_tex_with_tag (prefix, "HOLThmTag") o fst) thms @ 627 [S "}", NL] 628 ) 629 end; 630 631fun pp_theory_as_tex name = 632 let val _ = current_theory_name := name 633 val typs = datatype_theorems name 634 val defns = non_type_definitions name 635 val thms = non_type_theorems name 636 val time = Date.fromTimeLocal (stamp name handle HOL_ERR _ => Time.now()) 637 val u = current_trace "Unicode" 638 val _ = set_trace "Unicode" 0 639 in 640 if null typs andalso null defns andalso null thms then 641 (set_trace "Unicode" u; raise Fail (name ^ "Theory is empty.\n")) 642 else 643 B [ 644 pp_newcommand (date_prefix()), 645 S (Date.fmt "%d %B %Y" time), S "}", NL, 646 pp_newcommand (time_prefix()), 647 S (Date.fmt "%H:%M" time), S "}", NL, 648 pp_datatypes_as_tex typs, 649 pp_defnitions_as_tex defns, 650 pp_theorems_as_tex thms 651 ] before (set_trace "Unicode" u; current_theory_name := "") 652 end; 653 654fun print_theory_as_tex name = 655 let val name = case name of "-" => current_theory() | _ => name 656 val path = if !emitTeXDir = "" then !current_path else !emitTeXDir 657 val path = if path = "" then Path.currentArc else path 658 val _ = FileSys.access(path, []) orelse can FileSys.mkDir path 659 val _ = FileSys.access(path, [FileSys.A_WRITE, FileSys.A_EXEC]) 660 orelse failwith ("Cannot create/access directory: " ^ path) 661 val filename = Path.concat(path, prefix_escape name ^ ".tex") 662 val ostrm = TextIO.openOut filename 663 in 664 PP.prettyPrint (curry TextIO.output ostrm, !texLinewidth) 665 (pp_theory_as_tex name) 666 handle e => (TextIO.closeOut ostrm; raise e); 667 TextIO.closeOut ostrm 668 end; 669 670(* ......................................................................... *) 671 672val sec_divide = 673 "% :::::::::::::::::::::::::::::::::::::\ 674 \:::::::::::::::::::::::::::::::::::::"; 675 676val subsec_divide = 677 "% ....................................."; 678 679fun pp_parents_as_tex_doc names = 680 B ( 681 if null names then [S "% No parents", NL] 682 else [ 683 S "\\begin{flushleft}", NL, 684 S ("\\textbf{Built:} " ^ "\\" ^ date_prefix() ^ " \\\\[2pt]"), NL, 685 S "\\textbf{Parent Theories:} ", 686 B (PP.pr_list S [S ",", PP.add_break(1,0)] names), NL, 687 S "\\end{flushleft}", NL 688 ] 689 ) 690 691fun pp_datatypes_as_tex_doc empty = 692 let val i = index_string() ^ "!Datatypes" 693 in 694 B ( 695 if empty then [S "% No datatypes", NL] 696 else [ 697 S "\\subsection{Datatypes}", NL, 698 S i, S "}", NL, 699 S subsec_divide, NL, NL, 700 S ("\\" ^ datatype_prefix()), NL 701 ] 702 ) 703 end; 704 705fun pp_defnitions_as_tex_doc empty = 706 let val i = index_string() ^ "!Definitions" 707 in 708 B ( 709 if empty then [S "% No definitions", NL] 710 else [ 711 S "\\subsection{Definitions}", NL, 712 S i, S "}", NL, 713 S subsec_divide, NL, NL, 714 S ("\\" ^ definition_prefix()), NL 715 ] 716 ) 717 end; 718 719fun pp_theorems_as_tex_doc empty = 720 let val i = index_string() ^ "!Theorems" 721 in 722 B ( 723 if empty then [S "% No theorems", NL] 724 else [ 725 S "\\subsection{Theorems}", NL, 726 S i, S "}", NL, 727 S subsec_divide, NL, NL, 728 S ("\\" ^ theorem_prefix()), NL 729 ] 730 ) 731 end; 732 733fun pp_theory_as_tex_doc name = 734 let val _ = current_theory_name := name 735 val names = parents name handle HOL_ERR _ => [] 736 val typs = datatype_theorems name 737 val defns = non_type_definitions name 738 val thms = non_type_theorems name 739 in 740 B ( 741 if null names then [] 742 else [ 743 S sec_divide, NL, 744 S "\\section{", S name, S " Theory}", NL, 745 S (index_string()), S "}", NL, 746 pp_parents_as_tex_doc names, 747 S sec_divide, NL, NL, 748 pp_datatypes_as_tex_doc (null typs), NL, 749 pp_defnitions_as_tex_doc (null defns), NL, 750 pp_theorems_as_tex_doc (null thms) 751 ] 752 ) before 753 current_theory_name := "" 754 end; 755 756(* ......................................................................... *) 757 758fun pp_theories_as_tex_doc names = 759 B [ 760 S "\\documentclass[", S texOptions, S "]{article}", NL, 761 S "\\usepackage{holtex}", NL, NL, 762 S "\\makeindex", NL, NL, 763 S "\\begin{document}", NL, NL, 764 B (PP.pr_list (fn x => (S ("\\input{" ^ (prefix_escape x) ^ "}"))) 765 [NL] names), NL, 766 S "\\tableofcontents", NL, 767 S "\\cleardoublepage", NL, 768 S "\\HOLpagestyle", NL, NL, 769 B (PP.pr_list pp_theory_as_tex_doc [NL] names), 770 S "\\HOLindex", NL, NL, 771 S "\\end{document}" 772 ] 773 774local 775 fun tex_suffix s = 776 if Path.ext s = SOME "tex" then s 777 else Path.joinBaseExt {base = s, ext = SOME "tex"} 778in 779 fun print_theories_as_tex_doc names path = 780 let val {dir, file} = Path.splitDirFile path 781 val dir = if Path.isAbsolute path orelse !emitTeXDir = "" then 782 dir 783 else 784 Path.concat(!emitTeXDir, dir) 785 val filename = Path.concat(dir, tex_suffix file) 786 val _ = not (FileSys.access (filename, [])) orelse 787 (TextIO.output(TextIO.stdErr, 788 "File " ^ path ^ " already exists.\n"); 789 failwith "File exists") 790 val _ = current_path := dir 791 val _ = app print_theory_as_tex names 792 val _ = current_path := Path.currentArc 793 val ostrm = TextIO.openOut filename 794 in 795 PP.prettyPrint (curry TextIO.output ostrm, !texLinewidth) 796 (pp_theories_as_tex_doc names) 797 handle e => (TextIO.closeOut ostrm; raise e); 798 TextIO.closeOut ostrm 799 end 800end 801 802fun tex_theory s = 803let val c = case s of "-" => current_theory() | _ => s in 804 print_theories_as_tex_doc [c] c 805end; 806 807 808(* lower monadic printers to what signature wants (pprinters) *) 809val raw_pp_type_as_tex = fn ovm => Parse.mlower o raw_pp_type_as_tex ovm 810val raw_pp_term_as_tex = fn ovm => Parse.mlower o raw_pp_term_as_tex ovm 811val raw_pp_theorem_as_tex = fn ovm => Parse.mlower o raw_pp_theorem_as_tex ovm 812 813end 814