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