text_formalization/jordan/goal_printer.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Jordan                                                               *)
   5 (* Copied from HOL Light jordan directory *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-07-08                                                           *)
   8 (* ========================================================================== *)
   9
  10 (* needs tactics_fix.ml;;
  11    tactics_refine.ml ;;
  12    lib_ext.ml *)
  13
  14 module Goal_printer = struct
  15
  16 open Refinement;;
  17 open Hash_term;;
  18 open Lib_ext;;
  19 (* This file is in severe need of a rewrite! *)
  20
  21 Parse_ext_override_interface.unambiguous_interface();;
  22 Parse_ext_override_interface.prioritize_real();;
  23
  24 (*
  25
  26    To restore HOL-light defaults, type
  27    #install_printer print_goal;;
  28    #install_printer print_goalstack;;
  29
  30 *)
  31
  32
  33 (* To install:
  34 #install_printer Goal_printer.print_goal_hashed;;
  35 #install_printer Goal_printer.print_goalstack_hashed;;
  36
  37    To install printer that reverses the assumption list, but no hashing:
  38
  39    #install_printer Goal_printer.print_rev_goal;;
  40    #install_printer Goal_printer.print_rev_goalstack;;
  41
  42 *)
  43
  44
  45
  46 (* ------------------------------------------------------------------------- *)
  47 (* A printer for goals etc.                                                  *)
  48 (* ------------------------------------------------------------------------- *)
  49
  50
  51
  52
  53 (* had (rev asl) in this method.  I don't want to reverse the list *)
  54
  55
  56 let print_hyp n (s,th) =
  57   open_hbox();
  58   print_string " ";
  59   print_as 4 (string_of_int (hash_of_term (concl th)));
  60   print_string " [";
  61   print_qterm (concl th);
  62   print_string "]";
  63   (if not (s = "") then (print_string (" ("^s^")")) else ());
  64   close_box();
  65   print_newline();;
  66
  67 let rec print_hyps n asl =
  68   if asl = [] then () else
  69   (print_hyp n (hd asl);
  70    print_hyps (n + 1) (tl asl));;
  71
  72 let (print_goal_hashed:goal->unit) =
  73   fun gl ->
  74     let (asl,w)= dest_goal gl in
  75       print_newline();
  76       if asl <> [] then (print_hyps 0 (asl); print_newline()) else ();
  77       print_qterm w; print_newline();;
  78
  79 let (print_goalstate_hashed:int->goalstate->unit) =
  80   fun k gs -> let (_,gl,_) = gs in
  81               let n = length gl in
  82               let s = if n = 0 then "No subgoals" else
  83                         (string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
  84                      ^" ("^(string_of_int n)^" total)" in
  85               print_string s; print_newline();
  86               if gl = [] then () else
  87               do_list (print_goal_hashed o C el gl) (rev(0--(k-1)));;
  88
  89 let (print_goalstack_hashed:goalstack->unit) =
  90   fun l ->
  91     if l = [] then print_string "Empty goalstack"
  92     else if tl l = [] then
  93       let (_,gl,_ as gs) = hd l in
  94       print_goalstate_hashed 1 gs
  95     else
  96       let (_,gl,_ as gs) = hd l
  97       and (_,gl0,_) = hd(tl l) in
  98       let p = length gl - length gl0 in
  99       let p' = if p < 1 then 1 else p + 1 in
 100       print_goalstate_hashed p' gs;;
 101
 102
 103
 104 (* To install printers:
 105 #install_printer print_rev_goal;;
 106 #install_printer print_rev_goalstack;;
 107 *)
 108
 109
 110 (* ------------------------------------------------------------------------- *)
 111 (* A printer that reverses the assumption list *)
 112 (* ------------------------------------------------------------------------- *)
 113
 114 (*
 115
 116    Objective version of HOL-light uses (rev asl) in the method print_goal.
 117    This means that the numbers printed next to the assumptions
 118    are the reverse of the numbering in the list.
 119
 120    I want it the opposite way.
 121    This reverses the numbering on the assumption list,
 122    so that the printed numbers match the list order.
 123
 124    To restore HOL-light defaults, type
 125    #install_printer print_goal;;
 126    #install_printer print_goalstack;;
 127
 128 *)
 129
 130 let (print_rev_goal:goal->unit) =
 131   fun gl ->
 132     let (asl,w) = dest_goal gl in
 133       print_goal (mk_goal(rev asl,w));;
 134
 135 let (print_rev_goalstate:int->goalstate->unit) =
 136   fun k gs -> let (_,gl,_) = gs in
 137               let n = length gl in
 138               let s = if n = 0 then "No subgoals" else
 139                         (string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
 140                      ^" ("^(string_of_int n)^" total)" in
 141               print_string s; print_newline();
 142               if gl = [] then () else
 143               do_list (print_rev_goal o C el gl) (rev(0--(k-1)));;
 144
 145
 146 let (print_rev_goalstack:goalstack->unit) =
 147   fun l ->
 148     if l = [] then print_string "Empty goalstack"
 149     else if tl l = [] then
 150       let (_,gl,_ as gs) = hd l in
 151       print_rev_goalstate 1 gs
 152     else
 153       let (_,gl,_ as gs) = hd l
 154       and (_,gl0,_) = hd(tl l) in
 155       let p = length gl - length gl0 in
 156       let p' = if p < 1 then 1 else p + 1 in
 157       print_rev_goalstate p' gs;;
 158
 159
 160 end;;