1structure term_pp :> term_pp = 2struct 3 4open Portable HolKernel term_grammar 5 HOLtokens HOLgrammars GrammarSpecials 6 PrecAnalysis 7 8val PP_ERR = mk_HOL_ERR "term_pp"; 9 10fun PRINT s = print (s ^ "\n") 11fun LEN l = Int.toString (length l) 12fun option_to_string p NONE = "NONE" 13 | option_to_string p (SOME x) = "SOME(" ^ p x ^ ")" 14 15(*--------------------------------------------------------------------------- 16 Miscellaneous syntax stuff. 17 ---------------------------------------------------------------------------*) 18 19fun ellist_size els = 20 let 21 fun recurse A els = 22 case els of 23 [] => A 24 | e::rest => 25 case e of 26 PPBlock(more_els, (sty, ind)) => recurse A (more_els @ rest) 27 | HardSpace n => recurse (A + n) rest 28 | BreakSpace (n, m) => recurse 0 rest 29 | RE (TOK s) => recurse (A + UTF8.size s) rest 30 | _ => recurse 0 rest 31 in 32 recurse 0 els 33 end 34 35val dest_pair = sdest_binop (",", "pair") (PP_ERR "dest_pair" ""); 36val is_pair = Lib.can dest_pair; 37 38fun isSuffix s1 s2 = (* s1 is a suffix of s2 *) let 39 val ss = Substring.full s2 40 val (pref, suff) = Substring.position s1 ss 41in 42 Substring.size suff = String.size s1 43end 44 45fun acc_strip_comb M rands = 46 let val (Rator,Rand) = dest_comb M 47 in acc_strip_comb Rator (Rand::rands) 48 end 49 handle HOL_ERR _ => (M,rands); 50 51fun strip_comb tm = acc_strip_comb tm []; 52 53fun string_of_nspaces n = String.concat (List.tabulate(n, (fn _ => " "))) 54val isPrefix = String.isPrefix 55 56fun lose_constrec_ty {Name,Ty,Thy} = {Name = Name, Thy = Thy} 57 58(* while f is still of functional type, dest_abs the abs term and apply the 59 f to the variable just stripped from the abs *) 60fun apply_absargs f abs = 61 if can dom_rng (type_of f) then let 62 val (v, body) = dest_abs abs 63 in 64 apply_absargs (mk_comb(f, v)) body 65 end 66 else 67 (f, abs) 68 69(*--------------------------------------------------------------------------- 70 Type antiquotations (required in term parser) 71 ---------------------------------------------------------------------------*) 72 73 74val casesplit_munger = ref (NONE: (term -> term * (term * term)list) option) 75fun init_casesplit_munger f = 76 case !casesplit_munger of 77 NONE => casesplit_munger := SOME f 78 | _ => raise PP_ERR "init_casesplit_munger" 79 "casesplit munger already initialised" 80 81exception CaseConversionFailed 82fun convert_case tm = 83 case !casesplit_munger of 84 NONE => raise CaseConversionFailed 85 | (SOME f) => let 86 val (split_on, splits) = f tm 87 handle HOL_ERR _ => raise CaseConversionFailed 88 val _ = not (null splits) orelse raise CaseConversionFailed 89 in 90 (split_on, splits) 91 end 92 93val prettyprint_cases = ref true; 94val prettyprint_cases_dt = ref false; 95val _ = register_btrace ("pp_cases", prettyprint_cases) 96val _ = register_btrace ("pp_cases_dt", prettyprint_cases_dt) 97 98fun prettyprint_cases_name () = if !prettyprint_cases_dt then "dtcase" else "case"; 99 100 101 102(* ---------------------------------------------------------------------- 103 A flag controlling whether to print escaped syntax with a dollar 104 or enclosing parentheses. Thus whether the term mk_comb(+, 3) comes 105 out as 106 $+ 3 107 or 108 (+) 3 109 The parser accepts either form. 110 ---------------------------------------------------------------------- *) 111open HOLPP smpp term_pp_types term_pp_utils 112 113val dollar_escape = ref true 114 115(* When printing with parentheses, make consecutive calls to the 116 supplied printing function (add_string) so that the "tokens" 117 aren't merged prematurely. This is important to catch possible 118 unwanted comment tokens. 119 120 In the dollar-branch, we're happy to have the dollar smashed up 121 against what follows it. *) 122fun dollarise contentpfn parenpfn s = 123 if !dollar_escape then contentpfn ("$" ^ s) >> return (UTF8.size s + 1) 124 else parenpfn "(" >> contentpfn s >> parenpfn ")" >> 125 return (UTF8.size s + 2) 126 127 128val _ = Feedback.register_btrace ("pp_dollar_escapes", dollar_escape); 129 130(* ---------------------------------------------------------------------- 131 Functions for manipulating the "printing info" data that is carried 132 along by the monadic printer 133 ---------------------------------------------------------------------- *) 134 135open smpp term_pp_types term_pp_utils 136infix || ||| 137 138val start_info = dflt_pinfo 139 140fun getlaststring x = 141 (fupdate (fn x => x) >- 142 (fn (i:printing_info) => return (#last_string i))) 143 x 144 145fun setlaststring s = let 146 fun set {seen_frees,current_bvars,last_string,in_gspec} = 147 {seen_frees=seen_frees, current_bvars = current_bvars, 148 last_string = s, in_gspec = in_gspec} 149in 150 fupdate set >> return () 151end 152 153 154(* ---------------------------------------------------------------------- 155 Control symbol merging 156 ---------------------------------------------------------------------- *) 157 158(* A character is symbolic if it is listed on the first line of the 159 symbolic characters given in DESCRIPTION, section 1.1.1(ii) (page 2). 160 The function "Char.contains" is slow on the first argument, but 161 fast on its second argument. 162*) 163 164val avoid_symbol_merges = ref true 165val _ = register_btrace("pp_avoids_symbol_merges", avoid_symbol_merges) 166 167fun creates_comment(s1, s2) = let 168 val last = String.sub(s1, size s1 - 1) 169 val first = String.sub(s2, 0) 170in 171 last = #"(" andalso first = #"*" orelse 172 last = #"*" andalso first = #")" 173end 174 175 176fun avoid_symbolmerge G (add_string, add_xstring, add_break) = let 177 open term_grammar 178 val op>> = smpp.>> 179 infix >> 180 val keywords = #endbinding (specials G) :: grammar_tokens G @ 181 known_constants G 182 val split = term_tokens.user_split_ident keywords 183 fun bad_merge (s1, s2) = let 184 val combined = s1 ^ s2 185 val (x,y) = split combined 186 in 187 y <> s2 188 end handle base_tokens.LEX_ERR _ => true 189 fun new_addxstring f (xstr as {s,sz,ann}) ls = let 190 val allspaces = str_all (equal #" ") s 191 in 192 case s of 193 "" => nothing 194 | _ => (if ls = " " orelse allspaces then f xstr 195 else if not (!avoid_symbol_merges) then f xstr 196 else if String.sub(ls, size ls - 1) = #"\"" then f xstr 197 (* special case the quotation because term_tokens relies on 198 the base token technology (see base_lexer) to separate the 199 end of a string from the next character *) 200 else if creates_comment (ls, s) orelse bad_merge (ls, s) then 201 add_string " " >> f xstr 202 else 203 f xstr) >> 204 setlaststring (if allspaces then " " else s) 205 end 206 fun new_addstring f s = new_addxstring (fn{s,...}=>f s) {s=s,sz=NONE,ann=NONE} 207 fun new_add_break (p as (n,m)) = 208 (if n > 0 then setlaststring " " else nothing) >> add_break p 209in 210 ((fn s => getlaststring >- new_addstring add_string s), 211 (fn xstr => getlaststring >- new_addxstring add_xstring xstr), 212 new_add_break) 213end 214 215 216fun grav_name (Prec(n, s)) = s | grav_name _ = "" 217fun grav_prec (Prec(n,s)) = n | grav_prec _ = ~1 218 219fun pneeded_by_style (rr: term_grammar.rule_record, pgrav, fname, fprec) = 220 case #paren_style rr of 221 Always => true 222 | OnlyIfNecessary => false 223 | NotEvenIfRand => false 224 | ParoundName => grav_name pgrav <> fname 225 | ParoundPrec => grav_prec pgrav <> fprec 226 227fun countP P [] = 0 228 | countP P (x::xs) = if P x then 1 + countP P xs else countP P xs 229val numTMs = countP (fn TM => true | _ => false) 230 231fun find_partial f = 232 let fun find [] = NONE 233 | find (x::xs) = 234 case f x 235 of NONE => find xs 236 | result => result 237 in find end; 238 239 240fun splitP P thelist = let 241 fun with_acc acc [] = acc 242 | with_acc (inlist, outlist) (x::xs) = let 243 in 244 if P x then with_acc (x::inlist, outlist) xs 245 else with_acc (inlist, x::outlist) xs 246 end 247in 248 with_acc ([], []) (List.rev thelist) 249end 250 251fun find_lspec els = 252 let 253 fun find_lspec1 e = 254 case e of 255 ListForm l => SOME l 256 | PPBlock(els, _) => recurse els 257 | _ => NONE 258 and recurse els = 259 case els of 260 [] => NONE 261 | e :: rest => (case find_lspec1 e of NONE => recurse rest | x => x) 262 in 263 recurse els 264 end 265 266fun grule_term_names G grule = let 267 fun lift f (rr as {term_name,timestamp,elements,...}) = 268 if term_name_is_lform term_name then 269 case find_lspec elements of 270 NONE => [] (* probably a bad rule *) 271 | SOME {nilstr,cons,...} => 272 map (fn s => (s, (timestamp, f [rr]))) [nilstr, cons] 273 else if term_name = GrammarSpecials.fnapp_special then [] 274 else 275 [(term_name, (timestamp, f [rr]))] 276 val suffix = lift (SUFFIX o STD_suffix) 277 val prefix = lift (PREFIX o STD_prefix) 278 fun mkifix a = lift (fn rrs => INFIX (STD_infix(rrs, a))) 279 val closefix = lift CLOSEFIX 280 fun bstamp LAMBDA = 0 281 | bstamp (BinderString r) = #timestamp r 282in 283 case grule of 284 PREFIX (STD_prefix list) => List.concat (map prefix list) 285 | PREFIX (BINDER list) => 286 map (fn b => (binder_to_string G b, (bstamp b, PREFIX (BINDER [b])))) list 287 (* binder_to_string is incomplete on LAMBDA, but this doesn't matter 288 here as the information generated here is not used to print 289 pure LAMBDAs *) 290 | SUFFIX (STD_suffix list) => List.concat (map suffix list) 291 | SUFFIX TYPE_annotation => [] 292 | INFIX (STD_infix(list, a)) => List.concat (map (mkifix a) list) 293 | INFIX RESQUAN_OP => [(resquan_special, (0, grule))] 294 | INFIX (FNAPP lst) => 295 (fnapp_special, (0, INFIX (FNAPP []))) :: 296 List.concat (map (mkifix LEFT) lst) 297 | INFIX VSCONS => [(vs_cons_special, (0, INFIX VSCONS))] 298 | CLOSEFIX lst => List.concat (map closefix lst) 299end 300 301exception DoneExit 302 303(* fun symbolic s = List.all HOLsym (String.explode s) *) 304 305fun symbolic s = HOLsym (String.sub(s,String.size(s)-1)); 306 307(* term tm can be seen to have name s according to grammar G *) 308fun has_name G s tm = 309 grammar_name G tm = SOME s orelse 310 (case dest_term tm of 311 VAR(s', _) => s' = s 312 | _ => false) 313 314(* term tm might be the product of parsing name s - 315 weaker than has_name *) 316fun has_name_by_parser G s tm = let 317 val oinfo = term_grammar.overload_info G 318in 319 case dest_term tm of 320 VAR(vnm, _) => vnm = s orelse 321 (case dest_fakeconst_name vnm of 322 SOME{fake,...} => fake = s 323 | NONE => false) 324 | _ => 325 (case Overload.info_for_name oinfo s of 326 NONE => false 327 | SOME {actual_ops,...} => 328 List.exists (fn t => can (match_term t) tm) actual_ops) 329end 330 331(* use of has_name_by_parser for nilstr allows for scenario where you have a 332 chain of cons-like things, and cons does indeed want to print as the cons 333 string, but the bottom nil equivalent would prefer to print some other way 334 (perhaps with Unicode). 335 In this scenario (e.g., in pred_sets, where EMPTY is the bottom of the 336 list-form, but is overloaded to the Unicode symbol for empty set as well 337 as the string "EMPTY"), you probably still want the list-form. 338*) 339fun is_list G (r as {nilstr, cons}) tm = 340 has_name_by_parser G nilstr tm orelse 341 (is_comb tm andalso 342 let 343 val (conshd, tail) = dest_comb tm 344 in 345 is_comb conshd andalso 346 has_name G cons (rator conshd) andalso 347 is_list G r tail 348 end) 349 350(* 351val is_list = fn G => fn (r as {nilstr,cons}) => fn tm => 352 let 353 val b = is_list G r tm 354 in 355 PRINT ("is_list{nilstr=\""^nilstr^"\",cons=\""^cons^"\"}" ^ 356 debugprint G tm ^ " --> " ^ Bool.toString b); 357 b 358 end 359*) 360 361fun str_unicode_ok s = CharVector.all Char.isPrint s 362 363fun overloads_to_string_form G = term_grammar.strlit_map G 364 365fun oi_strip_comb' oinfo t = 366 if current_trace "PP.avoid_unicode" = 0 then Overload.oi_strip_comb oinfo t 367 else Overload.oi_strip_combP oinfo str_unicode_ok t 368 369fun overloading_of_term' oinfo t = 370 if current_trace "PP.avoid_unicode" = 0 then 371 Overload.overloading_of_term oinfo t 372 else 373 Overload.overloading_of_termP oinfo str_unicode_ok t 374 375fun pp_unicode_free ppel = 376 case ppel of 377 PPBlock(ppels, _) => List.all pp_unicode_free ppels 378 | RE (TOK s) => str_unicode_ok s 379 | ListForm {separator,...} => List.all pp_unicode_free separator 380 | _ => true 381 382fun is_unicode_ok_rule r = 383 current_trace "PP.avoid_unicode" = 0 orelse 384 (case r of 385 PREFIX (STD_prefix rrs) => 386 List.all (fn {elements,...} => List.all pp_unicode_free elements) 387 rrs 388 | PREFIX (BINDER bs) => 389 List.all (fn LAMBDA => true | BinderString {tok,...} => str_unicode_ok tok) 390 bs 391 | SUFFIX TYPE_annotation => true 392 | SUFFIX (STD_suffix rrs) => 393 List.all (fn {elements,...} => List.all pp_unicode_free elements) 394 rrs 395 | INFIX (STD_infix (rrs, _)) => 396 List.all (fn {elements,...} => List.all pp_unicode_free elements) 397 rrs 398 | INFIX (FNAPP rrs) => 399 List.all (fn {elements,...} => List.all pp_unicode_free elements) 400 rrs 401 | INFIX VSCONS => true 402 | INFIX RESQUAN_OP => true 403 | CLOSEFIX rrs => 404 List.all (fn {elements,...} => List.all pp_unicode_free elements) 405 rrs) 406 407fun rule_to_rr rule = 408 case rule of 409 INFIX (STD_infix (slist, _)) => slist 410 | PREFIX (STD_prefix slist) => slist 411 | SUFFIX (STD_suffix slist) => slist 412 | CLOSEFIX slist => slist 413 | _ => [] 414 415(* gives the "wrong" lexicographic order, but is more likely to 416 resolve differences with one comparison because types/terms with 417 the same name are rare, but it's quite reasonable for many 418 types/terms to share the same theory *) 419fun nthy_compare ({Name = n1, Thy = thy1}, {Name = n2, Thy = thy2}) = 420 case String.compare(n1, n2) of 421 EQUAL => String.compare(thy1, thy2) 422 | x => x 423 424val pp_print_firstcasebar = ref false 425val _ = register_btrace ("PP.print_firstcasebar", pp_print_firstcasebar) 426 427val unfakeconst = Option.map #fake o GrammarSpecials.dest_fakeconst_name 428 429fun unsafe_style s = 430 let 431 open UTF8 432 fun trans (CP c) = 433 if c = 10(* NL *) then "\\n" 434 else if c = 9 (* TAB *) then "\\t" 435 else if c = 41 (* ")" *) then "\\)" 436 else if UnicodeChars.isSpace_i c andalso c <> 32 (* SPC *) then 437 String.translate 438 (fn c => "\\" ^ 439 StringCvt.padLeft #"0" 3 (Int.toString (Char.ord c))) 440 (UTF8.chr c) 441 else UTF8.chr c 442 | trans (RB b) = "\\" ^ Int.toString b 443 val scpts = safe_explode s 444 val s' = String.concat (map trans scpts) 445 val s'' = if not (null scpts) andalso last scpts = CP 42 (* * *) then 446 s' ^ "\\z" 447 else s' 448 in 449 "$var$(" ^ s'' ^ ")" 450 end 451fun unicode_supdigit 0 = UnicodeChars.sup_0 452 | unicode_supdigit 1 = UnicodeChars.sup_1 453 | unicode_supdigit 2 = UnicodeChars.sup_2 454 | unicode_supdigit 3 = UnicodeChars.sup_3 455 | unicode_supdigit 4 = UnicodeChars.sup_4 456 | unicode_supdigit 5 = UnicodeChars.sup_5 457 | unicode_supdigit 6 = UnicodeChars.sup_6 458 | unicode_supdigit 7 = UnicodeChars.sup_7 459 | unicode_supdigit 8 = UnicodeChars.sup_8 460 | unicode_supdigit 9 = UnicodeChars.sup_9 461 | unicode_supdigit _ = raise Fail "unicode_supdigit: i < 0 or i > 9" 462fun prettynumbers false i = Int.toString i 463 | prettynumbers true i = 464 let 465 fun recurse A i = 466 if i = 0 then String.concat A 467 else 468 recurse (unicode_supdigit (i mod 10) :: A) (i div 10) 469 in 470 if i = 0 then UnicodeChars.sup_0 471 else if i < 0 then UnicodeChars.sup_minus ^ recurse [] (~i) 472 else recurse [] i 473 end 474 475fun vname_styling unicode s = 476 if not (Lexis.is_clean_varname s) then unsafe_style s 477 else 478 let val (s0,n) = Lib.extract_pc s 479 in 480 if n > 2 then s0 ^ "'" ^ prettynumbers unicode n ^ "'" 481 else s 482 end 483 484fun atom_name tm = let 485 val (vnm, _) = dest_var tm 486in 487 case unfakeconst vnm of 488 NONE => vnm 489 | SOME s => s 490end handle HOL_ERR _ => fst (dest_const tm) 491 492fun is_fakeconst tm = let 493 val (vnm, _) = dest_var tm 494in 495 String.isPrefix GrammarSpecials.fakeconst_special vnm 496end handle HOL_ERR _ => false 497 498fun is_constish tm = is_const tm orelse is_fakeconst tm 499 500fun pp_term (G : grammar) TyG backend = let 501 val G = #tm_grammar_upd (#extras backend) G 502 val TyG = #ty_grammar_upd (#extras backend) TyG 503 val block = smpp.block 504 fun tystr ty = 505 PP.pp_to_string 10000 506 (fn ty => 507 lower (type_pp.pp_type TyG PPBackEnd.raw_terminal ty) dflt_pinfo 508 |> valOf |> #1) 509 ty 510 val {restr_binders,lambda,endbinding,type_intro,res_quanop} = specials G 511 val overload_info = overload_info G 512 val spec_table = 513 HOLset.addList (HOLset.empty String.compare, grammar_tokens G) 514 val num_info = numeral_info G 515 fun insert ((nopt, grule), acc) = let 516 val keys_n_rules = grule_term_names G grule 517 val n = case nopt of SOME n => n | NONE => 0 (* doesn't matter *) 518 fun sortinsert (tstamp,r) [] = [(n,tstamp,r)] 519 | sortinsert (tstamp,r) ((h as (_,t',r')) :: rest) = 520 if tstamp < t' then h :: sortinsert (tstamp,r) rest 521 else (n,tstamp,r) :: h :: rest 522 fun val_insert (tstamp,r) NONE = [(n,tstamp,r)] 523 | val_insert (tstamp,r) (SOME l) = sortinsert (tstamp,r) l 524 fun myinsert ((k, (tstamp, r)), acc) = let 525 val existing = Binarymap.peek(acc, k) 526 val newvalue = 527 case existing of 528 NONE => [(n,tstamp,r)] 529 | SOME [] => [(n,tstamp,r)] 530 | SOME ((old as (_,t',_))::rest) => 531 if tstamp > t' then (n,tstamp,r)::old::rest 532 else old::(n,tstamp,r)::rest 533 in 534 Binarymap.insert(acc, k, newvalue) 535 end 536 in 537 (List.foldl myinsert acc keys_n_rules) 538 end 539 val rule_table = List.foldl insert 540 (Binarymap.mkDict String.compare) 541 (term_grammar.rules G) 542 fun lookup_term s = Binarymap.peek(rule_table, s) 543 val comb_prec = #1 (hd (valOf (lookup_term fnapp_special))) 544 handle Option => 545 raise PP_ERR "pp_term" "Grammar has no function application" 546 val recsel_info = (* (precedence, upd_tok) option *) 547 case lookup_term recsel_special of 548 SOME [(n, _, INFIX (STD_infix([{elements = [RE(TOK s)],...}], _)))] => 549 SOME (n, s) 550 | SOME _ => 551 raise PP_ERR "pp_term" "Invalid rule for record field select operator" 552 | NONE => NONE 553 val recupd_info = (* (precedence, upd_tok) option *) 554 case lookup_term recupd_special of 555 SOME [(n, _, INFIX (STD_infix([{elements = [RE(TOK s)],...}], _)))] => 556 SOME (Prec(n, recupd_special), s) 557 | SOME _ => 558 raise PP_ERR "pp_term" "Invalid rule for record update operator" 559 | NONE => NONE 560 val recfupd_info = (* (precedence, with_tok) option *) 561 case lookup_term recfupd_special of 562 SOME [(n, _, INFIX (STD_infix([{elements = [RE(TOK s)],...}], _)))] => 563 SOME (Prec(n, recfupd_special), s) 564 | SOME _ => 565 raise PP_ERR "pp_term" "Invalid rule for record f-update operator" 566 | NONE => NONE 567 val recwith_info = (* (precedence, with_tok) option *) 568 case (lookup_term recwith_special) of 569 SOME [(n, _, INFIX (STD_infix([{elements = [RE(TOK s)],...}], _)))] => 570 SOME (n, s) 571 | SOME _ => 572 raise PP_ERR "pp_term" 573 "Invalid form of rule for record with \"operator\"" 574 | NONE => NONE 575 val reclist_info = (* (leftdelim, rightdelim, sep) option *) 576 case lookup_term reccons_special of 577 SOME [(_, _, CLOSEFIX[{elements,...}])] => 578 let 579 fun find_listform pfx els = 580 case els of 581 [] => raise PP_ERR "pp_term" "No list-form in record literal rule" 582 | ListForm{separator,...} :: rest => 583 (List.rev pfx, rest, separator) 584 | e :: rest => find_listform (e::pfx) rest 585 in 586 SOME (find_listform [] elements) 587 end 588 | SOME _ => 589 raise PP_ERR "pp_term" 590 "Invalid form of rule for record update list" 591 | NONE => NONE 592 593 594 val resquan_op_prec = 595 case (lookup_term resquan_special) of 596 SOME [] => raise Fail "term_pp : This really shouldn't happen" 597 | SOME (x::xs) => SOME (#1 x) 598 | NONE => NONE 599 val vscons_prec = #1 (hd (valOf (lookup_term vs_cons_special))) 600 handle Option => 601 raise PP_ERR "pp_term" "Grammar has no vstruct cons" 602 val open_res_list_allowed = 603 case resquan_op_prec of 604 NONE => false 605 | SOME p => p < vscons_prec 606 607 val uprinters = user_printers G 608 val printers_exist = FCNet.size uprinters > 0 609 610 val my_dest_abs = term_pp_utils.pp_dest_abs G 611 val my_is_abs = term_pp_utils.pp_is_abs G 612 613 fun dest_vstruct bndr res t = 614 term_pp_utils.dest_vstruct G {binder = bndr, restrictor = res} t 615 616 617 618 fun strip_vstructs bndr res tm = 619 term_pp_utils.strip_vstructs G {binder = bndr, restrictor = res} tm 620 621 622 datatype comb_posn = RatorCP | RandCP | NoCP 623 624 fun pr_term binderp showtypes showtypes_v ppfns combpos (tm:term) 625 pgrav lgrav rgrav depth apps = 626 let 627 val full_pr_term = pr_term 628 val pr_term = pr_term binderp showtypes showtypes_v ppfns combpos 629 fun pr0 tm = pr_term0 binderp showtypes showtypes_v ppfns combpos tm 630 pgrav lgrav rgrav 631 depth 632 in 633 if printers_exist then 634 let 635 fun sysprint { gravs = (pg,lg,rg), binderp, depth} tm = 636 full_pr_term binderp showtypes showtypes_v ppfns combpos tm 637 pg lg rg depth 638 fun test (pat,_,_) = FCNet.can_match_term pat tm 639 val candidates = filter test (FCNet.match tm uprinters) 640 fun printwith f = f (TyG, G) 641 backend sysprint ppfns 642 (pgrav, lgrav, rgrav) 643 depth tm 644 fun runfirst [] = pr0 tm 645 | runfirst ((_, "", _) :: _) = pr0 tm 646 | runfirst ((_,_,f)::t) = 647 (printwith f 648 handle UserPP_Failed => runfirst t) || runfirst t 649 in 650 runfirst candidates 651 end 652 else pr0 tm 653 end apps 654 and pr_term0 binderp showtypes showtypes_v ppfns combpos tm 655 pgrav lgrav rgrav depth apps = 656 let 657 val full_pr_term = pr_term 658 val pr_term = pr_term binderp showtypes showtypes_v ppfns NoCP 659 val {add_string,add_break,add_xstring,...} = ppfns 660 fun add_ann_string (s,ann) = add_xstring {s=s,ann=SOME ann,sz=NONE} >> 661 return (UTF8.size s) 662 fun uadd_ann_string x = add_ann_string x >> return () 663 fun var_ann t s = let 664 val (vnm, ty) = dest_var t 665 fun k bvs = 666 add_ann_string(s, 667 ((if HOLset.member(bvs, t) then PPBackEnd.BV 668 else PPBackEnd.FV) 669 (ty, fn () => vnm ^ " :" ^ tystr ty))) 670 in 671 getbvs >- k 672 end 673 674 fun constann t s = let 675 val (Thy,Name,Ty,fake) = let 676 val {Thy,Name,Ty} = dest_thy_const t 677 in 678 (Thy,Name,Ty,Name) 679 end handle HOL_ERR _ => let 680 val (s, ty) = dest_var t 681 in 682 case GrammarSpecials.dest_fakeconst_name s of 683 SOME{original = SOME{Thy,Name},fake} => (Thy,Name,ty,fake) 684 | SOME{original = NONE, fake} => ("", fake, ty, fake) 685 | NONE => raise mk_HOL_ERR "term_pp" "constann" 686 "Called on non-const (fake or o/wise)" 687 end 688 fun isAlphaNum_ish c = Char.isAlphaNum c orelse c = #"'" orelse c = #"_" 689 val constr = if CharVector.all isAlphaNum_ish s then PPBackEnd.Const 690 else PPBackEnd.SymConst 691 in 692 add_ann_string(s, constr {Thy = Thy, Name = Name, Ty = (Ty, fn () => tystr Ty)}) 693 end 694 fun block_by_style (rr, pgrav, fname, fprec) = let 695 val needed = 696 case #1 (#block_style (rr:rule_record)) of 697 AroundSameName => grav_name pgrav <> fname 698 | AroundSamePrec => grav_prec pgrav <> fprec 699 | AroundEachPhrase => true 700 | NoPhrasing => false 701 in 702 if needed then 703 let 704 val (c, i) = #2 (#block_style rr) 705 in 706 block c i 707 end 708 else 709 I 710 end 711 fun paren b p = 712 if b then 713 block INCONSISTENT 1 ( 714 add_string "(" >> (p >- (fn r => add_string ")" >> return r)) 715 ) 716 else p 717 718 fun spacep b = if b then add_break(1, 0) else nothing 719 fun hardspace n = add_string (string_of_nspaces n) 720 fun sizedbreak n = add_break(n, 0) 721 722 fun doTy ty = 723 type_pp.pp_type_with_depth TyG backend (decdepth depth) ty 724 725 (* Prints "elements" from a concrete syntax rule. 726 727 els is the list of pp_elements; 728 args is a list of terms to be inserted in place of RE TM elements; 729 fopt is a term corresponding to the constant (if any) at the head 730 position of the term. 731 732 Returns the unused args *) 733 fun print_ellist fopt (lprec, cprec, rprec) (els, args : term list) = let 734 (* val _ = PRINT 735 ("print_ellist: "^Int.toString (length els)^" elements; "^ 736 " args = [" ^ 737 String.concatWith ", " (map (debugprint G) args) ^ "]") *) 738 fun onetok acc [] = acc 739 | onetok NONE (RE (TOK s) :: rest) = onetok (SOME s) rest 740 | onetok (SOME _) (RE (TOK s) :: rest) = NONE 741 | onetok acc (_ :: rest) = onetok acc rest 742 val tok_string = 743 case (fopt, onetok NONE els) of 744 (SOME f, SOME _) => 745 if is_constish f then constann f else var_ann f 746 | _ => (fn s => add_string s >> return (UTF8.size s)) 747 fun addwidth (SOME n) a = 748 a >- (fn (r,NONE) => return (r,NONE) 749 | (r,SOME m) => return (r, SOME (m + n))) 750 | addwidth NONE a = a >- (fn (r, _) => return (r, NONE)) 751 fun recurse (els, args) = 752 case els of 753 [] => return (args, SOME 0) 754 | (e :: es) => let 755 (* val _ = PRINT ("print_ellist.recurse.cons: "^ 756 Int.toString (length args) ^ " args") *) 757 in 758 case e of 759 PPBlock(more_els, (sty, ind)) => 760 block sty ind (recurse (more_els,args)) >- 761 (fn (rest, nopt) => addwidth nopt (recurse (es,rest))) 762 | HardSpace n => 763 hardspace n >> addwidth (SOME n) (recurse (es, args)) 764 | BreakSpace (n, m) => 765 add_break(n,m) >> addwidth NONE (recurse (es, args)) 766 | RE (TOK s) => (tok_string s >- 767 (fn m => addwidth (SOME m) (recurse (es, args)))) 768 | RE TM => (pr_term (hd args) Top Top Top (decdepth depth) >> 769 addwidth NONE (recurse (es, tl args))) 770 | RE (ListTM _) => raise Fail "term_pp - encountered (RE ListTM)" 771 | FirstTM => 772 pr_term (hd args) cprec lprec cprec (decdepth depth) >> 773 addwidth NONE (recurse (es, tl args)) 774 | LastTM => 775 pr_term (hd args) cprec cprec rprec (decdepth depth) >> 776 addwidth NONE(recurse (es, tl args)) 777 | EndInitialBlock _ => raise Fail "term_pp - encountered EIB" 778 | BeginFinalBlock _ => raise Fail "term_pp - encountered BFB" 779 | ListForm lspec => 780 pr_lspec lspec (hd args) >- 781 (fn wopt => addwidth wopt (recurse (es, tl args))) 782 end 783 and pr_lspec (r as {nilstr, cons, block_info,...}) t = 784 let 785 (* val _ = PRINT ("pr_lspec: "^debugprint G t^" {nilstr=\""^nilstr^ 786 "\"}")*) 787 val sep = #separator r 788 (* val (consistency, breakspacing) = block_info *) 789 (* list will never be empty *) 790 fun pr_list tm = let 791 fun lrecurse depth tm = let 792 val (_, args) = strip_comb tm 793 val head = hd args 794 handle Empty => raise Fail ("pr_list empty list with t = "^ 795 debugprint G t) 796 val tail = List.nth(args, 1) 797 in 798 if depth = 0 then add_string "..." 799 else if has_name_by_parser G nilstr tail then 800 (* last element *) 801 pr_term head Top Top Top (decdepth depth) 802 else let 803 in 804 pr_term head Top Top Top (decdepth depth) >> 805 recurse (sep, []) >> 806 lrecurse (decdepth depth) tail 807 end 808 end 809 in 810 lrecurse depth t 811 end 812 in 813 if has_name_by_parser G nilstr t then return (SOME 0) 814 else pr_list t >> return NONE 815 end 816 in 817 recurse (els, args) (* before 818 PRINT "print_ellist terminated" *) 819 end 820 821 822 823 fun pr_vstruct bv = let 824 val pr_t = 825 if showtypes then full_pr_term true true showtypes_v ppfns NoCP 826 else full_pr_term true false showtypes_v ppfns NoCP 827 in 828 case bv of 829 Simple tm => let 830 in 831 if (is_pair tm orelse is_var tm) then 832 record_bvars (free_vars tm) 833 (pr_t tm Top Top Top (decdepth depth)) 834 else 835 raise PP_ERR "pr_vstruct" 836 "Can only handle pairs and vars as vstructs" 837 end 838 | Restricted{Bvar, Restrictor} => let 839 in 840 block CONSISTENT 0 841 (add_string "(" >> 842 pr_vstruct (Simple Bvar) >> 843 add_string (res_quanop) >> 844 add_break(0,2) >> 845 pr_term Restrictor Top Top Top (decdepth depth) >> 846 add_string ")") 847 end 848 end 849 850 (* this function is only called in circumstances when all of a 851 vstruct list is restricted with the same term and when the 852 relative precedences of the res_quan_op (traditionally "::") is 853 less than that of VSCONS. If this situation pertains, then we 854 can print out all of the vstruct items in a row, and then 855 finish off with a single :: <tm>. For example \x y z::Q. 856 857 The accompanying can_print_vstructl function spots when the 858 situation as described above pertains. 859 860 One final wrinkle has to be dealt with: 861 The restricting term might have an occurrence in it of 862 something that needs to be printed so that it looks like the 863 endbinding token. If this happens, then the restriction needs 864 to be parenthesised. In particular, the standard syntax has 865 "." as the endbinding token and as the infix record selection 866 operator, so that if you write 867 !x y :: (rec.fld1). body 868 the parenthesisation needs to be preserved. 869 870 So, we have one last auxiliary function which determines whether 871 or not the restrictor might print an endbinding token. *) 872 873 infix might_print nmight_print 874 fun tm nmight_print str = let 875 val {Name,...} = dest_thy_const tm 876 val actual_name0 = 877 case overloading_of_term' overload_info tm of 878 NONE => Name 879 | SOME s => s 880 fun testit s = if isPrefix s actual_name0 then SOME s else NONE 881 val actual_name = 882 case find_partial testit [recsel_special, recupd_special, 883 recfupd_special] of 884 NONE => actual_name0 885 | SOME s => s 886 val rule = lookup_term actual_name 887 in 888 case rule of 889 NONE => Name = str 890 | SOME rrlist => 891 List.exists (mem str o term_grammar.rule_tokens G o #3) rrlist 892 end 893 894 fun tm might_print str = 895 case (dest_term tm) of 896 COMB(Rator, Rand) => Rator might_print str orelse Rand might_print str 897 | LAMB(_,Body) => Body might_print str 898 | VAR(Name,Ty) => Name = str 899 | CONST x => tm nmight_print str 900 901 902 fun pr_res_vstructl restrictor res_op vsl body = let 903 val bvts = map bv2term vsl 904 val simples = map Simple bvts 905 val add_final_parens = restrictor might_print endbinding 906 in 907 block CONSISTENT 2 ( 908 block INCONSISTENT 2 (pr_list pr_vstruct (add_break(1,0)) simples) >> 909 add_string res_op >> 910 paren add_final_parens ( 911 pr_term restrictor Top Top Top (decdepth depth) 912 ) 913 ) >> 914 add_string endbinding >> add_break (1,0) >> 915 record_bvars (free_varsl bvts) 916 (block CONSISTENT 0 917 (pr_term body Top Top Top (decdepth depth))) 918 end 919 fun can_print_vstructl vsl = let 920 fun recurse acc _ [] = SOME acc 921 | recurse acc _ ((Simple _)::_) = NONE 922 | recurse acc bvs (Restricted{Restrictor = t,Bvar}::xs) = let 923 in 924 if aconv t acc andalso List.all (fn v => not (free_in v t)) bvs then 925 recurse acc (Bvar::bvs) xs 926 else NONE 927 end 928 in 929 case vsl of 930 [] => raise PP_ERR "can_print_vstructl" "Empty list!" 931 | (Simple _::xs) => NONE 932 | (Restricted{Restrictor = t,Bvar}::xs) => recurse t [Bvar] xs 933 end 934 935 (* the pr_vstructl function figures out which way to print a given 936 list of vstructs *) 937 fun pr_vstructl vsl b = 938 case can_print_vstructl vsl of 939 SOME r => pr_res_vstructl r res_quanop vsl b 940 | _ => 941 let 942 fun recurse [] = raise Fail "pr_vstructl.recurse: Empty List!" 943 | recurse [bv] = 944 pr_vstruct bv >> add_string endbinding >> add_break (1,0) >> 945 record_bvars (free_vars (bv2term bv)) 946 (block CONSISTENT 0 947 (pr_term b Top Top Top (decdepth depth))) 948 | recurse (bv::rest) = 949 pr_vstruct bv >> add_break (1,0) >> 950 record_bvars (free_vars (bv2term bv)) (recurse rest) 951 in 952 block INCONSISTENT 2 (recurse vsl) 953 end 954 955 fun pr_abs tm = let 956 val addparens = lgrav <> RealTop orelse rgrav <> RealTop 957 val restr_binder = 958 find_partial (fn (b,s) => if b = NONE then SOME s else NONE) 959 restr_binders 960 val (bvars, body) = strip_vstructs NONE restr_binder tm 961 val bvars_seen_here = List.concat (map (free_vars o bv2term) bvars) 962 val lambda' = if current_trace "PP.avoid_unicode" > 0 then 963 List.filter str_unicode_ok lambda 964 else lambda 965 val tok = case lambda' of 966 [] => raise PP_ERR "pr_abs" "No token for lambda abstraction" 967 | h::_ => h 968 in 969 paren addparens 970 (block CONSISTENT 2 (add_string tok >> pr_vstructl bvars body)) 971 end 972 973 fun can_pr_numeral stropt = List.exists (fn (k,s') => s' = stropt) num_info 974 fun pr_numeral injtermopt tm = let 975 open Overload 976 val numty = Type.mk_thy_type {Tyop="num", Thy="num", Args=[]} 977 val num2numty = numty --> numty 978 val numinfo_search_string = Option.map (fst o dest_const) injtermopt 979 val inj_t = 980 case injtermopt of 981 NONE => mk_thy_const {Name = nat_elim_term, Thy = "arithmetic", 982 Ty = numty --> numty} 983 | SOME t => t 984 val injty = type_of inj_t 985 val is_a_real_numeral = (* i.e. doesn't need a suffix *) 986 case info_for_name overload_info fromNum_str of 987 NONE => false 988 | SOME oi => op_mem aconv inj_t (#actual_ops oi) 989 val numeral_str = Arbnum.toString (Literal.dest_numeral tm) 990 val sfx = 991 if not is_a_real_numeral orelse !Globals.show_numeral_types then let 992 val (k, _) = 993 valOf (List.find (fn (_, s') => s' = numinfo_search_string) 994 num_info) 995 in 996 str k 997 end 998 else "" 999 in 1000 paren showtypes ( 1001 add_ann_string (numeral_str ^ sfx, 1002 PPBackEnd.Literal PPBackEnd.NumLit) >> 1003 (if showtypes then 1004 add_string (" "^type_intro) >> 1005 block INCONSISTENT (1 + UTF8.size (numeral_str ^ sfx) + 1006 UTF8.size type_intro) 1007 (doTy (#2 (dom_rng injty))) >> 1008 setlaststring " " 1009 else nothing) 1010 ) 1011 end 1012 1013 exception NotReallyARecord 1014 1015 fun check_for_field_selection t1 t2 = let 1016 fun getfldname s = 1017 if isSome recsel_info then 1018 if isPrefix recsel_special s then 1019 SOME (String.extract(s, size recsel_special, NONE), t2) 1020 else NONE 1021 else NONE 1022 in 1023 if is_const t1 orelse is_fakeconst t1 then 1024 case grammar_name G t1 of 1025 SOME s => let 1026 val fldname = getfldname s 1027 in 1028 case fldname of 1029 SOME(fldname, t2) => let 1030 val (prec0, fldtok) = valOf recsel_info 1031 (* assumes that field selection is always left associative *) 1032 val add_l = 1033 case lgrav of 1034 Prec(n, _) => n >= prec0 1035 | _ => false 1036 val add_r = 1037 case rgrav of 1038 Prec(n, _) => n > prec0 1039 | _ => false 1040 val prec = Prec(prec0, recsel_special) 1041 val add_parens = add_l orelse add_r 1042 val lprec = if add_parens then Top else lgrav 1043 open PPBackEnd 1044 in 1045 block INCONSISTENT 0 ( 1046 paren add_parens ( 1047 pr_term t2 prec lprec prec (decdepth depth) >> 1048 add_string fldtok >> 1049 add_break(0,0) >> 1050 add_ann_string (fldname, Literal FldName) >> return () 1051 ) 1052 ) 1053 end 1054 | NONE => fail 1055 end 1056 | NONE => fail 1057 else fail 1058 end 1059 1060 fun check_for_record_update wholetm t1 t2 = 1061 if isSome recwith_info andalso isSome reclist_info andalso 1062 isSome recfupd_info andalso isSome recupd_info 1063 then let 1064 open Overload 1065 fun ap1 t = let val (d,_) = dom_rng (type_of t) 1066 in mk_comb(t,genvar d) end 1067 fun ap2 t = t |> ap1 |> ap1 1068 val fupdhelper = Option.map (atom_name o #1) o 1069 Overload.oi_strip_comb overload_info 1070 fun fupdstr0 wholetm_opt t = 1071 case wholetm_opt of 1072 NONE => t |> ap2 |> fupdhelper 1073 | SOME t => t |> fupdhelper 1074 fun fupdstr wholetm_opt = 1075 Option.join o Lib.total (fupdstr0 wholetm_opt) 1076 (* function to determine if t is a record update *) 1077 fun is_record_update wholetm_opt t = 1078 if is_comb t andalso is_const (rator t) then 1079 case fupdstr wholetm_opt (rator t) of 1080 SOME s => isPrefix recfupd_special s 1081 | NONE => false 1082 else false 1083 (* descend the rands of a term until one that is not a record 1084 update is found. Return this and the list of rators up to 1085 this point. *) 1086 fun find_first_non_update acc t = 1087 if is_comb t andalso is_record_update NONE (rator t) then 1088 find_first_non_update ((rator t)::acc) (rand t) 1089 else 1090 (List.rev acc, t) 1091 fun categorise_update t = let 1092 (* t is an update. Here we generate 1093 a list of real updates (i.e., the terms corresponding to the 1094 new value in the update), each with an accompanying field 1095 string, and a boolean, which is true iff the update is a value 1096 update (not a "fupd") *) 1097 val (fld, value) = dest_comb t 1098 val rname = valOf (fupdstr NONE fld) 1099 in 1100 assert (isPrefix recfupd_special) rname 1101 handle HOL_ERR _ => raise NotReallyARecord; 1102 let 1103 val (f, x) = dest_comb value 1104 val {Thy, Name,...} = dest_thy_const f 1105 val fldname = String.extract(rname,size recfupd_special, NONE) 1106 in 1107 if Thy = "combin" andalso Name = "K" then [(fldname, x, true)] 1108 else [(fldname, value, false)] 1109 end handle HOL_ERR _ => 1110 [(String.extract(rname,size recfupd_special, NONE), 1111 value, false)] 1112 end 1113 in 1114 if is_record_update (SOME wholetm) t1 then let 1115 val (updates0, base) = find_first_non_update [] t2 1116 val updates = List.concat (map categorise_update (t1::updates0)) 1117 val (with_prec, with_tok) = valOf recwith_info 1118 val (ldelim, rdelim, sep) = valOf reclist_info 1119 fun print_update depth (fld, value, normal_upd) = let 1120 val (upd_prec, updtok) = 1121 if normal_upd then valOf recupd_info 1122 else valOf recfupd_info 1123 in 1124 block INCONSISTENT 2 1125 (add_ann_string 1126 (fld, PPBackEnd.Literal PPBackEnd.FldName) >> 1127 add_string " " >> 1128 add_string updtok >> 1129 add_break(1,0) >> 1130 pr_term value upd_prec upd_prec Top (decdepth depth)) 1131 end 1132 fun print_updlist updates = let 1133 fun recurse depth upds = 1134 if depth = 0 then add_string "..." 1135 else 1136 case upds of 1137 [] => nothing (* should never happen *) 1138 | [u] => print_update (decdepth depth) u 1139 | u::us => (print_update (decdepth depth) u >> 1140 print_ellist NONE (Top,Top,Top) (sep, []) >> 1141 recurse (decdepth depth) us) 1142 val ldelim_size = ellist_size ldelim 1143 in 1144 block INCONSISTENT ldelim_size ( 1145 print_ellist NONE (Top,Top,Top) (ldelim, []) >> 1146 recurse depth updates >> 1147 print_ellist NONE (Top,Top,Top) (rdelim, []) >> return () 1148 ) 1149 end 1150 in 1151 if is_const base andalso fst (dest_const base) = "ARB" then 1152 print_updlist updates 1153 else let 1154 val add_l = 1155 case lgrav of 1156 Prec(n, _) => n > with_prec 1157 | _ => false 1158 val add_r = 1159 case rgrav of 1160 Prec(n, _) => n > with_prec 1161 | _ => false 1162 val addparens = add_l orelse add_r 1163 val lprec = if addparens then Top else lgrav 1164 val with_grav = Prec(with_prec, recwith_special) 1165 in 1166 paren addparens ( 1167 block INCONSISTENT 0 ( 1168 pr_term base with_grav lprec with_grav (decdepth depth) >> 1169 add_string " " >> 1170 add_string with_tok >> 1171 add_break (1,0) >> 1172 (if length updates = 1 then print_update depth (hd updates) 1173 else print_updlist updates) 1174 ) 1175 ) 1176 end 1177 end handle NotReallyARecord => fail 1178 else fail 1179 end 1180 else fail 1181 1182 fun comb_show_type (f, args) = let 1183 val _ = (showtypes andalso combpos <> RatorCP) orelse raise PP_ERR "" "" 1184 1185 (* find out how the printer will map this constant into a string, 1186 and then see how this string maps back into constants. The 1187 base_type will encompass the simulated polymorphism of the 1188 overloading system as well as any genuine polymorphism in 1189 the underlying constant. *) 1190 val base_ty = let 1191 in 1192 if is_fakeconst f then let 1193 (* f prints to the atom-name *) 1194 val nm = atom_name f 1195 in 1196 #base_type (valOf (Overload.info_for_name overload_info nm)) 1197 end 1198 else 1199 case overloading_of_term' overload_info f of 1200 NONE => let 1201 val {Thy,Name,Ty} = dest_thy_const f 1202 in 1203 type_of (prim_mk_const {Thy = Thy, Name = Name}) 1204 end 1205 | SOME print_name => 1206 #base_type 1207 (valOf (Overload.info_for_name overload_info print_name)) 1208 end 1209 val base_ptyM = Pretype.rename_typevars [] (Pretype.fromType base_ty) 1210 open errormonad 1211 fun foldthis (tm,acc) = let 1212 open Pretype 1213 val fn_ptyM = lift (fn ty => mk_fun_ty(fromType (type_of tm), ty)) 1214 new_uvar 1215 in 1216 acc >- (fn ty1 => fn_ptyM >- (fn ty2 => unify ty1 ty2 >> chase ty1)) 1217 end 1218 val resultM = List.foldl foldthis base_ptyM args 1219 in 1220 case (resultM >- Pretype.has_unbound_uvar) Pretype.Env.empty of 1221 Error _ => false 1222 | Some (_, b) => b 1223 end handle HOL_ERR _ => false 1224 | Option => false 1225 1226 fun pr_comb tm t1 t2 = let 1227 val add_l = 1228 case lgrav of 1229 Prec (n, _) => (n >= comb_prec) 1230 | _ => false 1231 val add_r = 1232 case rgrav of 1233 Prec (n, _) => (n > comb_prec) 1234 | _ => false 1235 val addparens = add_l orelse add_r 1236 1237 val (f, args) = strip_comb tm 1238 val comb_show_type = comb_show_type(f,args) 1239 val prec = Prec(comb_prec, fnapp_special) 1240 val lprec = if addparens then Top else lgrav 1241 val rprec = if addparens then Top else rgrav 1242 in 1243 paren (addparens orelse comb_show_type) ( 1244 block INCONSISTENT 0 ( 1245 full_pr_term binderp showtypes showtypes_v ppfns RatorCP t1 1246 prec lprec prec (decdepth depth) >> 1247 add_break (1, 2) >> 1248 full_pr_term binderp showtypes showtypes_v ppfns RandCP t2 1249 prec prec rprec (decdepth depth) >> 1250 (if comb_show_type then 1251 add_string (" "^type_intro) >> add_break (0,0) >> 1252 doTy (type_of tm) >> setlaststring " " 1253 else nothing) 1254 ) 1255 ) 1256 end 1257 1258 fun pr_sole_name tm n rules = let 1259 (* This function prints a solitary name n. The rules are possibly 1260 relevant rules from the grammar. If one is a list rule, and our 1261 n is the name of the nil case, then we should print that 1262 list's delimiters around nothing. 1263 Otherwise, the presence of a rule with our name n in it, is a 1264 probable indication that our name will need a $ printed out in 1265 front of it. *) 1266 (* monadically, it returns (best guess at) width of what it's just 1267 printed , SOME w, or NONE (for giving up on it) *) 1268 (* val _ = PRINT ("pr_sole_name: "^debugprint G tm) *) 1269 fun check_rule rule = 1270 case rule of 1271 CLOSEFIX [{elements,...}] => 1272 (case find_lspec elements of 1273 NONE => NONE 1274 | SOME{nilstr,...} => if nilstr = n then SOME elements else NONE) 1275 | _ => NONE 1276 val nilrule = find_partial check_rule rules 1277 val ty = type_of tm 1278 fun add s = 1279 if is_constish tm then constann tm s 1280 else var_ann tm s 1281 in 1282 case nilrule of 1283 SOME els => ((* PRINT ("Found a nil-rule for "^n); *) 1284 print_ellist NONE (Top,Top,Top) (els, [tm]) >- 1285 (return o #2)) 1286 | NONE => let 1287 (* if only rule is a list form rule and we've got to here, it 1288 will be a rule allowing this to the cons part of a list form. 1289 Such functions don't need to be dollar-ed *) 1290 in 1291 if HOLset.member(spec_table, n) then 1292 dollarise add add_string n >- (return o SOME) 1293 else add n >> return (SOME (UTF8.size n)) 1294 end 1295 end 1296 1297 1298 fun pr_comb_with_rule frule fterm args Rand = let 1299 val {fname,fprec,f} = fterm 1300 val comb_show_type = comb_show_type(f,args @ [Rand]) 1301 fun ptype_block p = 1302 if comb_show_type then 1303 paren true ( 1304 block CONSISTENT 0 ( 1305 p >- 1306 (fn r => add_break (1,2) >> add_string type_intro >> 1307 doTy (type_of tm) >> return r) 1308 ) 1309 ) 1310 else p 1311 fun block_up_els acc els = 1312 case els of 1313 [] => List.rev acc 1314 | (e::es) => let 1315 in 1316 case e of 1317 EndInitialBlock bi => 1318 block_up_els [PPBlock(List.rev acc, bi)] es 1319 | BeginFinalBlock bi => let 1320 val block_of_rest = block_up_els [] es 1321 in 1322 List.rev (PPBlock(block_of_rest, bi)::acc) 1323 end 1324 | x => block_up_els (x::acc) es 1325 end 1326 val print_ellist = fn x => fn y => fn z => print_ellist x y z >> return () 1327 in 1328 case frule of 1329 INFIX(STD_infix(lst, fassoc)) => let 1330 val rr = hd lst 1331 val elements = #elements rr 1332 fun check_grav a grav = 1333 case grav of 1334 Prec(n, _) => 1335 (n > fprec) orelse (n = fprec andalso a <> fassoc) 1336 | _ => false 1337 val parens_needed_outright = 1338 check_grav RIGHT lgrav orelse check_grav LEFT rgrav 1339 val parens_needed_by_style = 1340 pneeded_by_style(rr, pgrav, fname, fprec) 1341 val addparens = parens_needed_outright orelse parens_needed_by_style 1342 val prec = Prec(fprec, fname) 1343 val lprec = if addparens then Top else lgrav 1344 val rprec = if addparens then Top else rgrav 1345 val arg_terms = args @ [Rand] 1346 val pp_elements = block_up_els [] ((FirstTM::elements) @ [LastTM]) 1347 val begblock = block_by_style(rr, pgrav, fname, fprec) 1348 in 1349 ptype_block ( 1350 paren (addparens orelse comb_show_type) ( 1351 begblock 1352 (print_ellist (SOME f) 1353 (lprec, prec, rprec) 1354 (pp_elements, arg_terms)) 1355 ) 1356 ) 1357 end 1358 | INFIX RESQUAN_OP => raise Fail "Res. quans shouldn't arise" 1359 | INFIX (FNAPP _) => raise PP_ERR "pr_term" "fn apps can't arise" 1360 | INFIX VSCONS => raise PP_ERR "pr_term" "vs cons can't arise" 1361 | SUFFIX (STD_suffix lst) => let 1362 val rr = hd lst 1363 val elements = #elements rr 1364 val parens_needed_outright = 1365 case lgrav of 1366 Prec(n, _) => n > fprec 1367 | _ => false 1368 val parens_needed_by_style = 1369 pneeded_by_style (rr, pgrav, fname, fprec) 1370 val addparens = parens_needed_outright orelse parens_needed_by_style 1371 val lprec = if addparens then Top else lgrav 1372 val prec = Prec(fprec, fname) 1373 val real_args = args @ [Rand] 1374 val pp_elements = block_up_els [] (FirstTM :: elements) 1375 val begblock = 1376 block_by_style(rr, pgrav, fname, fprec) 1377 in 1378 ptype_block ( 1379 paren (addparens orelse comb_show_type) ( 1380 begblock ( 1381 print_ellist (SOME f) 1382 (lprec, prec, Top) 1383 (pp_elements, real_args) 1384 ) 1385 ) 1386 ) 1387 end 1388 | SUFFIX TYPE_annotation => 1389 raise Fail "Type annotation shouldn't arise" 1390 | PREFIX (STD_prefix lst) => let 1391 val rr = hd lst 1392 val elements = #elements rr 1393 val parens_needed_outright = 1394 case rgrav of 1395 Prec(n, _) => n > fprec 1396 | _ => false 1397 val addparens = 1398 parens_needed_outright orelse 1399 pneeded_by_style(rr, pgrav, fname, fprec) orelse 1400 (combpos = RandCP andalso #paren_style rr <> NotEvenIfRand) 1401 val rprec = if addparens then Top else rgrav 1402 val pp_elements = block_up_els [] (elements @ [LastTM]) 1403 val real_args = args @ [Rand] 1404 val prec = Prec(fprec, fname) 1405 val begblock = block_by_style(rr, pgrav, fname, fprec) 1406 in 1407 ptype_block ( 1408 paren (addparens orelse comb_show_type) ( 1409 begblock ( 1410 print_ellist (SOME f) 1411 (Top, prec, rprec) 1412 (pp_elements, real_args) 1413 ) 1414 ) 1415 ) 1416 end 1417 | PREFIX (BINDER lst) => let 1418 val tok = case hd lst of 1419 LAMBDA => hd lambda (* should never happen *) 1420 | BinderString r => #tok r 1421 fun find (bopt, s) = if bopt = SOME fname then SOME s else NONE 1422 val restr_binder = find_partial find restr_binders 1423 val (bvs, body) = strip_vstructs (SOME fname) restr_binder tm 1424 val bvars_seen_here = List.concat (map (free_vars o bv2term) bvs) 1425 val addparens = 1426 case rgrav of 1427 Prec(n, _) => n > fprec 1428 | _ => false 1429 val addparens = addparens orelse combpos = RandCP 1430 val print_tok = if is_constish f then constann f tok 1431 else var_ann f tok 1432 in 1433 ptype_block ( 1434 paren (addparens orelse comb_show_type) ( 1435 block INCONSISTENT 2 (print_tok >> pr_vstructl bvs body) 1436 ) 1437 ) 1438 end 1439 | CLOSEFIX lst => let 1440 val rr = hd lst 1441 val elements = #elements rr 1442 in 1443 ptype_block 1444 (uncurry block (#2 (#block_style rr)) 1445 (print_ellist (SOME f) 1446 (Top, Top, Top) 1447 (elements, args @ [Rand]) >> 1448 return ())) 1449 end 1450 end 1451 1452 fun print_ty_antiq tm = let 1453 val ty = parse_type.dest_ty_antiq tm 1454 in 1455 block CONSISTENT 2 1456 (add_string "(ty_antiq(" >> 1457 add_break(0,0) >> 1458 add_string "`:" >> 1459 doTy ty >> 1460 add_string "`))") 1461 end 1462 1463 (* used to determine whether or not to print out disambiguating type 1464 information when showtypes_v is true *) 1465 fun const_is_polymorphic c = 1466 if is_const c then let 1467 val {Name,Thy,Ty} = dest_thy_const c 1468 val genconst = prim_mk_const {Name=Name,Thy=Thy} 1469 in 1470 Type.polymorphic (type_of genconst) 1471 end handle HOL_ERR _ => false 1472 (* the exception is possible if the constant is out of date *) 1473 else if is_fakeconst c then 1474 case Overload.info_for_name overload_info (atom_name c) of 1475 NONE => (* peculiar, printing but not parsing *) true 1476 | SOME {base_type,...} => Type.polymorphic base_type 1477 else false 1478 1479 fun const_has_multi_ovl tm = 1480 case overloading_of_term' overload_info tm of 1481 NONE => (* no printing form *) true 1482 | SOME s => 1483 case Overload.info_for_name overload_info s of 1484 NONE => true (* seems pretty unlikely *) 1485 | SOME {actual_ops,...} => length actual_ops > 1 1486 1487 fun const_is_ambiguous t = 1488 const_is_polymorphic t orelse const_has_multi_ovl t 1489 1490 in 1491 if depth = 0 then add_string "..." 1492 else if parse_type.is_ty_antiq tm then print_ty_antiq tm 1493 else 1494 case dest_term tm of 1495 VAR(vname, Ty) => let 1496 val (isfake, vname) = 1497 (true, valOf (unfakeconst vname)) 1498 handle Option => (false, vname) 1499 val vrule = lookup_term vname 1500 fun add_type wopt = 1501 case wopt of 1502 NONE => 1503 add_string (" "^type_intro) >> add_break(0,0) >> 1504 block INCONSISTENT 0 (doTy Ty) >> setlaststring " " 1505 | SOME i => add_string (" " ^ type_intro) >> 1506 block INCONSISTENT (i + 1 + UTF8.size type_intro) 1507 (doTy Ty) >> 1508 setlaststring " " 1509 fun new_freevar ({seen_frees,current_bvars,...}:printing_info) = 1510 showtypes andalso not isfake andalso 1511 not (HOLset.member(seen_frees, tm)) andalso 1512 not (HOLset.member(current_bvars, tm)) andalso not binderp 1513 fun calc_print_type nfv = 1514 showtypes_v orelse 1515 showtypes andalso not isfake andalso (binderp orelse nfv) 1516 val adds = 1517 if is_constish tm then constann tm else var_ann tm 1518 val uok = current_trace "PP.avoid_unicode" = 0 1519 val styled_name = if isfake then vname else vname_styling uok vname 1520 in 1521 fupdate (fn x => x) >- return o new_freevar >- 1522 (fn is_new => 1523 (if is_new then spotfv tm else nothing) >> 1524 return (calc_print_type is_new)) >- 1525 (fn print_type => 1526 block INCONSISTENT 0 ( 1527 paren print_type ( 1528 (if isSome vrule then 1529 pr_sole_name tm vname (map #3 (valOf vrule)) 1530 else 1531 if HOLset.member(spec_table, vname) then 1532 dollarise adds add_string styled_name >- 1533 (return o SOME) 1534 else adds styled_name >- (return o SOME)) >- 1535 (fn w => if print_type then add_type w else nothing) 1536 ) 1537 ) 1538 ) 1539 end 1540 | CONST(c as {Name, Thy, Ty}) => let 1541 val add_ann_string = constann tm 1542 fun add_prim_name() = add_ann_string (Thy ^ "$" ^ Name) >> 1543 return (SOME (size Thy + size Name + 1)) 1544 fun with_type action = let 1545 in 1546 if Name = "the_value" andalso Thy = "bool" then 1547 action() >> return () 1548 else 1549 paren true (action() >- (fn wopt => 1550 add_string (" "^type_intro) >> 1551 (case wopt of 1552 NONE => add_break(0,0) >> 1553 block INCONSISTENT 0 (doTy Ty) 1554 | SOME w => 1555 block INCONSISTENT 1556 (w + UTF8.size type_intro + 1) 1557 (doTy Ty)) >> 1558 setlaststring " ")) 1559 end 1560 val r = {Name = Name, Thy = Thy} 1561 fun normal_const () = let 1562 fun cope_with_rules s = let 1563 val crules = 1564 Option.map (List.filter (is_unicode_ok_rule o #3)) 1565 (lookup_term s) 1566 open PPBackEnd 1567 in 1568 if isSome crules then 1569 pr_sole_name tm s (map #3 (valOf crules)) 1570 else if s = "0" andalso can_pr_numeral NONE then 1571 pr_numeral NONE tm >> return NONE 1572 else if Literal.is_emptystring tm then 1573 add_xstring {s="\"\"", sz = NONE, 1574 ann = SOME (Literal StringLit)} >> 1575 return (SOME 2) 1576 else add_ann_string s >- (return o SOME) 1577 end 1578 in 1579 if Name = "the_value" andalso Thy = "bool" then let 1580 val {Args,...} = dest_thy_type Ty 1581 in (* TODO: annotate all of this as the constant somehow *) 1582 add_string "(" >> 1583 block CONSISTENT 0 (add_string type_intro >> doTy (hd Args)) >> 1584 add_string ")" >> return NONE 1585 end 1586 else 1587 case overloading_of_term' overload_info tm of 1588 NONE => add_prim_name() 1589 | SOME s => 1590 (* term is overloaded *) 1591 if s = "case" then cope_with_rules Name 1592 else cope_with_rules s 1593 end 1594 in 1595 case (showtypes_v, const_is_polymorphic tm, const_has_multi_ovl tm) of 1596 (true, false, true) => add_prim_name() >> return () 1597 | (true, true, true) => with_type add_prim_name 1598 | (true, true, false) => with_type normal_const 1599 | _ => if !show_types andalso combpos <> RatorCP andalso 1600 const_is_polymorphic tm 1601 then 1602 with_type normal_const 1603 else normal_const() >> return () 1604 end 1605 | COMB(Rator, Rand) => let 1606 val (f, args) = strip_comb Rator 1607 val (oif, oiargs, overloadedp) = 1608 case oi_strip_comb' overload_info tm of 1609 NONE => (f, args @ [Rand], false) 1610 | SOME (f, args) => (f, args, true) 1611 1612 fun is_atom tm = is_const tm orelse is_var tm 1613 fun pr_atomf (f,args0) = let 1614 (* the tm, Rator and Rand bindings that we began with are 1615 overridden by the f and args values that may be the product of 1616 oi_strip_comb.*) 1617 val fname = atom_name f 1618 (* val _ = PRINT ("pr_atomf: "^fname^" and "^ 1619 Int.toString (length args0) ^ " args") *) 1620 val tm = list_mk_comb (f, args0) 1621 val Rator = rator tm 1622 val (args,Rand) = front_last args0 1623 val candidate_rules = 1624 Option.map (List.filter (is_unicode_ok_rule o #3)) 1625 (lookup_term fname) 1626 (* val _ = PRINT ("pr_atomf: "^debugprint G tm^", "^ 1627 (case candidate_rules of 1628 NONE => "rules = NONE" 1629 | SOME l => 1630 Int.toString (length l)^ " candidate rules")) 1631 *) 1632 1633 1634 val restr_binder = 1635 find_partial (fn (b,s) => if s=fname then SOME b else NONE) 1636 restr_binders 1637 val restr_binder_rule = 1638 if isSome restr_binder andalso length args = 1 andalso 1639 my_is_abs Rand 1640 then let 1641 val bindex = case valOf restr_binder of 1642 NONE => binder_to_string G LAMBDA 1643 | SOME s => s 1644 val optrule = Option.map (List.filter (is_unicode_ok_rule o #3)) 1645 (lookup_term bindex) 1646 fun ok_rule (_, _, r) = 1647 case r of 1648 PREFIX(BINDER b) => true 1649 | otherwise => false 1650 in 1651 case optrule of 1652 SOME (r::_) => if ok_rule r then SOME r else NONE 1653 | otherwise => NONE 1654 end 1655 else NONE 1656 fun check_rrec_args f rrec args = 1657 let 1658 val rels = f (rule_elements (#elements rrec)) 1659 (*val _ = PRINT ("check_rrec_args: rels = [" ^ 1660 String.concatWith ", " (map reltoString rels) ^ 1661 "]; args = [" ^ 1662 String.concatWith ", " (map (debugprint G) args)^ 1663 "]")*) 1664 fun recurse rels args = 1665 case (rels, args) of 1666 ([], []) => true 1667 | ([], _) => false 1668 | (TM :: rrest, _ :: arest) => recurse rrest arest 1669 | (TOK _ :: rrest, _) => recurse rrest args 1670 | (_, []) => false 1671 | (ListTM {nilstr,cons,...} :: rrest, a :: arest) => 1672 is_list G {nilstr=nilstr,cons=cons} a andalso 1673 recurse rrest arest 1674 in 1675 recurse rels args 1676 end 1677 in 1678 case candidate_rules of 1679 NONE => 1680 let 1681 in 1682 case restr_binder of 1683 NONE => pr_comb tm Rator Rand 1684 | SOME NONE => 1685 if isSome restr_binder_rule then pr_abs tm 1686 else pr_comb tm Rator Rand 1687 | SOME (SOME fname) => 1688 if isSome restr_binder_rule then 1689 pr_comb_with_rule(#3(valOf restr_binder_rule)) 1690 {fprec = #1 (valOf restr_binder_rule), 1691 fname = fname, 1692 f = f} args Rand 1693 else 1694 pr_comb tm Rator Rand 1695 end 1696 | SOME crules0 => 1697 let 1698 datatype ruletype = Norm of (int * grammar_rule) 1699 | List of pp_element list 1700 fun suitable_rule (prec, _, rule) = 1701 case rule of 1702 INFIX(STD_infix(rrlist, _)) => 1703 if check_rrec_args mkrels_infix (hd rrlist) args0 then 1704 SOME (Norm(prec, rule)) 1705 else NONE 1706 | INFIX RESQUAN_OP => raise Fail "Can't happen 90212" 1707 | PREFIX (STD_prefix list) => 1708 if check_rrec_args mkrels_prefix (hd list) args0 then 1709 SOME (Norm (prec, rule)) 1710 else NONE 1711 | PREFIX (BINDER _) => 1712 if my_is_abs Rand andalso length args = 0 then 1713 SOME (Norm(prec, rule)) 1714 else NONE 1715 | SUFFIX (STD_suffix list) => 1716 if check_rrec_args mkrels_suffix (hd list) args0 then 1717 SOME (Norm(prec, rule)) 1718 else NONE 1719 | SUFFIX Type_annotation => raise Fail "Can't happen 90210" 1720 | CLOSEFIX list => 1721 let 1722 (* val _ = PRINT "suitable_rule: closefix check" *) 1723 val r = hd list 1724 in 1725 if term_name_is_lform (#term_name r) then 1726 ((* PRINT ("rule term-name is empty - testing " ^ 1727 debugprint G tm); *) 1728 case find_lspec (#elements r) of 1729 SOME {nilstr,cons,...} => 1730 if is_list G {nilstr=nilstr,cons=cons} tm then 1731 SOME (List (#elements r)) 1732 else NONE 1733 | NONE => NONE) 1734 else if check_rrec_args mkrels_closefix r args0 then 1735 SOME (Norm(prec, rule)) 1736 else NONE 1737 end 1738 | INFIX (FNAPP _) => raise Fail "Can't happen 90211" 1739 | INFIX VSCONS => raise Fail "Can't happen 90213" 1740 in 1741 case List.mapPartial suitable_rule crules0 of 1742 Norm (prec,rule) :: _ => 1743 pr_comb_with_rule 1744 rule 1745 {fprec = prec, fname=fname, f=f} args Rand 1746 | List els :: _ => 1747 ((* PRINT "printing a List rule"; *) 1748 print_ellist NONE (Top,Top,Top) (els, [tm]) >> return ()) 1749 | [] => (*(PRINT "No suitable rules, printing with pr_comb";*) 1750 pr_comb tm Rator Rand 1751 (* before PRINT "Finished pr_comb") *) 1752 end 1753 end (* pr_atomf *) 1754 fun maybe_pr_atomf () = 1755 if grammar_name G oif = SOME "case" then 1756 pr_atomf (strip_comb tm) 1757 else if overloadedp then 1758 case oiargs of 1759 [] => (* term is a comb, but it somehow overloads to a 1760 single "constant" *) 1761 pr_term oif pgrav lgrav rgrav depth 1762 | _ => pr_atomf (oif, oiargs) 1763 else if is_var f then pr_atomf (f, args @ [Rand]) 1764 else pr_comb tm Rator Rand 1765 in 1766 (* check for various literal and special forms *) 1767 1768 (* strings *) 1769 (case total Literal.dest_string_lit tm of 1770 NONE => fail 1771 | SOME s => 1772 uadd_ann_string 1773 (Literal.string_literalpp {ldelim="\"", rdelim = "\""} s, 1774 PPBackEnd.Literal PPBackEnd.StringLit)) ||| 1775 1776 (* overloaded strings - with special designated rator to a rand 1777 which is in turn a string literal *) 1778 (fn _ => case total Literal.dest_string_lit (rand tm) of 1779 SOME s => 1780 (case overloads_to_string_form G {tmnm=atom_name f} of 1781 NONE => fail 1782 | SOME ldelim => 1783 uadd_ann_string 1784 (Literal.string_literalpp 1785 (Literal.delim_pair {ldelim=ldelim}) 1786 s, 1787 PPBackEnd.Literal PPBackEnd.StringLit)) 1788 | NONE => fail) ||| 1789 1790 (* characters *) 1791 (fn _ => case total Literal.dest_char_lit tm of 1792 NONE => fail 1793 | SOME c => uadd_ann_string ("#" ^ Lib.mlquote (str c), 1794 PPBackEnd.Literal PPBackEnd.CharLit))||| 1795 1796 (* numerals *) 1797 (fn _ => if Literal.is_numeral tm andalso can_pr_numeral NONE then 1798 pr_numeral NONE tm 1799 else fail) ||| 1800 (fn _ => (if Literal.is_numeral Rand andalso 1801 can_pr_numeral (SOME (atom_name Rator)) 1802 then pr_numeral (SOME Rator) Rand 1803 else fail) handle HOL_ERR _ => fail) ||| 1804 1805 (* binders *) 1806 (fn _ => if my_is_abs tm then pr_abs tm else fail) ||| 1807 1808 (* record forms *) 1809 (fn _ => 1810 case oiargs of 1811 [] => fail 1812 | _ => let 1813 val (args, Rand) = front_last oiargs 1814 in 1815 check_for_field_selection (list_mk_comb(oif,args)) Rand 1816 end) ||| 1817 (fn _ => check_for_record_update tm Rator Rand) ||| 1818 1819 (* case expressions *) 1820 (fn () => 1821 if (is_const f andalso (!prettyprint_cases)) then 1822 case grammar_name G oif of 1823 SOME "case" => 1824 (let 1825 val (split_on, splits) = convert_case tm 1826 val parens = (case rgrav of Prec _ => true | _ => false) 1827 orelse 1828 combpos = RandCP 1829 fun p body = 1830 get_gspec >- 1831 (fn b => if b orelse parens then 1832 block PP.CONSISTENT 1 ( 1833 add_string "(" >> body >> add_string ")" 1834 ) 1835 else 1836 block PP.CONSISTENT 0 body) 1837 val casebar = 1838 add_break(1,0) >> add_string "|" >> hardspace 1 1839 fun do_split rprec (l,r) = 1840 record_bvars 1841 (free_vars l) 1842 (block PP.CONSISTENT 0 ( 1843 pr_term l Top Top Top (decdepth depth) >> 1844 hardspace 1 >> 1845 add_string "=>" >> add_break(1,2) >> 1846 block PP.CONSISTENT 0 1847 (pr_term r Top Top rprec (decdepth depth))) 1848 ) 1849 in 1850 p (block PP.CONSISTENT 0 1851 (add_string (prettyprint_cases_name ()) >> 1852 add_break(1,2) >> 1853 pr_term split_on Top Top Top (decdepth depth) >> 1854 add_break(1,0) >> add_string "of") >> 1855 (if !pp_print_firstcasebar then 1856 casebar 1857 else 1858 add_break (1,2)) >> 1859 (if length splits > 1 then 1860 pr_list (do_split (Prec(0,"casebar"))) 1861 casebar (butlast splits) >> 1862 casebar >> 1863 do_split (if parens then Top else rgrav) 1864 (last splits) 1865 else 1866 do_split (if parens then Top else rgrav) 1867 (hd splits))) 1868 end handle CaseConversionFailed => fail) 1869 | _ => fail 1870 else fail) ||| 1871 1872 (fn _ => if showtypes_v then 1873 if const_is_ambiguous f then 1874 pr_comb tm Rator Rand 1875 else 1876 maybe_pr_atomf() 1877 else maybe_pr_atomf()) 1878 end 1879 | LAMB(Bvar, Body) => pr_abs tm 1880 end apps 1881 val avoid_merge = avoid_symbolmerge G 1882 open PPBackEnd 1883in 1884 fn t => 1885 let 1886 val {add_string,add_break,ublock,add_xstring,add_newline,ustyle,...} = 1887 backend 1888 val (add_string, add_xstring, add_break) = 1889 avoid_merge (add_string, add_xstring, add_break) 1890 val ppfns = {add_string = add_string, 1891 add_xstring = add_xstring, 1892 add_break = add_break, 1893 add_newline = add_newline, 1894 ublock = ublock, 1895 ustyle = ustyle, 1896 extras = ()} 1897 in 1898 ublock CONSISTENT 0 ( 1899 pr_term false 1900 (!Globals.show_types orelse !Globals.show_types_verbosely) 1901 (!Globals.show_types_verbosely) 1902 ppfns NoCP t RealTop RealTop RealTop 1903 (!Globals.max_print_depth) 1904 ) 1905 end 1906end 1907 1908end; (* term_pp *) 1909