author | blanchet |
Mon, 31 Jan 2022 16:09:23 +0100 | |
changeset 75034 | 890b70f96fe4 |
parent 73975 | 8d93f9ca6518 |
child 75040 | fada390d49dd |
permissions | -rw-r--r-- |
55287 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML |
52555 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
Author: Steffen Juilf Smolka, TU Muenchen |
|
4 |
||
5 |
Reconstructors. |
|
6 |
*) |
|
7 |
||
55287 | 8 |
signature SLEDGEHAMMER_PROOF_METHODS = |
52555 | 9 |
sig |
10 |
type stature = ATP_Problem_Generate.stature |
|
11 |
||
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
12 |
datatype SMT_backend = |
72798
e732c98b02e6
tuned proof preplay to explicitly refer to Z3 backend
desharna
parents:
72518
diff
changeset
|
13 |
SMT_Z3 | |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
14 |
SMT_Verit of string |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
15 |
|
55285 | 16 |
datatype proof_method = |
17 |
Metis_Method of string option * string option | |
|
18 |
Meson_Method | |
|
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
19 |
SMT_Method of SMT_backend | |
56852
b38c5b9cf590
added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
blanchet
parents:
56093
diff
changeset
|
20 |
SATx_Method | |
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
21 |
Blast_Method | |
55285 | 22 |
Simp_Method | |
23 |
Auto_Method | |
|
58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58075
diff
changeset
|
24 |
Fastforce_Method | |
55285 | 25 |
Force_Method | |
58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58075
diff
changeset
|
26 |
Moura_Method | |
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
27 |
Linarith_Method | |
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
28 |
Presburger_Method | |
55285 | 29 |
Algebra_Method |
52555 | 30 |
|
54824 | 31 |
datatype play_outcome = |
32 |
Played of Time.time | |
|
33 |
Play_Timed_Out of Time.time | |
|
56093 | 34 |
Play_Failed |
52555 | 35 |
|
54824 | 36 |
type one_line_params = |
57739 | 37 |
((string * stature) list * (proof_method * play_outcome)) * string * int * int |
52555 | 38 |
|
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
39 |
val is_proof_method_direct : proof_method -> bool |
72401
2783779b7dd3
removed obsolete unmaintained experimental prover Pirate
blanchet
parents:
70586
diff
changeset
|
40 |
val string_of_proof_method : string list -> proof_method -> string |
57054 | 41 |
val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic |
55211 | 42 |
val string_of_play_outcome : play_outcome -> string |
70586 | 43 |
val play_outcome_ord : play_outcome ord |
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
44 |
val one_line_proof_text : Proof.context -> int -> one_line_params -> string |
54495 | 45 |
end; |
52555 | 46 |
|
55287 | 47 |
structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS = |
52555 | 48 |
struct |
49 |
||
54828 | 50 |
open ATP_Util |
52555 | 51 |
open ATP_Problem_Generate |
55211 | 52 |
open ATP_Proof_Reconstruct |
52555 | 53 |
|
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
54 |
datatype SMT_backend = |
72798
e732c98b02e6
tuned proof preplay to explicitly refer to Z3 backend
desharna
parents:
72518
diff
changeset
|
55 |
SMT_Z3 | |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
56 |
SMT_Verit of string |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
57 |
|
55285 | 58 |
datatype proof_method = |
59 |
Metis_Method of string option * string option | |
|
60 |
Meson_Method | |
|
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
61 |
SMT_Method of SMT_backend | |
56852
b38c5b9cf590
added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
blanchet
parents:
56093
diff
changeset
|
62 |
SATx_Method | |
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
63 |
Blast_Method | |
55285 | 64 |
Simp_Method | |
65 |
Auto_Method | |
|
58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58075
diff
changeset
|
66 |
Fastforce_Method | |
55285 | 67 |
Force_Method | |
58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58075
diff
changeset
|
68 |
Moura_Method | |
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
69 |
Linarith_Method | |
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
70 |
Presburger_Method | |
55285 | 71 |
Algebra_Method |
52555 | 72 |
|
54824 | 73 |
datatype play_outcome = |
74 |
Played of Time.time | |
|
75 |
Play_Timed_Out of Time.time | |
|
56093 | 76 |
Play_Failed |
52555 | 77 |
|
57739 | 78 |
type one_line_params = |
79 |
((string * stature) list * (proof_method * play_outcome)) * string * int * int |
|
55211 | 80 |
|
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
81 |
fun is_proof_method_direct (Metis_Method _) = true |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
82 |
| is_proof_method_direct Meson_Method = true |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
83 |
| is_proof_method_direct (SMT_Method _) = true |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
84 |
| is_proof_method_direct Simp_Method = true |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
85 |
| is_proof_method_direct _ = false |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
86 |
|
58499
094efe6ac459
don't affect other subgoals with 'auto' in one-liner proofs
blanchet
parents:
58092
diff
changeset
|
87 |
fun is_proof_method_multi_goal Auto_Method = true |
094efe6ac459
don't affect other subgoals with 'auto' in one-liner proofs
blanchet
parents:
58092
diff
changeset
|
88 |
| is_proof_method_multi_goal _ = false |
094efe6ac459
don't affect other subgoals with 'auto' in one-liner proofs
blanchet
parents:
58092
diff
changeset
|
89 |
|
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
90 |
fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
91 |
|
72401
2783779b7dd3
removed obsolete unmaintained experimental prover Pirate
blanchet
parents:
70586
diff
changeset
|
92 |
fun string_of_proof_method ss meth = |
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
93 |
let |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
94 |
val meth_s = |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
95 |
(case meth of |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
96 |
Metis_Method (NONE, NONE) => "metis" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
97 |
| Metis_Method (type_enc_opt, lam_trans_opt) => |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
98 |
"metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
99 |
| Meson_Method => "meson" |
72798
e732c98b02e6
tuned proof preplay to explicitly refer to Z3 backend
desharna
parents:
72518
diff
changeset
|
100 |
| SMT_Method SMT_Z3 => "smt (z3)" |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
101 |
| SMT_Method (SMT_Verit strategy) => |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
102 |
"smt (" ^ commas ("verit" :: (if strategy = "default" then [] else [strategy])) ^ ")" |
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
103 |
| SATx_Method => "satx" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
104 |
| Blast_Method => "blast" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
105 |
| Simp_Method => if null ss then "simp" else "simp add:" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
106 |
| Auto_Method => "auto" |
58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58075
diff
changeset
|
107 |
| Fastforce_Method => "fastforce" |
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
108 |
| Force_Method => "force" |
58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58075
diff
changeset
|
109 |
| Moura_Method => "moura" |
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
110 |
| Linarith_Method => "linarith" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
111 |
| Presburger_Method => "presburger" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
112 |
| Algebra_Method => "algebra") |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
113 |
in |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
114 |
maybe_paren (space_implode " " (meth_s :: ss)) |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
115 |
end |
55285 | 116 |
|
57054 | 117 |
fun tac_of_proof_method ctxt (local_facts, global_facts) meth = |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
118 |
let |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
119 |
fun tac_of_metis (type_enc_opt, lam_trans_opt) = |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
120 |
let |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
121 |
val ctxt = ctxt |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
122 |
|> Config.put Metis_Tactic.verbose false |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
123 |
|> Config.put Metis_Tactic.trace false |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
124 |
in |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
125 |
SELECT_GOAL (Metis_Tactic.metis_method ((Option.map single type_enc_opt, lam_trans_opt), |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
126 |
global_facts) ctxt local_facts) |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
127 |
end |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
128 |
|
72798
e732c98b02e6
tuned proof preplay to explicitly refer to Z3 backend
desharna
parents:
72518
diff
changeset
|
129 |
fun tac_of_smt SMT_Z3 = SMT_Solver.smt_tac |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
130 |
| tac_of_smt (SMT_Verit strategy) = Verit_Proof.verit_tac_stgy strategy |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
131 |
in |
55285 | 132 |
(case meth of |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
133 |
Metis_Method options => tac_of_metis options |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
134 |
| SMT_Method backend => tac_of_smt backend ctxt (local_facts @ global_facts) |
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
135 |
| _ => |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
136 |
Method.insert_tac ctxt local_facts THEN' |
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
137 |
(case meth of |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
138 |
Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
139 |
| Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts) |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
140 |
| _ => |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
141 |
Method.insert_tac ctxt global_facts THEN' |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
142 |
(case meth of |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
143 |
SATx_Method => SAT.satx_tac ctxt |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
144 |
| Blast_Method => blast_tac ctxt |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
145 |
| Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt) |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
146 |
| Fastforce_Method => Clasimp.fast_force_tac ctxt |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
147 |
| Force_Method => Clasimp.force_tac ctxt |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
148 |
| Moura_Method => moura_tac ctxt |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
149 |
| Linarith_Method => Lin_Arith.tac ctxt |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
150 |
| Presburger_Method => Cooper.tac true [] [] ctxt |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
151 |
| Algebra_Method => Groebner.algebra_tac [] [] ctxt))) |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
152 |
end |
55211 | 153 |
|
54828 | 154 |
fun string_of_play_outcome (Played time) = string_of_ext_time (false, time) |
56093 | 155 |
| string_of_play_outcome (Play_Timed_Out time) = |
156 |
if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out" |
|
54828 | 157 |
| string_of_play_outcome Play_Failed = "failed" |
158 |
||
55269 | 159 |
fun play_outcome_ord (Played time1, Played time2) = |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58499
diff
changeset
|
160 |
int_ord (apply2 Time.toMilliseconds (time1, time2)) |
55269 | 161 |
| play_outcome_ord (Played _, _) = LESS |
162 |
| play_outcome_ord (_, Played _) = GREATER |
|
163 |
| play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) = |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58499
diff
changeset
|
164 |
int_ord (apply2 Time.toMilliseconds (time1, time2)) |
55269 | 165 |
| play_outcome_ord (Play_Timed_Out _, _) = LESS |
166 |
| play_outcome_ord (_, Play_Timed_Out _) = GREATER |
|
167 |
| play_outcome_ord (Play_Failed, Play_Failed) = EQUAL |
|
168 |
||
55211 | 169 |
fun apply_on_subgoal _ 1 = "by " |
170 |
| apply_on_subgoal 1 _ = "apply " |
|
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
171 |
| apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n |
55211 | 172 |
|
55285 | 173 |
(* FIXME *) |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
174 |
fun proof_method_command meth i n used_chaineds _(*num_chained*) extras = |
60252
2c468c062589
improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset
|
175 |
let |
2c468c062589
improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset
|
176 |
val (indirect_ss, direct_ss) = |
73975
8d93f9ca6518
revisited ac28714b7478: more faithful preplaying with chained facts
blanchet
parents:
72798
diff
changeset
|
177 |
if is_proof_method_direct meth then ([], extras) else (extras, []) |
60252
2c468c062589
improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset
|
178 |
in |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
179 |
(if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^ |
72401
2783779b7dd3
removed obsolete unmaintained experimental prover Pirate
blanchet
parents:
70586
diff
changeset
|
180 |
apply_on_subgoal i n ^ string_of_proof_method direct_ss meth ^ |
58499
094efe6ac459
don't affect other subgoals with 'auto' in one-liner proofs
blanchet
parents:
58092
diff
changeset
|
181 |
(if is_proof_method_multi_goal meth andalso n <> 1 then "[1]" else "") |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
182 |
end |
55211 | 183 |
|
56093 | 184 |
fun try_command_line banner play command = |
185 |
let val s = string_of_play_outcome play in |
|
75034 | 186 |
banner ^ Active.sendback_markup_command command ^ |
63692 | 187 |
(s |> s <> "" ? enclose " (" ")") |
56093 | 188 |
end |
52555 | 189 |
|
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
190 |
fun one_line_proof_text _ num_chained |
57739 | 191 |
((used_facts, (meth, play)), banner, subgoal, subgoal_count) = |
57777 | 192 |
let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in |
57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57720
diff
changeset
|
193 |
map fst extra |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72401
diff
changeset
|
194 |
|> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained |
63692 | 195 |
|> (if play = Play_Failed then prefix "One-line proof reconstruction failed: " |
57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57720
diff
changeset
|
196 |
else try_command_line banner play) |
55211 | 197 |
end |
52555 | 198 |
|
54495 | 199 |
end; |