1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_preplay.ML |
|
2 Author: Steffen Juilf Smolka, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 |
|
5 Preplaying of Isar proofs. |
|
6 *) |
|
7 |
|
8 signature SLEDGEHAMMER_PREPLAY = |
|
9 sig |
|
10 type play_outcome = Sledgehammer_Reconstructor.play_outcome |
|
11 type isar_proof = Sledgehammer_Proof.isar_proof |
|
12 type isar_step = Sledgehammer_Proof.isar_step |
|
13 type label = Sledgehammer_Proof.label |
|
14 |
|
15 val trace: bool Config.T |
|
16 |
|
17 type preplay_interface = |
|
18 {get_preplay_outcome: label -> play_outcome, |
|
19 set_preplay_outcome: label -> play_outcome -> unit, |
|
20 preplay_quietly: Time.time -> isar_step -> play_outcome, |
|
21 overall_preplay_outcome: isar_proof -> play_outcome} |
|
22 |
|
23 val proof_preplay_interface: bool -> Proof.context -> string -> string -> bool -> Time.time -> |
|
24 isar_proof -> preplay_interface |
|
25 end; |
|
26 |
|
27 structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY = |
|
28 struct |
|
29 |
|
30 open ATP_Util |
|
31 open Sledgehammer_Util |
|
32 open Sledgehammer_Reconstructor |
|
33 open Sledgehammer_Proof |
|
34 |
|
35 val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false) |
|
36 |
|
37 fun preplay_trace ctxt assmsp concl result = |
|
38 let |
|
39 val ctxt = ctxt |> Config.put show_markup true |
|
40 val assms = op @ assmsp |
|
41 val time = "[" ^ string_of_play_outcome result ^ "]" |> Pretty.str |
|
42 val nr_of_assms = length assms |
|
43 val assms = assms |
|
44 |> map (Display.pretty_thm ctxt) |
|
45 |> (fn [] => Pretty.str "" |
|
46 | [a] => a |
|
47 | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms) (* Syntax.pretty_term!? *) |
|
48 val concl = concl |> Syntax.pretty_term ctxt |
|
49 val trace_list = [] |
|
50 |> cons concl |
|
51 |> nr_of_assms > 0 ? cons (Pretty.str "\<Longrightarrow>") |
|
52 |> cons assms |
|
53 |> cons time |
|
54 val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list) |
|
55 in |
|
56 tracing (Pretty.string_of pretty_trace) |
|
57 end |
|
58 |
|
59 fun take_time timeout tac arg = |
|
60 let val timing = Timing.start () in |
|
61 (TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing))) |
|
62 handle TimeLimit.TimeOut => Play_Timed_Out timeout |
|
63 end |
|
64 |
|
65 fun resolve_fact_names ctxt names = |
|
66 (names |
|
67 |>> map string_of_label |
|
68 |> pairself (maps (thms_of_name ctxt))) |
|
69 handle ERROR msg => error ("preplay error: " ^ msg) |
|
70 |
|
71 fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) = |
|
72 let |
|
73 val thy = Proof_Context.theory_of ctxt |
|
74 |
|
75 val concl = |
|
76 (case try List.last steps of |
|
77 SOME (Prove (_, [], _, t, _, _)) => t |
|
78 | _ => raise Fail "preplay error: malformed subproof") |
|
79 |
|
80 val var_idx = maxidx_of_term concl + 1 |
|
81 fun var_of_free (x, T) = Var ((x, var_idx), T) |
|
82 val subst = map (`var_of_free #> swap #> apfst Free) fixed_frees |
|
83 in |
|
84 Logic.list_implies (assms |> map snd, concl) |
|
85 |> subst_free subst |
|
86 |> Skip_Proof.make_thm thy |
|
87 end |
|
88 |
|
89 fun tac_of_method meth type_enc lam_trans ctxt (local_facts, global_facts) = |
|
90 Method.insert_tac local_facts THEN' |
|
91 (case meth of |
|
92 Meson_Method => Meson.meson_tac ctxt global_facts |
|
93 | Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt global_facts |
|
94 | _ => |
|
95 Method.insert_tac global_facts THEN' |
|
96 (case meth of |
|
97 Simp_Method => Simplifier.asm_full_simp_tac ctxt |
|
98 | Simp_Size_Method => |
|
99 Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt) |
|
100 | Auto_Method => K (Clasimp.auto_tac ctxt) |
|
101 | Fastforce_Method => Clasimp.fast_force_tac ctxt |
|
102 | Force_Method => Clasimp.force_tac ctxt |
|
103 | Arith_Method => Arith_Data.arith_tac ctxt |
|
104 | Blast_Method => blast_tac ctxt |
|
105 | _ => raise Fail "Sledgehammer_Preplay: tac_of_method")) |
|
106 |
|
107 (* main function for preplaying Isar steps; may throw exceptions *) |
|
108 fun preplay_raw _ _ _ _ _ (Let _) = Played Time.zeroTime |
|
109 | preplay_raw debug type_enc lam_trans ctxt timeout |
|
110 (Prove (_, xs, _, t, subproofs, (fact_names, (meth :: _) :: _))) = |
|
111 let |
|
112 val goal = |
|
113 (case xs of |
|
114 [] => t |
|
115 | _ => |
|
116 (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis |
|
117 (cf. "~~/src/Pure/Isar/obtain.ML") *) |
|
118 let |
|
119 (* FIXME: generate fresh name *) |
|
120 val thesis = Free ("thesis", HOLogic.boolT) |
|
121 val thesis_prop = thesis |> HOLogic.mk_Trueprop |
|
122 val frees = map Free xs |
|
123 |
|
124 (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) |
|
125 val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) |
|
126 in |
|
127 (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) |
|
128 Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) |
|
129 end) |
|
130 |
|
131 val facts = |
|
132 resolve_fact_names ctxt fact_names |
|
133 |>> append (map (thm_of_proof ctxt) subproofs) |
|
134 |
|
135 val ctxt' = ctxt |> silence_reconstructors debug |
|
136 |
|
137 fun prove () = |
|
138 Goal.prove ctxt' [] [] goal (fn {context = ctxt, ...} => |
|
139 HEADGOAL (tac_of_method meth type_enc lam_trans ctxt facts)) |
|
140 handle ERROR msg => error ("Preplay error: " ^ msg) |
|
141 |
|
142 val play_outcome = take_time timeout prove () |
|
143 in |
|
144 (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else (); |
|
145 play_outcome) |
|
146 end |
|
147 |
|
148 |
|
149 (*** proof preplay interface ***) |
|
150 |
|
151 type preplay_interface = |
|
152 {get_preplay_outcome: label -> play_outcome, |
|
153 set_preplay_outcome: label -> play_outcome -> unit, |
|
154 preplay_quietly: Time.time -> isar_step -> play_outcome, |
|
155 overall_preplay_outcome: isar_proof -> play_outcome} |
|
156 |
|
157 fun enrich_context_with_local_facts proof ctxt = |
|
158 let |
|
159 val thy = Proof_Context.theory_of ctxt |
|
160 |
|
161 fun enrich_with_fact l t = |
|
162 Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t]) |
|
163 |
|
164 val enrich_with_assms = fold (uncurry enrich_with_fact) |
|
165 |
|
166 fun enrich_with_proof (Proof (_, assms, isar_steps)) = |
|
167 enrich_with_assms assms #> fold enrich_with_step isar_steps |
|
168 and enrich_with_step (Let _) = I |
|
169 | enrich_with_step (Prove (_, _, l, t, subproofs, _)) = |
|
170 enrich_with_fact l t #> fold enrich_with_proof subproofs |
|
171 in |
|
172 enrich_with_proof proof ctxt |
|
173 end |
|
174 |
|
175 fun merge_preplay_outcomes _ Play_Failed = Play_Failed |
|
176 | merge_preplay_outcomes Play_Failed _ = Play_Failed |
|
177 | merge_preplay_outcomes (Play_Timed_Out t1) (Play_Timed_Out t2) = |
|
178 Play_Timed_Out (Time.+ (t1, t2)) |
|
179 | merge_preplay_outcomes (Played t1) (Play_Timed_Out t2) = Play_Timed_Out (Time.+ (t1, t2)) |
|
180 | merge_preplay_outcomes (Play_Timed_Out t1) (Played t2) = Play_Timed_Out (Time.+ (t1, t2)) |
|
181 | merge_preplay_outcomes (Played t1) (Played t2) = Played (Time.+ (t1, t2)) |
|
182 |
|
183 (* Given a proof, produces an imperative preplay interface with a shared table mapping from labels |
|
184 to preplay results. The preplay results are caluclated lazyly and cached to avoid repeated |
|
185 calculation. |
|
186 |
|
187 Precondition: The proof must be labeled canonically; cf. |
|
188 "Slegehammer_Proof.relabel_proof_canonically". *) |
|
189 fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay preplay_timeout proof = |
|
190 if not do_preplay then |
|
191 (* the "dont_preplay" option pretends that everything works just fine *) |
|
192 {get_preplay_outcome = K (Played Time.zeroTime), |
|
193 set_preplay_outcome = K (K ()), |
|
194 preplay_quietly = K (K (Played Time.zeroTime)), |
|
195 overall_preplay_outcome = K (Played Time.zeroTime)} : preplay_interface |
|
196 else |
|
197 let |
|
198 val ctxt = enrich_context_with_local_facts proof ctxt |
|
199 |
|
200 fun preplay quietly timeout step = |
|
201 preplay_raw debug type_enc lam_trans ctxt timeout step |
|
202 handle exn => |
|
203 if Exn.is_interrupt exn then |
|
204 reraise exn |
|
205 else |
|
206 (if not quietly andalso debug then |
|
207 warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^ |
|
208 @{make_string} exn) |
|
209 else |
|
210 (); |
|
211 Play_Failed) |
|
212 |
|
213 (* preplay steps treating exceptions like timeouts *) |
|
214 fun preplay_quietly timeout = preplay true timeout |
|
215 |
|
216 val preplay_tab = |
|
217 let |
|
218 fun add_step_to_tab step tab = |
|
219 (case label_of_step step of |
|
220 NONE => tab |
|
221 | SOME l => |
|
222 Canonical_Lbl_Tab.update_new |
|
223 (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab) |
|
224 handle Canonical_Lbl_Tab.DUP _ => raise Fail "Sledgehammer_Preplay: preplay time table" |
|
225 in |
|
226 Canonical_Lbl_Tab.empty |
|
227 |> fold_isar_steps add_step_to_tab (steps_of_proof proof) |
|
228 |> Unsynchronized.ref |
|
229 end |
|
230 |
|
231 fun get_preplay_outcome l = |
|
232 Canonical_Lbl_Tab.lookup (!preplay_tab) l |> the |> Lazy.force |
|
233 handle Option.Option => raise Fail "Sledgehammer_Preplay: preplay time table" |
|
234 |
|
235 fun set_preplay_outcome l result = |
|
236 preplay_tab := Canonical_Lbl_Tab.update (l, Lazy.value result) (!preplay_tab) |
|
237 |
|
238 val result_of_step = |
|
239 try (label_of_step #> the #> get_preplay_outcome) |
|
240 #> the_default (Played Time.zeroTime) |
|
241 |
|
242 fun overall_preplay_outcome (Proof (_, _, steps)) = |
|
243 fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime) |
|
244 in |
|
245 {get_preplay_outcome = get_preplay_outcome, |
|
246 set_preplay_outcome = set_preplay_outcome, |
|
247 preplay_quietly = preplay_quietly, |
|
248 overall_preplay_outcome = overall_preplay_outcome} |
|
249 end |
|
250 |
|
251 end; |
|