14 type label = Sledgehammer_Isar_Proof.label |
14 type label = Sledgehammer_Isar_Proof.label |
15 |
15 |
16 val trace : bool Config.T |
16 val trace : bool Config.T |
17 |
17 |
18 type isar_preplay_data = |
18 type isar_preplay_data = |
19 {reset_preplay_outcomes: isar_step -> unit, |
19 {set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit, |
20 set_preplay_outcome: label -> proof_method -> play_outcome -> unit, |
|
21 preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy, |
20 preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy, |
22 preplay_quietly: Time.time -> isar_step -> play_outcome, |
21 preplay_quietly: Time.time -> isar_step -> play_outcome, |
23 overall_preplay_outcome: isar_proof -> play_outcome} |
22 overall_preplay_outcome: isar_proof -> play_outcome} |
24 |
23 |
25 val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> bool -> Time.time -> |
24 val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> bool -> Time.time -> |
134 (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else (); |
133 (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else (); |
135 play_outcome) |
134 play_outcome) |
136 end |
135 end |
137 |
136 |
138 type isar_preplay_data = |
137 type isar_preplay_data = |
139 {reset_preplay_outcomes: isar_step -> unit, |
138 {set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit, |
140 set_preplay_outcome: label -> proof_method -> play_outcome -> unit, |
|
141 preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy, |
139 preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy, |
142 preplay_quietly: Time.time -> isar_step -> play_outcome, |
140 preplay_quietly: Time.time -> isar_step -> play_outcome, |
143 overall_preplay_outcome: isar_proof -> play_outcome} |
141 overall_preplay_outcome: isar_proof -> play_outcome} |
144 |
142 |
145 fun enrich_context_with_local_facts proof ctxt = |
143 fun enrich_context_with_local_facts proof ctxt = |
175 Precondition: The proof must be labeled canonically; cf. |
173 Precondition: The proof must be labeled canonically; cf. |
176 "Slegehammer_Isar_Proof.relabel_isar_proof_canonically". *) |
174 "Slegehammer_Isar_Proof.relabel_isar_proof_canonically". *) |
177 fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof = |
175 fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof = |
178 if not do_preplay then |
176 if not do_preplay then |
179 (* the "dont_preplay" option pretends that everything works just fine *) |
177 (* the "dont_preplay" option pretends that everything works just fine *) |
180 {reset_preplay_outcomes = K (), |
178 {set_preplay_outcomes = K (K ()), |
181 set_preplay_outcome = K (K (K ())), |
|
182 preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))), |
179 preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))), |
183 preplay_quietly = K (K (Played Time.zeroTime)), |
180 preplay_quietly = K (K (Played Time.zeroTime)), |
184 overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data |
181 overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data |
185 else |
182 else |
186 let |
183 let |
203 preplay true timeout meth step |
200 preplay true timeout meth step |
204 | preplay_quietly _ _ = Played Time.zeroTime |
201 | preplay_quietly _ _ = Played Time.zeroTime |
205 |
202 |
206 val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty |
203 val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty |
207 |
204 |
208 fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) = |
205 fun set_preplay_outcomes l meths_outcomes = |
209 preplay_tab := Canonical_Label_Tab.update (l, map (fn meth => |
206 preplay_tab := Canonical_Label_Tab.map_entry l (fold (AList.update (op =)) meths_outcomes) |
210 (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths) |
207 (!preplay_tab) |
211 (!preplay_tab) |
|
212 | reset_preplay_outcomes _ = () |
|
213 |
|
214 fun set_preplay_outcome l meth result = |
|
215 preplay_tab := Canonical_Label_Tab.map_entry l |
|
216 (AList.update (op =) (meth, Lazy.value result)) (!preplay_tab) |
|
217 |
208 |
218 fun preplay_outcome l meth = |
209 fun preplay_outcome l meth = |
219 (case Canonical_Label_Tab.lookup (!preplay_tab) l of |
210 (case Canonical_Label_Tab.lookup (!preplay_tab) l of |
220 SOME meths_outcomes => |
211 SOME meths_outcomes => |
221 (case AList.lookup (op =) meths_outcomes meth of |
212 (case AList.lookup (op =) meths_outcomes meth of |
222 SOME outcome => outcome |
213 SOME outcome => outcome |
223 | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method") |
214 | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method") |
224 | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label") |
215 | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label") |
225 |
216 |
226 val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) () |
|
227 |
|
228 fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) = |
217 fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) = |
229 Lazy.force (preplay_outcome l meth) |
218 Lazy.force (preplay_outcome l meth) |
230 | result_of_step _ = Played Time.zeroTime |
219 | result_of_step _ = Played Time.zeroTime |
231 |
220 |
232 fun overall_preplay_outcome (Proof (_, _, steps)) = |
221 fun overall_preplay_outcome (Proof (_, _, steps)) = |
233 fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime) |
222 fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime) |
|
223 |
|
224 fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) = |
|
225 preplay_tab := Canonical_Label_Tab.update (l, map (fn meth => |
|
226 (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths) |
|
227 (!preplay_tab) |
|
228 | reset_preplay_outcomes _ = () |
|
229 |
|
230 val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) () |
234 in |
231 in |
235 {reset_preplay_outcomes = reset_preplay_outcomes, |
232 {set_preplay_outcomes = set_preplay_outcomes, |
236 set_preplay_outcome = set_preplay_outcome, |
|
237 preplay_outcome = preplay_outcome, |
233 preplay_outcome = preplay_outcome, |
238 preplay_quietly = preplay_quietly, |
234 preplay_quietly = preplay_quietly, |
239 overall_preplay_outcome = overall_preplay_outcome} |
235 overall_preplay_outcome = overall_preplay_outcome} |
240 end |
236 end |
241 |
237 |