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