emacs/print-types.ml

   1
   2 (*
   3    Print the types of the atoms of terms, thms and the goal.
   4 *)
   5 module Print_types
   6   : sig
   7       val goal_types: unit -> unit
   8       val print_thm_types: thm -> unit
   9       val print_term_types: term -> unit
  10
  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
  16
  17     end =
  18 struct
  19
  20   let suppressed = ref
  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"]
  24
  25   let suppress s = suppressed := s :: !suppressed
  26
  27   let unsuppress s = suppressed := List.filter ((!=) s) (!suppressed)
  28
  29   let rec get_type_list tm =
  30     match tm with
  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
  35
  36   let print_atom_type : string * hol_type -> unit =
  37     fun (s,t) ->
  38       begin
  39         print_string ("(\"" ^ s ^ "\", ");
  40         print_type t;
  41         print_string ")\n"
  42       end
  43
  44   let setify_types tm = ((sort (<)) o setify o get_type_list) tm
  45
  46   let print_term_types = List.iter print_atom_type o setify_types
  47
  48   let print_thm_types tm = print_term_types (concl tm)
  49
  50   let goal_types() =
  51     let (asms,g) = top_goal() in
  52     let tms = g::asms in
  53     let tm = end_itlist (curry mk_conj) tms in
  54       (print_term_types tm)
  55
  56 end;;
  57
  58 open Print_types;;