3 Print the types of the atoms of terms, thms and the goal.
7 val goal_types: unit -> unit
8 val print_thm_types: thm -> unit
9 val print_term_types: term -> unit
11 (* I've elided the common symbols from the list
12 to avoid clutter. You can add and remove names
13 of constants from this list with (un)suppress *)
14 val suppress: string -> unit
15 val unsuppress: string -> unit
21 ["==>";"?";"!";"/\\";"\\/";",";"~";"APPEND";"CONS";"HD";"LAST";
22 "NIL";"=";"real_lt";"real_gt";"real_le";"real_ge";"BIT0";"BIT1";"NUMERAL";
23 "real_of_num";"_0";"_1";"real_div";"real_mul";"real_pow";"COND"]
25 let suppress s = suppressed := s :: !suppressed
27 let unsuppress s = suppressed := List.filter ((!=) s) (!suppressed)
29 let rec get_type_list tm =
31 Var(s,t) -> if mem s !suppressed then [] else [(s,t)]
32 | Const(s,t) -> if mem s !suppressed then [] else [(s,t)]
33 | Comb (t1,t2) -> get_type_list t1 @ get_type_list t2
34 | Abs (t1,t2) -> get_type_list t1 @ get_type_list t2
36 let print_atom_type : string * hol_type -> unit =
39 print_string ("(\"" ^ s ^ "\", ");
44 let setify_types tm = ((sort (<)) o setify o get_type_list) tm
46 let print_term_types = List.iter print_atom_type o setify_types
48 let print_thm_types tm = print_term_types (concl tm)
51 let (asms,g) = top_goal() in
53 let tm = end_itlist (curry mk_conj) tms in