author | wenzelm |
Fri, 05 Mar 2021 16:09:42 +0100 | |
changeset 73383 | 6b104dc069de |
parent 72584 | 4ea19e5dc67e |
child 75123 | 66eb6fdfc244 |
permissions | -rw-r--r-- |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML |
54712 | 2 |
Author: Steffen Juilf Smolka, TU Muenchen |
50923 | 3 |
Author: Jasmin Blanchette, TU Muenchen |
4 |
||
54763 | 5 |
Preplaying of Isar proofs. |
50923 | 6 |
*) |
7 |
||
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
8 |
signature SLEDGEHAMMER_ISAR_PREPLAY = |
50923 | 9 |
sig |
55287 | 10 |
type play_outcome = Sledgehammer_Proof_Methods.play_outcome |
58426 | 11 |
type proof_method = Sledgehammer_Proof_Methods.proof_method |
55212 | 12 |
type isar_step = Sledgehammer_Isar_Proof.isar_step |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
13 |
type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
14 |
type label = Sledgehammer_Isar_Proof.label |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
15 |
|
55212 | 16 |
val trace : bool Config.T |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
17 |
|
55260 | 18 |
type isar_preplay_data |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
19 |
|
58079
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
57775
diff
changeset
|
20 |
val peek_at_outcome : play_outcome Lazy.lazy -> play_outcome |
55256 | 21 |
val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context |
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61268
diff
changeset
|
22 |
val preplay_isar_step_for_method : Proof.context -> thm list -> Time.time -> proof_method -> |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61268
diff
changeset
|
23 |
isar_step -> play_outcome |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61268
diff
changeset
|
24 |
val preplay_isar_step : Proof.context -> thm list -> Time.time -> proof_method list -> |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61268
diff
changeset
|
25 |
isar_step -> (proof_method * play_outcome) list |
57054 | 26 |
val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time -> |
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
27 |
isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit |
55272 | 28 |
val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome |
55266 | 29 |
val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method -> |
55260 | 30 |
play_outcome Lazy.lazy |
55266 | 31 |
val fastest_method_of_isar_step : isar_preplay_data -> label -> proof_method |
55260 | 32 |
val preplay_outcome_of_isar_proof : isar_preplay_data -> isar_proof -> play_outcome |
54504 | 33 |
end; |
50923 | 34 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
35 |
structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY = |
50923 | 36 |
struct |
37 |
||
55257 | 38 |
open ATP_Proof_Reconstruct |
50923 | 39 |
open Sledgehammer_Util |
55287 | 40 |
open Sledgehammer_Proof_Methods |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
41 |
open Sledgehammer_Isar_Proof |
50923 | 42 |
|
69593 | 43 |
val trace = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_preplay_trace\<close> (K false) |
50924 | 44 |
|
58079
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
57775
diff
changeset
|
45 |
fun peek_at_outcome outcome = |
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
57775
diff
changeset
|
46 |
if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime |
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
57775
diff
changeset
|
47 |
|
57775 | 48 |
fun par_list_map_filter_with_timeout _ _ _ _ [] = [] |
49 |
| par_list_map_filter_with_timeout get_time min_timeout timeout0 f xs = |
|
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57725
diff
changeset
|
50 |
let |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57725
diff
changeset
|
51 |
val next_timeout = Unsynchronized.ref timeout0 |
57725
a297879fe5b8
cascading timeout in parallel evaluation, to rapidly find optimum
blanchet
parents:
57054
diff
changeset
|
52 |
|
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57725
diff
changeset
|
53 |
fun apply_f x = |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57725
diff
changeset
|
54 |
let val timeout = !next_timeout in |
62826 | 55 |
if timeout <= min_timeout then |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57725
diff
changeset
|
56 |
NONE |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57725
diff
changeset
|
57 |
else |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57725
diff
changeset
|
58 |
let val y = f timeout x in |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57725
diff
changeset
|
59 |
(case get_time y of |
73383
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
72584
diff
changeset
|
60 |
SOME time => next_timeout := Time.min (time, !next_timeout) |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57725
diff
changeset
|
61 |
| _ => ()); |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57725
diff
changeset
|
62 |
SOME y |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57725
diff
changeset
|
63 |
end |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57725
diff
changeset
|
64 |
end |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57725
diff
changeset
|
65 |
in |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
69593
diff
changeset
|
66 |
chop_groups (Multithreading.max_threads ()) xs |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
69593
diff
changeset
|
67 |
|> map (map_filter I o Par_List.map apply_f) |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
69593
diff
changeset
|
68 |
|> flat |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57725
diff
changeset
|
69 |
end |
57725
a297879fe5b8
cascading timeout in parallel evaluation, to rapidly find optimum
blanchet
parents:
57054
diff
changeset
|
70 |
|
55256 | 71 |
fun enrich_context_with_local_facts proof ctxt = |
72 |
let |
|
73 |
val thy = Proof_Context.theory_of ctxt |
|
74 |
||
75 |
fun enrich_with_fact l t = |
|
76 |
Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t]) |
|
77 |
||
78 |
val enrich_with_assms = fold (uncurry enrich_with_fact) |
|
79 |
||
72582 | 80 |
fun enrich_with_proof (Proof {assumptions, steps = isar_steps, ...}) = |
81 |
enrich_with_assms assumptions #> fold enrich_with_step isar_steps |
|
72584 | 82 |
and enrich_with_step (Prove {label, goal, subproofs, ...}) = |
83 |
enrich_with_fact label goal #> fold enrich_with_proof subproofs |
|
55299 | 84 |
| enrich_with_step _ = I |
55256 | 85 |
in |
86 |
enrich_with_proof proof ctxt |
|
87 |
end |
|
88 |
||
55260 | 89 |
fun preplay_trace ctxt assmsp concl outcome = |
51879 | 90 |
let |
91 |
val ctxt = ctxt |> Config.put show_markup true |
|
55194 | 92 |
val assms = op @ assmsp |
55260 | 93 |
val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]") |
61268 | 94 |
val assms = Pretty.enum " and " "using " " shows " (map (Thm.pretty_thm ctxt) assms) |
55251 | 95 |
val concl = Syntax.pretty_term ctxt concl |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
96 |
in |
55251 | 97 |
tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl]))) |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
98 |
end |
51879 | 99 |
|
50923 | 100 |
fun take_time timeout tac arg = |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
101 |
let val timing = Timing.start () in |
62519 | 102 |
(Timeout.apply timeout tac arg; Played (#cpu (Timing.result timing))) |
103 |
handle Timeout.TIMEOUT _ => Play_Timed_Out timeout |
|
50923 | 104 |
end |
105 |
||
106 |
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
|
107 |
(names |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
108 |
|>> map string_of_label |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58426
diff
changeset
|
109 |
|> apply2 (maps (thms_of_name ctxt))) |
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
|
110 |
handle ERROR msg => error ("preplay error: " ^ msg) |
50923 | 111 |
|
72582 | 112 |
fun thm_of_proof ctxt (Proof {fixes, assumptions, steps}) = |
50923 | 113 |
let |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
114 |
val thy = Proof_Context.theory_of ctxt |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
115 |
|
54700 | 116 |
val concl = |
117 |
(case try List.last steps of |
|
72584 | 118 |
SOME (Prove {obtains = [], goal, ...}) => goal |
54700 | 119 |
| _ => raise Fail "preplay error: malformed subproof") |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
120 |
|
51178 | 121 |
val var_idx = maxidx_of_term concl + 1 |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
122 |
fun var_of_free (x, T) = Var ((x, var_idx), T) |
72582 | 123 |
val subst = map (`var_of_free #> swap #> apfst Free) fixes |
51178 | 124 |
in |
72582 | 125 |
Logic.list_implies (assumptions |> map snd, concl) |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
126 |
|> subst_free subst |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
127 |
|> Skip_Proof.make_thm thy |
51178 | 128 |
end |
129 |
||
55299 | 130 |
(* may throw exceptions *) |
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61268
diff
changeset
|
131 |
fun raw_preplay_step_for_method ctxt chained timeout meth |
72584 | 132 |
(Prove {obtains = xs, goal, subproofs, facts, ...}) = |
55258 | 133 |
let |
134 |
val goal = |
|
135 |
(case xs of |
|
72584 | 136 |
[] => goal |
55258 | 137 |
| _ => |
60549 | 138 |
(* proof obligation: !!thesis. (!!x1...xn. t ==> thesis) ==> thesis |
55258 | 139 |
(cf. "~~/src/Pure/Isar/obtain.ML") *) |
140 |
let |
|
55294 | 141 |
val frees = map Free xs |
142 |
val thesis = |
|
143 |
Free (singleton (Variable.variant_frees ctxt frees) ("thesis", HOLogic.boolT)) |
|
55258 | 144 |
val thesis_prop = HOLogic.mk_Trueprop thesis |
50923 | 145 |
|
60549 | 146 |
(* !!x1...xn. t ==> thesis *) |
72584 | 147 |
val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (goal, thesis_prop)) |
55258 | 148 |
in |
60549 | 149 |
(* !!thesis. (!!x1...xn. t ==> thesis) ==> thesis *) |
55258 | 150 |
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) |
151 |
end) |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
152 |
|
55299 | 153 |
val assmsp = |
154 |
resolve_fact_names ctxt facts |
|
55258 | 155 |
|>> append (map (thm_of_proof ctxt) subproofs) |
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61268
diff
changeset
|
156 |
|>> append chained |
55194 | 157 |
|
55258 | 158 |
fun prove () = |
159 |
Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} => |
|
57054 | 160 |
HEADGOAL (tac_of_proof_method ctxt assmsp meth)) |
55258 | 161 |
handle ERROR msg => error ("Preplay error: " ^ msg) |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
162 |
|
55258 | 163 |
val play_outcome = take_time timeout prove () |
164 |
in |
|
55329
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
165 |
if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else (); |
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
166 |
play_outcome |
55258 | 167 |
end |
168 |
||
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61268
diff
changeset
|
169 |
fun preplay_isar_step_for_method ctxt chained timeout meth = |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61268
diff
changeset
|
170 |
try (raw_preplay_step_for_method ctxt chained timeout meth) #> the_default Play_Failed |
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
171 |
|
57775 | 172 |
val min_preplay_timeout = seconds 0.002 |
173 |
||
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61268
diff
changeset
|
174 |
fun preplay_isar_step ctxt chained timeout0 hopeless step = |
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
175 |
let |
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61268
diff
changeset
|
176 |
fun preplay timeout meth = (meth, preplay_isar_step_for_method ctxt chained timeout meth step) |
57725
a297879fe5b8
cascading timeout in parallel evaluation, to rapidly find optimum
blanchet
parents:
57054
diff
changeset
|
177 |
fun get_time (_, Played time) = SOME time |
a297879fe5b8
cascading timeout in parallel evaluation, to rapidly find optimum
blanchet
parents:
57054
diff
changeset
|
178 |
| get_time _ = NONE |
55328 | 179 |
|
180 |
val meths = proof_methods_of_isar_step step |> subtract (op =) hopeless |
|
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
181 |
in |
57775 | 182 |
par_list_map_filter_with_timeout get_time min_preplay_timeout timeout0 preplay meths |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58426
diff
changeset
|
183 |
|> sort (play_outcome_ord o apply2 snd) |
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
184 |
end |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
185 |
|
55260 | 186 |
type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
187 |
|
55256 | 188 |
fun time_of_play (Played time) = time |
189 |
| time_of_play (Play_Timed_Out time) = time |
|
50923 | 190 |
|
55260 | 191 |
fun add_preplay_outcomes Play_Failed _ = Play_Failed |
192 |
| add_preplay_outcomes _ Play_Failed = Play_Failed |
|
62826 | 193 |
| add_preplay_outcomes (Played time1) (Played time2) = Played (time1 + time2) |
55260 | 194 |
| add_preplay_outcomes play1 play2 = |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58426
diff
changeset
|
195 |
Play_Timed_Out (Time.+ (apply2 time_of_play (play1, play2))) |
54827 | 196 |
|
57054 | 197 |
fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data |
72584 | 198 |
(step as Prove {label = l, proof_methods, ...}) meths_outcomes0 = |
55264 | 199 |
let |
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
200 |
fun lazy_preplay meth = |
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61268
diff
changeset
|
201 |
Lazy.lazy (fn () => preplay_isar_step_for_method ctxt [] timeout meth step) |
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
202 |
val meths_outcomes = meths_outcomes0 |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
203 |
|> map (apsnd Lazy.value) |
72584 | 204 |
|> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) proof_methods |
55264 | 205 |
in |
55308
dc68f6fb88d2
properly overwrite replay data from one compression iteration to another
blanchet
parents:
55299
diff
changeset
|
206 |
preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes []) |
dc68f6fb88d2
properly overwrite replay data from one compression iteration to another
blanchet
parents:
55299
diff
changeset
|
207 |
(!preplay_data) |
55264 | 208 |
end |
57054 | 209 |
| set_preplay_outcomes_of_isar_step _ _ _ _ _ = () |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
210 |
|
55275 | 211 |
fun get_best_method_outcome force = |
57725
a297879fe5b8
cascading timeout in parallel evaluation, to rapidly find optimum
blanchet
parents:
57054
diff
changeset
|
212 |
tap (List.app (K () o Lazy.future Future.default_params o snd)) (* could be parallelized *) |
55275 | 213 |
#> map (apsnd force) |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58426
diff
changeset
|
214 |
#> sort (play_outcome_ord o apply2 snd) |
55275 | 215 |
#> hd |
216 |
||
55272 | 217 |
fun forced_intermediate_preplay_outcome_of_isar_step preplay_data l = |
55269 | 218 |
let |
55309 | 219 |
val meths_outcomes as (_, outcome1) :: _ = the (Canonical_Label_Tab.lookup preplay_data l) |
55269 | 220 |
in |
55275 | 221 |
if forall (not o Lazy.is_finished o snd) meths_outcomes then |
222 |
(case Lazy.force outcome1 of |
|
223 |
outcome as Played _ => outcome |
|
224 |
| _ => snd (get_best_method_outcome Lazy.force meths_outcomes)) |
|
225 |
else |
|
56093 | 226 |
let val outcome = snd (get_best_method_outcome peek_at_outcome meths_outcomes) in |
227 |
if outcome = Play_Timed_Out Time.zeroTime then |
|
228 |
snd (get_best_method_outcome Lazy.force meths_outcomes) |
|
229 |
else |
|
230 |
outcome |
|
231 |
end |
|
55269 | 232 |
end |
233 |
||
55268 | 234 |
fun preplay_outcome_of_isar_step_for_method preplay_data l = |
55329
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
235 |
AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l)) |
56093 | 236 |
#> the_default (Lazy.value (Play_Timed_Out Time.zeroTime)) |
55252 | 237 |
|
55268 | 238 |
fun fastest_method_of_isar_step preplay_data = |
55269 | 239 |
the o Canonical_Label_Tab.lookup preplay_data |
55275 | 240 |
#> get_best_method_outcome Lazy.force |
241 |
#> fst |
|
55266 | 242 |
|
72584 | 243 |
fun forced_outcome_of_step preplay_data (Prove {label, proof_methods, ...}) = |
244 |
Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data label (hd proof_methods)) |
|
55260 | 245 |
| forced_outcome_of_step _ _ = Played Time.zeroTime |
55252 | 246 |
|
72582 | 247 |
fun preplay_outcome_of_isar_proof preplay_data (Proof {steps, ...}) = |
55260 | 248 |
fold_isar_steps (add_preplay_outcomes o forced_outcome_of_step preplay_data) steps |
249 |
(Played Time.zeroTime) |
|
50923 | 250 |
|
54504 | 251 |
end; |