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 {info = result, ...} => result 265 | NONE => (UTF8.translate char_map s, 266 case sz of NONE => String.size s | SOME sz => sz) 267 268 fun smap overrides (s,sz) = 269 case overrides s of 270 NONE => string_map (s,sz) 271 | SOME r => r 272 fun varmunge s = 273 if String.sub(s,0) = #"_" andalso 274 CharVector.all (fn c => Char.isDigit c) (String.extract(s,1,NONE)) 275 then 276 ("\\HOLTokenUnderscore{}", "") 277 else let 278 open Substring 279 val ss = full s 280 val (pfx,primes) = splitr (equal #"'") ss 281 val prime_str_interior = translate (fn _ => "\\prime") primes 282 val prime_str = if prime_str_interior = "" then "" 283 else "\\sp{" ^ prime_str_interior ^ "}" 284 val (core,digits) = splitr Char.isDigit pfx 285 val dsz = size digits 286 val digitstr = if 0 < dsz andalso dsz <= 2 then 287 "\\sb{\\mathrm{" ^ string digits ^ "}}" 288 else string digits 289 val core_s = UTF8.translate (fn "_" => "\\HOLTokenUnderscore{}" 290 | s => s) 291 (string core) 292 in 293 (core_s, digitstr ^ prime_str) 294 end 295 296 val stringmunge = 297 UTF8.translate (fn "\\" => "\\HOLTokenBackslash{}" 298 | "~" => "\\HOLTokenTilde{}" 299 | s => s) 300 301 fun ann_string overrides (s,sz_opt,ann) = let 302 open PPBackEnd 303 val (dollarpfx,dollarsfx,s,szdelta) = 304 if String.sub(s,0) = #"$" andalso size s > 1 then 305 if !dollar_parens then ("(", ")", String.extract(s,1,NONE),2) 306 else ("", "", String.extract(s,1,NONE),0) 307 else ("", "", s,0) 308 fun addann2 ty (s1,s2) = 309 let val base = "\\" ^ !texPrefix ^ ty ^ "{" ^ s1 ^ "}" 310 in 311 if size s2 = 0 then base 312 else 313 "\\ensuremath{" ^ base ^ s2 ^ "}" 314 end 315 fun addann ty s = addann2 ty (s,"") 316 fun smapper s = smap overrides (s, sz_opt) 317 val unmapped_sz = case sz_opt of NONE => size s | SOME i => i 318 val (string_to_print, sz) = 319 case ann of 320 BV _ => apfst (addann2 "BoundVar" o varmunge) (smapper s) 321 | FV _ => apfst (addann2 "FreeVar" o varmunge) (smapper s) 322 | Const _ => apfst (addann "Const") (smapper s) 323 | SymConst _ => apfst (addann "SymConst") (smapper s) 324 | TyOp _ => apfst (addann "TyOp") (smapper s) 325 | Literal StringLit => 326 let 327 val c1i = case UTF8.getChar s of 328 SOME ((_, i), _) => i 329 | NONE => failwith "String literal with no content" 330 val ann = 331 case c1i of 332 34 => (* " *) "StringLit" 333 | 0xAB => (* double guillemet *) "StringLitDG" 334 | 0x2039 => (* single guillemet *) "StringLitSG" 335 | _ => failwith 336 ("Don't understand string literal delimiter: "^s) 337 (* contents of strings are 8-bit chars, but delimiters are 338 potentially Unicode *) 339 in 340 (addann ann 341 (stringmunge 342 (UTF8.substring(s, 1, UTF8.size s - 2))), 343 unmapped_sz) 344 end 345 | Literal FldName => apfst (addann "FieldName") (smapper s) 346 | Literal NumLit => (addann "NumLit" s, unmapped_sz) 347 | Literal CharList => (addann "CharLit" 348 (String.substring(s, 2, size s - 3)), 349 unmapped_sz) 350 | _ => smapper s 351 in 352 smpp.add_stringsz (dollarpfx ^ string_to_print ^ dollarsfx, sz + szdelta) 353 end 354 355 fun add_string overrides (s,sz) = smpp.add_stringsz (smap overrides (s,sz)) 356 fun add_xstring overrides {s,sz,ann} = 357 if isSome ann then ann_string overrides (s,sz,valOf ann) 358 else add_string overrides (s,sz) 359in 360 fun emit_latex overrides = 361 {add_break = smpp.add_break, 362 add_string = (fn s => add_string overrides (s,NONE)), 363 add_xstring = add_xstring overrides, 364 add_newline = smpp.add_newline, 365 ublock = smpp.block, 366 ustyle = fn sty => fn p => p , 367 extras = { 368 tm_grammar_upd = (fn g => g), 369 ty_grammar_upd = (fn g => g), 370 name = "emit_latex" 371 } 372 } 373end; 374 375(* ------------------------------------------------------------------------- *) 376(* pp_datatype_theorem : ppstream -> thm -> unit *) 377(* Pretty-printer for datatype theorems *) 378(* ------------------------------------------------------------------------- *) 379 380val print_datatype_names_as_types = ref false 381val _ = register_btrace ("EmitTeX: print datatype names as types", print_datatype_names_as_types) 382 383val print_datatypes_compactly = ref false 384val _ = register_btrace ("EmitTeX: print datatypes compactly", 385 print_datatypes_compactly) 386 387fun pp_datatype_theorem backend thm = 388let open smpp 389 val {add_string,add_break,ublock,add_newline,add_xstring,...} = backend 390 val S = add_string 391 val SX = add_xstring 392 val BR = add_break 393 val BB = ublock 394 val NL = add_newline 395 val trace = Feedback.trace 396 fun PT0 tm = 397 term_pp.pp_term (Parse.term_grammar()) (Parse.type_grammar()) 398 backend tm 399 val PT = Parse.mlower o (PT0 |> trace ("types", 0)) 400 val TP0 = type_pp.pp_type (Parse.type_grammar()) backend 401 val adest_type = type_grammar.abb_dest_type (Parse.type_grammar()) 402 fun TP ty = 403 if is_vartype ty orelse null (#Args (adest_type ty)) then TP0 ty 404 else 405 S "(" >> BB PP.INCONSISTENT 1 (TP0 ty) >> S")" 406 407 fun strip_type t = 408 if is_vartype t then 409 [t] 410 else 411 case dest_type t of 412 ("fun", [a, b]) => a :: strip_type b 413 | _ => [t] 414 415 fun pp_clause t = 416 let val l = strip_type (type_of t) 417 val ll = length l 418 in 419 BB PP.CONSISTENT 0 ( 420 lift PT t >> 421 (if ll < 2 then nothing 422 else 423 S " " >> 424 BB PP.INCONSISTENT 0 ( 425 mapp (fn x => (TP x >> BR(1,0))) (List.take(l, ll - 2)) >> 426 TP (List.nth(l, ll - 2)) 427 )) 428 ) 429 end 430 431 fun enumerated_type n = 432 let val l = butlast (strip_type (type_of n)) 433 val typ = fst (dest_var n) 434 in 435 all (fn x => fst (dest_type x) = typ) l 436 end 437 438 fun pp_type_name n = 439 let val l = strip_type (type_of n) 440 in 441 TP0 (last (strip_type (hd l))) 442 end 443 444 fun pp_constructor_spec (n, l) = let 445 val PT0 = if !print_datatype_names_as_types then pp_type_name else lift PT 446 val tylen = n |> dest_var |> #1 |> size 447 in 448 if enumerated_type n then 449 BB PP.CONSISTENT 0 ( 450 PT0 n >> S " " >> 451 BB PP.INCONSISTENT (tylen + 1) ( 452 S "=" >> S " " >> 453 pr_list pp_clause (BR(1,0) >> S"|" >> S " ") l 454 ) 455 ) 456 else 457 BB (if !print_datatypes_compactly then PP.INCONSISTENT 458 else PP.CONSISTENT) 2 ( 459 PT0 n >> S " " >> S "=" >> BR(1,2) >> 460 pr_list pp_clause (BR(1,0) >> S"|" >> S " ") l 461 ) 462 end 463 464 fun pp_record_spec ty l = 465 let val ll = tl l 466 fun pp_record x = 467 let 468 val (x,ty) = dest_var x 469 val ann = SOME (PPBackEnd.Literal PPBackEnd.FldName) 470 in 471 BB PP.INCONSISTENT 2 ( 472 SX {s=x,sz=NONE,ann=ann} >> S " " >> S ":" >> BR(1,0) >> 473 TP0 ty 474 ) 475 end 476 in 477 if !KRrecordtypes then ( 478 BB PP.CONSISTENT 3 ( 479 (if !print_datatype_names_as_types then TP0 (snd(dest_var(hd l))) 480 else lift PT (hd l)) >> 481 S " = " >> 482 S "<|" >> BR(1,0) >> 483 pr_list pp_record (S ";" >> BR(1,0)) ll >> 484 BR(1,~3) >> S "|>" 485 ) 486 ) else ( 487 BB PP.CONSISTENT 0 ( 488 (if !print_datatype_names_as_types then TP0 (snd(dest_var(hd l))) 489 else lift PT (hd l)) >> 490 S " =" >> BR(1,2) >> 491 BB PP.CONSISTENT 2 ( 492 S "<|" >> BR(1,0) >> 493 pr_list pp_record (S ";" >> BR(1,0)) ll >> 494 BR(1,~2) >> 495 S "|>" 496 ) 497 ) 498 ) 499 end 500 501 fun pp_binding (n, l) = 502 let val (x,ty) = dest_var n in 503 if x = "record" then 504 pp_record_spec ty l 505 else 506 pp_constructor_spec (n, l) 507 end 508 509 val t = map strip_comb (strip_conj (snd (dest_comb (concl thm)))) 510in 511 BB PP.CONSISTENT 0 (pr_list pp_binding (S " ;" >> NL >> NL) t) 512end; 513 514val datatype_thm_to_string = 515 PP.pp_to_string (!Globals.linewidth) 516 (Parse.mlower o pp_datatype_theorem PPBackEnd.raw_terminal) 517 518fun print_datatypes s = 519 app (fn (_,x) => 520 HOLPP.prettyPrint(print,!Globals.linewidth) 521 (Parse.mlower 522 (pp_datatype_theorem PPBackEnd.raw_terminal x))) 523 (datatype_theorems s); 524 525(* ------------------------------------------------------------------------- *) 526(* Various pretty-printers *) 527(* ------------------------------------------------------------------------- *) 528 529type override_map = string -> (string * int) option 530 531fun UnicodeOff f = trace ("Unicode", 0) f 532 (* can't eta-convert because of value restriction *) 533 534fun raw_pp_term_as_tex overrides tm mdata = 535 term_pp.pp_term (Parse.term_grammar()) 536 (Parse.type_grammar()) 537 (emit_latex overrides) 538 tm 539 mdata 540 (* eta-expanded into the monad for the sake of side-effects *) 541 542fun pp_term_as_tex tm = raw_pp_term_as_tex (K NONE) tm |> UnicodeOff 543 544fun raw_pp_type_as_tex overrides ty md = 545 type_pp.pp_type (Parse.type_grammar()) (emit_latex overrides) ty md 546 547fun pp_type_as_tex ty = UnicodeOff (raw_pp_type_as_tex (K NONE) ty) 548 549val print_thm_turnstile = ref true 550val _ = register_btrace ("EmitTeX: print thm turnstiles", print_thm_turnstile) 551 552fun raw_pp_theorem_as_tex overrides thm = 553 if is_datatype_thm thm then 554 pp_datatype_theorem (emit_latex overrides) thm 555 else 556 let 557 open PP smpp 558 val (turnstrs, width) = 559 if (!print_thm_turnstile) then 560 case overrides "$Turnstile$" of 561 NONE => ([(token_string "Turnstile", 2), (" ",1)], 3) 562 | SOME p => ([p], snd p) 563 else ([], 0) 564 in 565 block INCONSISTENT width ( 566 mapp add_stringsz turnstrs >> 567 raw_pp_term_as_tex overrides (concl thm) 568 ) 569 end; 570 571fun pp_theorem_as_tex ostrm = 572 raw_pp_theorem_as_tex (K NONE) ostrm |> UnicodeOff 573 |> trace ("pp_dollar_escapes", 0) 574 575fun pprint f = PP.prettyPrint (print, !Globals.linewidth) o f 576val pp_type_as_tex = fn ty => Parse.mlower (pp_type_as_tex ty) 577val pp_term_as_tex = fn tm => Parse.mlower (pp_term_as_tex tm) 578val pp_theorem_as_tex = fn th => Parse.mlower (pp_theorem_as_tex th) 579 580val print_term_as_tex = pprint pp_term_as_tex; 581val print_type_as_tex = pprint pp_type_as_tex; 582val print_theorem_as_tex = pprint pp_theorem_as_tex; 583 584val S = PP.add_string 585val NL = PP.add_newline 586val B = PP.block PP.CONSISTENT 0 587 588fun pp_hol_as_tex_command prefix (s, thm) = 589 let 590 val es = prefix ^ tex_command_escape s 591 in 592 B [ 593 S ("\\begin{SaveVerbatim}{" ^ es ^ "}"), NL, 594 pp_theorem_as_tex thm, NL, 595 S "\\end{SaveVerbatim}", NL, 596 S ("\\newcommand{\\" ^ es ^ "}{\\UseVerbatim{" ^ es ^ "}}"), NL 597 ] 598 end; 599 600fun pp_hol_as_tex p s = PP.add_string ("\\" ^ p ^ tex_command_escape s); 601 602fun pp_hol_as_tex_with_tag (p1,p2) s = 603 let val c = p2 ^ tex_command_escape s 604 in 605 B [ 606 S ("\\" ^ p2 ^ "{" ^ !current_theory_name ^ "}" ^ "{" ^ s ^ "}"), 607 pp_hol_as_tex p1 s, NL 608 ] 609 end; 610 611(* ......................................................................... *) 612 613fun pp_newcommand c = PP.add_string ("\\newcommand{\\" ^ c ^ "}{") 614 615fun pp_datatypes_as_tex thms = 616 let val prefix = datatype_prefix() 617 in 618 if null thms then B [] 619 else 620 B ( 621 map (pp_hol_as_tex_command prefix) thms @ 622 [pp_newcommand prefix, NL] @ 623 map (pp_hol_as_tex prefix o fst) thms @ 624 [S "}", NL] 625 ) 626 end; 627 628fun pp_defnitions_as_tex thms = 629 let val prefix = definition_prefix() 630 in 631 PP.block PP.CONSISTENT 0 ( 632 if null thms then [] 633 else 634 map (pp_hol_as_tex_command prefix) thms @ 635 [pp_newcommand prefix, NL] @ 636 map (pp_hol_as_tex_with_tag (prefix, "HOLDfnTag") o fst) thms @ 637 [S "}", NL] 638 ) 639 end; 640 641fun pp_theorems_as_tex thms = 642 let val prefix = theorem_prefix() 643 in 644 B ( 645 if null thms then [] 646 else 647 map (pp_hol_as_tex_command prefix) thms @ 648 [pp_newcommand prefix, NL] @ 649 map (pp_hol_as_tex_with_tag (prefix, "HOLThmTag") o fst) thms @ 650 [S "}", NL] 651 ) 652 end; 653 654fun pp_theory_as_tex name = 655 let val _ = current_theory_name := name 656 val typs = datatype_theorems name 657 val defns = non_type_definitions name 658 val thms = non_type_theorems name 659 val time = Date.fromTimeLocal (stamp name handle HOL_ERR _ => Time.now()) 660 val u = current_trace "Unicode" 661 val _ = set_trace "Unicode" 0 662 in 663 if null typs andalso null defns andalso null thms then 664 (set_trace "Unicode" u; raise Fail (name ^ "Theory is empty.\n")) 665 else 666 B [ 667 pp_newcommand (date_prefix()), 668 S (Date.fmt "%d %B %Y" time), S "}", NL, 669 pp_newcommand (time_prefix()), 670 S (Date.fmt "%H:%M" time), S "}", NL, 671 pp_datatypes_as_tex typs, 672 pp_defnitions_as_tex defns, 673 pp_theorems_as_tex thms 674 ] before (set_trace "Unicode" u; current_theory_name := "") 675 end; 676 677fun print_theory_as_tex name = 678 let val name = case name of "-" => current_theory() | _ => name 679 val path = if !emitTeXDir = "" then !current_path else !emitTeXDir 680 val path = if path = "" then Path.currentArc else path 681 val _ = FileSys.access(path, []) orelse can FileSys.mkDir path 682 val _ = FileSys.access(path, [FileSys.A_WRITE, FileSys.A_EXEC]) 683 orelse failwith ("Cannot create/access directory: " ^ path) 684 val filename = Path.concat(path, prefix_escape name ^ ".tex") 685 val ostrm = TextIO.openOut filename 686 in 687 PP.prettyPrint (curry TextIO.output ostrm, !texLinewidth) 688 (pp_theory_as_tex name) 689 handle e => (TextIO.closeOut ostrm; raise e); 690 TextIO.closeOut ostrm 691 end; 692 693(* ......................................................................... *) 694 695val sec_divide = 696 "% :::::::::::::::::::::::::::::::::::::\ 697 \:::::::::::::::::::::::::::::::::::::"; 698 699val subsec_divide = 700 "% ....................................."; 701 702fun pp_parents_as_tex_doc names = 703 B ( 704 if null names then [S "% No parents", NL] 705 else [ 706 S "\\begin{flushleft}", NL, 707 S ("\\textbf{Built:} " ^ "\\" ^ date_prefix() ^ " \\\\[2pt]"), NL, 708 S "\\textbf{Parent Theories:} ", 709 B (PP.pr_list S [S ",", PP.add_break(1,0)] names), NL, 710 S "\\end{flushleft}", NL 711 ] 712 ) 713 714fun pp_datatypes_as_tex_doc empty = 715 let val i = index_string() ^ "!Datatypes" 716 in 717 B ( 718 if empty then [S "% No datatypes", NL] 719 else [ 720 S "\\subsection{Datatypes}", NL, 721 S i, S "}", NL, 722 S subsec_divide, NL, NL, 723 S ("\\" ^ datatype_prefix()), NL 724 ] 725 ) 726 end; 727 728fun pp_defnitions_as_tex_doc empty = 729 let val i = index_string() ^ "!Definitions" 730 in 731 B ( 732 if empty then [S "% No definitions", NL] 733 else [ 734 S "\\subsection{Definitions}", NL, 735 S i, S "}", NL, 736 S subsec_divide, NL, NL, 737 S ("\\" ^ definition_prefix()), NL 738 ] 739 ) 740 end; 741 742fun pp_theorems_as_tex_doc empty = 743 let val i = index_string() ^ "!Theorems" 744 in 745 B ( 746 if empty then [S "% No theorems", NL] 747 else [ 748 S "\\subsection{Theorems}", NL, 749 S i, S "}", NL, 750 S subsec_divide, NL, NL, 751 S ("\\" ^ theorem_prefix()), NL 752 ] 753 ) 754 end; 755 756fun pp_theory_as_tex_doc name = 757 let val _ = current_theory_name := name 758 val names = parents name handle HOL_ERR _ => [] 759 val typs = datatype_theorems name 760 val defns = non_type_definitions name 761 val thms = non_type_theorems name 762 in 763 B ( 764 if null names then [] 765 else [ 766 S sec_divide, NL, 767 S "\\section{", S name, S " Theory}", NL, 768 S (index_string()), S "}", NL, 769 pp_parents_as_tex_doc names, 770 S sec_divide, NL, NL, 771 pp_datatypes_as_tex_doc (null typs), NL, 772 pp_defnitions_as_tex_doc (null defns), NL, 773 pp_theorems_as_tex_doc (null thms) 774 ] 775 ) before 776 current_theory_name := "" 777 end; 778 779(* ......................................................................... *) 780 781fun pp_theories_as_tex_doc names = 782 B [ 783 S "\\documentclass[", S texOptions, S "]{article}", NL, 784 S "\\usepackage{holtex}", NL, NL, 785 S "\\makeindex", NL, NL, 786 S "\\begin{document}", NL, NL, 787 B (PP.pr_list (fn x => (S ("\\input{" ^ (prefix_escape x) ^ "}"))) 788 [NL] names), NL, 789 S "\\tableofcontents", NL, 790 S "\\cleardoublepage", NL, 791 S "\\HOLpagestyle", NL, NL, 792 B (PP.pr_list pp_theory_as_tex_doc [NL] names), 793 S "\\HOLindex", NL, NL, 794 S "\\end{document}" 795 ] 796 797local 798 fun tex_suffix s = 799 if Path.ext s = SOME "tex" then s 800 else Path.joinBaseExt {base = s, ext = SOME "tex"} 801in 802 fun print_theories_as_tex_doc names path = 803 let val {dir, file} = Path.splitDirFile path 804 val dir = if Path.isAbsolute path orelse !emitTeXDir = "" then 805 dir 806 else 807 Path.concat(!emitTeXDir, dir) 808 val filename = Path.concat(dir, tex_suffix file) 809 val _ = not (FileSys.access (filename, [])) orelse 810 (TextIO.output(TextIO.stdErr, 811 "File " ^ path ^ " already exists.\n"); 812 failwith "File exists") 813 val _ = current_path := dir 814 val _ = app print_theory_as_tex names 815 val _ = current_path := Path.currentArc 816 val ostrm = TextIO.openOut filename 817 in 818 PP.prettyPrint (curry TextIO.output ostrm, !texLinewidth) 819 (pp_theories_as_tex_doc names) 820 handle e => (TextIO.closeOut ostrm; raise e); 821 TextIO.closeOut ostrm 822 end 823end 824 825fun tex_theory s = 826let val c = case s of "-" => current_theory() | _ => s in 827 print_theories_as_tex_doc [c] c 828end; 829 830 831(* lower monadic printers to what signature wants (pprinters) *) 832val raw_pp_type_as_tex = fn ovm => Parse.mlower o raw_pp_type_as_tex ovm 833val raw_pp_term_as_tex = fn ovm => Parse.mlower o raw_pp_term_as_tex ovm 834val raw_pp_theorem_as_tex = fn ovm => Parse.mlower o raw_pp_theorem_as_tex ovm 835 836end 837