52590
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
|
52555
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
|
3 |
Author: Steffen Juilf Smolka, TU Muenchen
|
|
4 |
|
|
5 |
Reconstructors.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature SLEDGEHAMMER_RECONSTRUCTOR =
|
|
9 |
sig
|
|
10 |
type stature = ATP_Problem_Generate.stature
|
|
11 |
|
55285
|
12 |
datatype proof_method =
|
|
13 |
Metis_Method of string option * string option |
|
|
14 |
Meson_Method |
|
|
15 |
SMT_Method |
|
|
16 |
Simp_Method |
|
|
17 |
Simp_Size_Method |
|
|
18 |
Auto_Method |
|
|
19 |
Fastforce_Method |
|
|
20 |
Force_Method |
|
|
21 |
Arith_Method |
|
|
22 |
Blast_Method |
|
|
23 |
Algebra_Method
|
52555
|
24 |
|
54824
|
25 |
datatype play_outcome =
|
|
26 |
Played of Time.time |
|
|
27 |
Play_Timed_Out of Time.time |
|
|
28 |
Play_Failed |
|
|
29 |
Not_Played
|
52555
|
30 |
|
|
31 |
type minimize_command = string list -> string
|
54824
|
32 |
type one_line_params =
|
55285
|
33 |
(proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
|
52555
|
34 |
|
|
35 |
val smtN : string
|
55212
|
36 |
|
55285
|
37 |
val string_of_proof_method : proof_method -> string
|
|
38 |
val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
|
55211
|
39 |
val string_of_play_outcome : play_outcome -> string
|
55269
|
40 |
val play_outcome_ord : play_outcome * play_outcome -> order
|
55211
|
41 |
val one_line_proof_text : int -> one_line_params -> string
|
55285
|
42 |
val silence_proof_methods : bool -> Proof.context -> Proof.context
|
54495
|
43 |
end;
|
52555
|
44 |
|
|
45 |
structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
|
|
46 |
struct
|
|
47 |
|
54828
|
48 |
open ATP_Util
|
52555
|
49 |
open ATP_Problem_Generate
|
55211
|
50 |
open ATP_Proof_Reconstruct
|
52555
|
51 |
|
55285
|
52 |
datatype proof_method =
|
|
53 |
Metis_Method of string option * string option |
|
|
54 |
Meson_Method |
|
|
55 |
SMT_Method |
|
|
56 |
Simp_Method |
|
|
57 |
Simp_Size_Method |
|
|
58 |
Auto_Method |
|
|
59 |
Fastforce_Method |
|
|
60 |
Force_Method |
|
|
61 |
Arith_Method |
|
|
62 |
Blast_Method |
|
|
63 |
Algebra_Method
|
52555
|
64 |
|
54824
|
65 |
datatype play_outcome =
|
|
66 |
Played of Time.time |
|
|
67 |
Play_Timed_Out of Time.time |
|
|
68 |
Play_Failed |
|
|
69 |
Not_Played
|
52555
|
70 |
|
55211
|
71 |
type minimize_command = string list -> string
|
|
72 |
type one_line_params =
|
55285
|
73 |
(proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
|
55211
|
74 |
|
|
75 |
val smtN = "smt"
|
|
76 |
|
55285
|
77 |
fun string_of_proof_method meth =
|
|
78 |
(case meth of
|
|
79 |
Metis_Method (NONE, NONE) => "metis"
|
|
80 |
| Metis_Method (type_enc_opt, lam_trans_opt) =>
|
|
81 |
"metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
|
|
82 |
| Meson_Method => "meson"
|
|
83 |
| SMT_Method => "smt"
|
|
84 |
| Simp_Method => "simp"
|
|
85 |
| Simp_Size_Method => "simp add: size_ne_size_imp_ne"
|
|
86 |
| Auto_Method => "auto"
|
|
87 |
| Fastforce_Method => "fastforce"
|
|
88 |
| Force_Method => "force"
|
|
89 |
| Arith_Method => "arith"
|
|
90 |
| Blast_Method => "blast"
|
|
91 |
| Algebra_Method => "algebra")
|
|
92 |
|
|
93 |
fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
|
|
94 |
Method.insert_tac local_facts THEN'
|
|
95 |
(case meth of
|
|
96 |
Metis_Method (type_enc_opt, lam_trans_opt) =>
|
|
97 |
Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc]
|
|
98 |
(the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts
|
|
99 |
| SMT_Method => SMT_Solver.smt_tac ctxt global_facts
|
|
100 |
| Meson_Method => Meson.meson_tac ctxt global_facts
|
|
101 |
| _ =>
|
|
102 |
Method.insert_tac global_facts THEN'
|
|
103 |
(case meth of
|
|
104 |
Simp_Method => Simplifier.asm_full_simp_tac ctxt
|
|
105 |
| Simp_Size_Method =>
|
|
106 |
Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
|
|
107 |
| Auto_Method => K (Clasimp.auto_tac ctxt)
|
|
108 |
| Fastforce_Method => Clasimp.fast_force_tac ctxt
|
|
109 |
| Force_Method => Clasimp.force_tac ctxt
|
|
110 |
| Arith_Method => Arith_Data.arith_tac ctxt
|
|
111 |
| Blast_Method => blast_tac ctxt
|
|
112 |
| Algebra_Method => Groebner.algebra_tac [] [] ctxt))
|
55211
|
113 |
|
54828
|
114 |
fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
|
|
115 |
| string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
|
|
116 |
| string_of_play_outcome Play_Failed = "failed"
|
|
117 |
| string_of_play_outcome _ = "unknown"
|
|
118 |
|
55269
|
119 |
fun play_outcome_ord (Played time1, Played time2) =
|
|
120 |
int_ord (pairself Time.toMilliseconds (time1, time2))
|
|
121 |
| play_outcome_ord (Played _, _) = LESS
|
|
122 |
| play_outcome_ord (_, Played _) = GREATER
|
|
123 |
| play_outcome_ord (Not_Played, Not_Played) = EQUAL
|
|
124 |
| play_outcome_ord (Not_Played, _) = LESS
|
|
125 |
| play_outcome_ord (_, Not_Played) = GREATER
|
|
126 |
| play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) =
|
|
127 |
int_ord (pairself Time.toMilliseconds (time1, time2))
|
|
128 |
| play_outcome_ord (Play_Timed_Out _, _) = LESS
|
|
129 |
| play_outcome_ord (_, Play_Timed_Out _) = GREATER
|
|
130 |
| play_outcome_ord (Play_Failed, Play_Failed) = EQUAL
|
|
131 |
|
55211
|
132 |
(* FIXME: Various bugs, esp. with "unfolding"
|
|
133 |
fun unusing_chained_facts _ 0 = ""
|
|
134 |
| unusing_chained_facts used_chaineds num_chained =
|
|
135 |
if length used_chaineds = num_chained then ""
|
|
136 |
else if null used_chaineds then "(* using no facts *) "
|
|
137 |
else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
|
|
138 |
*)
|
|
139 |
|
|
140 |
fun apply_on_subgoal _ 1 = "by "
|
|
141 |
| apply_on_subgoal 1 _ = "apply "
|
|
142 |
| apply_on_subgoal i n =
|
|
143 |
"prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
|
|
144 |
|
|
145 |
fun command_call name [] =
|
|
146 |
name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
|
|
147 |
| command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
|
|
148 |
|
55285
|
149 |
(* FIXME *)
|
|
150 |
fun proof_method_command meth i n used_chaineds num_chained ss =
|
55211
|
151 |
(* unusing_chained_facts used_chaineds num_chained ^ *)
|
55285
|
152 |
apply_on_subgoal i n ^ command_call (string_of_proof_method meth) ss
|
55211
|
153 |
|
|
154 |
fun show_time NONE = ""
|
|
155 |
| show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
|
|
156 |
|
|
157 |
fun try_command_line banner time command =
|
|
158 |
banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^ show_time time ^ "."
|
52555
|
159 |
|
55211
|
160 |
fun minimize_line _ [] = ""
|
|
161 |
| minimize_line minimize_command ss =
|
|
162 |
(case minimize_command ss of
|
|
163 |
"" => ""
|
|
164 |
| command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] command ^ ".")
|
|
165 |
|
|
166 |
fun split_used_facts facts =
|
|
167 |
facts
|
|
168 |
|> List.partition (fn (_, (sc, _)) => sc = Chained)
|
|
169 |
|> pairself (sort_distinct (string_ord o pairself fst))
|
|
170 |
|
|
171 |
fun one_line_proof_text num_chained
|
55285
|
172 |
((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
|
55211
|
173 |
let
|
|
174 |
val (chained, extra) = split_used_facts used_facts
|
|
175 |
|
|
176 |
val (failed, ext_time) =
|
|
177 |
(case play of
|
|
178 |
Played time => (false, (SOME (false, time)))
|
|
179 |
| Play_Timed_Out time => (false, SOME (true, time))
|
|
180 |
| Play_Failed => (true, NONE)
|
|
181 |
| Not_Played => (false, NONE))
|
|
182 |
|
|
183 |
val try_line =
|
|
184 |
map fst extra
|
55285
|
185 |
|> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained
|
55211
|
186 |
|> (if failed then
|
|
187 |
enclose "One-line proof reconstruction failed: "
|
|
188 |
".\n(Invoking \"sledgehammer\" with \"[strict]\" might solve this.)"
|
|
189 |
else
|
|
190 |
try_command_line banner ext_time)
|
|
191 |
in
|
|
192 |
try_line ^ minimize_line minimize_command (map fst (extra @ chained))
|
|
193 |
end
|
52555
|
194 |
|
55285
|
195 |
(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound
|
|
196 |
exceeded" warnings and the like. *)
|
|
197 |
fun silence_proof_methods debug =
|
55180
|
198 |
Try0.silence_methods debug
|
55170
|
199 |
#> Config.put SMT_Config.verbose debug
|
|
200 |
|
54495
|
201 |
end;
|