author | smolkas |
Fri, 12 Jul 2013 19:54:36 +0200 | |
changeset 52627 | ecb4a858991d |
parent 52626 | 79a4e7f8d758 |
child 52629 | d6f2a7c196f7 |
permissions | -rw-r--r-- |
51130
76d68444cd59
renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents:
51128
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_preplay.ML |
50923 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
Author: Steffen Juilf Smolka, TU Muenchen |
|
4 |
||
50924 | 5 |
Preplaying of isar proofs. |
50923 | 6 |
*) |
7 |
||
8 |
signature SLEDGEHAMMER_PREPLAY = |
|
9 |
sig |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
10 |
type isar_proof = Sledgehammer_Proof.isar_proof |
50923 | 11 |
type isar_step = Sledgehammer_Proof.isar_step |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
12 |
type label = Sledgehammer_Proof.label |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
13 |
|
50924 | 14 |
eqtype preplay_time |
52626 | 15 |
|
16 |
datatype preplay_result = |
|
17 |
PplFail of exn | |
|
18 |
PplSucc of preplay_time |
|
19 |
||
50924 | 20 |
val zero_preplay_time : preplay_time |
21 |
val some_preplay_time : preplay_time |
|
22 |
val add_preplay_time : preplay_time -> preplay_time -> preplay_time |
|
23 |
val string_of_preplay_time : preplay_time -> string |
|
52626 | 24 |
(*val preplay_raw : bool -> bool -> string -> string -> Proof.context -> |
25 |
Time.time -> isar_step -> preplay_time*) |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
26 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
27 |
type preplay_interface = |
52626 | 28 |
{ get_preplay_result : label -> preplay_result, |
29 |
set_preplay_result : label -> preplay_result -> unit, |
|
30 |
get_preplay_time : label -> preplay_time, |
|
31 |
set_preplay_time : label -> preplay_time -> unit, |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
32 |
preplay_quietly : Time.time -> isar_step -> preplay_time, |
52626 | 33 |
(* the returned flag signals a preplay failure *) |
34 |
overall_preplay_stats : isar_proof -> preplay_time * bool } |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
35 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
36 |
val proof_preplay_interface : |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
37 |
bool -> Proof.context -> string -> string -> bool -> Time.time -> bool |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
38 |
-> isar_proof -> preplay_interface |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
39 |
|
50923 | 40 |
end |
41 |
||
42 |
structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY = |
|
43 |
struct |
|
44 |
||
45 |
open Sledgehammer_Util |
|
46 |
open Sledgehammer_Proof |
|
47 |
||
50924 | 48 |
(* The boolean flag encodes whether the time is exact (false) or an lower bound |
51131 | 49 |
(true): |
50 |
(t, false) = "t ms" |
|
51 |
(t, true) = "> t ms" *) |
|
50924 | 52 |
type preplay_time = bool * Time.time |
53 |
||
52626 | 54 |
datatype preplay_result = |
55 |
PplFail of exn | |
|
56 |
PplSucc of preplay_time |
|
57 |
||
51131 | 58 |
val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *) |
59 |
val some_preplay_time = (true, Time.zeroTime) (* > 0 ms *) |
|
50924 | 60 |
|
61 |
fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2)) |
|
62 |
||
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
63 |
val string_of_preplay_time = ATP_Util.string_of_ext_time |
50924 | 64 |
|
51879 | 65 |
(* preplay tracing *) |
66 |
fun preplay_trace ctxt assms concl time = |
|
67 |
let |
|
68 |
val ctxt = ctxt |> Config.put show_markup true |
|
69 |
val time = "[" ^ (string_of_preplay_time time) ^ "]" |> Pretty.str |
|
70 |
val nr_of_assms = length assms |
|
71 |
val assms = assms |> map (Display.pretty_thm ctxt) |
|
72 |
|> (fn [] => Pretty.str "" |
|
73 |
| [a] => a |
|
74 |
| assms => Pretty.enum ";" "⟦" "⟧" assms) |
|
75 |
val concl = concl |> Syntax.pretty_term ctxt |
|
76 |
val trace_list = [] |> cons concl |
|
77 |
|> nr_of_assms>0 ? cons (Pretty.str "⟹") |
|
78 |
|> cons assms |
|
79 |
|> cons time |
|
80 |
val pretty_trace = Pretty.blk(2, Pretty.breaks trace_list) |
|
81 |
in tracing (Pretty.string_of pretty_trace) end |
|
82 |
||
50923 | 83 |
(* timing *) |
84 |
fun take_time timeout tac arg = |
|
85 |
let |
|
86 |
val timing = Timing.start () |
|
87 |
in |
|
50924 | 88 |
(TimeLimit.timeLimit timeout tac arg; |
89 |
Timing.result timing |> #cpu |> pair false) |
|
90 |
handle TimeLimit.TimeOut => (true, timeout) |
|
50923 | 91 |
end |
92 |
||
93 |
(* lookup facts in context *) |
|
94 |
fun resolve_fact_names ctxt names = |
|
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
95 |
(names |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset
|
96 |
|>> map string_of_label |
50923 | 97 |
|> op @ |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
98 |
|> maps (thms_of_name ctxt)) |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
99 |
handle ERROR msg => error ("preplay error: " ^ msg) |
50923 | 100 |
|
51879 | 101 |
(* turn terms/proofs into theorems *) |
51178 | 102 |
fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
51879 | 103 |
fun thm_of_proof ctxt (Proof (Fix fixed_frees, Assume assms, steps)) = |
50923 | 104 |
let |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
105 |
val concl = (case try List.last steps of |
52454 | 106 |
SOME (Prove (_, Fix [], _, t, _, _)) => t |
51876 | 107 |
| _ => raise Fail "preplay error: malformed subproof") |
51178 | 108 |
val var_idx = maxidx_of_term concl + 1 |
109 |
fun var_of_free (x, T) = Var((x, var_idx), T) |
|
110 |
val substitutions = |
|
111 |
map (`var_of_free #> swap #> apfst Free) fixed_frees |
|
112 |
in |
|
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
113 |
Logic.list_implies (assms |> map snd, concl) |
51178 | 114 |
|> subst_free substitutions |
115 |
|> thm_of_term ctxt |
|
116 |
end |
|
117 |
||
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
118 |
(* mapping of proof methods to tactics *) |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
119 |
fun tac_of_method method type_enc lam_trans ctxt facts = |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
120 |
case method of |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
121 |
MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
122 |
| _ => |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
123 |
Method.insert_tac facts |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
124 |
THEN' (case method of |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
125 |
SimpM => Simplifier.asm_full_simp_tac |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
126 |
| AutoM => (fn ctxt => K (Clasimp.auto_tac ctxt)) |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
127 |
| FastforceM => Clasimp.fast_force_tac |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
128 |
| ArithM => Arith_Data.arith_tac |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
129 |
| _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
130 |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
131 |
|
52626 | 132 |
(* main function for preplaying isar_steps; may throw exceptions *) |
133 |
fun preplay_raw _ _ _ _ _ _ (Let _) = zero_preplay_time |
|
134 |
| preplay_raw debug trace type_enc lam_trans ctxt timeout |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
135 |
(Prove (_, Fix xs, _, t, subproofs, By (fact_names, proof_method))) = |
51178 | 136 |
let |
52453 | 137 |
val (prop, obtain) = |
138 |
(case xs of |
|
139 |
[] => (t, false) |
|
140 |
| _ => |
|
141 |
(* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis |
|
50923 | 142 |
(see ~~/src/Pure/Isar/obtain.ML) *) |
143 |
let |
|
144 |
val thesis = Term.Free ("thesis", HOLogic.boolT) |
|
145 |
val thesis_prop = thesis |> HOLogic.mk_Trueprop |
|
146 |
val frees = map Term.Free xs |
|
147 |
||
148 |
(* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) |
|
149 |
val inner_prop = |
|
150 |
fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) |
|
151 |
||
152 |
(* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) |
|
153 |
val prop = |
|
154 |
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) |
|
155 |
in |
|
52453 | 156 |
(prop, true) |
157 |
end) |
|
50923 | 158 |
val facts = |
51879 | 159 |
map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names |
50923 | 160 |
val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug |
161 |
|> obtain ? Config.put Metis_Tactic.new_skolem true |
|
162 |
val goal = |
|
51879 | 163 |
Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] prop |
50923 | 164 |
fun tac {context = ctxt, prems = _} = |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
165 |
HEADGOAL (tac_of_method proof_method type_enc lam_trans ctxt facts) |
51879 | 166 |
fun run_tac () = goal tac |
52627 | 167 |
handle ERROR msg => error ("Preplay error: " ^ msg) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
168 |
val preplay_time = take_time timeout run_tac () |
50923 | 169 |
in |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
170 |
(* tracing *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
171 |
(if trace then preplay_trace ctxt facts prop preplay_time else () ; |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
172 |
preplay_time) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
173 |
end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
174 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
175 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
176 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
177 |
(*** proof preplay interface ***) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
178 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
179 |
type preplay_interface = |
52626 | 180 |
{ get_preplay_result : label -> preplay_result, |
181 |
set_preplay_result : label -> preplay_result -> unit, |
|
182 |
get_preplay_time : label -> preplay_time, |
|
183 |
set_preplay_time : label -> preplay_time -> unit, |
|
184 |
preplay_quietly : Time.time -> isar_step -> preplay_time, |
|
185 |
(* the returned flag signals a preplay failure *) |
|
186 |
overall_preplay_stats : isar_proof -> preplay_time * bool } |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
187 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
188 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
189 |
(* enriches context with local proof facts *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
190 |
fun enrich_context proof ctxt = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
191 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
192 |
val thy = Proof_Context.theory_of ctxt |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
193 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
194 |
fun enrich_with_fact l t = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
195 |
Proof_Context.put_thms false |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
196 |
(string_of_label l, SOME [Skip_Proof.make_thm thy t]) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
197 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
198 |
val enrich_with_assms = fold (uncurry enrich_with_fact) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
199 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
200 |
fun enrich_with_proof (Proof (_, Assume assms, isar_steps)) = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
201 |
enrich_with_assms assms #> fold enrich_with_step isar_steps |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
202 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
203 |
and enrich_with_step (Let _) = I |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
204 |
| enrich_with_step (Prove (_, _, l, t, subproofs, _)) = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
205 |
enrich_with_fact l t #> fold enrich_with_proof subproofs |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
206 |
in |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
207 |
enrich_with_proof proof ctxt |
50923 | 208 |
end |
209 |
||
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
210 |
|
52626 | 211 |
(* Given a proof, produces an imperative preplay interface with a shared table |
212 |
mapping from labels to preplay results. |
|
213 |
The preplay results are caluclated lazyly and cached to avoid repeated |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
214 |
calculation. |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
215 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
216 |
PRE CONDITION: the proof must be labeled canocially, see |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
217 |
Slegehammer_Proof.relabel_proof_canonically |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
218 |
*) |
52626 | 219 |
|
220 |
||
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
221 |
fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
222 |
preplay_timeout preplay_trace proof : preplay_interface = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
223 |
if not do_preplay then |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
224 |
(* the dont_preplay option pretends that everything works just fine *) |
52626 | 225 |
{ get_preplay_result = K (PplSucc zero_preplay_time), |
226 |
set_preplay_result = K (K ()), |
|
227 |
get_preplay_time = K zero_preplay_time, |
|
228 |
set_preplay_time = K (K ()), |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
229 |
preplay_quietly = K (K zero_preplay_time), |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
230 |
overall_preplay_stats = K (zero_preplay_time, false)} |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
231 |
else |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
232 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
233 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
234 |
(* add local proof facts to context *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
235 |
val ctxt = enrich_context proof ctxt |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
236 |
|
52627 | 237 |
fun preplay quietly timeout step = |
52626 | 238 |
preplay_raw debug preplay_trace type_enc lam_trans ctxt timeout step |
239 |
|> PplSucc |
|
240 |
handle exn => |
|
52627 | 241 |
if Exn.is_interrupt exn then |
242 |
reraise exn |
|
243 |
else if not quietly andalso debug then |
|
244 |
(warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " |
|
245 |
^ @{make_string} exn); |
|
246 |
PplFail exn) |
|
247 |
else |
|
248 |
PplFail exn |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
249 |
|
52626 | 250 |
(* preplay steps treating exceptions like timeouts *) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
251 |
fun preplay_quietly timeout step = |
52627 | 252 |
case preplay true timeout step of |
52626 | 253 |
PplSucc preplay_time => preplay_time |
254 |
| PplFail _ => (true, timeout) |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
255 |
|
52626 | 256 |
val preplay_tab = |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
257 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
258 |
fun add_step_to_tab step tab = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
259 |
case label_of_step step of |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
260 |
NONE => tab |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
261 |
| SOME l => |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
262 |
Canonical_Lbl_Tab.update_new |
52627 | 263 |
(l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
264 |
tab |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
265 |
handle Canonical_Lbl_Tab.DUP _ => |
52575 | 266 |
raise Fail "Sledgehammer_Preplay: preplay time table" |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
267 |
in |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
268 |
Canonical_Lbl_Tab.empty |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
269 |
|> fold_isar_steps add_step_to_tab (steps_of_proof proof) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
270 |
|> Unsynchronized.ref |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
271 |
end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
272 |
|
52626 | 273 |
fun get_preplay_result lbl = |
274 |
Canonical_Lbl_Tab.lookup (!preplay_tab) lbl |> the |> Lazy.force |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
275 |
handle |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
276 |
Option.Option => |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
277 |
raise Fail "Sledgehammer_Preplay: preplay time table" |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
278 |
|
52626 | 279 |
fun set_preplay_result lbl result = |
280 |
preplay_tab := |
|
281 |
Canonical_Lbl_Tab.update (lbl, Lazy.value result) (!preplay_tab) |
|
282 |
||
283 |
fun get_preplay_time lbl = |
|
284 |
case get_preplay_result lbl of |
|
285 |
PplSucc preplay_time => preplay_time |
|
286 |
| PplFail _ => some_preplay_time (* best approximation possible *) |
|
287 |
||
288 |
fun set_preplay_time lbl time = set_preplay_result lbl (PplSucc time) |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
289 |
|
52626 | 290 |
fun overall_preplay_stats (Proof(_, _, steps)) = |
291 |
let |
|
292 |
fun result_of_step step = |
|
293 |
try (label_of_step #> the #> get_preplay_result) step |
|
294 |
|> the_default (PplSucc zero_preplay_time) |
|
295 |
fun do_step step = |
|
296 |
case result_of_step step of |
|
297 |
PplSucc preplay_time => apfst (add_preplay_time preplay_time) |
|
298 |
| PplFail _ => apsnd (K true) |
|
299 |
in |
|
300 |
fold_isar_steps do_step steps (zero_preplay_time, false) |
|
301 |
end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
302 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
303 |
in |
52626 | 304 |
{ get_preplay_result = get_preplay_result, |
305 |
set_preplay_result = set_preplay_result, |
|
306 |
get_preplay_time = get_preplay_time, |
|
307 |
set_preplay_time = set_preplay_time, |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
308 |
preplay_quietly = preplay_quietly, |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
309 |
overall_preplay_stats = overall_preplay_stats} |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
310 |
end |
50923 | 311 |
|
312 |
end |