1structure type_pp :> type_pp =
2struct
3
4open Feedback Type Portable HOLgrammars type_grammar
5
6datatype mygrav = Sfx
7                | Lfx of int * string
8                | Rfx of int * string
9                | Top
10
11datatype single_rule = IR of int * associativity * string
12
13val ERR = mk_HOL_ERR "type_pp" "pp_type";
14
15val avoid_unicode = ref (Systeml.OS = "winNT")
16local
17  open Globals
18  fun ascii_delims () =
19    (List.app (fn r => r := "``") [type_pp_prefix, type_pp_suffix,
20                                   term_pp_prefix, term_pp_suffix];
21     thm_pp_prefix := "|- ";
22     thm_pp_suffix := "")
23  fun unicode_delims () =
24    (List.app (fn r => r := UnicodeChars.ldquo)
25              [type_pp_prefix, term_pp_prefix];
26     List.app (fn r => r := UnicodeChars.rdquo)
27              [type_pp_suffix, term_pp_suffix];
28     thm_pp_prefix := UnicodeChars.turnstile ^ " ";
29     thm_pp_suffix := "")
30  fun avoidset i = if i = 0 then (unicode_delims(); avoid_unicode := false)
31                   else (ascii_delims(); avoid_unicode := true)
32  fun avoidget () = if !avoid_unicode then 1 else 0
33in
34
35val _ = register_ftrace("PP.avoid_unicode", (avoidget, avoidset), 1)
36val _ = register_ftrace("Unicode",
37                        (fn () => 1 - avoidget(), fn n => avoidset (1 - n)),
38                        1)
39val _ = avoidset (avoidget())
40end
41
42
43val pp_num_types = ref true
44val _ = register_btrace("pp_num_types", pp_num_types)
45
46val pp_annotations = ref (!Globals.interactive)
47val _ = register_btrace ("pp_annotations", pp_annotations)
48
49fun dest_numtype ty = let
50  open Arbnum
51  val _ = (* respect pp_num_types flag *)
52      !pp_num_types orelse raise mk_HOL_ERR "" "" ""
53  val _ = (* exception: don't print :one as one *)
54      let val {Thy,Tyop,Args} = dest_thy_type ty
55      in
56        if Thy = "one" andalso Tyop = "one" then raise mk_HOL_ERR "" "" ""
57        else ()
58      end
59  fun recurse (base, acc) ty = let
60    val {Thy,Tyop,Args} = dest_thy_type ty
61  in
62    case (Thy,Tyop) of
63      ("one", "one") => acc + base
64    | ("fcp", "bit1") => recurse (two * base, acc + base) (hd Args)
65    | ("fcp", "bit0") => recurse (two * base, acc) (hd Args)
66    | _ => raise mk_HOL_ERR "" "" ""
67  end
68in
69  toString (recurse (one, zero) ty)
70end
71
72val greek4 = let
73  open UnicodeChars
74in
75  [alpha, beta, gamma, delta]
76end
77
78fun structure_to_string st = let
79  fun recurse paren st =
80      case st of
81        TYOP {Thy,Tyop,Args} => let
82          val opstr = Thy ^ "$" ^ Tyop
83        in
84          case Args of
85            [] => opstr
86          | [x] => recurse false x ^ " " ^ opstr
87          | [x,y] => if Thy = "min" andalso Tyop = "fun" then
88                       (if paren then "(" else "") ^
89                       recurse true x ^ " -> " ^
90                       recurse false y ^
91                       (if paren then ")" else "")
92                     else
93                       "(" ^ recurse false x ^ ", " ^ recurse false y ^ ") " ^
94                       opstr
95          | _ => "(" ^ String.concatWith ", " (map (recurse false) Args) ^
96                 ") " ^ opstr
97        end
98      | PARAM i => if i < 4 then List.nth(greek4, i)
99                   else "'" ^ str (Char.chr (Char.ord #"a" + i))
100in
101  recurse false st
102end
103
104val pp_array_types = ref true
105val _ = register_btrace ("pp_array_types", pp_array_types)
106
107fun pp_type0 (G:grammar) (backend: PPBackEnd.t) = let
108  val {infixes,suffixes} = rules G
109  fun lookup_tyop s = let
110    fun recurse [] = NONE
111      | recurse (x::xs) = let
112        in
113          case x of
114            (p, INFIX (slist, a)) => let
115              val res = List.find (fn r => #opname r = s) slist
116            in
117              case res of
118                NONE => recurse xs
119              | SOME r => SOME(IR(p, a,#parse_string r))
120            end
121        end
122  in
123    recurse infixes : single_rule option
124  end
125  fun pr_ty ty grav depth = let
126    open HOLPP smpp PPBackEnd
127    val {add_string, add_break, ublock, add_xstring,...} = backend
128    fun add_ann_string (s,ann) = add_xstring {s=s,ann=SOME ann,sz=NONE}
129    fun paren b p = if b then add_string "(" >> p >> add_string ")" else p
130    fun uniconvert s =
131        if not (!avoid_unicode) andalso get_tracefn "Greek tyvars" () = 1
132           andalso size s = 2
133        then
134          let
135            val i = Char.ord (String.sub(s, 1)) - Char.ord #"a" + 0x3B1
136          in
137            if 0x3B1 <= i andalso i <= 0x3C9 andalso i <> 0x3BB then UTF8.chr i
138            else s
139          end
140        else s
141  in
142    if depth = 0 then add_string "..."
143    else
144      if is_vartype ty then
145        add_ann_string (uniconvert (dest_vartype ty), TyV)
146      else let
147          val s = dest_numtype ty
148        in
149          add_string s
150        end handle HOL_ERR _ =>
151        let
152          fun realtype ty = let val {Thy,Tyop,...} = dest_thy_type ty
153                            in Thy ^ "$" ^ Tyop end
154          val {Tyop = abop, Args = abargs, Thy = thyopt} =
155              type_grammar.abb_dest_type G ty
156          val abop_s =
157              case thyopt of
158                  NONE => abop
159                | SOME thy => KernelSig.name_toString {Thy = thy, Name = abop}
160          fun tooltip () =
161            let
162              val abbs = type_grammar.parse_map G
163              fun doabbrev st =
164                let
165                  val numps = num_params st
166                in
167                  if 0 < numps then let
168                      val params =
169                          if numps <= 4 then List.take(greek4, numps)
170                          else let
171                              fun tab i = str (Char.chr (Char.ord #"e" + i))
172                            in
173                              greek4 @ List.tabulate(numps - 4, tab)
174                            end
175                    in
176                      UnicodeChars.lambda ^
177                      String.concatWith " " params ^ ". " ^
178                      structure_to_string st
179                    end
180                  else structure_to_string st
181                end
182            in
183              case thyopt of
184                SOME thy => (* unprivileged abbrev *)
185                let
186                  val knm = {Thy = thy, Name = abop}
187                in
188                  case Binarymap.peek (abbs, knm) of
189                      NONE => realtype ty (* probably shouldn't happen *)
190                    | SOME st => doabbrev st
191                end
192              | NONE =>
193                let
194                  val privabbs = type_grammar.privileged_abbrevs G
195                in
196                  case Binarymap.peek (privabbs, abop) of
197                      NONE => realtype ty
198                    | SOME thy =>
199                      let
200                        val knm = {Thy = thy, Name = abop}
201                      in
202                        case Binarymap.peek (abbs, knm) of
203                            NONE => raise Fail "Very confused tyabbrev"
204                          | SOME st => doabbrev st
205                      end
206                end
207            end
208          fun print_args grav0 args = let
209            val parens_needed = case args of [_] => false | _ => true
210            val grav = if parens_needed then Top else grav0
211          in
212            paren parens_needed (
213              ublock INCONSISTENT 0 (
214                pr_list (fn arg => pr_ty arg grav (depth - 1))
215                        (add_string "," >> add_break (1, 0)) args
216              )
217            )
218          end
219          val {Thy, Tyop = realTyop, Args = realArgs} = dest_thy_type ty
220        in
221          if abop = "cart" andalso length abargs = 2 andalso
222             Thy = "fcp" andalso realTyop = "cart" andalso !pp_array_types
223          then
224            pr_ty (hd realArgs) Sfx (depth - 1) >>
225            add_string "[" >>
226            pr_ty (hd (tl realArgs)) Top (depth - 1) >>
227            add_string "]"
228          else
229            case abargs of
230              [] => add_ann_string (abop_s, TyOp tooltip)
231            | [arg1, arg2] =>
232              let
233                fun print_suffix_style () =
234                   ublock INCONSISTENT 0 (
235                    (* knowing that there are two args, we know that they will
236                       be printed with parentheses, so the gravity we pass in
237                       here makes no difference. *)
238                     print_args Top abargs >>
239                     add_break(1,0) >>
240                     add_ann_string (abop_s, TyOp tooltip)
241                   )
242              in
243                if isSome thyopt then print_suffix_style()
244                else
245                  case lookup_tyop abop of
246                      SOME (IR(prec, assoc, printthis)) =>
247                      let
248                        val parens_needed =
249                            case grav of
250                                Sfx => true
251                              | Lfx (n, s) => if s = printthis then
252                                                assoc <> LEFT
253                                              else (n >= prec)
254                              | Rfx (n, s) => if s = printthis then
255                                                assoc <> RIGHT
256                                              else (n >= prec)
257                              | _ => false
258                      in
259                        paren parens_needed (
260                          ublock INCONSISTENT 0 (
261                            pr_ty arg1 (Lfx (prec, printthis)) (depth - 1) >>
262                            add_break(1,0) >>
263                            add_ann_string (printthis, TySyn tooltip) >>
264                            add_break(1,0) >>
265                            pr_ty arg2 (Rfx (prec, printthis)) (depth -1)
266                          )
267                        )
268                      end
269                    | NONE => print_suffix_style()
270              end
271            | _ =>
272                ublock INCONSISTENT 0 (
273                  print_args Sfx abargs >>
274                  add_break(1,0) >>
275                  add_ann_string (abop_s, TyOp tooltip)
276                )
277          end
278  end
279in
280  pr_ty
281end
282
283fun pp_type G backend = let
284  val baseprinter = pp_type0 G backend
285in
286  (fn ty => baseprinter ty Top (!Globals.max_print_depth))
287end
288
289fun pp_type_with_depth G backend = let
290  val baseprinter = pp_type0 G backend
291in
292  (fn depth => fn ty => baseprinter ty Top depth)
293end
294
295end; (* struct *)
296
297(* testing
298
299val G = parse_type.BaseHOLgrammar;
300fun p ty =
301  Portable.pp_to_string 75
302   (fn pp => fn ty => type_pp.pp_type G pp ty type_pp.Top 100) ty;
303
304new_type {Name = "fmap", Arity = 2};
305
306val G' = [(0, parse_type.INFIX("->", "fun", parse_type.RIGHT)),
307     (1, parse_type.INFIX("=>", "fmap", parse_type.NONASSOC)),
308     (2, parse_type.INFIX("+", "sum", parse_type.LEFT)),
309     (3, parse_type.INFIX("#", "prod", parse_type.RIGHT)),
310     (100, parse_type.SUFFIX("list", true)),
311     (101, parse_type.SUFFIX("fun", false)),
312     (102, parse_type.SUFFIX("prod", false)),
313     (103, parse_type.SUFFIX("sum", false))];
314fun p ty =
315  Portable.pp_to_string 75
316   (fn pp => fn ty => type_pp.pp_type G' pp ty type_pp.Top 100) ty;
317
318p (Type`:(bool,num)fmap`)
319
320*)
321