2 copied from repository 'http://seanmcl-ocaml-lib.googlecode.com/svn'
5 Print the types of the atoms of terms, thms and the goal.
9 val print_goal_types: unit -> unit
10 val print_thm_types: thm -> unit
11 val print_term_types: term -> unit
12 val print_goal_var_overload: unit -> unit
14 val get_term_types: term -> (string*hol_type) list
15 val get_const_types: term -> (string*hol_type) list
17 (* I've elided the common symbols from the list
18 to avoid clutter. You can add and remove names
19 of constants from this list with (un)suppress *)
20 val suppress: string -> unit
21 val unsuppress: string -> unit
27 ["==>";"?";"!";"/\\";"\\/";",";"~";"APPEND";"CONS";"HD";"LAST";
28 "NIL";"=";"real_lt";"real_gt";"real_le";"real_ge";"BIT0";"BIT1";"NUMERAL";
29 "DECIMAL";"real_sub";"real_add";"real_neg";
30 "real_of_num";"_0";"_1";"real_div";"real_mul";"real_pow";"COND";"LET";"LET_END"]
32 let suppress s = suppressed := s :: !suppressed
34 let unsuppress s = suppressed := List.filter ((!=) s) (!suppressed)
36 let rec get_term_types tm =
38 Var(s,t) -> if mem s !suppressed then [] else [(s,t)]
39 | Const(s,t) -> if mem s !suppressed then [] else [(s,t)]
40 | Comb (t1,t2) -> get_term_types t1 @ get_term_types t2
41 | Abs (t1,t2) -> get_term_types t1 @ get_term_types t2
43 let rec get_const_types tm =
46 | Const(s,t) -> if mem s !suppressed then [] else [(s,t)]
47 | Comb (t1,t2) -> get_const_types t1 @ get_const_types t2
48 | Abs (t1,t2) -> get_const_types t1 @ get_const_types t2
50 let rec get_var_types = function
53 | Comb (t1,t2) -> get_var_types t1 @ get_var_types t2
54 | Abs (t1,t2) -> get_var_types t1 @ get_var_types t2
56 let print_atom_type : string * hol_type -> unit =
59 print_string ("(\"" ^ s ^ "\", ");
64 let setify_types tm = ((sort (<)) o setify o get_term_types) tm
66 let print_term_types = List.iter print_atom_type o setify_types
68 let print_thm_types tm = print_term_types (concl tm)
70 let print_goal_types() =
71 let (asms,g) = top_goal() in
73 let tm = end_itlist (curry mk_conj) tms in
76 let print_goal_var_overload() =
77 let (asms,g) = top_goal() in
79 let tm = end_itlist (curry mk_conj) tms in
80 let vt = ((sort (<)) o setify) (get_var_types tm) in
81 let ct = ((sort (<)) o setify) (get_const_types tm @ vt) in
82 let ft x = filter (fun t -> (fst t = fst x) && not(snd t = snd x)) ct in
83 let ov = ((sort (<)) o setify) (List.flatten ( map ft vt )) in
84 if (List.length ov >0) then
85 (print_string "Warning: type-overloaded variables\n";
86 List.iter print_atom_type ov)