author | blanchet |
Thu, 19 Dec 2013 16:11:20 +0100 | |
changeset 54821 | a12796872603 |
parent 54815 | 4f6ec8754bf5 |
child 54823 | a510fc40559c |
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 |
|
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
|
15 |
val one_line_proof_text : int -> one_line_params -> string |
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
16 |
val string_of_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string |
52555 | 17 |
end; |
18 |
||
19 |
structure Sledgehammer_Print : SLEDGEHAMMER_PRINT = |
|
20 |
struct |
|
21 |
||
22 |
open ATP_Util |
|
23 |
open ATP_Proof |
|
24 |
open ATP_Problem_Generate |
|
25 |
open ATP_Proof_Reconstruct |
|
26 |
open Sledgehammer_Util |
|
27 |
open Sledgehammer_Reconstructor |
|
28 |
open Sledgehammer_Proof |
|
29 |
open Sledgehammer_Annotate |
|
30 |
||
31 |
||
32 |
(** reconstructors **) |
|
33 |
||
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
34 |
fun string_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans |
52555 | 35 |
| string_of_reconstructor SMT = smtN |
36 |
||
37 |
||
38 |
(** one-liner reconstructor proofs **) |
|
39 |
||
40 |
fun show_time NONE = "" |
|
41 |
| show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")" |
|
42 |
||
43 |
(* FIXME: Various bugs, esp. with "unfolding" |
|
44 |
fun unusing_chained_facts _ 0 = "" |
|
45 |
| unusing_chained_facts used_chaineds num_chained = |
|
46 |
if length used_chaineds = num_chained then "" |
|
47 |
else if null used_chaineds then "(* using no facts *) " |
|
48 |
else "(* using only " ^ space_implode " " used_chaineds ^ " *) " |
|
49 |
*) |
|
50 |
||
51 |
fun apply_on_subgoal _ 1 = "by " |
|
52 |
| apply_on_subgoal 1 _ = "apply " |
|
53 |
| apply_on_subgoal i n = |
|
54 |
"prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n |
|
55 |
||
56 |
fun using_labels [] = "" |
|
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
57 |
| using_labels ls = "using " ^ space_implode " " (map string_of_label ls) ^ " " |
52555 | 58 |
|
59 |
fun command_call name [] = |
|
60 |
name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")" |
|
61 |
| command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" |
|
62 |
||
63 |
fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) = |
|
64 |
(* unusing_chained_facts used_chaineds num_chained ^ *) |
|
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
65 |
using_labels ls ^ apply_on_subgoal i n ^ command_call (string_of_reconstructor reconstr) ss |
52555 | 66 |
|
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
|
67 |
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
|
68 |
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
|
69 |
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
|
70 |
show_time time ^ "." |
52555 | 71 |
|
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
|
72 |
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
|
73 |
| minimize_line minimize_command ss = |
52555 | 74 |
case minimize_command ss of |
75 |
"" => "" |
|
76 |
| 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
|
77 |
"\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
|
78 |
Active.sendback_markup [Markup.padding_command] command ^ "." |
52555 | 79 |
|
80 |
fun split_used_facts facts = |
|
81 |
facts |> List.partition (fn (_, (sc, _)) => sc = Chained) |
|
82 |
|> pairself (sort_distinct (string_ord o pairself fst)) |
|
83 |
||
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 |
fun one_line_proof_text num_chained |
54771
85879aa61334
move some Z3 specifics out (and into private repository with the rest of the Z3-specific code)
blanchet
parents:
54767
diff
changeset
|
85 |
(preplay, banner, used_facts, minimize_command, subgoal, subgoal_count) = |
52555 | 86 |
let |
87 |
val (chained, extra) = split_used_facts used_facts |
|
88 |
val (failed, reconstr, ext_time) = |
|
54815 | 89 |
(case preplay of |
52555 | 90 |
Played (reconstr, time) => (false, reconstr, (SOME (false, time))) |
54813 | 91 |
| Play_Timed_Out (reconstr, time) => |
54815 | 92 |
(false, reconstr, if time = Time.zeroTime then NONE else SOME (true, time)) |
93 |
| Play_Failed reconstr => (true, reconstr, NONE)) |
|
52555 | 94 |
val try_line = |
95 |
([], map fst extra) |
|
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
96 |
|> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained |
52555 | 97 |
|> (if failed then |
98 |
enclose "One-line proof reconstruction failed: " |
|
99 |
".\n(Invoking \"sledgehammer\" with \"[strict]\" might \ |
|
100 |
\solve this.)" |
|
101 |
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
|
102 |
try_command_line banner ext_time) |
54771
85879aa61334
move some Z3 specifics out (and into private repository with the rest of the Z3-specific code)
blanchet
parents:
54767
diff
changeset
|
103 |
in |
85879aa61334
move some Z3 specifics out (and into private repository with the rest of the Z3-specific code)
blanchet
parents:
54767
diff
changeset
|
104 |
try_line ^ minimize_line minimize_command (map fst (extra @ chained)) |
85879aa61334
move some Z3 specifics out (and into private repository with the rest of the Z3-specific code)
blanchet
parents:
54767
diff
changeset
|
105 |
end |
52555 | 106 |
|
107 |
||
108 |
(** detailed Isar proofs **) |
|
109 |
||
110 |
val indent_size = 2 |
|
111 |
||
112 |
fun string_of_proof ctxt type_enc lam_trans i n proof = |
|
113 |
let |
|
114 |
val ctxt = |
|
115 |
(* make sure type constraint are actually printed *) |
|
116 |
ctxt |> Config.put show_markup false |
|
117 |
(* make sure only type constraints inserted by sh_annotate are printed *) |
|
118 |
|> Config.put Printer.show_type_emphasis false |
|
119 |
|> Config.put show_types false |
|
120 |
|> Config.put show_sorts false |
|
121 |
|> Config.put show_consts false |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
122 |
|
52555 | 123 |
val register_fixes = map Free #> fold Variable.auto_fixes |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
124 |
|
52555 | 125 |
fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt) |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
126 |
|
52555 | 127 |
fun of_indent ind = replicate_string (ind * indent_size) " " |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
128 |
|
52555 | 129 |
fun of_moreover ind = of_indent ind ^ "moreover\n" |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
130 |
|
52555 | 131 |
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
|
132 |
|
52555 | 133 |
fun of_obtain qs nr = |
134 |
(if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then |
|
135 |
"ultimately " |
|
52994 | 136 |
else if nr = 1 orelse member (op =) qs Then then |
52555 | 137 |
"then " |
138 |
else |
|
139 |
"") ^ "obtain" |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
140 |
|
52555 | 141 |
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
|
142 |
|
52555 | 143 |
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
|
144 |
|
54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset
|
145 |
fun of_have qs nr = |
52555 | 146 |
if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then |
147 |
"ultimately " ^ of_show_have qs |
|
54821 | 148 |
else if nr = 1 orelse member (op =) qs Then then |
52555 | 149 |
of_thus_hence qs |
150 |
else |
|
151 |
of_show_have qs |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
152 |
|
52555 | 153 |
fun add_term term (s, ctxt) = |
154 |
(s ^ (term |
|
155 |
|> singleton (Syntax.uncheck_terms ctxt) |
|
156 |
|> annotate_types ctxt |
|
157 |
|> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of) |
|
158 |
|> simplify_spaces |
|
159 |
|> maybe_quote), |
|
160 |
ctxt |> Variable.auto_fixes term) |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
161 |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54754
diff
changeset
|
162 |
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
|
163 |
(case meth of |
54765 | 164 |
Simp_Method => "simp" |
165 |
| Auto_Method => "auto" |
|
166 |
| Fastforce_Method => "fastforce" |
|
167 |
| Force_Method => "force" |
|
168 |
| Arith_Method => "arith" |
|
169 |
| Blast_Method => "blast" |
|
170 |
| Meson_Method => "meson" |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
171 |
| _ => raise Fail "Sledgehammer_Print: by_method") |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
172 |
|
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
173 |
fun using_facts [] [] = "" |
54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset
|
174 |
| using_facts ls ss = "using " ^ space_implode " " (map string_of_label ls @ ss) ^ " " |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
175 |
|
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
176 |
fun of_metis ls ss = reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss) |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
177 |
|
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
178 |
fun of_method ls ss Metis_Method = of_metis ls ss |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
179 |
| of_method ls ss Metis_New_Skolem_Method = "using [[metis_new_skolem]] " ^ of_metis ls ss |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54754
diff
changeset
|
180 |
| 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
|
181 |
|
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
182 |
fun of_byline ind (ls, ss) meth = |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
183 |
let |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
184 |
val ls = ls |> sort_distinct label_ord |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
185 |
val ss = ss |> sort_distinct string_ord |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
186 |
in |
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
187 |
"\n" ^ of_indent (ind + 1) ^ of_method ls ss meth |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
188 |
end |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
189 |
|
52555 | 190 |
fun of_free (s, T) = |
191 |
maybe_quote s ^ " :: " ^ |
|
54821 | 192 |
maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T)) |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
193 |
|
52555 | 194 |
fun add_frees xs (s, ctxt) = |
195 |
(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
|
196 |
|
52555 | 197 |
fun add_fix _ [] = I |
198 |
| add_fix ind xs = add_suffix (of_indent ind ^ "fix ") |
|
199 |
#> add_frees xs |
|
200 |
#> add_suffix "\n" |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
201 |
|
52555 | 202 |
fun add_assm ind (l, t) = |
203 |
add_suffix (of_indent ind ^ "assume " ^ of_label l) |
|
204 |
#> add_term t |
|
205 |
#> add_suffix "\n" |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
206 |
|
52555 | 207 |
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
|
208 |
|
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
209 |
fun add_step_post ind l t facts meth = |
52555 | 210 |
add_suffix (of_label l) |
211 |
#> add_term t |
|
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
212 |
#> add_suffix (of_byline ind facts meth ^ "\n") |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
213 |
|
52555 | 214 |
fun of_subproof ind ctxt proof = |
215 |
let |
|
216 |
val ind = ind + 1 |
|
217 |
val s = of_proof ind ctxt proof |
|
218 |
val prefix = "{ " |
|
219 |
val suffix = " }" |
|
220 |
in |
|
221 |
replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ |
|
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
222 |
String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^ |
52555 | 223 |
suffix ^ "\n" |
224 |
end |
|
225 |
and of_subproofs _ _ _ [] = "" |
|
226 |
| of_subproofs ind ctxt qs subproofs = |
|
227 |
(if member (op =) qs Then then of_moreover ind else "") ^ |
|
228 |
space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs) |
|
229 |
and add_step_pre ind qs subproofs (s, ctxt) = |
|
230 |
(s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt) |
|
231 |
and add_step ind (Let (t1, t2)) = |
|
232 |
add_suffix (of_indent ind ^ "let ") |
|
233 |
#> add_term t1 |
|
234 |
#> add_suffix " = " |
|
235 |
#> add_term t2 |
|
236 |
#> add_suffix "\n" |
|
54799 | 237 |
| add_step ind (Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) = |
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
238 |
add_step_pre ind qs subproofs |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
239 |
#> (case xs of |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
240 |
[] => add_suffix (of_have qs (length subproofs) ^ " ") |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
241 |
| _ => |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
242 |
add_suffix (of_obtain qs (length subproofs) ^ " ") |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
243 |
#> add_frees xs |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
244 |
#> add_suffix " where ") |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
245 |
#> add_step_post ind l t facts meth |
52555 | 246 |
and add_steps ind = fold (add_step ind) |
54700 | 247 |
and of_proof ind ctxt (Proof (xs, assms, steps)) = |
248 |
("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst |
|
52555 | 249 |
in |
54700 | 250 |
(* One-step Metis proofs are pointless; better use the one-liner directly. *) |
251 |
(case proof of |
|
54754 | 252 |
Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *) |
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
253 |
| Proof ([], [], [Prove (_, [], _, _, [], (_, (Metis_Method :: _) :: _))]) => "" |
54700 | 254 |
| _ => |
255 |
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ |
|
256 |
of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ |
|
257 |
of_indent 0 ^ (if n <> 1 then "next" else "qed")) |
|
52555 | 258 |
end |
259 |
||
54504 | 260 |
end; |