text_formalization/general/print_types.hl

   1 (*
   2 copied from repository 'http://seanmcl-ocaml-lib.googlecode.com/svn'
   3 *)
   4 (*
   5    Print the types of the atoms of terms, thms and the goal.
   6 *)
   7 module Print_types
   8   : sig
   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
  13
  14       val get_term_types: term -> (string*hol_type) list
  15       val get_const_types: term -> (string*hol_type) list
  16
  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
  22
  23     end =
  24 struct
  25
  26   let suppressed = ref
  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"]
  31
  32   let suppress s = suppressed := s :: !suppressed
  33
  34   let unsuppress s = suppressed := List.filter ((!=) s) (!suppressed)
  35
  36   let rec get_term_types tm =
  37     match tm with
  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
  42
  43   let rec get_const_types tm =
  44     match tm with
  45         Var(s,t) -> []
  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
  49
  50   let rec get_var_types = function
  51         Var(s,t) -> [(s,t)]
  52       | Const(s,t) -> []
  53       | Comb (t1,t2) -> get_var_types t1 @ get_var_types t2
  54       | Abs (t1,t2) -> get_var_types t1 @ get_var_types t2
  55
  56   let print_atom_type : string * hol_type -> unit =
  57     fun (s,t) ->
  58       begin
  59         print_string ("(\"" ^ s ^ "\", ");
  60         print_type t;
  61         print_string ")\n"
  62       end
  63
  64   let setify_types tm = ((sort (<)) o setify o get_term_types) tm
  65
  66   let print_term_types = List.iter print_atom_type o setify_types
  67
  68   let print_thm_types tm = print_term_types (concl tm)
  69
  70   let print_goal_types() =
  71     let (asms,g) = top_goal() in
  72     let tms = g::asms in
  73     let tm = end_itlist (curry mk_conj) tms in
  74       (print_term_types tm)
  75
  76   let print_goal_var_overload() =
  77     let (asms,g) = top_goal() in
  78     let tms = g::asms 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)
  87       else ();;
  88
  89
  90 end;;
  91
  92 open Print_types;;