Rqe/util.ml

   1 (* ---------------------------------------------------------------------- *)
   2 (*  Strings                                                               *)
   3 (* ---------------------------------------------------------------------- *)
   4
   5
   6 let string_of_char c = String.make 1 c;;
   7
   8
   9
  10 (* ---------------------------------------------------------------------- *)
  11 (*  Types                                                                 *)
  12 (* ---------------------------------------------------------------------- *)
  13
  14
  15 let gensort = sort (<);;
  16 let suppress = ref ([]:string list);;
  17 suppress := ["==>";"?";"!";"/\\";"\\/";",";"~";"APPEND";"CONS";"HD";"LAST";
  18   "NIL";"=";"real_lt";"real_gt";"real_le";"real_ge";"BIT0";"BIT1";"NUMERAL";
  19   "real_of_num";"_0";"_1";"real_div";"real_mul";"real_pow";"COND"];;
  20
  21 let rec get_type_list tm =
  22   match tm with
  23       Var(s,t) -> if mem s !suppress then [] else [(s,t)]
  24     | Const(s,t) -> if mem s !suppress then [] else [(s,t)]
  25     | Comb (t1,t2) -> get_type_list t1 @ get_type_list t2
  26     | Abs (t1,t2) -> get_type_list t1 @ get_type_list t2;;
  27
  28 let my_print_type (s,t) =
  29   print_string ("(\"" ^ s ^ "\", ");
  30   print_qtype t;
  31   print_string ")\n";;
  32
  33 let rec my_print_typel l =
  34   match l with
  35       [] -> ();
  36     | (h::t) -> my_print_type h; my_print_typel t;;
  37
  38 let set_types tm = (gensort o setify o get_type_list) tm;;
  39
  40 let print_term_types  = my_print_typel o set_types;;
  41 let print_thm_types tm = print_term_types (concl tm);;
  42 let goal_types() = (print_term_types o snd o top_goal)();;
  43
  44 let assum i = (rev_ith i o fst o top_goal)();;
  45 let assum_types i = (print_term_types o rev_ith i o fst o top_goal)();;
  46
  47 let (get_type:string->thm->hol_type) =
  48   fun s thm -> assoc s (get_type_list (concl thm));;
  49
  50
  51 (* ---------------------------------------------------------------------- *)
  52 (* Proof Stack                                                            *)
  53 (* ---------------------------------------------------------------------- *)
  54
  55 exception Empty_stack;;
  56 let proof_stack = ref ([]:goalstack list);;
  57 let push_proof t =
  58   proof_stack := [!current_goalstack] @ !proof_stack;
  59   g t;;
  60
  61 let pop_proof() =
  62   match !proof_stack with
  63       [] -> raise Empty_stack
  64     | h::t -> current_goalstack := h; proof_stack := t;
  65         p();;
  66
  67 (* ---------------------------------------------------------------------- *)
  68 (*  Printing                                                              *)
  69 (* ---------------------------------------------------------------------- *)
  70
  71 let print_thm_no_hyps th =
  72   let asl,tm = dest_thm th in
  73   (if not (asl = []) then
  74      print_string "..."
  75    else ();
  76    open_hbox();
  77    print_string "|- ";
  78    print_term tm;
  79    close_box());;
  80
  81
  82 let print_trace_thm hyps msg th =
  83   let asl,tm = dest_thm th in
  84    open_hbox();
  85    print_string "------------------------\n ";
  86    print_string (msg ^ "\n");
  87    if hyps then print_thm th else print_thm_no_hyps th;
  88    print_string "\n========================\n ";
  89    close_box();;
  90
  91 (*
  92 #install_printer print_thm_no_hyps;;
  93 #install_printer print_thm;;
  94 *)
  95
  96