author | smolkas |
Tue, 09 Jul 2013 18:45:06 +0200 | |
changeset 52556 | c8357085217c |
parent 52454 | b528a975b256 |
child 52575 | e78ea835b5f8 |
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 |
15 |
val zero_preplay_time : preplay_time |
|
16 |
val some_preplay_time : preplay_time |
|
17 |
val add_preplay_time : preplay_time -> preplay_time -> preplay_time |
|
18 |
val string_of_preplay_time : preplay_time -> string |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
19 |
val preplay : bool -> bool -> string -> string -> Proof.context -> |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
20 |
Time.time -> isar_step -> preplay_time |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
21 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
22 |
type preplay_interface = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
23 |
{ get_time : label -> preplay_time, |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
24 |
set_time : label -> preplay_time -> unit, |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
25 |
preplay_quietly : Time.time -> isar_step -> preplay_time, |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
26 |
preplay_fail : unit -> bool, |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
27 |
overall_preplay_stats : unit -> preplay_time * bool } |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
28 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
29 |
val proof_preplay_interface : |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
30 |
bool -> Proof.context -> string -> string -> bool -> Time.time option |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
31 |
-> bool -> isar_proof -> preplay_interface |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
32 |
|
50923 | 33 |
end |
34 |
||
35 |
structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY = |
|
36 |
struct |
|
37 |
||
38 |
open Sledgehammer_Util |
|
39 |
open Sledgehammer_Proof |
|
40 |
||
50924 | 41 |
(* The boolean flag encodes whether the time is exact (false) or an lower bound |
51131 | 42 |
(true): |
43 |
(t, false) = "t ms" |
|
44 |
(t, true) = "> t ms" *) |
|
50924 | 45 |
type preplay_time = bool * Time.time |
46 |
||
51131 | 47 |
val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *) |
48 |
val some_preplay_time = (true, Time.zeroTime) (* > 0 ms *) |
|
50924 | 49 |
|
50 |
fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2)) |
|
51 |
||
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
52 |
val string_of_preplay_time = ATP_Util.string_of_ext_time |
50924 | 53 |
|
51879 | 54 |
(* preplay tracing *) |
55 |
fun preplay_trace ctxt assms concl time = |
|
56 |
let |
|
57 |
val ctxt = ctxt |> Config.put show_markup true |
|
58 |
val time = "[" ^ (string_of_preplay_time time) ^ "]" |> Pretty.str |
|
59 |
val nr_of_assms = length assms |
|
60 |
val assms = assms |> map (Display.pretty_thm ctxt) |
|
61 |
|> (fn [] => Pretty.str "" |
|
62 |
| [a] => a |
|
63 |
| assms => Pretty.enum ";" "⟦" "⟧" assms) |
|
64 |
val concl = concl |> Syntax.pretty_term ctxt |
|
65 |
val trace_list = [] |> cons concl |
|
66 |
|> nr_of_assms>0 ? cons (Pretty.str "⟹") |
|
67 |
|> cons assms |
|
68 |
|> cons time |
|
69 |
val pretty_trace = Pretty.blk(2, Pretty.breaks trace_list) |
|
70 |
in tracing (Pretty.string_of pretty_trace) end |
|
71 |
||
50923 | 72 |
(* timing *) |
73 |
fun take_time timeout tac arg = |
|
74 |
let |
|
75 |
val timing = Timing.start () |
|
76 |
in |
|
50924 | 77 |
(TimeLimit.timeLimit timeout tac arg; |
78 |
Timing.result timing |> #cpu |> pair false) |
|
79 |
handle TimeLimit.TimeOut => (true, timeout) |
|
50923 | 80 |
end |
81 |
||
82 |
(* lookup facts in context *) |
|
83 |
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
|
84 |
(names |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset
|
85 |
|>> map string_of_label |
50923 | 86 |
|> 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
|
87 |
|> 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
|
88 |
handle ERROR msg => error ("preplay error: " ^ msg) |
50923 | 89 |
|
51879 | 90 |
(* turn terms/proofs into theorems *) |
51178 | 91 |
fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
51879 | 92 |
fun thm_of_proof ctxt (Proof (Fix fixed_frees, Assume assms, steps)) = |
50923 | 93 |
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
|
94 |
val concl = (case try List.last steps of |
52454 | 95 |
SOME (Prove (_, Fix [], _, t, _, _)) => t |
51876 | 96 |
| _ => raise Fail "preplay error: malformed subproof") |
51178 | 97 |
val var_idx = maxidx_of_term concl + 1 |
98 |
fun var_of_free (x, T) = Var((x, var_idx), T) |
|
99 |
val substitutions = |
|
100 |
map (`var_of_free #> swap #> apfst Free) fixed_frees |
|
101 |
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
|
102 |
Logic.list_implies (assms |> map snd, concl) |
51178 | 103 |
|> subst_free substitutions |
104 |
|> thm_of_term ctxt |
|
105 |
end |
|
106 |
||
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
107 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
108 |
(* main function for preplaying isar_steps *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
109 |
fun preplay _ _ _ _ _ _ (Let _) = zero_preplay_time |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
110 |
| preplay debug trace type_enc lam_trans ctxt timeout |
52454 | 111 |
(Prove (_, Fix xs, _, t, subproofs, By_Metis fact_names)) = |
51178 | 112 |
let |
52453 | 113 |
val (prop, obtain) = |
114 |
(case xs of |
|
115 |
[] => (t, false) |
|
116 |
| _ => |
|
117 |
(* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis |
|
50923 | 118 |
(see ~~/src/Pure/Isar/obtain.ML) *) |
119 |
let |
|
120 |
val thesis = Term.Free ("thesis", HOLogic.boolT) |
|
121 |
val thesis_prop = thesis |> HOLogic.mk_Trueprop |
|
122 |
val frees = map Term.Free xs |
|
123 |
||
124 |
(* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) |
|
125 |
val inner_prop = |
|
126 |
fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) |
|
127 |
||
128 |
(* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) |
|
129 |
val prop = |
|
130 |
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) |
|
131 |
in |
|
52453 | 132 |
(prop, true) |
133 |
end) |
|
50923 | 134 |
val facts = |
51879 | 135 |
map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names |
50923 | 136 |
val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug |
137 |
|> obtain ? Config.put Metis_Tactic.new_skolem true |
|
138 |
val goal = |
|
51879 | 139 |
Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] prop |
50923 | 140 |
fun tac {context = ctxt, prems = _} = |
141 |
Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 |
|
51879 | 142 |
fun run_tac () = goal tac |
143 |
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
|
144 |
val preplay_time = take_time timeout run_tac () |
50923 | 145 |
in |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
146 |
(* tracing *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
147 |
(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
|
148 |
preplay_time) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
149 |
end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
150 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
151 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
152 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
153 |
(*** proof preplay interface ***) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
154 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
155 |
type preplay_interface = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
156 |
{ get_time : label -> preplay_time, |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
157 |
set_time : label -> preplay_time -> unit, |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
158 |
preplay_quietly : Time.time -> isar_step -> preplay_time, |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
159 |
preplay_fail : unit -> bool, |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
160 |
overall_preplay_stats : unit -> preplay_time * bool } |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
161 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
162 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
163 |
(* enriches context with local proof facts *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
164 |
fun enrich_context proof ctxt = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
165 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
166 |
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
|
167 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
168 |
fun enrich_with_fact l t = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
169 |
Proof_Context.put_thms false |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
170 |
(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
|
171 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
172 |
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
|
173 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
174 |
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
|
175 |
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
|
176 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
177 |
and enrich_with_step (Let _) = I |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
178 |
| 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
|
179 |
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
|
180 |
in |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
181 |
enrich_with_proof proof ctxt |
50923 | 182 |
end |
183 |
||
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
184 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
185 |
(* Given a proof, produces an imperative preplay interface with a shared state. |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
186 |
The preplay times are caluclated lazyly and cached to avoid repeated |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
187 |
calculation. |
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 |
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
|
190 |
Slegehammer_Proof.relabel_proof_canonically |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
191 |
*) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
192 |
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
|
193 |
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
|
194 |
if not do_preplay then |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
195 |
(* the dont_preplay option pretends that everything works just fine *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
196 |
{ get_time = K zero_preplay_time, |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
197 |
set_time = K (K ()), |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
198 |
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
|
199 |
preplay_fail = K false, |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
200 |
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
|
201 |
else |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
202 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
203 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
204 |
(* 60 seconds seems like a good interpreation of "no timeout" *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
205 |
val preplay_timeout = preplay_timeout |> the_default (seconds 60.0) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
206 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
207 |
(* add local proof facts to context *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
208 |
val ctxt = enrich_context proof ctxt |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
209 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
210 |
val fail = Unsynchronized.ref false |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
211 |
fun preplay_fail () = !fail |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
212 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
213 |
fun preplay' timeout step = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
214 |
(* after preplay has failed once, exact preplay times are pointless *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
215 |
if preplay_fail () then some_preplay_time |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
216 |
else preplay debug preplay_trace type_enc lam_trans ctxt timeout step |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
217 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
218 |
(* preplay steps without registering preplay_fails, treating exceptions |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
219 |
like timeouts *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
220 |
fun preplay_quietly timeout step = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
221 |
try (preplay' timeout) step |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
222 |
|> the_default (true, timeout) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
223 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
224 |
val preplay_time_tab = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
225 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
226 |
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
|
227 |
case label_of_step step of |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
228 |
NONE => tab |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
229 |
| SOME l => |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
230 |
Canonical_Lbl_Tab.update_new |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
231 |
(l, (fn () => preplay' preplay_timeout step) |> Lazy.lazy) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
232 |
tab |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
233 |
handle (exn as Canonical_Lbl_Tab.DUP _) => |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
234 |
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
|
235 |
^ PolyML.makestring exn) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
236 |
in |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
237 |
Canonical_Lbl_Tab.empty |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
238 |
|> 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
|
239 |
|> Unsynchronized.ref |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
240 |
end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
241 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
242 |
fun register_preplay_fail lazy_time = Lazy.force lazy_time |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
243 |
handle exn => |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
244 |
if Exn.is_interrupt exn orelse debug then reraise exn |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
245 |
else (fail := true; some_preplay_time) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
246 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
247 |
fun get_time lbl = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
248 |
register_preplay_fail |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
249 |
(Canonical_Lbl_Tab.lookup (!preplay_time_tab) lbl |> the) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
250 |
handle |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
251 |
Option.Option => |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
252 |
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
|
253 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
254 |
fun set_time lbl time = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
255 |
preplay_time_tab := |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
256 |
Canonical_Lbl_Tab.update (lbl, Lazy.value time) (!preplay_time_tab) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
257 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
258 |
fun total_preplay_time () = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
259 |
Canonical_Lbl_Tab.fold |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
260 |
(snd #> register_preplay_fail #> add_preplay_time) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
261 |
(!preplay_time_tab) zero_preplay_time |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
262 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
263 |
fun overall_preplay_stats () = (total_preplay_time (), preplay_fail ()) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
264 |
in |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
265 |
{ get_time = get_time, |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
266 |
set_time = set_time, |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
267 |
preplay_quietly = preplay_quietly, |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
268 |
preplay_fail = preplay_fail, |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
269 |
overall_preplay_stats = overall_preplay_stats} |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
270 |
end |
50923 | 271 |
|
272 |
end |