include Format;;
set_max_boxes 100;;
(* ------------------------------------------------------------------------- *)
(* Protection for HTML output *)
(* ------------------------------------------------------------------------- *)
let output_functions = get_all_formatter_output_functions();;
let make n s=
let rec make_aux n s str =
match n with
| 0 -> str
| _ -> make_aux (n - 1) s (str ^ s)
in
make_aux n s "";;
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));;
let restore_output_functions (x,y,z,w) = set_all_formatter_output_functions x y z w;;
let pp_print_string' = pp_print_string;;
let print_string' = print_string;;
let rec pp_print_string fmt str =
match (String.length str) with
| 0 -> ()
|_->
if (Str.string_match (Str.regexp "!") str 0)
then begin
pp_print_as fmt 1 "∀";
pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
end
else
if (Str.string_match (Str.regexp "\?") str 0)
then begin
pp_print_as fmt 1 "∃";
pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
end
else
if (Str.string_match (Str.regexp "--") str 0)
then begin
pp_print_as fmt 1 "−";
pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
end
else
if (Str.string_match (Str.regexp "|-") str 0)
then begin
pp_print_as fmt 1 "⊢";
pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
end
else
if (Str.string_match (Str.regexp "~") str 0)
then begin
pp_print_as fmt 1 "¬";
pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
end
else
if (Str.string_match (Str.regexp "<=>") str 0)
then begin
pp_print_as fmt 1 "⇔";
pp_print_string fmt (String.sub str 3 ((String.length str) - 3))
end
else
if (Str.string_match (Str.regexp "==>") str 0)
then begin
pp_print_as fmt 1 "⇒";
pp_print_string fmt (String.sub str 3 ((String.length str) - 3))
end
else
if (Str.string_match (Str.regexp ">=") str 0)
then begin
pp_print_as fmt 1 "≥";
pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
end
else
if (Str.string_match (Str.regexp "<=") str 0)
then begin
pp_print_as fmt 1 "≤";
pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
end
else
if (Str.string_match (Str.regexp "\\\\/") str 0)
then begin
pp_print_as fmt 1 "∨";
pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
end
else
if (Str.string_match (Str.regexp "/\\\\") str 0)
then begin
pp_print_as fmt 1 "∧";
pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
end
else
if (Str.string_match (Str.regexp "\\\\") str 0)
then begin
pp_print_as fmt 1 "λ";
pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
end
else
if (Str.string_match (Str.regexp ">") str 0)
then begin
pp_print_as fmt 1 ">";
pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
end
else
if (Str.string_match (Str.regexp "<") str 0)
then begin
pp_print_as fmt 1 "<";
pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
end
else
if (Str.string_match (Str.regexp " ") str 0)
then begin
pp_print_as fmt 1 " ";
pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
end
else
begin
pp_print_as fmt 1 (String.sub str 0 1);
pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
end;;
let print_string = pp_print_string std_formatter;;
(* ------------------------------------------------------------------------- *)
(* Determine binary operators that print without surrounding spaces. *)
(* ------------------------------------------------------------------------- *)
let unspaced_binops = ref [","; ".."; "$"];;
(* ------------------------------------------------------------------------- *)
(* Binary operators to print at start of line when breaking. *)
(* ------------------------------------------------------------------------- *)
let prebroken_binops = ref ["==>"];;
(* ------------------------------------------------------------------------- *)
(* Force explicit indications of bound variables in set abstractions. *)
(* ------------------------------------------------------------------------- *)
(* let print_unambiguous_comprehensions = ref false;; *)
(* ------------------------------------------------------------------------- *)
(* Print the universal set UNIV:A->bool as "(:A)". *)
(* ------------------------------------------------------------------------- *)
let typify_universal_set = ref true;;
(* ------------------------------------------------------------------------- *)
(* Flag controlling whether hypotheses print. *)
(* ------------------------------------------------------------------------- *)
let print_all_thm = ref true;;
(* ------------------------------------------------------------------------- *)
(* Flag determining whether interface/overloading is reversed on printing. *)
(* ------------------------------------------------------------------------- *)
let reverse_interface_mapping = ref true;;
(* ------------------------------------------------------------------------- *)
(* Uses the_interface to lookup the names of operators *)
(* ------------------------------------------------------------------------- *)
let reverse_interface (s0,ty0) =
if not(!reverse_interface_mapping) then s0 else
try fst(find (fun (s,(s',ty)) -> s' = s0 & can (type_match ty ty0) [])
(!the_interface))
with Failure _ -> s0;;
(* ------------------------------------------------------------------------- *)
(* Get the name of a constant or variable. *)
(* ------------------------------------------------------------------------- *)
let name_of tm =
match tm with
Var(x,ty) | Const(x,ty) -> x
| _ -> "";;
(* ------------------------------------------------------------------------- *)
(* Printer for types. *)
(* ------------------------------------------------------------------------- *)
let pp_print_type,pp_print_qtype =
let soc sep flag ss =
if ss = [] then "" else
let s = end_itlist (fun s1 s2 -> s1^sep^s2) ss in
if flag then "("^s^")" else s in
let rec sot pr ty =
try dest_vartype ty with Failure _ ->
match dest_type ty with
con,[] -> con
| "fun",[ty1;ty2] -> soc "->" (pr > 0) [sot 1 ty1; sot 0 ty2]
| "sum",[ty1;ty2] -> soc "+" (pr > 2) [sot 3 ty1; sot 2 ty2]
| "prod",[ty1;ty2] -> soc "#" (pr > 4) [sot 5 ty1; sot 4 ty2]
| "cart",[ty1;ty2] -> soc "^" (pr > 6) [sot 6 ty1; sot 7 ty2]
| con,args -> (soc "," true (map (sot 0) args))^con in
(fun fmt ty -> pp_print_string fmt (sot 0 ty)),
(fun fmt ty -> pp_print_string fmt ("`:" ^ sot 0 ty ^ "`"));;
(* ------------------------------------------------------------------------- *)
(* This returns L and R if OP = c in (tm:= L OP R) *)
(* ------------------------------------------------------------------------- *)
let dest_binary' c tm =
try let il,r = dest_comb tm in
let i,l = dest_comb il in
if i = c or
(is_const i & is_const c &
reverse_interface(dest_const i) = reverse_interface(dest_const c))
then l,r else fail()
with Failure _ -> failwith "dest_binary";;
(* ------------------------------------------------------------------------- *)
(* string -> bool Lookup to see if operator of string is right assoc *)
(* ------------------------------------------------------------------------- *)
let is_right_assoc s =
match snd(get_infix_status s) with
|"right" -> true
| _ -> false;;
(* ------------------------------------------------------------------------- *)
(* num -> bool *)
(* ------------------------------------------------------------------------- *)
let rec power_of_10 n =
if abs_num n </ Int 1 then false
else if n =/ Int 1 then true
else power_of_10 (n // Int 10);;
(* ------------------------------------------------------------------------- *)
(* term -> bool converts bool term to ocaml bool *)
(* ------------------------------------------------------------------------- *)
let bool_of_term t =
match t with
Const("T",_) -> true
| Const("F",_) -> false
| _ -> failwith "bool_of_term";;
(* ------------------------------------------------------------------------- *)
(* term -> int converts ASCII term into int equiv *)
(* ------------------------------------------------------------------------- *)
let code_of_term t =
let f,tms = strip_comb t in
if not(is_const f & fst(dest_const f) = "ASCII")
or not(length tms = 8) then failwith "code_of_term"
else
itlist (fun b f -> if b then 1 + 2 * f else 2 * f)
(map bool_of_term (rev tms)) 0;;
(* ------------------------------------------------------------------------- *)
(* *)
(* ------------------------------------------------------------------------- *)
let rec dest_clause tm =
let pbod = snd(strip_exists(body(body tm))) in
let s,args = strip_comb pbod in
if name_of s = "_UNGUARDED_PATTERN" & length args = 2 then
[rand(rator(hd args));rand(rator(hd(tl args)))]
else if name_of s = "_GUARDED_PATTERN" & length args = 3 then
[rand(rator(hd args)); hd(tl args); rand(rator(hd(tl(tl args))))]
else failwith "dest_clause" ;;
(* ------------------------------------------------------------------------- *)
(* *)
(* ------------------------------------------------------------------------- *)
let rec dest_clauses tm =
let s,args = strip_comb tm in
if name_of s = "_SEQPATTERN" & length args = 2 then
dest_clause (hd args)::dest_clauses(hd(tl args))
else [dest_clause tm];;
(* ------------------------------------------------------------------------- *)
(* Allow the installation of user printers. Must fail quickly if N/A. *)
(* ------------------------------------------------------------------------- *)
let install_user_printer,delete_user_printer,try_user_printer =
let user_printers = ref ([]:(string*(term->unit))list) in
(fun pr -> user_printers := pr::(!user_printers)),
(fun s -> user_printers := snd(remove (fun (s',_) -> s = s')
(!user_printers))),
(fun tm -> tryfind (fun (_,pr) -> pr tm) (!user_printers));;
(* ------------------------------------------------------------------------- *)
(* Type to determine how/(what tag) to print *)
(* ------------------------------------------------------------------------- *)
type term_type = Numeral | List | Char_list | Generalized_abstraction |
Empty | Universal | G_spec | Let | Decimal | Match | Function |
Insert | Cond | Other;;
(* ------------------------------------------------------------------------- *)
(* term -> term_type *)
(* ------------------------------------------------------------------------- *)
let rec get_term_type tm =
if is_numeral tm then Numeral
else if is_list tm then
begin
try if fst(dest_type(hd(snd(dest_type(type_of tm))))) <> "char"
then fail()
else Char_list with Failure _ -> List
end
else if is_gabs tm then Generalized_abstraction
else
begin
let hop,args = strip_comb tm in
let s0 = name_of hop
and ty0 = type_of hop in
let s = reverse_interface (s0,ty0) in
if s = "EMPTY" & is_const tm & args = [] then Empty
else if s = "UNIV" & !typify_universal_set & is_const tm & args = []
then Universal
else if s = "INSERT" &
is_const (snd(splitlist (dest_binary "INSERT") tm)) &
fst(
dest_const (
snd(
splitlist (
dest_binary "INSERT") tm))) = "EMPTY" then Insert
else if (s = "GSPEC") &
fst(dest_const (
(rator o
fst o dest_comb o
fst o dest_comb o
snd o strip_exists
o body o rand)tm )) = "SETSPEC" then G_spec
else if is_let tm then Let
else if s = "DECIMAL" &
(power_of_10 ((dest_numeral o hd o tl)args)) then Decimal
else if s = "_MATCH" &
length args = 2 then Match
else if s = "_FUNCTION" &
length args = 1 then Function
else if s = "COND" & length args = 3 then Cond
else Other
end;;
(* ------------------------------------------------------------------------- *)
(* Printer for terms. *)
(* ------------------------------------------------------------------------- *)
let pp_print_term =
fun fmt ->
let rec print_subterm prec tm =
try try_user_printer tm with Failure _ ->
let hop,args = strip_comb tm in
let s0 = name_of hop
and ty0 = type_of hop in
let s = reverse_interface (s0,ty0) in
match get_term_type tm with
| Numeral ->
begin
open_tag "span class=\"Numeral\"";
pp_print_string fmt (string_of_num(dest_numeral tm));
close_tag();
end;
|Char_list ->
begin
open_tag "span class=\"Char_list\"";
pp_print_string fmt (
"\"" ^ String.escaped (implode (map (
String.make 1 o
Char.chr o
code_of_term )
(dest_list tm) )) ^ "\"");
close_tag();
end;
|List ->
begin
open_tag "span class=\"List\"";
pp_print_string fmt "[";
print_term_sequence "; " 0 (dest_list tm);
pp_print_string fmt "]";
close_tag();
end;
|Generalized_abstraction ->
begin
open_tag "span class=\"Generalized_abstraction\"";
print_binder prec tm;
close_tag();
end
|Empty ->
begin
open_tag "span class=\"Empty\"";
pp_print_string fmt "{}";
close_tag();
end
|Universal ->
begin
let ty = fst(dest_fun_ty(type_of tm)) in
begin
open_tag "span class=\"Universal\"";
pp_print_string fmt "(:";
pp_print_type fmt ty;
pp_print_string fmt ")";
close_tag();
end
end;
|Insert ->
begin
open_tag "span class=\"Insert\"";
pp_print_string fmt "{";
print_term_sequence ", " 14 (
fst(
splitlist (dest_binary "INSERT") tm));
pp_print_string fmt "}";
close_tag();
end;
|G_spec ->
begin
let evs,bod = strip_exists(body(rand tm)) in
let bod1,fabs = dest_comb bod in
let bod2,babs = dest_comb bod1 in
(* let c = rator bod2 in*)
(* (let fvs = frees fabs and bvs = frees babs in
if not(!print_unambiguous_comprehensions) &
set_eq evs
(if (length fvs <= 1 or bvs = []) then fvs
else intersect fvs bvs)
then ()
else (print_term_sequence "," 14 evs;
pp_print_string fmt " | "));
*)
open_tag "span class=\"G_spec\"";
pp_print_string fmt "{";
print_subterm 0 fabs;
pp_print_string fmt " | ";
print_subterm 0 babs;
pp_print_string fmt "}";
close_tag();
end;
|Let ->
begin
open_tag "span class=\"Let\"";
let eqs,bod = dest_let tm in
(if prec = 0 then pp_open_hvbox fmt 0
else (pp_open_hvbox fmt 1; pp_print_string fmt "(");
pp_print_string fmt "let ";
print_subterm 0 (mk_eq(hd eqs));
do_list (fun (v,t) -> pp_print_break fmt 1 0;
pp_print_string fmt "and ";
print_subterm 0 (mk_eq(v,t)))
(tl eqs);
pp_print_string fmt " in";
pp_print_break fmt 1 0;
print_subterm 0 bod;
if prec = 0 then () else pp_print_string fmt ")";
pp_close_box fmt ());
close_tag();
end;
|Decimal ->
begin
open_tag "span class=\"Decimal\"";
let n_num = dest_numeral (hd args)
and n_den = dest_numeral (hd(tl args)) in
let s_num = string_of_num(quo_num n_num n_den) in
let s_den = implode(
tl(explode(string_of_num
(n_den +/ (mod_num n_num n_den))))) in
pp_print_string fmt(
"#"^s_num^(if n_den = Int 1 then "" else ".")^s_den);
close_tag();
end;
|Match ->
begin
open_tag "span class=\"Match\"";
let cls = dest_clauses(hd(tl args)) in
(if prec = 0 then () else pp_print_string fmt "(";
pp_open_hvbox fmt 0;
pp_print_string fmt "match ";
print_subterm 0 (hd args);
pp_print_string fmt " with";
pp_print_break fmt 1 2;
print_clauses cls;
pp_close_box fmt ();
if prec = 0 then () else pp_print_string fmt ")");
close_tag();
end
|Function ->
begin
open_tag "span class=\"Function\"";
let cls = dest_clauses(hd args) in
(if prec = 0 then () else pp_print_string fmt "(";
pp_open_hvbox fmt 0;
pp_print_string fmt "function";
pp_print_break fmt 1 2;
print_clauses cls;
pp_close_box fmt ();
if prec = 0 then () else pp_print_string fmt ")");
close_tag();
end
|Cond ->
begin
open_tag "span class=\"Cond\"";
(if prec = 0 then () else pp_print_string fmt "(";
pp_open_hvbox fmt (-1);
pp_print_string fmt "if ";
print_subterm 0 (hd args);
pp_print_break fmt 0 0;
pp_print_string fmt " then ";
print_subterm 0 (hd(tl args));
pp_print_break fmt 0 0;
pp_print_string fmt " else ";
print_subterm 0 (hd(tl(tl args)));
pp_close_box fmt ();
if prec = 0 then () else pp_print_string fmt ")");
close_tag();
end
|_ ->
begin
if is_prefix s & length args = 1 then
(if prec = 1000 then pp_print_string fmt "(" else ();
pp_print_string fmt s;
(if isalnum s or
s = "--" &
length args = 1 &
(try let l,r = dest_comb(hd args) in
let s0 = name_of l in
s0 = "--" or
mem (fst(dest_const l)) ["real_of_num"; "int_of_num"]
with Failure _ -> false) or
s = "~" & length args = 1 & is_neg(hd args)
then pp_print_string fmt " " else ());
print_subterm 999 (hd args);
if prec = 1000 then pp_print_string fmt ")" else ())
else if parses_as_binder s & length args = 1 & is_gabs (hd args) then
print_binder prec tm
else if can get_infix_status s & length args = 2 then
let bargs =
if is_right_assoc s then
let tms,tmt = splitlist (dest_binary' hop) tm in tms@[tmt]
else
let tmt,tms = rev_splitlist (dest_binary' hop) tm in tmt::tms in
let newprec = fst(get_infix_status s) in
(if newprec <= prec then
(pp_open_hvbox fmt 1; pp_print_string fmt "(")
else pp_open_hvbox fmt 0;
print_subterm newprec (hd bargs);
do_list (fun x -> if mem s (!unspaced_binops) then ()
else if mem s (!prebroken_binops)
then pp_print_break fmt 1 0
else pp_print_string fmt " ";
pp_print_string fmt s;
if mem s (!unspaced_binops)
then pp_print_break fmt 0 0
else if mem s (!prebroken_binops)
then pp_print_string fmt " "
else pp_print_break fmt 1 0;
print_subterm newprec x) (tl bargs);
if newprec <= prec then pp_print_string fmt ")" else ();
pp_close_box fmt ())
else if (is_const hop or is_var hop) & args = [] then
let s' = if parses_as_binder s or can get_infix_status s or is_prefix s
then "("^s^")" else s in
pp_print_string fmt s'
else
let l,r = dest_comb tm in
(pp_open_hvbox fmt 0;
if prec = 1000 then pp_print_string fmt "(" else ();
print_subterm 999 l;
(if try mem (fst(dest_const l)) ["real_of_num"; "int_of_num"]
with Failure _ -> false
then () else pp_print_space fmt ());
print_subterm 1000 r;
if prec = 1000 then pp_print_string fmt ")" else ();
pp_close_box fmt ())
end
(* Code is safe down here *)
and print_term_sequence sep prec tms =
if tms = [] then () else
(print_subterm prec (hd tms);
let ttms = tl tms in
if ttms = [] then ()
else (pp_print_string fmt sep; print_term_sequence sep prec ttms))
and print_clauses cls =
match cls with
[c] -> print_clause c
| c::cs -> (print_clause c;
pp_print_break fmt 1 0;
pp_print_string fmt "| ";
print_clauses cs)
and print_binder prec tm =
let absf = is_gabs tm in
let s = if absf then "\\" else name_of(rator tm) in
let rec collectvs tm =
if absf then
if is_abs tm then
let v,t = dest_abs tm in
let vs,bod = collectvs t in (false,v)::vs,bod
else if is_gabs tm then
let v,t = dest_gabs tm in
let vs,bod = collectvs t in (true,v)::vs,bod
else [],tm
else if is_comb tm & name_of(rator tm) = s then
if is_abs(rand tm) then
let v,t = dest_abs(rand tm) in
let vs,bod = collectvs t in (false,v)::vs,bod
else if is_gabs(rand tm) then
let v,t = dest_gabs(rand tm) in
let vs,bod = collectvs t in (true,v)::vs,bod
else [],tm
else [],tm in
let vs,bod = collectvs tm in
begin
open_tag "span class=\"binder\"";
(if prec = 0 then pp_open_hvbox fmt 4
else (pp_open_hvbox fmt 5; pp_print_string fmt "("));
pp_print_string fmt s;
(if isalnum s then pp_print_string fmt " " else ());
do_list (fun (b,x) ->
(if b then pp_print_string fmt "(" else ());
print_subterm 0 x;
(if b then pp_print_string fmt ")" else ());
pp_print_string fmt " ") (butlast vs);
(if fst(last vs) then pp_print_string fmt "(" else ());
print_subterm 0 (snd(last vs));
(if fst(last vs) then pp_print_string fmt ")" else ());
pp_print_string fmt ".";
(if length vs = 1 then pp_print_string fmt " "
else pp_print_space fmt ());
print_subterm 0 bod;
(if prec = 0 then () else pp_print_string fmt ")");
pp_close_box fmt ();
close_tag();
end;
and print_clause cl =
match cl with
[p;g;r] -> (print_subterm 1 p;
pp_print_string fmt " when ";
print_subterm 1 g;
pp_print_string fmt " -> ";
print_subterm 1 r)
| [p;r] -> (print_subterm 1 p;
pp_print_string fmt " -> ";
print_subterm 1 r)
in print_subterm 0;;
(* ------------------------------------------------------------------------- *)
(* Print term with quotes. *)
(* ------------------------------------------------------------------------- *)
let pp_print_qterm fmt tm =
new_output_functions output_functions;
open_tag "HTML";
open_tag "HEAD";
open_tag "TITLE";
close_tag ();
open_tag "style type=\"text/css\"";
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;}";
close_tag();
close_tag();
open_tag "BODY";
open_tag "TT";
pp_print_term fmt tm;
close_tag();
close_tag();
close_tag();
restore_output_functions output_functions;;
(* ------------------------------------------------------------------------- *)
(* Printer for theorems. *)
(* ------------------------------------------------------------------------- *)
let pp_print_thm fmt th =
let asl,tm = dest_thm th in
(if not (asl = []) then
(if !print_all_thm then
(pp_print_term fmt (hd asl);
do_list (fun x -> pp_print_string fmt ",";
pp_print_space fmt ();
pp_print_term fmt x)
(tl asl))
else pp_print_string fmt "...";
pp_print_space fmt ())
else ();
pp_open_hbox fmt();
pp_print_string fmt "|- ";
pp_print_term fmt tm;
pp_close_box fmt ());;
let pp_print_thm' = pp_print_thm;;
let pp_print_thm fmt tm =
new_output_functions output_functions;
open_tag "HTML";
open_tag "HEAD";
open_tag "TITLE";
close_tag();
open_tag "style type=\"text/css\"";
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;}";
close_tag();
close_tag();
open_tag "BODY";
open_tag "TT";
pp_print_thm fmt tm;
close_tag();
close_tag();
close_tag();
restore_output_functions output_functions;;
(* ------------------------------------------------------------------------- *)
(* Print on standard output. *)
(* ------------------------------------------------------------------------- *)
let print_type = pp_print_type std_formatter;;
let print_qtype = pp_print_qtype std_formatter;;
let print_term = pp_print_term std_formatter;;
let print_qterm = pp_print_qterm std_formatter;;
let print_thm = pp_print_thm std_formatter;;
(* ------------------------------------------------------------------------- *)
(* Install all the printers. *)
(* ------------------------------------------------------------------------- *)
#install_printer print_qtype;;
#install_printer print_qterm;;
#install_printer print_thm;;
(* ------------------------------------------------------------------------- *)
(* Conversions to string. *)
(* ------------------------------------------------------------------------- *)
let print_to_string printer =
let sbuff = ref "" in
let output s m n = sbuff := (!sbuff)^(String.sub s m n) and flush() = () in
let fmt = make_formatter output flush in
ignore(pp_set_max_boxes fmt 100);
fun i -> ignore(printer fmt i);
ignore(pp_print_flush fmt ());
let s = !sbuff in sbuff := ""; s;;
let string_of_type = print_to_string pp_print_type;;
let string_of_term = print_to_string pp_print_term;;
let string_of_thm = print_to_string pp_print_thm;;
(* ------------------------------------------------------------------------- *)
(* Print types *)
(* ------------------------------------------------------------------------- *)
let print_typed_var tm =
let s,ty = dest_var tm in
begin
open_tag("span class=\""^(string_of_type ty)^"\"");
print_string(s);
close_tag();
end in
install_user_printer("print_typed_var", print_typed_var);;
set_mark_tags true;;
let pp_print_string = pp_print_string';;
let print_string = print_string';;