author | blanchet |
Mon, 16 Dec 2013 12:02:28 +0100 | |
changeset 54765 | b05b0ea06306 |
parent 54764 | 1c9ef5c834e8 |
child 54766 | 6ac273f176cd |
permissions | -rw-r--r-- |
52590 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_print.ML |
52555 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
Author: Steffen Juilf Smolka, TU Muenchen |
|
4 |
||
5 |
Basic mapping from proof data structures to proof strings. |
|
6 |
*) |
|
7 |
||
8 |
signature SLEDGEHAMMER_PRINT = |
|
9 |
sig |
|
10 |
type isar_proof = Sledgehammer_Proof.isar_proof |
|
11 |
type reconstructor = Sledgehammer_Reconstructor.reconstructor |
|
12 |
type one_line_params = Sledgehammer_Reconstructor.one_line_params |
|
13 |
||
14 |
val string_of_reconstructor : reconstructor -> string |
|
15 |
||
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset
|
16 |
val one_line_proof_text : int -> one_line_params -> string |
52555 | 17 |
|
18 |
val string_of_proof : |
|
19 |
Proof.context -> string -> string -> int -> int -> isar_proof -> string |
|
20 |
end; |
|
21 |
||
22 |
structure Sledgehammer_Print : SLEDGEHAMMER_PRINT = |
|
23 |
struct |
|
24 |
||
25 |
open ATP_Util |
|
26 |
open ATP_Proof |
|
27 |
open ATP_Problem_Generate |
|
28 |
open ATP_Proof_Reconstruct |
|
29 |
open Sledgehammer_Util |
|
30 |
open Sledgehammer_Reconstructor |
|
31 |
open Sledgehammer_Proof |
|
32 |
open Sledgehammer_Annotate |
|
33 |
||
34 |
||
35 |
(** reconstructors **) |
|
36 |
||
37 |
fun string_of_reconstructor (Metis (type_enc, lam_trans)) = |
|
38 |
metis_call type_enc lam_trans |
|
39 |
| string_of_reconstructor SMT = smtN |
|
40 |
||
41 |
||
42 |
||
43 |
(** one-liner reconstructor proofs **) |
|
44 |
||
45 |
fun show_time NONE = "" |
|
46 |
| show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")" |
|
47 |
||
48 |
(* FIXME: Various bugs, esp. with "unfolding" |
|
49 |
fun unusing_chained_facts _ 0 = "" |
|
50 |
| unusing_chained_facts used_chaineds num_chained = |
|
51 |
if length used_chaineds = num_chained then "" |
|
52 |
else if null used_chaineds then "(* using no facts *) " |
|
53 |
else "(* using only " ^ space_implode " " used_chaineds ^ " *) " |
|
54 |
*) |
|
55 |
||
56 |
fun apply_on_subgoal _ 1 = "by " |
|
57 |
| apply_on_subgoal 1 _ = "apply " |
|
58 |
| apply_on_subgoal i n = |
|
59 |
"prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n |
|
60 |
||
61 |
fun using_labels [] = "" |
|
62 |
| using_labels ls = |
|
63 |
"using " ^ space_implode " " (map string_of_label ls) ^ " " |
|
64 |
||
65 |
fun command_call name [] = |
|
66 |
name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")" |
|
67 |
| command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" |
|
68 |
||
69 |
fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) = |
|
70 |
(* unusing_chained_facts used_chaineds num_chained ^ *) |
|
71 |
using_labels ls ^ apply_on_subgoal i n ^ |
|
72 |
command_call (string_of_reconstructor reconstr) ss |
|
73 |
||
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset
|
74 |
fun try_command_line banner time command = |
52697
6fb98a20c349
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm
parents:
52629
diff
changeset
|
75 |
banner ^ ": " ^ |
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset
|
76 |
Active.sendback_markup [Markup.padding_command] command ^ |
52697
6fb98a20c349
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm
parents:
52629
diff
changeset
|
77 |
show_time time ^ "." |
52555 | 78 |
|
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset
|
79 |
fun minimize_line _ [] = "" |
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset
|
80 |
| minimize_line minimize_command ss = |
52555 | 81 |
case minimize_command ss of |
82 |
"" => "" |
|
83 |
| command => |
|
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset
|
84 |
"\nTo minimize: " ^ |
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset
|
85 |
Active.sendback_markup [Markup.padding_command] command ^ "." |
52555 | 86 |
|
87 |
fun split_used_facts facts = |
|
88 |
facts |> List.partition (fn (_, (sc, _)) => sc = Chained) |
|
89 |
|> pairself (sort_distinct (string_ord o pairself fst)) |
|
90 |
||
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset
|
91 |
fun one_line_proof_text num_chained |
52555 | 92 |
(preplay, banner, used_facts, minimize_command, subgoal, |
93 |
subgoal_count) = |
|
94 |
let |
|
95 |
val (chained, extra) = split_used_facts used_facts |
|
96 |
val (failed, reconstr, ext_time) = |
|
97 |
case preplay of |
|
98 |
Played (reconstr, time) => (false, reconstr, (SOME (false, time))) |
|
99 |
| Trust_Playable (reconstr, time) => |
|
100 |
(false, reconstr, |
|
101 |
case time of |
|
102 |
NONE => NONE |
|
103 |
| SOME time => |
|
104 |
if time = Time.zeroTime then NONE else SOME (true, time)) |
|
105 |
| Failed_to_Play reconstr => (true, reconstr, NONE) |
|
106 |
val try_line = |
|
107 |
([], map fst extra) |
|
108 |
|> reconstructor_command reconstr subgoal subgoal_count (map fst chained) |
|
109 |
num_chained |
|
110 |
|> (if failed then |
|
111 |
enclose "One-line proof reconstruction failed: " |
|
112 |
".\n(Invoking \"sledgehammer\" with \"[strict]\" might \ |
|
113 |
\solve this.)" |
|
114 |
else |
|
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset
|
115 |
try_command_line banner ext_time) |
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset
|
116 |
in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end |
52555 | 117 |
|
118 |
||
119 |
||
120 |
||
121 |
(** detailed Isar proofs **) |
|
122 |
||
123 |
val indent_size = 2 |
|
124 |
||
125 |
fun string_of_proof ctxt type_enc lam_trans i n proof = |
|
126 |
let |
|
127 |
val ctxt = |
|
128 |
(* make sure type constraint are actually printed *) |
|
129 |
ctxt |> Config.put show_markup false |
|
130 |
(* make sure only type constraints inserted by sh_annotate are printed *) |
|
131 |
|> Config.put Printer.show_type_emphasis false |
|
132 |
|> Config.put show_types false |
|
133 |
|> Config.put show_sorts false |
|
134 |
|> Config.put show_consts false |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
135 |
|
52555 | 136 |
val register_fixes = map Free #> fold Variable.auto_fixes |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
137 |
|
52555 | 138 |
fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt) |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
139 |
|
52555 | 140 |
fun of_indent ind = replicate_string (ind * indent_size) " " |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
141 |
|
52555 | 142 |
fun of_moreover ind = of_indent ind ^ "moreover\n" |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
143 |
|
52555 | 144 |
fun of_label l = if l = no_label then "" else string_of_label l ^ ": " |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
145 |
|
52555 | 146 |
fun of_obtain qs nr = |
147 |
(if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then |
|
148 |
"ultimately " |
|
52994 | 149 |
else if nr = 1 orelse member (op =) qs Then then |
52555 | 150 |
"then " |
151 |
else |
|
152 |
"") ^ "obtain" |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
153 |
|
52555 | 154 |
fun of_show_have qs = if member (op =) qs Show then "show" else "have" |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
155 |
|
52555 | 156 |
fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence" |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
157 |
|
52555 | 158 |
fun of_prove qs nr = |
159 |
if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then |
|
160 |
"ultimately " ^ of_show_have qs |
|
161 |
else if nr=1 orelse member (op =) qs Then then |
|
162 |
of_thus_hence qs |
|
163 |
else |
|
164 |
of_show_have qs |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
165 |
|
52555 | 166 |
fun add_term term (s, ctxt) = |
167 |
(s ^ (term |
|
168 |
|> singleton (Syntax.uncheck_terms ctxt) |
|
169 |
|> annotate_types ctxt |
|
170 |
|> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of) |
|
171 |
|> simplify_spaces |
|
172 |
|> maybe_quote), |
|
173 |
ctxt |> Variable.auto_fixes term) |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
174 |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54754
diff
changeset
|
175 |
fun by_method meth = "by " ^ |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54754
diff
changeset
|
176 |
(case meth of |
54765 | 177 |
Simp_Method => "simp" |
178 |
| Auto_Method => "auto" |
|
179 |
| Fastforce_Method => "fastforce" |
|
180 |
| Force_Method => "force" |
|
181 |
| Arith_Method => "arith" |
|
182 |
| Blast_Method => "blast" |
|
183 |
| Meson_Method => "meson" |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
184 |
| _ => raise Fail "Sledgehammer_Print: by_method") |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
185 |
|
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
186 |
fun using_facts [] [] = "" |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
187 |
| using_facts ls ss = |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
188 |
"using " ^ space_implode " " (map string_of_label ls @ ss) ^ " " |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
189 |
|
54765 | 190 |
fun of_method ls ss Metis_Method = |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54754
diff
changeset
|
191 |
reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss) |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54754
diff
changeset
|
192 |
| of_method ls ss meth = using_facts ls ss ^ by_method meth |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
193 |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54754
diff
changeset
|
194 |
fun of_byline ind options (ls, ss) meth = |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
195 |
let |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
196 |
val ls = ls |> sort_distinct label_ord |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
197 |
val ss = ss |> sort_distinct string_ord |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
198 |
in |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54754
diff
changeset
|
199 |
"\n" ^ of_indent (ind + 1) ^ options ^ of_method ls ss meth |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
200 |
end |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
201 |
|
52555 | 202 |
fun of_free (s, T) = |
203 |
maybe_quote s ^ " :: " ^ |
|
204 |
maybe_quote (simplify_spaces (with_vanilla_print_mode |
|
205 |
(Syntax.string_of_typ ctxt) T)) |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
206 |
|
52555 | 207 |
fun add_frees xs (s, ctxt) = |
208 |
(s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs) |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
209 |
|
52555 | 210 |
fun add_fix _ [] = I |
211 |
| add_fix ind xs = add_suffix (of_indent ind ^ "fix ") |
|
212 |
#> add_frees xs |
|
213 |
#> add_suffix "\n" |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
214 |
|
52555 | 215 |
fun add_assm ind (l, t) = |
216 |
add_suffix (of_indent ind ^ "assume " ^ of_label l) |
|
217 |
#> add_term t |
|
218 |
#> add_suffix "\n" |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
219 |
|
52555 | 220 |
fun add_assms ind assms = fold (add_assm ind) assms |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
221 |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54754
diff
changeset
|
222 |
fun add_step_post ind l t facts meth options = |
52555 | 223 |
add_suffix (of_label l) |
224 |
#> add_term t |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54754
diff
changeset
|
225 |
#> add_suffix (of_byline ind options facts meth ^ "\n") |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
226 |
|
52555 | 227 |
fun of_subproof ind ctxt proof = |
228 |
let |
|
229 |
val ind = ind + 1 |
|
230 |
val s = of_proof ind ctxt proof |
|
231 |
val prefix = "{ " |
|
232 |
val suffix = " }" |
|
233 |
in |
|
234 |
replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ |
|
235 |
String.extract (s, ind * indent_size, |
|
236 |
SOME (size s - ind * indent_size - 1)) ^ |
|
237 |
suffix ^ "\n" |
|
238 |
end |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
239 |
|
52555 | 240 |
and of_subproofs _ _ _ [] = "" |
241 |
| of_subproofs ind ctxt qs subproofs = |
|
242 |
(if member (op =) qs Then then of_moreover ind else "") ^ |
|
243 |
space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs) |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
244 |
|
52555 | 245 |
and add_step_pre ind qs subproofs (s, ctxt) = |
246 |
(s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt) |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
247 |
|
52555 | 248 |
and add_step ind (Let (t1, t2)) = |
249 |
add_suffix (of_indent ind ^ "let ") |
|
250 |
#> add_term t1 |
|
251 |
#> add_suffix " = " |
|
252 |
#> add_term t2 |
|
253 |
#> add_suffix "\n" |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54754
diff
changeset
|
254 |
| add_step ind (step as Prove (qs, xs, l, t, subproofs, (facts, meth))) = |
52555 | 255 |
(case xs of |
256 |
[] => (* have *) |
|
54765 | 257 |
add_step_pre ind qs subproofs |
258 |
#> add_suffix (of_prove qs (length subproofs) ^ " ") |
|
259 |
#> add_step_post ind l t facts meth "" |
|
52555 | 260 |
| _ => (* obtain *) |
54765 | 261 |
add_step_pre ind qs subproofs |
262 |
#> add_suffix (of_obtain qs (length subproofs) ^ " ") |
|
263 |
#> add_frees xs |
|
264 |
#> add_suffix " where " |
|
265 |
#> add_step_post ind l t facts meth |
|
266 |
(if use_metis_new_skolem step then "using [[metis_new_skolem]] " else "")) |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
267 |
|
52555 | 268 |
and add_steps ind = fold (add_step ind) |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
269 |
|
54700 | 270 |
and of_proof ind ctxt (Proof (xs, assms, steps)) = |
271 |
("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst |
|
52555 | 272 |
in |
54700 | 273 |
(* One-step Metis proofs are pointless; better use the one-liner directly. *) |
274 |
(case proof of |
|
54754 | 275 |
Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *) |
54765 | 276 |
| Proof ([], [], [Prove (_, [], _, _, [], (_, Metis_Method))]) => "" |
54700 | 277 |
| _ => |
278 |
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ |
|
279 |
of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ |
|
280 |
of_indent 0 ^ (if n <> 1 then "next" else "qed")) |
|
52555 | 281 |
end |
282 |
||
54504 | 283 |
end; |