1structure mungeTools :> mungeTools = 2struct 3 4open Lib Feedback HolKernel Parse boolLib 5 6datatype command = Theorem | Term | Type 7datatype opt = Turnstile | Case | TT | Def | SpacedDef | AlignedDef 8 | TypeOf | TermThm 9 | Indent of int * bool 10 (* true: add spaces; false: just alter block indent *) 11 | NoSpec 12 | NoDefSym 13 | Inst of string * string 14 | OverrideUpd of (string * int) * string 15 | TraceSet of string * int 16 | NoTurnstile | Width of int 17 | Mathmode of string | NoMath 18 | AllTT | ShowTypes of int 19 | Conj of int 20 | Rule | StackedRule 21 | RuleName of string 22 | NoDollarParens 23 | Merge | NoMerge 24 | Unoverload of string 25 | Depth of int 26 27val numErrors = ref 0 28type posn = int * int 29 30fun inc ir = (ir := !ir + 1) 31fun warn ((l,c), s) = (TextIO.output(TextIO.stdErr, 32 Int.toString l ^ "." ^ Int.toString c ^ 33 ": " ^ s ^ "\n"); 34 inc numErrors; 35 TextIO.flushOut TextIO.stdErr) 36fun die s = (TextIO.output(TextIO.stdErr, s ^ "\n"); 37 TextIO.flushOut TextIO.stdErr; 38 OS.Process.exit OS.Process.failure) 39fun usage() = 40 die ("Usage:\n "^ 41 CommandLine.name()^ 42 " [-w<linewidth>] [-m[<math-spacing>]] [--nomergeanalysis] " ^ 43 "[overridesfile]\nor\n "^ 44 CommandLine.name()^" -index filename") 45 46fun stringOpt pos s = 47 case s of 48 "|-" => SOME Turnstile 49 | "aligneddef" => SOME AlignedDef 50 | "alltt" => SOME AllTT 51 | "case" => SOME Case 52 | "def" => SOME Def 53 | "K" => SOME TermThm 54 | "merge" => SOME Merge 55 | "nodefsym" => SOME NoDefSym 56 | "nodollarparens" => SOME NoDollarParens 57 | "nomerge" => SOME NoMerge 58 | "nomath" => SOME NoMath 59 | "nosp" => SOME NoSpec 60 | "nostile" => SOME NoTurnstile 61 | "of" => SOME TypeOf 62 | "rule" => SOME Rule 63 | "spaceddef" => SOME SpacedDef 64 | "stackedrule" => SOME StackedRule 65 | "tt" => SOME TT 66 | _ => let 67 in 68 if String.isPrefix "showtypes" s then let 69 val numpart_s = String.extract(s,9,NONE) 70 in 71 if numpart_s = "" then SOME (ShowTypes 1) else 72 case Int.fromString numpart_s of 73 NONE => (warn(pos, s ^ " is not a valid option"); NONE) 74 | SOME i => SOME (ShowTypes i) 75 end 76 else if String.isPrefix "tr'" s then let 77 val sfx = String.extract(s, 3, NONE) 78 val (pfx,eqsfx) = Substring.position "'=" (Substring.full sfx) 79 in 80 if Substring.size eqsfx = 0 then 81 (warn(pos, s ^ " is not a valid option"); NONE) 82 else 83 let 84 val numpart_s = String.extract (Substring.string eqsfx, 2, NONE) 85 in 86 case Int.fromString numpart_s of 87 NONE => (warn(pos, s ^ " is not a valid option"); NONE) 88 | SOME i => SOME(TraceSet(Substring.string pfx, i)) 89 end 90 end 91 else if String.isPrefix ">>" s then 92 let 93 val (addsp, num_i) = 94 if size s > 2 andalso String.sub(s,2) = #"~" then (false, 3) 95 else (true, 2) 96 val numpart_s = String.extract(s,num_i,NONE) 97 in 98 if numpart_s = "" then SOME (Indent (2, addsp)) 99 else 100 case Int.fromString numpart_s of 101 NONE => (warn(pos, s ^ " is not a valid option"); NONE) 102 | SOME i => if i < 0 then 103 (warn(pos, "Negative indents illegal"); NONE) 104 else SOME (Indent (i, addsp)) 105 end 106 else if String.isPrefix "rulename=" s then let 107 val name = String.extract(s,9,NONE) 108 in SOME (RuleName name) end 109 else if String.isPrefix "width=" s then let 110 val numpart_s = String.extract(s,6,NONE) 111 in 112 case Int.fromString numpart_s of 113 NONE => (warn(pos, s ^ " is not a valid option"); NONE) 114 | SOME i => SOME (Width i) 115 end 116 else if String.isPrefix "depth=" s then let 117 val numpart_s = String.extract(s,6,NONE) 118 in 119 case Int.fromString numpart_s of 120 NONE => (warn(pos, s ^ " is not a valid option"); NONE) 121 | SOME i => SOME (Depth i) 122 end 123 else if String.isPrefix "conj" s then let 124 val numpart_s = String.extract(s,4,NONE) 125 in 126 case Int.fromString numpart_s of 127 NONE => (warn(pos, s ^ " is not a valid option"); NONE) 128 | SOME i => if i <= 0 then 129 (warn(pos, "Negative/zero conj specs illegal"); NONE) 130 else SOME (Conj i) 131 end 132 else let 133 open Substring 134 val ss = full s 135 val (pfx,sfx) = position "/" ss 136 fun rmws ss = ss |> dropl Char.isSpace |> dropr Char.isSpace |> string 137 in 138 if size sfx < 2 then 139 if String.isPrefix "m" s then 140 SOME (Mathmode (String.extract(s,1,NONE))) 141 else if String.isPrefix "-" s then 142 if String.size s >= 2 then 143 SOME (Unoverload (String.extract(s,1,NONE))) 144 else 145 (warn (pos, s ^ " is not a valid option"); NONE) 146 else 147 (warn (pos, s ^ " is not a valid option"); NONE) 148 else if size sfx > 2 andalso sub(sfx,1) = #"/" then 149 SOME(OverrideUpd((rmws pfx, size sfx - 2),rmws (slice(sfx,2,NONE)))) 150 else 151 SOME (Inst (rmws pfx, rmws (slice(sfx,1,NONE)))) 152 end 153 end 154 155 156 157type override_map = (string,(string * int))Binarymap.dict 158fun read_overrides fname = let 159 val istrm = TextIO.openIn fname 160 handle _ => usage() 161 fun recurse count acc = 162 case TextIO.inputLine istrm of 163 NONE => acc 164 | SOME line => let 165 open Substring 166 val ss = full line 167 val ss = dropl Char.isSpace (dropr Char.isSpace ss) 168 val acc' = let 169 in 170 if size ss = 0 then acc 171 else let 172 val (word1, ss) = splitl (not o Char.isSpace) ss 173 val word1 = string word1 174 val ss = dropl Char.isSpace ss 175 val (num, ss) = splitl (not o Char.isSpace) ss 176 val word2 = string (dropl Char.isSpace ss) 177 in 178 case Int.fromString (string num) of 179 NONE => (warn ((count,0), 180 fname ^ "(overrides file): --" ^ 181 string (dropr Char.isSpace (full line)) ^ 182 "-- couldn't decode size number. Ignoring."); 183 acc) 184 | SOME n => let 185 in 186 case Binarymap.peek(acc, word1) of 187 NONE => Binarymap.insert(acc, word1, (word2, n)) 188 | SOME _ => (warn ((count,0), 189 fname ^ " rebinds " ^ word1); 190 Binarymap.insert(acc, word1, (word2, n))) 191 end 192 end 193 end 194 in 195 recurse (count + 1) acc' 196 end 197in 198 recurse 1 (Binarymap.mkDict String.compare) before 199 TextIO.closeIn istrm 200end 201 202structure OptSet : sig 203 type elem type set 204 val empty : set 205 val add : elem -> set -> set 206 val addList : elem list -> set -> set 207 val has : elem -> set -> bool 208 val listItems : set -> elem list 209 val fold : (elem * 'a -> 'a) -> 'a -> set -> 'a 210end where type elem = opt = struct 211 type elem = opt 212 type set = elem list 213 val empty = [] 214 fun add e s = e::s 215 fun addList s1 s2 = s1 @ s2 216 fun has e s = Lib.mem e s 217 fun listItems l = l 218 val fold = List.foldl 219end 220 221type optionset = OptSet.set 222 223fun optset_width s = get_first (fn Width i => SOME i | _ => NONE) s 224fun optset_depth s = get_first (fn Depth i => SOME i | _ => NONE) s 225fun spaces 0 = "" 226 | spaces 1 = " " 227 | spaces 2 = " " 228 | spaces 3 = " " 229 | spaces 4 = " " 230 | spaces n = CharVector.tabulate(n, (fn _ => #" ")) 231fun optset_indent s = 232 case get_first (fn Indent i => SOME i | _ => NONE) s of 233 NONE => (0, PP.add_string "") 234 | SOME (i,b) => 235 (i, if b then PP.add_string (spaces i) else PP.add_string "") 236 237fun optset_conjnum s = get_first (fn Conj i => SOME i | _ => NONE) s 238fun optset_mathmode s = get_first (fn Mathmode s => SOME s | _ => NONE) s 239fun optset_showtypes s = get_first (fn ShowTypes i => SOME i | _ => NONE) s 240fun optset_rulename s = get_first (fn RuleName s => SOME s | _ => NONE) s 241fun optset_nomath s = OptSet.has NoMath s 242 243val optset_unoverloads = 244 OptSet.fold (fn (e,l) => case e of Unoverload s => s :: l | _ => l) [] 245 246fun optset_traces opts f = 247 OptSet.fold (fn (e, f) => case e of TraceSet p => trace p f | _ => f) f opts 248 249val HOL = !EmitTeX.texPrefix 250val user_overrides = ref (Binarymap.mkDict String.compare) 251 252fun diag s = (TextIO.output(TextIO.stdErr, s ^ "\n"); 253 TextIO.flushOut TextIO.stdErr) 254fun overrides s = Binarymap.peek (!user_overrides, s) 255 256fun isChar x y = x = y 257 258fun mkinst loc opts tm = let 259 val insts = List.mapPartial (fn Inst(s1,s2) => SOME (s1,s2) | _ => NONE) 260 (OptSet.listItems opts) 261 val (tytheta,insts) = let 262 fun foldthis ((nm1, nm2), (tyacc, instacc)) = 263 if CharVector.sub(nm1,0) = #":" then 264 if CharVector.sub(nm2,0) = #":" then 265 ((Parse.Type [QUOTE nm2] |-> Parse.Type [QUOTE nm1]) :: tyacc, 266 instacc) 267 else (warn (loc, "Type substitution mal-formed"); die "") 268 else if CharVector.sub(nm2,0) = #":" then 269 (warn (loc, "Type substitution mal-formed"); die "") 270 else (tyacc, (nm1,nm2)::instacc) 271 in 272 List.foldl foldthis ([],[]) insts 273 end 274 val tm = Term.inst tytheta tm 275 val vs = FVL [tm] empty_tmset 276 fun foldthis (v, acc) = let 277 val (n,ty) = dest_var v 278 in 279 Binarymap.insert(acc,n,ty) 280 end 281 val vtypemap = HOLset.foldl foldthis (Binarymap.mkDict String.compare) vs 282 fun foldthis ((nm1,nm2),acc) = let 283 val ty = Binarymap.find(vtypemap, nm2) 284 in 285 (mk_var(nm2,ty) |-> mk_var(nm1,ty)) :: acc 286 end handle Binarymap.NotFound => acc 287in 288 (insts, tytheta, foldr foldthis [] insts) 289end 290 291fun mk_s2smap pairs = let 292 fun foldthis ((nm1,nm2), acc) = Binarymap.insert(acc, nm2, nm1) 293 val m = Binarymap.mkDict String.compare 294in 295 List.foldl foldthis m pairs 296end 297 298fun rename m t = let 299 val (v0, _) = dest_abs t 300 val (vnm, vty) = dest_var v0 301in 302 case Binarymap.peek (m, vnm) of 303 NONE => NO_CONV t 304 | SOME newname => ALPHA_CONV (mk_var(newname,vty)) t 305end 306 307fun depth1_conv c t = 308 (TRY_CONV c THENC TRY_CONV (SUB_CONV (depth1_conv c))) t 309 310fun updatef ((k, v), f) x = if x = k then SOME v else f x 311 312fun do_thminsts loc opts th = let 313 val (insts, tytheta, theta) = mkinst loc opts (concl th) 314 val th = INST_TYPE tytheta th 315 val m = mk_s2smap insts 316 val th = if null theta then th else INST theta th 317in 318 CONV_RULE (depth1_conv (rename m)) th 319end 320 321fun do_tminsts loc opts tm = let 322 val (insts, tytheta, theta) = mkinst loc opts tm 323 val tm = Term.inst tytheta tm 324 val tm = if null theta then tm else Term.subst theta tm 325 val m = mk_s2smap insts 326in 327 if null insts then tm 328 else 329 rhs (concl (QCONV (depth1_conv (rename m)) tm)) 330end 331 332local 333 val sm_t = prim_mk_const{Name = "stmarker", Thy = "marker"} 334 val exn = mk_HOL_ERR "EmitTeX" "replace_topeq" 335 "Definition clause not an equality" 336in 337fun replace_topeq tm = 338 let val (eqt,l,r) = 339 case strip_comb tm of 340 (f, [x,y]) => if same_const boolSyntax.equality f then (f, x, y) 341 else raise exn 342 | _ => raise exn 343 in 344 list_mk_comb(mk_icomb(sm_t, eqt), [l,r]) 345 end 346end 347 348local 349 open EmitTeX PP 350 val _ = set_trace "EmitTeX: print datatype names as types" 1 351 exception BadSpec 352 fun getThm spec = let 353 val (theory,theorem) = 354 case String.tokens (isChar #".") spec of 355 [thy,th] => (thy,th) 356 | _ => raise BadSpec 357 in 358 DB.fetch theory theorem 359 end 360 fun block_list begb pfun newl xs = begb (pr_list pfun [newl] xs) 361 type arg = {commpos : posn, argpos : posn, command : command, 362 options : optionset, argument : string} 363 val B = block CONSISTENT 0 364 val nothing = B [] 365in 366 fun replacement (argument:arg as {commpos = pos, argument = spec,...}) = 367 let 368 val {argpos = (argline, argcpos), command, options = opts, ...} = argument 369 val alltt = OptSet.has AllTT opts orelse 370 (command = Theorem andalso not (OptSet.has TT opts)) 371 val rulep = OptSet.has Rule opts orelse OptSet.has StackedRule opts 372 fun rule_print printer term = let 373 val (hs, c) = let 374 val (h, c) = dest_imp term 375 in 376 (strip_conj h, c) 377 end handle HOL_ERR _ => ([], term) 378 open Portable 379 fun addz s = add_stringsz (s, 0) 380 val (sep,hypbegin,hypend) = 381 if OptSet.has StackedRule opts then 382 (addz "\\\\", addz "\\begin{array}{c}", addz "\\end{array}") 383 else 384 (addz "&", nothing, nothing) 385 val rulename = 386 case optset_rulename opts of 387 NONE => nothing 388 | SOME s => B [addz"[\\HOLRuleName{", addz s, addz"}]"] 389 in 390 B [ 391 addz "\\infer", rulename, addz "{\\HOLinline{", 392 printer c, 393 addz "}}{", 394 hypbegin, 395 B ( 396 pr_list (fn t => B [addz "\\HOLinline{", printer t, addz "}"]) 397 [sep] hs 398 ), 399 hypend, addz "}" 400 ] 401 end 402 403 fun clear_overloads slist f = let 404 val tyg = type_grammar() 405 val oldg = term_grammar() 406 val _ = List.app temp_clear_overloads_on slist 407 val _ = List.map hide slist 408 val newg = term_grammar() 409 in 410 (fn x => (temp_set_grammars(tyg,newg); 411 f x before temp_set_grammars(tyg,oldg))) 412 end 413 414 fun optprintermod f = 415 f |> (case optset_showtypes opts of 416 NONE => trace ("types", 0) 417 | SOME i => trace ("types", i)) 418 |> (case optset_depth opts of 419 NONE => (fn f => f) 420 | SOME i => Lib.with_flag (Globals.max_print_depth, i)) 421 |> (if OptSet.has NoDollarParens opts then 422 trace ("EmitTeX: dollar parens", 0) 423 else 424 trace ("EmitTeX: dollar parens", 1)) 425 |> (if OptSet.has NoMerge opts then 426 trace ("pp_avoids_symbol_merges", 0) 427 else (fn f => f)) 428 |> (if OptSet.has Merge opts then 429 trace ("pp_avoids_symbol_merges", 1) 430 else (fn f => f)) 431 |> (case optset_unoverloads opts of 432 [] => (fn f => f) 433 | slist => clear_overloads slist) 434 |> optset_traces opts 435 436 val overrides = let 437 fun foldthis (opt, acc) = 438 case opt of 439 OverrideUpd (newsz,old) => updatef ((old,newsz), acc) 440 | _ => acc 441 in 442 OptSet.fold foldthis overrides opts 443 end 444 fun stdtermprint t = optprintermod (raw_pp_term_as_tex overrides) t 445 446 fun clear_abbrevs slist f = let 447 val oldg = type_grammar() 448 val tmg = term_grammar() 449 val _ = List.app temp_disable_tyabbrev_printing slist 450 val newg = type_grammar() 451 in 452 (fn x => (temp_set_grammars(newg,tmg); 453 f x before temp_set_grammars(oldg,tmg))) 454 end 455 456 fun opttyprintermod f = 457 f |> (case optset_unoverloads opts of 458 [] => (fn f => f) 459 | slist => clear_abbrevs slist) 460 461 fun stdtypeprint t = opttyprintermod (raw_pp_type_as_tex overrides) t 462 463 val start1 = 464 if not alltt andalso not rulep then add_string "\\HOLinline{" 465 else nothing 466 val parse_start = " (*#loc "^ Int.toString argline ^ " " ^ 467 Int.toString argcpos ^"*)" 468 val QQ = QUOTE 469 val result = 470 case command of 471 Theorem => let 472 val thm = getThm spec 473 val thm = 474 if OptSet.has NoSpec opts then thm 475 else 476 case optset_conjnum opts of 477 NONE => SPEC_ALL thm 478 | SOME i => List.nth(map SPEC_ALL (CONJUNCTS (SPEC_ALL thm)), 479 i - 1) 480 handle Subscript => 481 (warn(pos, 482 "Theorem "^spec^ 483 " does not have a conjunct #" ^ 484 Int.toString i); 485 SPEC_ALL thm) 486 val thm = do_thminsts pos opts thm 487 val (ind,iact) = optset_indent opts 488 fun ind_bl p = block CONSISTENT ind [iact, p] 489 in 490 if OptSet.has Def opts orelse OptSet.has SpacedDef opts orelse 491 OptSet.has AlignedDef opts 492 then let 493 val newline = if OptSet.has SpacedDef opts then 494 B [add_newline, add_newline] 495 else add_newline 496 val m = if OptSet.has NoDefSym opts then (fn t => t) 497 else replace_topeq 498 val lines = thm |> CONJUNCTS |> map (m o concl o SPEC_ALL) 499 val pr = 500 if OptSet.has AlignedDef opts then 501 let val overrides' = 502 updatef(("(HOLDefEquality)", 503 ("&\\HOLTokenDefEquality{}&", 1)), 504 overrides) 505 in 506 optprintermod (raw_pp_term_as_tex overrides') 507 end 508 else 509 stdtermprint 510 in 511 ind_bl ( 512 block_list (block INCONSISTENT 0) pr newline lines 513 ) 514 end 515 else if rulep then ind_bl (rule_print stdtermprint (concl thm)) 516 else let 517 val base = raw_pp_theorem_as_tex overrides 518 val printer = optprintermod base 519 val printer = 520 if OptSet.has NoTurnstile opts then 521 trace ("EmitTeX: print thm turnstiles", 0) printer 522 else printer 523 in 524 ind_bl (printer thm) 525 end 526 end 527 | Term => let 528 val term = if OptSet.has TermThm opts then 529 spec |> getThm |> concl |> rand |> do_tminsts pos opts 530 else if OptSet.has Case opts then 531 let 532 open Preterm errormonad 533 val a = Absyn [QQ parse_start, QQ spec] 534 val tm_M = 535 absyn_to_preterm a >- (fn ptm0 => 536 typecheck_phase1 NONE ptm0 >> 537 overloading_resolution ptm0 >- (fn (pt,b) => 538 report_ovl_ambiguity b >> 539 to_term pt)) 540 val tm = smash tm_M Pretype.Env.empty 541 in 542 do_tminsts pos opts tm 543 end 544 else 545 Parse.Term [QQ parse_start, QQ spec] 546 |> do_tminsts pos opts 547 val (ind,iact) = optset_indent opts 548 val s2 = if OptSet.has Turnstile opts then 549 B [add_stringsz ("\\"^HOL^"TokenTurnstile", 2), 550 add_string " "] 551 else nothing 552 in 553 if rulep then 554 block CONSISTENT ind [iact, s2, rule_print stdtermprint term] 555 else block CONSISTENT ind [iact, s2, stdtermprint term] 556 end 557 | Type => let 558 val typ = if OptSet.has TypeOf opts 559 then Parse.Term [QQ parse_start, QQ spec] 560 |> do_tminsts pos opts 561 |> Term.type_of 562 else Parse.Type [QQ parse_start, QQ spec] 563 val (ind, iact) = optset_indent opts 564 in 565 block CONSISTENT ind [iact, stdtypeprint typ] 566 end 567 val final = if not alltt andalso not rulep then add_string "}" 568 else nothing 569 in 570 B [start1, result, final] 571 end handle 572 BadSpec => (warn (pos, spec ^ " does not specify a theorem"); nothing) 573 | HOL_ERR e => (warn (pos, !Feedback.ERR_to_string e); nothing) 574 | e => (warn (pos, "Unknown exception: "^General.exnMessage e); nothing) 575end 576 577fun parseOpts pos opts = let 578 val toks = String.tokens (isChar #",") opts 579 val opts = List.mapPartial (stringOpt pos) toks 580in 581 OptSet.addList opts OptSet.empty 582end 583 584end ; 585