printer.ml

   1 (* ========================================================================= *)
   2 (* Simplistic HOL Light prettyprinter, using the OCaml "Format" library.     *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "nets.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Character discrimination.                                                 *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let isspace,issep,isbra,issymb,isalpha,isnum,isalnum =
  17   let charcode s = Char.code(String.get s 0) in
  18   let spaces = " \t\n\r"
  19   and separators = ",;"
  20   and brackets = "()[]{}"
  21   and symbs = "\\!@#$%^&*-+|\\<=>/?~.:"
  22   and alphas = "'abcdefghijklmnopqrstuvwxyz_ABCDEFGHIJKLMNOPQRSTUVWXYZ"
  23   and nums = "0123456789" in
  24   let allchars = spaces^separators^brackets^symbs^alphas^nums in
  25   let csetsize = itlist (max o charcode) (explode allchars) 256 in
  26   let ctable = Array.make csetsize 0 in
  27   do_list (fun c -> Array.set ctable (charcode c) 1) (explode spaces);
  28   do_list (fun c -> Array.set ctable (charcode c) 2) (explode separators);
  29   do_list (fun c -> Array.set ctable (charcode c) 4) (explode brackets);
  30   do_list (fun c -> Array.set ctable (charcode c) 8) (explode symbs);
  31   do_list (fun c -> Array.set ctable (charcode c) 16) (explode alphas);
  32   do_list (fun c -> Array.set ctable (charcode c) 32) (explode nums);
  33   let isspace c = Array.get ctable (charcode c) = 1
  34   and issep c  = Array.get ctable (charcode c) = 2
  35   and isbra c  = Array.get ctable (charcode c) = 4
  36   and issymb c = Array.get ctable (charcode c) = 8
  37   and isalpha c = Array.get ctable (charcode c) = 16
  38   and isnum c = Array.get ctable (charcode c) = 32
  39   and isalnum c = Array.get ctable (charcode c) >= 16 in
  40   isspace,issep,isbra,issymb,isalpha,isnum,isalnum;;
  41
  42 (* ------------------------------------------------------------------------- *)
  43 (* Reserved words.                                                           *)
  44 (* ------------------------------------------------------------------------- *)
  45
  46 let reserve_words,unreserve_words,is_reserved_word,reserved_words =
  47   let reswords = ref ["(";  ")"; "[";   "]";  "{";   "}";
  48                       ":";  ";";  ".";  "|";
  49                       "let"; "in"; "and"; "if"; "then"; "else";
  50                       "match"; "with"; "function"; "->"; "when"] in
  51   (fun ns  -> reswords := union (!reswords) ns),
  52   (fun ns  -> reswords := subtract (!reswords) ns),
  53   (fun n  -> mem n (!reswords)),
  54   (fun () -> !reswords);;
  55
  56 (* ------------------------------------------------------------------------- *)
  57 (* Functions to access the global tables controlling special parse status.   *)
  58 (*                                                                           *)
  59 (*  o List of binders;                                                       *)
  60 (*                                                                           *)
  61 (*  o List of prefixes (right-associated unary functions like negation).     *)
  62 (*                                                                           *)
  63 (*  o List of infixes with their precedences and associations.               *)
  64 (*                                                                           *)
  65 (* Note that these tables are independent of constant/variable status or     *)
  66 (* whether an identifier is symbolic.                                        *)
  67 (* ------------------------------------------------------------------------- *)
  68
  69 let unparse_as_binder,parse_as_binder,parses_as_binder,binders =
  70   let binder_list = ref ([]:string list) in
  71   (fun n  -> binder_list := subtract (!binder_list) [n]),
  72   (fun n  -> binder_list := union (!binder_list) [n]),
  73   (fun n  -> mem n (!binder_list)),
  74   (fun () -> !binder_list);;
  75
  76 let unparse_as_prefix,parse_as_prefix,is_prefix,prefixes =
  77   let prefix_list = ref ([]:string list) in
  78   (fun n  -> prefix_list := subtract (!prefix_list) [n]),
  79   (fun n  -> prefix_list := union (!prefix_list) [n]),
  80   (fun n  -> mem n (!prefix_list)),
  81   (fun () -> !prefix_list);;
  82
  83 let unparse_as_infix,parse_as_infix,get_infix_status,infixes =
  84   let cmp (s,(x,a)) (t,(y,b)) =
  85      x < y or x = y & a > b or x = y & a = b & s < t in
  86   let infix_list = ref ([]:(string * (int * string)) list) in
  87   (fun n     -> infix_list := filter (((<>) n) o fst) (!infix_list)),
  88   (fun (n,d) -> infix_list := sort cmp
  89      ((n,d)::(filter (((<>) n) o fst) (!infix_list)))),
  90   (fun n     -> assoc n (!infix_list)),
  91   (fun ()    -> !infix_list);;
  92
  93 (* ------------------------------------------------------------------------- *)
  94 (* Interface mapping.                                                        *)
  95 (* ------------------------------------------------------------------------- *)
  96
  97 let the_interface = ref ([] :(string * (string * hol_type)) list);;
  98
  99 let the_overload_skeletons = ref ([] : (string * hol_type) list);;
 100
 101 (* ------------------------------------------------------------------------- *)
 102 (* Now the printer.                                                          *)
 103 (* ------------------------------------------------------------------------- *)
 104
 105 include Format;;
 106
 107 set_max_boxes 100;;
 108
 109 (* ------------------------------------------------------------------------- *)
 110 (* Flag determining whether interface/overloading is reversed on printing.   *)
 111 (* ------------------------------------------------------------------------- *)
 112
 113 let reverse_interface_mapping = ref true;;
 114
 115 (* ------------------------------------------------------------------------- *)
 116 (* Determine binary operators that print without surrounding spaces.         *)
 117 (* ------------------------------------------------------------------------- *)
 118
 119 let unspaced_binops = ref [","; ".."; "$"];;
 120
 121 (* ------------------------------------------------------------------------- *)
 122 (* Binary operators to print at start of line when breaking.                 *)
 123 (* ------------------------------------------------------------------------- *)
 124
 125 let prebroken_binops = ref ["==>"];;
 126
 127 (* ------------------------------------------------------------------------- *)
 128 (* Force explicit indications of bound variables in set abstractions.        *)
 129 (* ------------------------------------------------------------------------- *)
 130
 131 let print_unambiguous_comprehensions = ref false;;
 132
 133 (* ------------------------------------------------------------------------- *)
 134 (* Print the universal set UNIV:A->bool as "(:A)".                           *)
 135 (* ------------------------------------------------------------------------- *)
 136
 137 let typify_universal_set = ref true;;
 138
 139 (* ------------------------------------------------------------------------- *)
 140 (* Flag controlling whether hypotheses print.                                *)
 141 (* ------------------------------------------------------------------------- *)
 142
 143 let print_all_thm = ref true;;
 144
 145 (* ------------------------------------------------------------------------- *)
 146 (* Get the name of a constant or variable.                                   *)
 147 (* ------------------------------------------------------------------------- *)
 148
 149 let name_of tm =
 150   match tm with
 151     Var(x,ty) | Const(x,ty) -> x
 152   | _ -> "";;
 153
 154 (* ------------------------------------------------------------------------- *)
 155 (* Printer for types.                                                        *)
 156 (* ------------------------------------------------------------------------- *)
 157
 158 let pp_print_type,pp_print_qtype =
 159   let soc sep flag ss =
 160     if ss = [] then "" else
 161     let s = end_itlist (fun s1 s2 -> s1^sep^s2) ss in
 162     if flag then "("^s^")" else s in
 163   let rec sot pr ty =
 164     try dest_vartype ty with Failure _ ->
 165     match dest_type ty with
 166       con,[] -> con
 167     | "fun",[ty1;ty2] -> soc "->" (pr > 0) [sot 1 ty1; sot 0 ty2]
 168     | "sum",[ty1;ty2] -> soc "+" (pr > 2) [sot 3 ty1; sot 2 ty2]
 169     | "prod",[ty1;ty2] -> soc "#" (pr > 4) [sot 5 ty1; sot 4 ty2]
 170     | "cart",[ty1;ty2] -> soc "^" (pr > 6) [sot 6 ty1; sot 7 ty2]
 171     | con,args -> (soc "," true (map (sot 0) args))^con in
 172   (fun fmt ty -> pp_print_string fmt (sot 0 ty)),
 173   (fun fmt ty -> pp_print_string fmt ("`:" ^ sot 0 ty ^ "`"));;
 174
 175 (* ------------------------------------------------------------------------- *)
 176 (* Allow the installation of user printers. Must fail quickly if N/A.        *)
 177 (* ------------------------------------------------------------------------- *)
 178
 179 let install_user_printer,delete_user_printer,try_user_printer =
 180   let user_printers = ref ([]:(string*(formatter->term->unit))list) in
 181   (fun pr -> user_printers := pr::(!user_printers)),
 182   (fun s -> user_printers := snd(remove (fun (s',_) -> s = s')
 183                                         (!user_printers))),
 184   (fun fmt -> fun tm -> tryfind (fun (_,pr) -> pr fmt tm) (!user_printers));;
 185
 186 (* ------------------------------------------------------------------------- *)
 187 (* Printer for terms.                                                        *)
 188 (* ------------------------------------------------------------------------- *)
 189
 190 let pp_print_term =
 191   let reverse_interface (s0,ty0) =
 192     if not(!reverse_interface_mapping) then s0 else
 193     try fst(find (fun (s,(s',ty)) -> s' = s0 & can (type_match ty ty0) [])
 194                  (!the_interface))
 195     with Failure _ -> s0 in
 196   let DEST_BINARY c tm =
 197     try let il,r = dest_comb tm in
 198         let i,l = dest_comb il in
 199         if i = c or
 200            (is_const i & is_const c &
 201             reverse_interface(dest_const i) = reverse_interface(dest_const c))
 202         then l,r else fail()
 203     with Failure _ -> failwith "DEST_BINARY"
 204   and ARIGHT s =
 205     match snd(get_infix_status s) with
 206     "right" -> true | _ -> false in
 207   let rec powerof10 n =
 208     if abs_num n </ Int 1 then false
 209     else if n =/ Int 1 then true
 210     else powerof10 (n // Int 10) in
 211   let bool_of_term t =
 212     match t with
 213       Const("T",_) -> true
 214     | Const("F",_) -> false
 215     | _ -> failwith "bool_of_term" in
 216   let code_of_term t =
 217     let f,tms = strip_comb t in
 218     if not(is_const f & fst(dest_const f) = "ASCII")
 219        or not(length tms = 8) then failwith "code_of_term"
 220     else
 221        itlist (fun b f -> if b then 1 + 2 * f else 2 * f)
 222               (map bool_of_term (rev tms)) 0 in
 223   let rec dest_clause tm =
 224     let pbod = snd(strip_exists(body(body tm))) in
 225     let s,args = strip_comb pbod in
 226     if name_of s = "_UNGUARDED_PATTERN" & length args = 2 then
 227       [rand(rator(hd args));rand(rator(hd(tl args)))]
 228     else if name_of s = "_GUARDED_PATTERN" & length args = 3 then
 229       [rand(rator(hd args)); hd(tl args); rand(rator(hd(tl(tl args))))]
 230     else failwith "dest_clause" in
 231   let rec dest_clauses tm =
 232     let s,args = strip_comb tm in
 233     if name_of s = "_SEQPATTERN" & length args = 2 then
 234       dest_clause (hd args)::dest_clauses(hd(tl args))
 235     else [dest_clause tm] in
 236   fun fmt ->
 237     let rec print_term prec tm =
 238       try try_user_printer fmt tm with Failure _ ->
 239       try pp_print_string fmt (string_of_num(dest_numeral tm)) with Failure _ ->
 240       try (let tms = dest_list tm in
 241            try if fst(dest_type(hd(snd(dest_type(type_of tm))))) <> "char"
 242                then fail() else
 243                let ccs = map (String.make 1 o Char.chr o code_of_term) tms in
 244                let s = "\"" ^ String.escaped (implode ccs) ^ "\"" in
 245                pp_print_string fmt s
 246            with Failure _ ->
 247                pp_print_string fmt "[";
 248                print_term_sequence "; " 0 tms;
 249                pp_print_string fmt "]")
 250       with Failure _ ->
 251       if is_gabs tm then print_binder prec tm else
 252       let hop,args = strip_comb tm in
 253       let s0 = name_of hop
 254       and ty0 = type_of hop in
 255       let s = reverse_interface (s0,ty0) in
 256       try if s = "EMPTY" & is_const tm & args = [] then
 257           pp_print_string fmt "{}" else fail()
 258       with Failure _ ->
 259       try if s = "UNIV" & !typify_universal_set & is_const tm & args = [] then
 260             let ty = fst(dest_fun_ty(type_of tm)) in
 261             (pp_print_string fmt "(:";
 262              pp_print_type fmt ty;
 263              pp_print_string fmt ")")
 264           else fail()
 265       with Failure _ ->
 266       try if s <> "INSERT" then fail() else
 267           let mems,oth = splitlist (dest_binary "INSERT") tm in
 268           if is_const oth & fst(dest_const oth) = "EMPTY" then
 269             (pp_print_string fmt "{";
 270              print_term_sequence ", " 14 mems;
 271              pp_print_string fmt "}")
 272           else fail()
 273       with Failure _ ->
 274       try if not (s = "GSPEC") then fail() else
 275           let evs,bod = strip_exists(body(rand tm)) in
 276           let bod1,fabs = dest_comb bod in
 277           let bod2,babs = dest_comb bod1 in
 278           let c = rator bod2 in
 279           if fst(dest_const c) <> "SETSPEC" then fail() else
 280           pp_print_string fmt "{";
 281           print_term 0 fabs;
 282           pp_print_string fmt " | ";
 283           (let fvs = frees fabs and bvs = frees babs in
 284            if not(!print_unambiguous_comprehensions) &
 285               set_eq evs
 286                (if (length fvs <= 1 or bvs = []) then fvs
 287                 else intersect fvs bvs)
 288            then ()
 289            else (print_term_sequence "," 14 evs;
 290                  pp_print_string fmt " | "));
 291           print_term 0 babs;
 292           pp_print_string fmt "}"
 293       with Failure _ ->
 294       try let eqs,bod = dest_let tm in
 295           (if prec = 0 then pp_open_hvbox fmt 0
 296            else (pp_open_hvbox fmt 1; pp_print_string fmt "(");
 297            pp_print_string fmt "let ";
 298            print_term 0 (mk_eq(hd eqs));
 299            do_list (fun (v,t) -> pp_print_break fmt 1 0;
 300                                  pp_print_string fmt "and ";
 301                                  print_term 0 (mk_eq(v,t)))
 302                    (tl eqs);
 303            pp_print_string fmt " in";
 304            pp_print_break fmt 1 0;
 305            print_term 0 bod;
 306            if prec = 0 then () else pp_print_string fmt ")";
 307            pp_close_box fmt ())
 308       with Failure _ -> try
 309         if s <> "DECIMAL" then fail() else
 310         let n_num = dest_numeral (hd args)
 311         and n_den = dest_numeral (hd(tl args)) in
 312         if not(powerof10 n_den) then fail() else
 313         let s_num = string_of_num(quo_num n_num n_den) in
 314         let s_den = implode(tl(explode(string_of_num
 315                         (n_den +/ (mod_num n_num n_den))))) in
 316         pp_print_string fmt("#"^s_num^(if n_den = Int 1 then "" else ".")^s_den)
 317       with Failure _ -> try
 318         if s <> "_MATCH" or length args <> 2 then failwith "" else
 319         let cls = dest_clauses(hd(tl args)) in
 320         (if prec = 0 then () else pp_print_string fmt "(";
 321          pp_open_hvbox fmt 0;
 322          pp_print_string fmt "match ";
 323          print_term 0 (hd args);
 324          pp_print_string fmt " with";
 325          pp_print_break fmt 1 2;
 326          print_clauses cls;
 327          pp_close_box fmt ();
 328          if prec = 0 then () else pp_print_string fmt ")")
 329       with Failure _ -> try
 330         if s <> "_FUNCTION" or length args <> 1 then failwith "" else
 331         let cls = dest_clauses(hd args) in
 332         (if prec = 0 then () else pp_print_string fmt "(";
 333          pp_open_hvbox fmt 0;
 334          pp_print_string fmt "function";
 335          pp_print_break fmt 1 2;
 336          print_clauses cls;
 337          pp_close_box fmt ();
 338          if prec = 0 then () else pp_print_string fmt ")")
 339       with Failure _ ->
 340       if s = "COND" & length args = 3 then
 341         (if prec = 0 then () else pp_print_string fmt "(";
 342          pp_open_hvbox fmt (-1);
 343          pp_print_string fmt "if ";
 344          print_term 0 (hd args);
 345          pp_print_break fmt 0 0;
 346          pp_print_string fmt " then ";
 347          print_term 0 (hd(tl args));
 348          pp_print_break fmt 0 0;
 349          pp_print_string fmt " else ";
 350          print_term 0 (hd(tl(tl args)));
 351          pp_close_box fmt ();
 352          if prec = 0 then () else pp_print_string fmt ")")
 353       else if is_prefix s & length args = 1 then
 354         (if prec = 1000 then pp_print_string fmt "(" else ();
 355          pp_print_string fmt s;
 356          (if isalnum s or
 357            s = "--" &
 358            length args = 1 &
 359            (try let l,r = dest_comb(hd args) in
 360                 let s0 = name_of l and ty0 = type_of l in
 361                 reverse_interface (s0,ty0) = "--" or
 362                 mem (fst(dest_const l)) ["real_of_num"; "int_of_num"]
 363             with Failure _ -> false) or
 364            s = "~" & length args = 1 & is_neg(hd args)
 365           then pp_print_string fmt " " else ());
 366          print_term 999 (hd args);
 367          if prec = 1000 then pp_print_string fmt ")" else ())
 368       else if parses_as_binder s & length args = 1 & is_gabs (hd args) then
 369         print_binder prec tm
 370       else if can get_infix_status s & length args = 2 then
 371         let bargs =
 372           if ARIGHT s then
 373             let tms,tmt = splitlist (DEST_BINARY hop) tm in tms@[tmt]
 374           else
 375             let tmt,tms = rev_splitlist (DEST_BINARY hop) tm in tmt::tms in
 376         let newprec = fst(get_infix_status s) in
 377         (if newprec <= prec then
 378           (pp_open_hvbox fmt 1; pp_print_string fmt "(")
 379          else pp_open_hvbox fmt 0;
 380          print_term newprec (hd bargs);
 381          do_list (fun x -> if mem s (!unspaced_binops) then ()
 382                            else if mem s (!prebroken_binops)
 383                            then pp_print_break fmt 1 0
 384                            else pp_print_string fmt " ";
 385                            pp_print_string fmt s;
 386                            if mem s (!unspaced_binops)
 387                            then pp_print_break fmt 0 0
 388                            else if mem s (!prebroken_binops)
 389                            then pp_print_string fmt " "
 390                            else pp_print_break fmt 1 0;
 391                            print_term newprec x) (tl bargs);
 392          if newprec <= prec then pp_print_string fmt ")" else ();
 393          pp_close_box fmt ())
 394       else if (is_const hop or is_var hop) & args = [] then
 395         let s' = if parses_as_binder s or can get_infix_status s or is_prefix s
 396                  then "("^s^")" else s in
 397         pp_print_string fmt s'
 398       else
 399         let l,r = dest_comb tm in
 400         (pp_open_hvbox fmt 0;
 401          if prec = 1000 then pp_print_string fmt "(" else ();
 402          print_term 999 l;
 403          (if try mem (fst(dest_const l)) ["real_of_num"; "int_of_num"]
 404              with Failure _ -> false
 405           then () else pp_print_space fmt ());
 406          print_term 1000 r;
 407          if prec = 1000 then pp_print_string fmt ")" else ();
 408          pp_close_box fmt ())
 409
 410     and print_term_sequence sep prec tms =
 411       if tms = [] then () else
 412       (print_term prec (hd tms);
 413        let ttms = tl tms in
 414        if ttms = [] then ()
 415        else (pp_print_string fmt sep; print_term_sequence sep prec ttms))
 416
 417     and print_binder prec tm =
 418       let absf = is_gabs tm in
 419       let s = if absf then "\\" else name_of(rator tm) in
 420       let rec collectvs tm =
 421         if absf then
 422           if is_abs tm then
 423             let v,t = dest_abs tm in
 424             let vs,bod = collectvs t in (false,v)::vs,bod
 425           else if is_gabs tm then
 426             let v,t = dest_gabs tm in
 427             let vs,bod = collectvs t in (true,v)::vs,bod
 428           else [],tm
 429         else if is_comb tm & name_of(rator tm) = s then
 430           if is_abs(rand tm) then
 431             let v,t = dest_abs(rand tm) in
 432             let vs,bod = collectvs t in (false,v)::vs,bod
 433           else if is_gabs(rand tm) then
 434             let v,t = dest_gabs(rand tm) in
 435             let vs,bod = collectvs t in (true,v)::vs,bod
 436           else [],tm
 437         else [],tm in
 438       let vs,bod = collectvs tm in
 439       ((if prec = 0 then pp_open_hvbox fmt 4
 440         else (pp_open_hvbox fmt 5; pp_print_string fmt "("));
 441        pp_print_string fmt s;
 442        (if isalnum s then pp_print_string fmt " " else ());
 443        do_list (fun (b,x) ->
 444          (if b then pp_print_string fmt "(" else ());
 445          print_term 0 x;
 446          (if b then pp_print_string fmt ")" else ());
 447          pp_print_string fmt " ") (butlast vs);
 448        (if fst(last vs) then pp_print_string fmt "(" else ());
 449        print_term 0 (snd(last vs));
 450        (if fst(last vs) then pp_print_string fmt ")" else ());
 451        pp_print_string fmt ".";
 452        (if length vs = 1 then pp_print_string fmt " "
 453         else pp_print_space fmt ());
 454        print_term 0 bod;
 455        (if prec = 0 then () else pp_print_string fmt ")");
 456        pp_close_box fmt ())
 457   and print_clauses cls =
 458     match cls with
 459       [c] -> print_clause c
 460     | c::cs -> (print_clause c;
 461                 pp_print_break fmt 1 0;
 462                 pp_print_string fmt "| ";
 463                 print_clauses cs)
 464   and print_clause cl =
 465     match cl with
 466      [p;g;r] -> (print_term 1 p;
 467                  pp_print_string fmt " when ";
 468                  print_term 1 g;
 469                  pp_print_string fmt " -> ";
 470                  print_term 1 r)
 471    | [p;r] -> (print_term 1 p;
 472                pp_print_string fmt " -> ";
 473                print_term 1 r)
 474   in print_term 0;;
 475
 476 (* ------------------------------------------------------------------------- *)
 477 (* Print term with quotes.                                                   *)
 478 (* ------------------------------------------------------------------------- *)
 479
 480 let pp_print_qterm fmt tm =
 481   pp_print_string fmt "`";
 482   pp_print_term fmt tm;
 483   pp_print_string fmt "`";;
 484
 485 (* ------------------------------------------------------------------------- *)
 486 (* Printer for theorems.                                                     *)
 487 (* ------------------------------------------------------------------------- *)
 488
 489 let pp_print_thm fmt th =
 490   let asl,tm = dest_thm th in
 491   (if not (asl = []) then
 492     (if !print_all_thm then
 493       (pp_print_term fmt (hd asl);
 494        do_list (fun x -> pp_print_string fmt ",";
 495                          pp_print_space fmt ();
 496                          pp_print_term fmt x)
 497                (tl asl))
 498      else pp_print_string fmt "...";
 499      pp_print_space fmt ())
 500    else ();
 501    pp_open_hbox fmt();
 502    pp_print_string fmt "|- ";
 503    pp_print_term fmt tm;
 504    pp_close_box fmt ());;
 505
 506 (* ------------------------------------------------------------------------- *)
 507 (* Print on standard output.                                                 *)
 508 (* ------------------------------------------------------------------------- *)
 509
 510 let print_type = pp_print_type std_formatter;;
 511 let print_qtype = pp_print_qtype std_formatter;;
 512 let print_term = pp_print_term std_formatter;;
 513 let print_qterm = pp_print_qterm std_formatter;;
 514 let print_thm = pp_print_thm std_formatter;;
 515
 516 (* ------------------------------------------------------------------------- *)
 517 (* Install all the printers.                                                 *)
 518 (* ------------------------------------------------------------------------- *)
 519
 520 #install_printer print_qtype;;
 521 #install_printer print_qterm;;
 522 #install_printer print_thm;;
 523
 524 (* ------------------------------------------------------------------------- *)
 525 (* Conversions to string.                                                    *)
 526 (* ------------------------------------------------------------------------- *)
 527
 528 let print_to_string printer =
 529   let buf = Buffer.create 16 in
 530   let fmt = formatter_of_buffer buf in
 531   let () = pp_set_max_boxes fmt 100 in
 532   let print = printer fmt in
 533   let flush = pp_print_flush fmt in
 534   fun x ->
 535     let () = pp_set_margin fmt (get_margin ()) in
 536     let () = print x in
 537     let () = flush () in
 538     let s = Buffer.contents buf in
 539     let () = Buffer.reset buf in
 540     s;;
 541
 542 let string_of_type = print_to_string pp_print_type;;
 543 let string_of_term = print_to_string pp_print_term;;
 544 let string_of_thm = print_to_string pp_print_thm;;