1 (* ========================================================================= *)
2 (* Simplistic HOL Light prettyprinter, using the OCaml "Format" library. *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* ========================================================================= *)
12 (* ------------------------------------------------------------------------- *)
13 (* Character discrimination. *)
14 (* ------------------------------------------------------------------------- *)
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"
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;;
42 (* ------------------------------------------------------------------------- *)
44 (* ------------------------------------------------------------------------- *)
46 let reserve_words,unreserve_words,is_reserved_word,reserved_words =
47 let reswords = ref ["("; ")"; "["; "]"; "{"; "}";
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);;
56 (* ------------------------------------------------------------------------- *)
57 (* Functions to access the global tables controlling special parse status. *)
59 (* o List of binders; *)
61 (* o List of prefixes (right-associated unary functions like negation). *)
63 (* o List of infixes with their precedences and associations. *)
65 (* Note that these tables are independent of constant/variable status or *)
66 (* whether an identifier is symbolic. *)
67 (* ------------------------------------------------------------------------- *)
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);;
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);;
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);;
93 (* ------------------------------------------------------------------------- *)
94 (* Interface mapping. *)
95 (* ------------------------------------------------------------------------- *)
97 let the_interface = ref ([] :(string * (string * hol_type)) list);;
99 let the_overload_skeletons = ref ([] : (string * hol_type) list);;
101 (* ------------------------------------------------------------------------- *)
102 (* Now the printer. *)
103 (* ------------------------------------------------------------------------- *)
109 (* ------------------------------------------------------------------------- *)
110 (* Flag determining whether interface/overloading is reversed on printing. *)
111 (* ------------------------------------------------------------------------- *)
113 let reverse_interface_mapping = ref true;;
115 (* ------------------------------------------------------------------------- *)
116 (* Determine binary operators that print without surrounding spaces. *)
117 (* ------------------------------------------------------------------------- *)
119 let unspaced_binops = ref [","; ".."; "$"];;
121 (* ------------------------------------------------------------------------- *)
122 (* Binary operators to print at start of line when breaking. *)
123 (* ------------------------------------------------------------------------- *)
125 let prebroken_binops = ref ["==>"];;
127 (* ------------------------------------------------------------------------- *)
128 (* Force explicit indications of bound variables in set abstractions. *)
129 (* ------------------------------------------------------------------------- *)
131 let print_unambiguous_comprehensions = ref false;;
133 (* ------------------------------------------------------------------------- *)
134 (* Print the universal set UNIV:A->bool as "(:A)". *)
135 (* ------------------------------------------------------------------------- *)
137 let typify_universal_set = ref true;;
139 (* ------------------------------------------------------------------------- *)
140 (* Flag controlling whether hypotheses print. *)
141 (* ------------------------------------------------------------------------- *)
143 let print_all_thm = ref true;;
145 (* ------------------------------------------------------------------------- *)
146 (* Get the name of a constant or variable. *)
147 (* ------------------------------------------------------------------------- *)
151 Var(x,ty) | Const(x,ty) -> x
154 (* ------------------------------------------------------------------------- *)
155 (* Printer for types. *)
156 (* ------------------------------------------------------------------------- *)
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
164 try dest_vartype ty with Failure _ ->
165 match dest_type ty with
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 ^ "`"));;
175 (* ------------------------------------------------------------------------- *)
176 (* Allow the installation of user printers. Must fail quickly if N/A. *)
177 (* ------------------------------------------------------------------------- *)
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')
184 (fun fmt -> fun tm -> tryfind (fun (_,pr) -> pr fmt tm) (!user_printers));;
186 (* ------------------------------------------------------------------------- *)
187 (* Printer for terms. *)
188 (* ------------------------------------------------------------------------- *)
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) [])
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
200 (is_const i & is_const c &
201 reverse_interface(dest_const i) = reverse_interface(dest_const c))
203 with Failure _ -> failwith "DEST_BINARY"
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
214 | Const("F",_) -> false
215 | _ -> failwith "bool_of_term" in
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"
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
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"
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
247 pp_print_string fmt "[";
248 print_term_sequence "; " 0 tms;
249 pp_print_string fmt "]")
251 if is_gabs tm then print_binder prec tm else
252 let hop,args = strip_comb tm in
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()
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 ")")
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 "}")
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 "{";
282 pp_print_string fmt " | ";
283 (let fvs = frees fabs and bvs = frees babs in
284 if not(!print_unambiguous_comprehensions) &
286 (if (length fvs <= 1 or bvs = []) then fvs
287 else intersect fvs bvs)
289 else (print_term_sequence "," 14 evs;
290 pp_print_string fmt " | "));
292 pp_print_string fmt "}"
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)))
303 pp_print_string fmt " in";
304 pp_print_break fmt 1 0;
306 if prec = 0 then () else pp_print_string 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 "(";
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;
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 "(";
334 pp_print_string fmt "function";
335 pp_print_break fmt 1 2;
338 if prec = 0 then () else pp_print_string fmt ")")
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)));
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;
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
370 else if can get_infix_status s & length args = 2 then
373 let tms,tmt = splitlist (DEST_BINARY hop) tm in tms@[tmt]
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 ();
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'
399 let l,r = dest_comb tm in
400 (pp_open_hvbox fmt 0;
401 if prec = 1000 then pp_print_string fmt "(" else ();
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 ());
407 if prec = 1000 then pp_print_string fmt ")" else ();
410 and print_term_sequence sep prec tms =
411 if tms = [] then () else
412 (print_term prec (hd tms);
415 else (pp_print_string fmt sep; print_term_sequence sep prec ttms))
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 =
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
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
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 ());
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 ());
455 (if prec = 0 then () else pp_print_string fmt ")");
457 and print_clauses cls =
459 [c] -> print_clause c
460 | c::cs -> (print_clause c;
461 pp_print_break fmt 1 0;
462 pp_print_string fmt "| ";
464 and print_clause cl =
466 [p;g;r] -> (print_term 1 p;
467 pp_print_string fmt " when ";
469 pp_print_string fmt " -> ";
471 | [p;r] -> (print_term 1 p;
472 pp_print_string fmt " -> ";
476 (* ------------------------------------------------------------------------- *)
477 (* Print term with quotes. *)
478 (* ------------------------------------------------------------------------- *)
480 let pp_print_qterm fmt tm =
481 pp_print_string fmt "`";
482 pp_print_term fmt tm;
483 pp_print_string fmt "`";;
485 (* ------------------------------------------------------------------------- *)
486 (* Printer for theorems. *)
487 (* ------------------------------------------------------------------------- *)
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 ();
498 else pp_print_string fmt "...";
499 pp_print_space fmt ())
502 pp_print_string fmt "|- ";
503 pp_print_term fmt tm;
504 pp_close_box fmt ());;
506 (* ------------------------------------------------------------------------- *)
507 (* Print on standard output. *)
508 (* ------------------------------------------------------------------------- *)
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;;
516 (* ------------------------------------------------------------------------- *)
517 (* Install all the printers. *)
518 (* ------------------------------------------------------------------------- *)
520 #install_printer print_qtype;;
521 #install_printer print_qterm;;
522 #install_printer print_thm;;
524 (* ------------------------------------------------------------------------- *)
525 (* Conversions to string. *)
526 (* ------------------------------------------------------------------------- *)
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
535 let () = pp_set_margin fmt (get_margin ()) in
538 let s = Buffer.contents buf in
539 let () = Buffer.reset buf in
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;;