6 (* ------------------------------------------------------------------------- *)
7 (* Protection for HTML output *)
8 (* ------------------------------------------------------------------------- *)
9 let output_functions = get_all_formatter_output_functions();;
11 let rec make_aux n s str =
14 | _ -> make_aux (n - 1) s (str ^ s)
18 let new_output_functions (x,y,z,w) = set_all_formatter_output_functions x y (fun () ->x "<br>" 0 4) (fun n -> x (make n " ") 0 (6 * n));;
19 let restore_output_functions (x,y,z,w) = set_all_formatter_output_functions x y z w;;
21 let pp_print_string' = pp_print_string;;
22 let print_string' = print_string;;
23 let rec pp_print_string fmt str =
24 match (String.length str) with
27 if (Str.string_match (Str.regexp "!") str 0)
29 pp_print_as fmt 1 "∀";
30 pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
33 if (Str.string_match (Str.regexp "\?") str 0)
35 pp_print_as fmt 1 "∃";
36 pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
39 if (Str.string_match (Str.regexp "--") str 0)
41 pp_print_as fmt 1 "−";
42 pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
45 if (Str.string_match (Str.regexp "|-") str 0)
47 pp_print_as fmt 1 "⊢";
48 pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
51 if (Str.string_match (Str.regexp "~") str 0)
53 pp_print_as fmt 1 "¬";
54 pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
57 if (Str.string_match (Str.regexp "<=>") str 0)
59 pp_print_as fmt 1 "⇔";
60 pp_print_string fmt (String.sub str 3 ((String.length str) - 3))
63 if (Str.string_match (Str.regexp "==>") str 0)
65 pp_print_as fmt 1 "⇒";
66 pp_print_string fmt (String.sub str 3 ((String.length str) - 3))
69 if (Str.string_match (Str.regexp ">=") str 0)
71 pp_print_as fmt 1 "≥";
72 pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
75 if (Str.string_match (Str.regexp "<=") str 0)
77 pp_print_as fmt 1 "≤";
78 pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
81 if (Str.string_match (Str.regexp "\\\\/") str 0)
83 pp_print_as fmt 1 "∨";
84 pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
87 if (Str.string_match (Str.regexp "/\\\\") str 0)
89 pp_print_as fmt 1 "∧";
90 pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
93 if (Str.string_match (Str.regexp "\\\\") str 0)
95 pp_print_as fmt 1 "λ";
96 pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
99 if (Str.string_match (Str.regexp ">") str 0)
101 pp_print_as fmt 1 ">";
102 pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
105 if (Str.string_match (Str.regexp "<") str 0)
107 pp_print_as fmt 1 "<";
108 pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
111 if (Str.string_match (Str.regexp " ") str 0)
113 pp_print_as fmt 1 " ";
114 pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
118 pp_print_as fmt 1 (String.sub str 0 1);
119 pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
121 let print_string = pp_print_string std_formatter;;
123 (* ------------------------------------------------------------------------- *)
124 (* Determine binary operators that print without surrounding spaces. *)
125 (* ------------------------------------------------------------------------- *)
127 let unspaced_binops = ref [","; ".."; "$"];;
129 (* ------------------------------------------------------------------------- *)
130 (* Binary operators to print at start of line when breaking. *)
131 (* ------------------------------------------------------------------------- *)
133 let prebroken_binops = ref ["==>"];;
135 (* ------------------------------------------------------------------------- *)
136 (* Force explicit indications of bound variables in set abstractions. *)
137 (* ------------------------------------------------------------------------- *)
139 (* let print_unambiguous_comprehensions = ref false;; *)
141 (* ------------------------------------------------------------------------- *)
142 (* Print the universal set UNIV:A->bool as "(:A)". *)
143 (* ------------------------------------------------------------------------- *)
145 let typify_universal_set = ref true;;
147 (* ------------------------------------------------------------------------- *)
148 (* Flag controlling whether hypotheses print. *)
149 (* ------------------------------------------------------------------------- *)
151 let print_all_thm = ref true;;
153 (* ------------------------------------------------------------------------- *)
154 (* Flag determining whether interface/overloading is reversed on printing. *)
155 (* ------------------------------------------------------------------------- *)
156 let reverse_interface_mapping = ref true;;
158 (* ------------------------------------------------------------------------- *)
159 (* Uses the_interface to lookup the names of operators *)
160 (* ------------------------------------------------------------------------- *)
161 let reverse_interface (s0,ty0) =
162 if not(!reverse_interface_mapping) then s0 else
163 try fst(find (fun (s,(s',ty)) -> s' = s0 & can (type_match ty ty0) [])
165 with Failure _ -> s0;;
167 (* ------------------------------------------------------------------------- *)
168 (* Get the name of a constant or variable. *)
169 (* ------------------------------------------------------------------------- *)
173 Var(x,ty) | Const(x,ty) -> x
176 (* ------------------------------------------------------------------------- *)
177 (* Printer for types. *)
178 (* ------------------------------------------------------------------------- *)
180 let pp_print_type,pp_print_qtype =
181 let soc sep flag ss =
182 if ss = [] then "" else
183 let s = end_itlist (fun s1 s2 -> s1^sep^s2) ss in
184 if flag then "("^s^")" else s in
186 try dest_vartype ty with Failure _ ->
187 match dest_type ty with
189 | "fun",[ty1;ty2] -> soc "->" (pr > 0) [sot 1 ty1; sot 0 ty2]
190 | "sum",[ty1;ty2] -> soc "+" (pr > 2) [sot 3 ty1; sot 2 ty2]
191 | "prod",[ty1;ty2] -> soc "#" (pr > 4) [sot 5 ty1; sot 4 ty2]
192 | "cart",[ty1;ty2] -> soc "^" (pr > 6) [sot 6 ty1; sot 7 ty2]
193 | con,args -> (soc "," true (map (sot 0) args))^con in
194 (fun fmt ty -> pp_print_string fmt (sot 0 ty)),
195 (fun fmt ty -> pp_print_string fmt ("`:" ^ sot 0 ty ^ "`"));;
197 (* ------------------------------------------------------------------------- *)
198 (* This returns L and R if OP = c in (tm:= L OP R) *)
199 (* ------------------------------------------------------------------------- *)
200 let dest_binary' c tm =
201 try let il,r = dest_comb tm in
202 let i,l = dest_comb il in
204 (is_const i & is_const c &
205 reverse_interface(dest_const i) = reverse_interface(dest_const c))
207 with Failure _ -> failwith "dest_binary";;
209 (* ------------------------------------------------------------------------- *)
210 (* string -> bool Lookup to see if operator of string is right assoc *)
211 (* ------------------------------------------------------------------------- *)
212 let is_right_assoc s =
213 match snd(get_infix_status s) with
217 (* ------------------------------------------------------------------------- *)
219 (* ------------------------------------------------------------------------- *)
220 let rec power_of_10 n =
221 if abs_num n </ Int 1 then false
222 else if n =/ Int 1 then true
223 else power_of_10 (n // Int 10);;
225 (* ------------------------------------------------------------------------- *)
226 (* term -> bool converts bool term to ocaml bool *)
227 (* ------------------------------------------------------------------------- *)
231 | Const("F",_) -> false
232 | _ -> failwith "bool_of_term";;
234 (* ------------------------------------------------------------------------- *)
235 (* term -> int converts ASCII term into int equiv *)
236 (* ------------------------------------------------------------------------- *)
238 let f,tms = strip_comb t in
239 if not(is_const f & fst(dest_const f) = "ASCII")
240 or not(length tms = 8) then failwith "code_of_term"
242 itlist (fun b f -> if b then 1 + 2 * f else 2 * f)
243 (map bool_of_term (rev tms)) 0;;
245 (* ------------------------------------------------------------------------- *)
247 (* ------------------------------------------------------------------------- *)
248 let rec dest_clause tm =
249 let pbod = snd(strip_exists(body(body tm))) in
250 let s,args = strip_comb pbod in
251 if name_of s = "_UNGUARDED_PATTERN" & length args = 2 then
252 [rand(rator(hd args));rand(rator(hd(tl args)))]
253 else if name_of s = "_GUARDED_PATTERN" & length args = 3 then
254 [rand(rator(hd args)); hd(tl args); rand(rator(hd(tl(tl args))))]
255 else failwith "dest_clause" ;;
257 (* ------------------------------------------------------------------------- *)
259 (* ------------------------------------------------------------------------- *)
260 let rec dest_clauses tm =
261 let s,args = strip_comb tm in
262 if name_of s = "_SEQPATTERN" & length args = 2 then
263 dest_clause (hd args)::dest_clauses(hd(tl args))
264 else [dest_clause tm];;
267 (* ------------------------------------------------------------------------- *)
268 (* Allow the installation of user printers. Must fail quickly if N/A. *)
269 (* ------------------------------------------------------------------------- *)
270 let install_user_printer,delete_user_printer,try_user_printer =
271 let user_printers = ref ([]:(string*(term->unit))list) in
272 (fun pr -> user_printers := pr::(!user_printers)),
273 (fun s -> user_printers := snd(remove (fun (s',_) -> s = s')
275 (fun tm -> tryfind (fun (_,pr) -> pr tm) (!user_printers));;
281 (* ------------------------------------------------------------------------- *)
282 (* Type to determine how/(what tag) to print *)
283 (* ------------------------------------------------------------------------- *)
284 type term_type = Numeral | List | Char_list | Generalized_abstraction |
285 Empty | Universal | G_spec | Let | Decimal | Match | Function |
286 Insert | Cond | Other;;
288 (* ------------------------------------------------------------------------- *)
289 (* term -> term_type *)
290 (* ------------------------------------------------------------------------- *)
291 let rec get_term_type tm =
292 if is_numeral tm then Numeral
293 else if is_list tm then
295 try if fst(dest_type(hd(snd(dest_type(type_of tm))))) <> "char"
297 else Char_list with Failure _ -> List
299 else if is_gabs tm then Generalized_abstraction
302 let hop,args = strip_comb tm in
304 and ty0 = type_of hop in
305 let s = reverse_interface (s0,ty0) in
306 if s = "EMPTY" & is_const tm & args = [] then Empty
307 else if s = "UNIV" & !typify_universal_set & is_const tm & args = []
309 else if s = "INSERT" &
310 is_const (snd(splitlist (dest_binary "INSERT") tm)) &
315 dest_binary "INSERT") tm))) = "EMPTY" then Insert
316 else if (s = "GSPEC") &
322 o body o rand)tm )) = "SETSPEC" then G_spec
323 else if is_let tm then Let
324 else if s = "DECIMAL" &
325 (power_of_10 ((dest_numeral o hd o tl)args)) then Decimal
326 else if s = "_MATCH" &
327 length args = 2 then Match
328 else if s = "_FUNCTION" &
329 length args = 1 then Function
330 else if s = "COND" & length args = 3 then Cond
335 (* ------------------------------------------------------------------------- *)
336 (* Printer for terms. *)
337 (* ------------------------------------------------------------------------- *)
340 let rec print_subterm prec tm =
341 try try_user_printer tm with Failure _ ->
342 let hop,args = strip_comb tm in
344 and ty0 = type_of hop in
345 let s = reverse_interface (s0,ty0) in
346 match get_term_type tm with
349 open_tag "span class=\"Numeral\"";
350 pp_print_string fmt (string_of_num(dest_numeral tm));
355 open_tag "span class=\"Char_list\"";
356 pp_print_string fmt (
357 "\"" ^ String.escaped (implode (map (
361 (dest_list tm) )) ^ "\"");
366 open_tag "span class=\"List\"";
367 pp_print_string fmt "[";
368 print_term_sequence "; " 0 (dest_list tm);
369 pp_print_string fmt "]";
372 |Generalized_abstraction ->
374 open_tag "span class=\"Generalized_abstraction\"";
375 print_binder prec tm;
380 open_tag "span class=\"Empty\"";
381 pp_print_string fmt "{}";
386 let ty = fst(dest_fun_ty(type_of tm)) in
388 open_tag "span class=\"Universal\"";
389 pp_print_string fmt "(:";
390 pp_print_type fmt ty;
391 pp_print_string fmt ")";
397 open_tag "span class=\"Insert\"";
398 pp_print_string fmt "{";
399 print_term_sequence ", " 14 (
401 splitlist (dest_binary "INSERT") tm));
402 pp_print_string fmt "}";
408 let evs,bod = strip_exists(body(rand tm)) in
409 let bod1,fabs = dest_comb bod in
410 let bod2,babs = dest_comb bod1 in
411 (* let c = rator bod2 in*)
413 (* (let fvs = frees fabs and bvs = frees babs in
414 if not(!print_unambiguous_comprehensions) &
416 (if (length fvs <= 1 or bvs = []) then fvs
417 else intersect fvs bvs)
419 else (print_term_sequence "," 14 evs;
420 pp_print_string fmt " | "));
422 open_tag "span class=\"G_spec\"";
423 pp_print_string fmt "{";
424 print_subterm 0 fabs;
425 pp_print_string fmt " | ";
426 print_subterm 0 babs;
427 pp_print_string fmt "}";
432 open_tag "span class=\"Let\"";
433 let eqs,bod = dest_let tm in
434 (if prec = 0 then pp_open_hvbox fmt 0
435 else (pp_open_hvbox fmt 1; pp_print_string fmt "(");
436 pp_print_string fmt "let ";
437 print_subterm 0 (mk_eq(hd eqs));
438 do_list (fun (v,t) -> pp_print_break fmt 1 0;
439 pp_print_string fmt "and ";
440 print_subterm 0 (mk_eq(v,t)))
442 pp_print_string fmt " in";
443 pp_print_break fmt 1 0;
445 if prec = 0 then () else pp_print_string fmt ")";
446 pp_close_box fmt ());
451 open_tag "span class=\"Decimal\"";
452 let n_num = dest_numeral (hd args)
453 and n_den = dest_numeral (hd(tl args)) in
454 let s_num = string_of_num(quo_num n_num n_den) in
456 tl(explode(string_of_num
457 (n_den +/ (mod_num n_num n_den))))) in
459 "#"^s_num^(if n_den = Int 1 then "" else ".")^s_den);
465 open_tag "span class=\"Match\"";
466 let cls = dest_clauses(hd(tl args)) in
467 (if prec = 0 then () else pp_print_string fmt "(";
469 pp_print_string fmt "match ";
470 print_subterm 0 (hd args);
471 pp_print_string fmt " with";
472 pp_print_break fmt 1 2;
475 if prec = 0 then () else pp_print_string fmt ")");
480 open_tag "span class=\"Function\"";
481 let cls = dest_clauses(hd args) in
482 (if prec = 0 then () else pp_print_string fmt "(";
484 pp_print_string fmt "function";
485 pp_print_break fmt 1 2;
488 if prec = 0 then () else pp_print_string fmt ")");
493 open_tag "span class=\"Cond\"";
495 (if prec = 0 then () else pp_print_string fmt "(";
496 pp_open_hvbox fmt (-1);
497 pp_print_string fmt "if ";
498 print_subterm 0 (hd args);
499 pp_print_break fmt 0 0;
500 pp_print_string fmt " then ";
501 print_subterm 0 (hd(tl args));
502 pp_print_break fmt 0 0;
503 pp_print_string fmt " else ";
504 print_subterm 0 (hd(tl(tl args)));
506 if prec = 0 then () else pp_print_string fmt ")");
511 if is_prefix s & length args = 1 then
512 (if prec = 1000 then pp_print_string fmt "(" else ();
513 pp_print_string fmt s;
517 (try let l,r = dest_comb(hd args) in
518 let s0 = name_of l in
520 mem (fst(dest_const l)) ["real_of_num"; "int_of_num"]
521 with Failure _ -> false) or
522 s = "~" & length args = 1 & is_neg(hd args)
523 then pp_print_string fmt " " else ());
524 print_subterm 999 (hd args);
525 if prec = 1000 then pp_print_string fmt ")" else ())
526 else if parses_as_binder s & length args = 1 & is_gabs (hd args) then
528 else if can get_infix_status s & length args = 2 then
530 if is_right_assoc s then
531 let tms,tmt = splitlist (dest_binary' hop) tm in tms@[tmt]
533 let tmt,tms = rev_splitlist (dest_binary' hop) tm in tmt::tms in
534 let newprec = fst(get_infix_status s) in
535 (if newprec <= prec then
536 (pp_open_hvbox fmt 1; pp_print_string fmt "(")
537 else pp_open_hvbox fmt 0;
538 print_subterm newprec (hd bargs);
539 do_list (fun x -> if mem s (!unspaced_binops) then ()
540 else if mem s (!prebroken_binops)
541 then pp_print_break fmt 1 0
542 else pp_print_string fmt " ";
543 pp_print_string fmt s;
544 if mem s (!unspaced_binops)
545 then pp_print_break fmt 0 0
546 else if mem s (!prebroken_binops)
547 then pp_print_string fmt " "
548 else pp_print_break fmt 1 0;
549 print_subterm newprec x) (tl bargs);
550 if newprec <= prec then pp_print_string fmt ")" else ();
552 else if (is_const hop or is_var hop) & args = [] then
553 let s' = if parses_as_binder s or can get_infix_status s or is_prefix s
554 then "("^s^")" else s in
555 pp_print_string fmt s'
557 let l,r = dest_comb tm in
558 (pp_open_hvbox fmt 0;
559 if prec = 1000 then pp_print_string fmt "(" else ();
561 (if try mem (fst(dest_const l)) ["real_of_num"; "int_of_num"]
562 with Failure _ -> false
563 then () else pp_print_space fmt ());
564 print_subterm 1000 r;
565 if prec = 1000 then pp_print_string fmt ")" else ();
572 (* Code is safe down here *)
577 and print_term_sequence sep prec tms =
578 if tms = [] then () else
579 (print_subterm prec (hd tms);
582 else (pp_print_string fmt sep; print_term_sequence sep prec ttms))
585 and print_clauses cls =
587 [c] -> print_clause c
588 | c::cs -> (print_clause c;
589 pp_print_break fmt 1 0;
590 pp_print_string fmt "| ";
593 and print_binder prec tm =
594 let absf = is_gabs tm in
595 let s = if absf then "\\" else name_of(rator tm) in
596 let rec collectvs tm =
599 let v,t = dest_abs tm in
600 let vs,bod = collectvs t in (false,v)::vs,bod
601 else if is_gabs tm then
602 let v,t = dest_gabs tm in
603 let vs,bod = collectvs t in (true,v)::vs,bod
605 else if is_comb tm & name_of(rator tm) = s then
606 if is_abs(rand tm) then
607 let v,t = dest_abs(rand tm) in
608 let vs,bod = collectvs t in (false,v)::vs,bod
609 else if is_gabs(rand tm) then
610 let v,t = dest_gabs(rand tm) in
611 let vs,bod = collectvs t in (true,v)::vs,bod
614 let vs,bod = collectvs tm in
616 open_tag "span class=\"binder\"";
617 (if prec = 0 then pp_open_hvbox fmt 4
618 else (pp_open_hvbox fmt 5; pp_print_string fmt "("));
619 pp_print_string fmt s;
620 (if isalnum s then pp_print_string fmt " " else ());
621 do_list (fun (b,x) ->
622 (if b then pp_print_string fmt "(" else ());
624 (if b then pp_print_string fmt ")" else ());
625 pp_print_string fmt " ") (butlast vs);
626 (if fst(last vs) then pp_print_string fmt "(" else ());
627 print_subterm 0 (snd(last vs));
628 (if fst(last vs) then pp_print_string fmt ")" else ());
629 pp_print_string fmt ".";
630 (if length vs = 1 then pp_print_string fmt " "
631 else pp_print_space fmt ());
633 (if prec = 0 then () else pp_print_string fmt ")");
638 and print_clause cl =
640 [p;g;r] -> (print_subterm 1 p;
641 pp_print_string fmt " when ";
643 pp_print_string fmt " -> ";
645 | [p;r] -> (print_subterm 1 p;
646 pp_print_string fmt " -> ";
650 (* ------------------------------------------------------------------------- *)
651 (* Print term with quotes. *)
652 (* ------------------------------------------------------------------------- *)
654 let pp_print_qterm fmt tm =
655 new_output_functions output_functions;
660 open_tag "style type=\"text/css\"";
661 pp_print_as fmt 0 ".real {color:teal; background-color:white; font-weight:bold; text-align:center;} .num {color:fuchsia; background-color:white; font-weight:bold; text-align:center;} .int {color:olive; background-color:white; font-weight:bold; text-align:center;}";
666 pp_print_term fmt tm;
670 restore_output_functions output_functions;;
673 (* ------------------------------------------------------------------------- *)
674 (* Printer for theorems. *)
675 (* ------------------------------------------------------------------------- *)
677 let pp_print_thm fmt th =
678 let asl,tm = dest_thm th in
679 (if not (asl = []) then
680 (if !print_all_thm then
681 (pp_print_term fmt (hd asl);
682 do_list (fun x -> pp_print_string fmt ",";
683 pp_print_space fmt ();
686 else pp_print_string fmt "...";
687 pp_print_space fmt ())
691 pp_print_string fmt "|- ";
692 pp_print_term fmt tm;
693 pp_close_box fmt ());;
695 let pp_print_thm' = pp_print_thm;;
696 let pp_print_thm fmt tm =
697 new_output_functions output_functions;
702 open_tag "style type=\"text/css\"";
703 pp_print_as fmt 0 ".real {color:teal; background-color:white; font-weight:bold; text-align:center;} .num {color:fuchsia; background-color:white; font-weight:bold; text-align:center;} .int {color:olive; background-color:white; font-weight:bold; text-align:center;}";
712 restore_output_functions output_functions;;
715 (* ------------------------------------------------------------------------- *)
716 (* Print on standard output. *)
717 (* ------------------------------------------------------------------------- *)
719 let print_type = pp_print_type std_formatter;;
720 let print_qtype = pp_print_qtype std_formatter;;
721 let print_term = pp_print_term std_formatter;;
722 let print_qterm = pp_print_qterm std_formatter;;
723 let print_thm = pp_print_thm std_formatter;;
725 (* ------------------------------------------------------------------------- *)
726 (* Install all the printers. *)
727 (* ------------------------------------------------------------------------- *)
729 #install_printer print_qtype;;
730 #install_printer print_qterm;;
731 #install_printer print_thm;;
733 (* ------------------------------------------------------------------------- *)
734 (* Conversions to string. *)
735 (* ------------------------------------------------------------------------- *)
737 let print_to_string printer =
738 let sbuff = ref "" in
739 let output s m n = sbuff := (!sbuff)^(String.sub s m n) and flush() = () in
740 let fmt = make_formatter output flush in
741 ignore(pp_set_max_boxes fmt 100);
742 fun i -> ignore(printer fmt i);
743 ignore(pp_print_flush fmt ());
744 let s = !sbuff in sbuff := ""; s;;
746 let string_of_type = print_to_string pp_print_type;;
747 let string_of_term = print_to_string pp_print_term;;
748 let string_of_thm = print_to_string pp_print_thm;;
750 (* ------------------------------------------------------------------------- *)
752 (* ------------------------------------------------------------------------- *)
754 let print_typed_var tm =
755 let s,ty = dest_var tm in
757 open_tag("span class=\""^(string_of_type ty)^"\"");
761 install_user_printer("print_typed_var", print_typed_var);;
764 let pp_print_string = pp_print_string';;
765 let print_string = print_string';;