1structure pred_setpp :> pred_setpp = 2struct 3 4open HolKernel smpp term_pp_types term_pp_utils 5 6val univ_printing = ref true 7val unicode_univ = ref true 8 9val _ = Feedback.register_btrace ("Univ pretty-printing", univ_printing) 10val _ = Feedback.register_btrace ("Unicode Univ printing", unicode_univ) 11 (* because the current unicode symbol for the universal set is 12 beyond the BMP, it may not be common in installed fonts. 13 So we provide a flag specifically to turn just it off. *) 14 15fun univ_printer (tyg, tmg) backend printer ppfns gravs depth tm = 16 let 17 val {add_string, ...} = ppfns : term_pp_types.ppstream_funs 18 in 19 if !univ_printing then 20 let 21 val (elty, _) = dom_rng (type_of tm) 22 val itself_t = Term.inst [{redex=alpha,residue=elty}] 23 boolSyntax.the_value 24 val U = if get_tracefn "Unicode" () = 1 andalso !unicode_univ then 25 UnicodeChars.universal_set 26 else "univ" 27 in 28 add_string U >> 29 printer {gravs = gravs, depth = depth, binderp = false} itself_t 30 end 31 else 32 case Overload.info_for_name (term_grammar.overload_info tmg) "UNIV" of 33 NONE => add_string "pred_set$UNIV" 34 | SOME _ => add_string "UNIV" 35 end 36 37val _ = term_grammar.userSyntaxFns.register_userPP 38 {name = "pred_set.UNIV", code = univ_printer} 39 40(* ---------------------------------------------------------------------- 41 A flag controlling printing of set comprehensions 42 ---------------------------------------------------------------------- *) 43 44val unamb_comp = ref 0 45val _ = Feedback.register_trace ("pp_unambiguous_comprehensions", unamb_comp, 2) 46 47 48fun setcomprehension_printer (tyg,tmg) backend printer ppfns gravs depth tm = 49 let 50 val unamb_comp = get_tracefn "pp_unambiguous_comprehensions" () 51 val _ = 52 case Overload.oi_strip_comb (term_grammar.overload_info tmg) tm of 53 SOME(f, _) => 54 if term_grammar.grammar_name tmg f = SOME "GSPEC" 55 then () 56 else raise UserPP_Failed 57 | NONE => raise UserPP_Failed 58 val _ = term_pp_utils.pp_is_abs tmg (rand tm) orelse raise UserPP_Failed 59 val {add_string, add_break, ...} = ppfns : term_pp_types.ppstream_funs 60 fun hardspace n = add_string (CharVector.tabulate(n, fn _ => #" ")) 61 fun spacep b = if b then add_break(1,0) else nothing 62 63 val (vs, body) = term_pp_utils.pp_dest_abs tmg (rand tm) 64 val vfrees = FVL [vs] empty_tmset 65 val bvars_seen_here = HOLset.listItems vfrees 66 67 val (l, r) = pairSyntax.dest_pair body 68 val lfrees = FVL [l] empty_tmset 69 val rfrees = FVL [r] empty_tmset 70 open HOLset 71 val tops = (Top,Top,Top) 72 fun pr t = 73 printer {gravs = tops, depth = decdepth depth, binderp = false} t 74 in 75 if ((equal(intersection(lfrees,rfrees), vfrees) orelse 76 (isEmpty lfrees andalso equal(rfrees, vfrees)) orelse 77 (isEmpty rfrees andalso equal(lfrees, vfrees))) 78 andalso unamb_comp = 0) orelse 79 unamb_comp = 2 80 then 81 block PP.CONSISTENT 0 ( 82 record_bvars bvars_seen_here ( 83 set_gspec ( 84 add_string "{" >> 85 block PP.CONSISTENT 1 ( 86 pr l >> hardspace 1 >> add_string "|" >> spacep true >> pr r 87 ) >> 88 add_string "}" 89 ) 90 ) 91 ) 92 else 93 block PP.CONSISTENT 0 ( 94 record_bvars bvars_seen_here ( 95 set_gspec ( 96 add_string "{" >> 97 block PP.CONSISTENT 1 ( 98 pr l >> hardspace 1 >> add_string "|" >> spacep true >> pr vs >> 99 hardspace 1 >> add_string "|" >> spacep true >> 100 pr r 101 ) >> 102 add_string "}" 103 ) 104 ) 105 ) 106 end handle HOL_ERR _ => raise UserPP_Failed 107 108val _ = term_grammar.userSyntaxFns.register_userPP 109 {name = "pred_set.GSPEC", code = setcomprehension_printer} 110 111 112end 113