1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Copied from HOL Light jordan directory *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
10 (* needs tactics_fix.ml;;
14 module Goal_printer = struct
19 (* This file is in severe need of a rewrite! *)
21 Parse_ext_override_interface.unambiguous_interface();;
22 Parse_ext_override_interface.prioritize_real();;
26 To restore HOL-light defaults, type
27 #install_printer print_goal;;
28 #install_printer print_goalstack;;
34 #install_printer Goal_printer.print_goal_hashed;;
35 #install_printer Goal_printer.print_goalstack_hashed;;
37 To install printer that reverses the assumption list, but no hashing:
39 #install_printer Goal_printer.print_rev_goal;;
40 #install_printer Goal_printer.print_rev_goalstack;;
46 (* ------------------------------------------------------------------------- *)
47 (* A printer for goals etc. *)
48 (* ------------------------------------------------------------------------- *)
53 (* had (rev asl) in this method. I don't want to reverse the list *)
56 let print_hyp n (s,th) =
59 print_as 4 (string_of_int (hash_of_term (concl th)));
61 print_qterm (concl th);
63 (if not (s = "") then (print_string (" ("^s^")")) else ());
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));;
72 let (print_goal_hashed:goal->unit) =
74 let (asl,w)= dest_goal gl in
76 if asl <> [] then (print_hyps 0 (asl); print_newline()) else ();
77 print_qterm w; print_newline();;
79 let (print_goalstate_hashed:int->goalstate->unit) =
80 fun k gs -> let (_,gl,_) = gs 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)));;
89 let (print_goalstack_hashed:goalstack->unit) =
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
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;;
104 (* To install printers:
105 #install_printer print_rev_goal;;
106 #install_printer print_rev_goalstack;;
110 (* ------------------------------------------------------------------------- *)
111 (* A printer that reverses the assumption list *)
112 (* ------------------------------------------------------------------------- *)
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.
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.
124 To restore HOL-light defaults, type
125 #install_printer print_goal;;
126 #install_printer print_goalstack;;
130 let (print_rev_goal:goal->unit) =
132 let (asl,w) = dest_goal gl in
133 print_goal (mk_goal(rev asl,w));;
135 let (print_rev_goalstate:int->goalstate->unit) =
136 fun k gs -> let (_,gl,_) = gs 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)));;
146 let (print_rev_goalstack:goalstack->unit) =
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
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;;