author | desharna |
Fri, 17 Dec 2021 09:57:22 +0100 | |
changeset 74950 | b350a1f2115d |
parent 73383 | 6b104dc069de |
permissions | -rw-r--r-- |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55183
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML |
54813 | 2 |
Author: Steffen Juilf Smolka, TU Muenchen |
50263 | 3 |
Author: Jasmin Blanchette, TU Muenchen |
4 |
||
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55183
diff
changeset
|
5 |
Compression of Isar proofs by merging steps. |
54712 | 6 |
Only proof steps using the same proof method are merged. |
50263 | 7 |
*) |
8 |
||
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55183
diff
changeset
|
9 |
signature SLEDGEHAMMER_ISAR_COMPRESS = |
50259 | 10 |
sig |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55183
diff
changeset
|
11 |
type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
55213 | 12 |
type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
13 |
|
57054 | 14 |
val compress_isar_proof : Proof.context -> real -> Time.time -> |
55329
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
15 |
isar_preplay_data Unsynchronized.ref -> isar_proof -> isar_proof |
54504 | 16 |
end; |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
17 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55183
diff
changeset
|
18 |
structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS = |
50259 | 19 |
struct |
20 |
||
50265 | 21 |
open Sledgehammer_Util |
55287 | 22 |
open Sledgehammer_Proof_Methods |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55183
diff
changeset
|
23 |
open Sledgehammer_Isar_Proof |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55183
diff
changeset
|
24 |
open Sledgehammer_Isar_Preplay |
50259 | 25 |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
26 |
fun collect_successors steps lbls = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
27 |
let |
55329
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
28 |
fun collect_steps _ (accum as ([], _)) = accum |
55263 | 29 |
| collect_steps [] accum = accum |
30 |
| collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum) |
|
72584 | 31 |
and collect_step (step as Prove {label, subproofs, ...}) x = |
55263 | 32 |
(case collect_subproofs subproofs x of |
72584 | 33 |
accum as ([], _) => accum |
34 |
| accum as (l' :: lbls', accu) => if label = l' then (lbls', step :: accu) else accum) |
|
55329
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
35 |
| collect_step _ accum = accum |
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
36 |
and collect_subproofs [] accum = accum |
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
37 |
| collect_subproofs (proof :: subproofs) accum = |
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
38 |
(case collect_steps (steps_of_isar_proof proof) accum of |
54712 | 39 |
accum as ([], _) => accum |
55263 | 40 |
| accum => collect_subproofs subproofs accum) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
41 |
in |
55313 | 42 |
rev (snd (collect_steps steps (lbls, []))) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
43 |
end |
50259 | 44 |
|
55332
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
45 |
fun update_steps updates steps = |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
46 |
let |
55263 | 47 |
fun update_steps [] updates = ([], updates) |
48 |
| update_steps steps [] = (steps, []) |
|
49 |
| update_steps (step :: steps) updates = update_step step (update_steps steps updates) |
|
50 |
and update_step step (steps, []) = (step :: steps, []) |
|
72584 | 51 |
| update_step (Prove {qualifiers = qs, obtains = xs, label = l, goal = t, subproofs, facts, |
52 |
proof_methods = meths, comment}) (steps, updates as Prove {qualifiers = qs', |
|
53 |
obtains = xs', label = l', goal = t', subproofs = subproofs', facts = facts', |
|
54 |
proof_methods = meths', comment = comment'} :: updates') = |
|
55299 | 55 |
(if l = l' then |
56 |
update_subproofs subproofs' updates' |
|
72584 | 57 |
|>> (fn subproofs'' => Prove { |
58 |
qualifiers = qs', |
|
59 |
obtains = xs', |
|
60 |
label = l', |
|
61 |
goal = t', |
|
62 |
subproofs = subproofs'', |
|
63 |
facts = facts', |
|
64 |
proof_methods = meths', |
|
65 |
comment = comment'}) |
|
55299 | 66 |
else |
67 |
update_subproofs subproofs updates |
|
72584 | 68 |
|>> (fn subproofs' => Prove { |
69 |
qualifiers = qs, |
|
70 |
obtains = xs, |
|
71 |
label = l, |
|
72 |
goal = t, |
|
73 |
subproofs = subproofs', |
|
74 |
facts = facts, |
|
75 |
proof_methods = meths, |
|
76 |
comment = comment})) |
|
55299 | 77 |
|>> (fn step => step :: steps) |
55329
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
78 |
| update_step step (steps, updates) = (step :: steps, updates) |
55263 | 79 |
and update_subproofs [] updates = ([], updates) |
80 |
| update_subproofs steps [] = (steps, []) |
|
81 |
| update_subproofs (proof :: subproofs) updates = |
|
82 |
update_proof proof (update_subproofs subproofs updates) |
|
83 |
and update_proof proof (proofs, []) = (proof :: proofs, []) |
|
72583 | 84 |
| update_proof (proof as Proof {steps, ...}) (proofs, updates) = |
57699 | 85 |
let val (steps', updates') = update_steps steps updates in |
72583 | 86 |
(isar_proof_with_steps proof steps' :: proofs, updates') |
54712 | 87 |
end |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
88 |
in |
55313 | 89 |
fst (update_steps steps (rev updates)) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
90 |
end |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
91 |
|
55283
b90c06d54d38
when merging, don't try methods that failed or timed out for either of the steps for the combined step
blanchet
parents:
55280
diff
changeset
|
92 |
fun merge_methods preplay_data (l1, meths1) (l2, meths2) = |
b90c06d54d38
when merging, don't try methods that failed or timed out for either of the steps for the combined step
blanchet
parents:
55280
diff
changeset
|
93 |
let |
55328 | 94 |
fun is_hopeful l meth = |
55283
b90c06d54d38
when merging, don't try methods that failed or timed out for either of the steps for the combined step
blanchet
parents:
55280
diff
changeset
|
95 |
let val outcome = preplay_outcome_of_isar_step_for_method preplay_data l meth in |
b90c06d54d38
when merging, don't try methods that failed or timed out for either of the steps for the combined step
blanchet
parents:
55280
diff
changeset
|
96 |
not (Lazy.is_finished outcome) orelse |
55328 | 97 |
(case Lazy.force outcome of Played _ => true | Play_Timed_Out _ => true | _ => false) |
55283
b90c06d54d38
when merging, don't try methods that failed or timed out for either of the steps for the combined step
blanchet
parents:
55280
diff
changeset
|
98 |
end |
55328 | 99 |
|
100 |
val (hopeful, hopeless) = |
|
101 |
meths2 @ subtract (op =) meths2 meths1 |
|
102 |
|> List.partition (is_hopeful l1 andf is_hopeful l2) |
|
55283
b90c06d54d38
when merging, don't try methods that failed or timed out for either of the steps for the combined step
blanchet
parents:
55280
diff
changeset
|
103 |
in |
55328 | 104 |
(hopeful @ hopeless, hopeless) |
55283
b90c06d54d38
when merging, don't try methods that failed or timed out for either of the steps for the combined step
blanchet
parents:
55280
diff
changeset
|
105 |
end |
b90c06d54d38
when merging, don't try methods that failed or timed out for either of the steps for the combined step
blanchet
parents:
55280
diff
changeset
|
106 |
|
72584 | 107 |
fun merge_steps preplay_data |
108 |
(Prove (p1 as {qualifiers = [], label = l1, goal = _, facts = (lfs1, gfs1), ...})) |
|
109 |
(Prove (p2 as {qualifiers = qs2, label = l2, goal = t, facts = (lfs2, gfs2), ...})) = |
|
55332
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
110 |
let |
72584 | 111 |
val (meths, hopeless) = |
112 |
merge_methods preplay_data (l1, #proof_methods p1) (l2, #proof_methods p2) |
|
55332
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
113 |
val lfs = union (op =) lfs1 (remove (op =) l1 lfs2) |
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
114 |
val gfs = union (op =) gfs1 gfs2 |
72584 | 115 |
val prove = Prove { |
116 |
qualifiers = qs2, |
|
117 |
obtains = inter (op =) (Term.add_frees t []) (#obtains p1 @ #obtains p2), |
|
118 |
label = l2, |
|
119 |
goal = t, |
|
120 |
subproofs = #subproofs p1 @ #subproofs p2, |
|
121 |
facts = sort_facts (lfs, gfs), |
|
122 |
proof_methods = meths, |
|
123 |
comment = #comment p1 ^ #comment p2} |
|
55332
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
124 |
in |
72584 | 125 |
(prove, hopeless) |
55332
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
126 |
end |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
127 |
|
57768
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57766
diff
changeset
|
128 |
val merge_slack_time = seconds 0.01 |
55329
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
129 |
val merge_slack_factor = 1.5 |
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
130 |
|
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
131 |
fun adjust_merge_timeout max time = |
73383
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
72584
diff
changeset
|
132 |
let val timeout = Time.scale merge_slack_factor (merge_slack_time + time) in |
62826 | 133 |
if max < timeout then max else timeout |
55329
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
134 |
end |
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
135 |
|
53763 | 136 |
val compress_degree = 2 |
55271
e78476a99c70
better time slack, to account for ultra-quick proof methods
blanchet
parents:
55270
diff
changeset
|
137 |
|
e78476a99c70
better time slack, to account for ultra-quick proof methods
blanchet
parents:
55270
diff
changeset
|
138 |
(* Precondition: The proof must be labeled canonically. *) |
57245 | 139 |
fun compress_isar_proof ctxt compress preplay_timeout preplay_data proof = |
140 |
if compress <= 1.0 then |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
141 |
proof |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
142 |
else |
54712 | 143 |
let |
144 |
val (compress_further, decrement_step_count) = |
|
145 |
let |
|
55260 | 146 |
val number_of_steps = add_isar_steps (steps_of_isar_proof proof) 0 |
57768
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57766
diff
changeset
|
147 |
val target_number_of_steps = Real.ceil (Real.fromInt number_of_steps / compress) |
54712 | 148 |
val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps) |
149 |
in |
|
150 |
(fn () => !delta > 0, fn () => delta := !delta - 1) |
|
151 |
end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
152 |
|
54712 | 153 |
val (get_successors, replace_successor) = |
154 |
let |
|
72584 | 155 |
fun add_refs (Prove {label, facts = (lfs, _), ...}) = |
156 |
fold (fn key => Canonical_Label_Tab.cons_list (key, label)) lfs |
|
55299 | 157 |
| add_refs _ = I |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
158 |
|
54712 | 159 |
val tab = |
55212 | 160 |
Canonical_Label_Tab.empty |
55260 | 161 |
|> fold_isar_steps add_refs (steps_of_isar_proof proof) |
54712 | 162 |
(* "rev" should have the same effect as "sort canonical_label_ord" *) |
55212 | 163 |
|> Canonical_Label_Tab.map (K rev) |
54712 | 164 |
|> Unsynchronized.ref |
51260 | 165 |
|
55212 | 166 |
fun get_successors l = Canonical_Label_Tab.lookup_list (!tab) l |
167 |
fun set_successors l refs = tab := Canonical_Label_Tab.update (l, refs) (!tab) |
|
54712 | 168 |
fun replace_successor old new dest = |
169 |
get_successors dest |
|
170 |
|> Ord_List.remove canonical_label_ord old |
|
171 |
|> Ord_List.union canonical_label_ord new |
|
172 |
|> set_successors dest |
|
173 |
in |
|
174 |
(get_successors, replace_successor) |
|
175 |
end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
176 |
|
55333
fa079fd40db8
more exception cleanup + more liberal compressions of steps that timed out
blanchet
parents:
55332
diff
changeset
|
177 |
fun reference_time l = |
fa079fd40db8
more exception cleanup + more liberal compressions of steps that timed out
blanchet
parents:
55332
diff
changeset
|
178 |
(case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of |
fa079fd40db8
more exception cleanup + more liberal compressions of steps that timed out
blanchet
parents:
55332
diff
changeset
|
179 |
Played time => time |
fa079fd40db8
more exception cleanup + more liberal compressions of steps that timed out
blanchet
parents:
55332
diff
changeset
|
180 |
| _ => preplay_timeout) |
fa079fd40db8
more exception cleanup + more liberal compressions of steps that timed out
blanchet
parents:
55332
diff
changeset
|
181 |
|
55243 | 182 |
(* elimination of trivial, one-step subproofs *) |
72584 | 183 |
fun elim_one_subproof time (step as Prove {qualifiers, obtains, label, goal, |
184 |
facts = (lfs, gfs), proof_methods, comment, ...}) subs |
|
55309 | 185 |
nontriv_subs = |
54712 | 186 |
if null subs orelse not (compress_further ()) then |
72584 | 187 |
Prove { |
188 |
qualifiers = qualifiers, |
|
189 |
obtains = obtains, |
|
190 |
label = label, |
|
191 |
goal = goal, |
|
192 |
subproofs = List.revAppend (nontriv_subs, subs), |
|
193 |
facts = (lfs, gfs), |
|
194 |
proof_methods = proof_methods, |
|
195 |
comment = comment} |
|
54712 | 196 |
else |
197 |
(case subs of |
|
72582 | 198 |
(sub as Proof {assumptions, |
72584 | 199 |
steps = [Prove {label = label', subproofs = [], facts = (lfs', gfs'), |
200 |
proof_methods = proof_methods', ...}], ...}) :: subs => |
|
55333
fa079fd40db8
more exception cleanup + more liberal compressions of steps that timed out
blanchet
parents:
55332
diff
changeset
|
201 |
let |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
202 |
(* merge steps *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
203 |
val subs'' = subs @ nontriv_subs |
72582 | 204 |
val lfs'' = union (op =) lfs (subtract (op =) (map fst assumptions) lfs') |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
205 |
val gfs'' = union (op =) gfs' gfs |
72584 | 206 |
val (proof_methods'' as _ :: _, hopeless) = |
207 |
merge_methods (!preplay_data) (label', proof_methods') (label, proof_methods) |
|
208 |
val step'' = Prove { |
|
209 |
qualifiers = qualifiers, |
|
210 |
obtains = obtains, |
|
211 |
label = label, |
|
212 |
goal = goal, |
|
213 |
subproofs = subs'', |
|
214 |
facts = (lfs'', gfs''), |
|
215 |
proof_methods = proof_methods'', |
|
216 |
comment = comment} |
|
52556
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 |
(* check if the modified step can be preplayed fast enough *) |
72584 | 219 |
val timeout = adjust_merge_timeout preplay_timeout (time + reference_time label') |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
220 |
in |
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61666
diff
changeset
|
221 |
(case preplay_isar_step ctxt [] timeout hopeless step'' of |
55333
fa079fd40db8
more exception cleanup + more liberal compressions of steps that timed out
blanchet
parents:
55332
diff
changeset
|
222 |
meths_outcomes as (_, Played time'') :: _ => |
57725
a297879fe5b8
cascading timeout in parallel evaluation, to rapidly find optimum
blanchet
parents:
57699
diff
changeset
|
223 |
(* "l'" successfully eliminated *) |
55333
fa079fd40db8
more exception cleanup + more liberal compressions of steps that timed out
blanchet
parents:
55332
diff
changeset
|
224 |
(decrement_step_count (); |
57054 | 225 |
set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes; |
72584 | 226 |
map (replace_successor label' [label]) lfs'; |
55333
fa079fd40db8
more exception cleanup + more liberal compressions of steps that timed out
blanchet
parents:
55332
diff
changeset
|
227 |
elim_one_subproof time'' step'' subs nontriv_subs) |
fa079fd40db8
more exception cleanup + more liberal compressions of steps that timed out
blanchet
parents:
55332
diff
changeset
|
228 |
| _ => elim_one_subproof time step subs (sub :: nontriv_subs)) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
229 |
end |
55333
fa079fd40db8
more exception cleanup + more liberal compressions of steps that timed out
blanchet
parents:
55332
diff
changeset
|
230 |
| sub :: subs => elim_one_subproof time step subs (sub :: nontriv_subs)) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
231 |
|
72584 | 232 |
fun elim_subproofs (step as Prove {label, subproofs, ...}) = |
55333
fa079fd40db8
more exception cleanup + more liberal compressions of steps that timed out
blanchet
parents:
55332
diff
changeset
|
233 |
if exists (null o tl o steps_of_isar_proof) subproofs then |
72584 | 234 |
elim_one_subproof (reference_time label) step subproofs [] |
55333
fa079fd40db8
more exception cleanup + more liberal compressions of steps that timed out
blanchet
parents:
55332
diff
changeset
|
235 |
else |
fa079fd40db8
more exception cleanup + more liberal compressions of steps that timed out
blanchet
parents:
55332
diff
changeset
|
236 |
step |
55299 | 237 |
| elim_subproofs step = step |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
238 |
|
54712 | 239 |
fun compress_top_level steps = |
240 |
let |
|
57764 | 241 |
val cand_key = apfst (length o get_successors) |
242 |
val cand_ord = |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58634
diff
changeset
|
243 |
prod_ord int_ord (prod_ord (int_ord o swap) (int_ord o swap)) o apply2 cand_key |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
244 |
|
55298 | 245 |
fun pop_next_candidate [] = (NONE, []) |
246 |
| pop_next_candidate (cands as (cand :: cands')) = |
|
67560 | 247 |
fold (fn x => fn y => if is_less (cand_ord (x, y)) then x else y) cands' cand |
55325 | 248 |
|> (fn best => (SOME best, remove (op =) best cands)) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
249 |
|
55332
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
250 |
fun try_eliminate i l labels steps = |
54712 | 251 |
let |
72584 | 252 |
val (steps_before, (cand as Prove {facts = (lfs, _), ...}) :: steps_after) = |
55332
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
253 |
chop i steps |
55330
547d23e2abf7
corrected wrong 'meth :: _' pattern maching + tuned code
blanchet
parents:
55329
diff
changeset
|
254 |
val succs = collect_successors steps_after labels |
55332
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
255 |
val (succs', hopelesses) = split_list (map (merge_steps (!preplay_data) cand) succs) |
54712 | 256 |
in |
55332
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
257 |
(case try (map ((fn Played time => time) o |
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
258 |
forced_intermediate_preplay_outcome_of_isar_step (!preplay_data))) labels of |
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
259 |
NONE => steps |
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
260 |
| SOME times0 => |
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
261 |
let |
61612
40859aa6d10c
generalized so that is also works for veriT proofs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59058
diff
changeset
|
262 |
val n = length labels |
62826 | 263 |
val total_time = Library.foldl (op +) (reference_time l, times0) |
61612
40859aa6d10c
generalized so that is also works for veriT proofs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59058
diff
changeset
|
264 |
val timeout = adjust_merge_timeout preplay_timeout |
40859aa6d10c
generalized so that is also works for veriT proofs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59058
diff
changeset
|
265 |
(Time.fromReal (Time.toReal total_time / Real.fromInt n)) |
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61666
diff
changeset
|
266 |
val meths_outcomess = |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61666
diff
changeset
|
267 |
@{map 2} (preplay_isar_step ctxt [] timeout) hopelesses succs' |
55332
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
268 |
in |
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
269 |
(case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of |
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
270 |
NONE => steps |
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
271 |
| SOME times => |
57725
a297879fe5b8
cascading timeout in parallel evaluation, to rapidly find optimum
blanchet
parents:
57699
diff
changeset
|
272 |
(* "l" successfully eliminated *) |
55332
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
273 |
(decrement_step_count (); |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
57776
diff
changeset
|
274 |
@{map 3} (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) |
55332
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
275 |
times succs' meths_outcomess; |
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
276 |
map (replace_successor l labels) lfs; |
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
277 |
steps_before @ update_steps succs' steps_after)) |
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
278 |
end) |
54712 | 279 |
end |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
280 |
|
54712 | 281 |
fun compression_loop candidates steps = |
282 |
if not (compress_further ()) then |
|
283 |
steps |
|
284 |
else |
|
55298 | 285 |
(case pop_next_candidate candidates of |
54712 | 286 |
(NONE, _) => steps (* no more candidates for elimination *) |
57766 | 287 |
| (SOME (l, (num_xs, _)), candidates') => |
55332
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
288 |
(case find_index (curry (op =) (SOME l) o label_of_isar_step) steps of |
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
289 |
~1 => steps |
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
290 |
| i => |
57766 | 291 |
let |
292 |
val successors = get_successors l |
|
293 |
val num_successors = length successors |
|
294 |
in |
|
295 |
(* Careful with "obtain", so we don't "obtain" twice the same variable after a |
|
296 |
merge. *) |
|
297 |
if num_successors > (if num_xs > 0 then 1 else compress_degree) then |
|
57162 | 298 |
steps |
299 |
else |
|
300 |
steps |
|
301 |
|> not (null successors) ? try_eliminate i l successors |
|
302 |
|> compression_loop candidates' |
|
55332
803a7400cc58
tuned code to avoid noncanonical (and risky) exception handling
blanchet
parents:
55331
diff
changeset
|
303 |
end)) |
55331 | 304 |
|
72584 | 305 |
fun add_cand (Prove {obtains, label, goal, ...}) = |
306 |
cons (label, (length obtains, size_of_term goal)) |
|
55331 | 307 |
| add_cand _ = I |
308 |
||
309 |
(* the very last step is not a candidate *) |
|
310 |
val candidates = fold add_cand (fst (split_last steps)) [] |
|
54712 | 311 |
in |
312 |
compression_loop candidates steps |
|
313 |
end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
314 |
|
55268 | 315 |
(* Proofs are compressed bottom-up, beginning with the innermost subproofs. On the innermost |
316 |
proof level, the proof steps have no subproofs. In the best case, these steps can be merged |
|
317 |
into just one step, resulting in a trivial subproof. Going one level up, trivial subproofs |
|
318 |
can be eliminated. In the best case, this once again leads to a proof whose proof steps do |
|
319 |
not have subproofs. Applying this approach recursively will result in a flat proof in the |
|
320 |
best cast. *) |
|
72583 | 321 |
fun compress_proof (proof as (Proof {steps, ...})) = |
72582 | 322 |
if compress_further () then |
72583 | 323 |
isar_proof_with_steps proof (compress_steps steps) |
72582 | 324 |
else |
325 |
proof |
|
55263 | 326 |
and compress_steps steps = |
54712 | 327 |
(* bottom-up: compress innermost proofs first *) |
57768
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57766
diff
changeset
|
328 |
steps |
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57766
diff
changeset
|
329 |
|> map (fn step => step |> compress_further () ? compress_sub_levels) |
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57766
diff
changeset
|
330 |
|> compress_further () ? compress_top_level |
72584 | 331 |
and compress_sub_levels (Prove {qualifiers, obtains, label, goal, subproofs, facts, |
332 |
proof_methods, comment}) = |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
333 |
(* compress subproofs *) |
72584 | 334 |
Prove { |
335 |
qualifiers = qualifiers, |
|
336 |
obtains = obtains, |
|
337 |
label = label, |
|
338 |
goal = goal, |
|
339 |
subproofs = map compress_proof subproofs, |
|
340 |
facts = facts, |
|
341 |
proof_methods = proof_methods, |
|
342 |
comment = comment} |
|
54712 | 343 |
(* eliminate trivial subproofs *) |
344 |
|> compress_further () ? elim_subproofs |
|
55329
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55328
diff
changeset
|
345 |
| compress_sub_levels step = step |
54712 | 346 |
in |
55263 | 347 |
compress_proof proof |
54712 | 348 |
end |
50259 | 349 |
|
54504 | 350 |
end; |