author | blanchet |
Mon, 03 Feb 2014 23:44:39 +0100 | |
changeset 55309 | 455a7f9924df |
parent 55307 | 59ab33f9d4de |
child 55312 | e7029ee73a97 |
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 |
|
55260 | 14 |
val compress_isar_proof : Proof.context -> real -> isar_preplay_data Unsynchronized.ref -> |
15 |
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 |
|
55212 | 26 |
val dummy_isar_step = Let (Term.dummy, Term.dummy) |
27 |
||
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
28 |
(* traverses steps in post-order and collects the steps with the given labels *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
29 |
fun collect_successors steps lbls = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
30 |
let |
55263 | 31 |
fun collect_steps _ ([], accu) = ([], accu) |
32 |
| collect_steps [] accum = accum |
|
33 |
| collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum) |
|
34 |
and collect_step (Let _) x = x |
|
55299 | 35 |
| collect_step (step as Prove (_, _, l, _, subproofs, _, _, _)) x = |
55263 | 36 |
(case collect_subproofs subproofs x of |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
37 |
([], accu) => ([], accu) |
54712 | 38 |
| accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum) |
55263 | 39 |
and collect_subproofs [] x = x |
40 |
| collect_subproofs (proof :: subproofs) x = |
|
41 |
(case collect_steps (steps_of_isar_proof proof) x of |
|
54712 | 42 |
accum as ([], _) => accum |
55263 | 43 |
| accum => collect_subproofs subproofs accum) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
44 |
in |
55263 | 45 |
(case collect_steps steps (lbls, []) of |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
46 |
([], succs) => rev succs |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55183
diff
changeset
|
47 |
| _ => raise Fail "Sledgehammer_Isar_Compress: collect_successors") |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
48 |
end |
50259 | 49 |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
50 |
(* traverses steps in reverse post-order and inserts the given updates *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
51 |
fun update_steps steps updates = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
52 |
let |
55263 | 53 |
fun update_steps [] updates = ([], updates) |
54 |
| update_steps steps [] = (steps, []) |
|
55 |
| update_steps (step :: steps) updates = update_step step (update_steps steps updates) |
|
56 |
and update_step step (steps, []) = (step :: steps, []) |
|
57 |
| update_step (step as Let _) (steps, updates) = (step :: steps, updates) |
|
55299 | 58 |
| update_step (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) |
59 |
(steps, |
|
60 |
updates as Prove (qs', xs', l', t', subproofs', facts', meths', comment') :: updates') = |
|
61 |
(if l = l' then |
|
62 |
update_subproofs subproofs' updates' |
|
63 |
|>> (fn subproofs' => Prove (qs', xs', l', t', subproofs', facts', meths', comment')) |
|
64 |
else |
|
65 |
update_subproofs subproofs updates |
|
66 |
|>> (fn subproofs => Prove (qs, xs, l, t, subproofs, facts, meths, comment))) |
|
67 |
|>> (fn step => step :: steps) |
|
55263 | 68 |
and update_subproofs [] updates = ([], updates) |
69 |
| update_subproofs steps [] = (steps, []) |
|
70 |
| update_subproofs (proof :: subproofs) updates = |
|
71 |
update_proof proof (update_subproofs subproofs updates) |
|
72 |
and update_proof proof (proofs, []) = (proof :: proofs, []) |
|
73 |
| update_proof (Proof (fix, assms, steps)) (proofs, updates) = |
|
74 |
let val (steps, updates) = update_steps steps updates in |
|
54712 | 75 |
(Proof (fix, assms, steps) :: proofs, updates) |
76 |
end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
77 |
in |
55263 | 78 |
(case update_steps steps (rev updates) of |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
79 |
(steps, []) => steps |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55183
diff
changeset
|
80 |
| _ => raise Fail "Sledgehammer_Isar_Compress: update_steps") |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
81 |
end |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
82 |
|
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
|
83 |
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
|
84 |
let |
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
|
85 |
fun is_method_hopeful l meth = |
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
|
86 |
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
|
87 |
not (Lazy.is_finished outcome) orelse |
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
|
88 |
(case Lazy.force outcome of Played _ => true | _ => false) |
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
|
89 |
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
|
90 |
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
|
91 |
inter (op =) (filter (is_method_hopeful l1) meths1) (filter (is_method_hopeful 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
|
92 |
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
|
93 |
|
55299 | 94 |
fun try_merge preplay_data (Prove (_, [], l1, _, subproofs1, (lfs1, gfs1), meths1, comment1)) |
95 |
(Prove (qs2, fix, l2, t, subproofs2, (lfs2, gfs2), meths2, comment2)) = |
|
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
|
96 |
(case merge_methods preplay_data (l1, meths1) (l2, meths2) of |
55247
4aa3e1c6222c
take intersection rather than union of methods when merging steps -- more efficient and natural
blanchet
parents:
55246
diff
changeset
|
97 |
[] => NONE |
4aa3e1c6222c
take intersection rather than union of methods when merging steps -- more efficient and natural
blanchet
parents:
55246
diff
changeset
|
98 |
| meths => |
4aa3e1c6222c
take intersection rather than union of methods when merging steps -- more efficient and natural
blanchet
parents:
55246
diff
changeset
|
99 |
let |
4aa3e1c6222c
take intersection rather than union of methods when merging steps -- more efficient and natural
blanchet
parents:
55246
diff
changeset
|
100 |
val lfs = union (op =) lfs1 (remove (op =) l1 lfs2) |
4aa3e1c6222c
take intersection rather than union of methods when merging steps -- more efficient and natural
blanchet
parents:
55246
diff
changeset
|
101 |
val gfs = union (op =) gfs1 gfs2 |
4aa3e1c6222c
take intersection rather than union of methods when merging steps -- more efficient and natural
blanchet
parents:
55246
diff
changeset
|
102 |
in |
55299 | 103 |
SOME (Prove (qs2, fix, l2, t, subproofs1 @ subproofs2, (lfs, gfs), meths, |
104 |
comment1 ^ comment2)) |
|
55247
4aa3e1c6222c
take intersection rather than union of methods when merging steps -- more efficient and natural
blanchet
parents:
55246
diff
changeset
|
105 |
end) |
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
|
106 |
| try_merge _ _ _ = NONE |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
107 |
|
53763 | 108 |
val compress_degree = 2 |
55271
e78476a99c70
better time slack, to account for ultra-quick proof methods
blanchet
parents:
55270
diff
changeset
|
109 |
val merge_timeout_slack_time = seconds 0.005 |
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55272
diff
changeset
|
110 |
val merge_timeout_slack_factor = 1.25 |
53762 | 111 |
|
55271
e78476a99c70
better time slack, to account for ultra-quick proof methods
blanchet
parents:
55270
diff
changeset
|
112 |
fun slackify_merge_timeout time = |
e78476a99c70
better time slack, to account for ultra-quick proof methods
blanchet
parents:
55270
diff
changeset
|
113 |
time_mult merge_timeout_slack_factor (Time.+ (merge_timeout_slack_time, time)) |
e78476a99c70
better time slack, to account for ultra-quick proof methods
blanchet
parents:
55270
diff
changeset
|
114 |
|
e78476a99c70
better time slack, to account for ultra-quick proof methods
blanchet
parents:
55270
diff
changeset
|
115 |
(* Precondition: The proof must be labeled canonically. *) |
55260 | 116 |
fun compress_isar_proof ctxt compress_isar preplay_data proof = |
55183
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
54828
diff
changeset
|
117 |
if compress_isar <= 1.0 then |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
118 |
proof |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
119 |
else |
54712 | 120 |
let |
121 |
val (compress_further, decrement_step_count) = |
|
122 |
let |
|
55260 | 123 |
val number_of_steps = add_isar_steps (steps_of_isar_proof proof) 0 |
55183
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
54828
diff
changeset
|
124 |
val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress_isar) |
54712 | 125 |
val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps) |
126 |
in |
|
127 |
(fn () => !delta > 0, fn () => delta := !delta - 1) |
|
128 |
end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
129 |
|
54712 | 130 |
val (get_successors, replace_successor) = |
131 |
let |
|
55299 | 132 |
fun add_refs (Prove (_, _, l, _, _, (lfs, _), _, _)) = |
133 |
fold (fn key => Canonical_Label_Tab.cons_list (key, l)) lfs |
|
134 |
| add_refs _ = I |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
135 |
|
54712 | 136 |
val tab = |
55212 | 137 |
Canonical_Label_Tab.empty |
55260 | 138 |
|> fold_isar_steps add_refs (steps_of_isar_proof proof) |
54712 | 139 |
(* "rev" should have the same effect as "sort canonical_label_ord" *) |
55212 | 140 |
|> Canonical_Label_Tab.map (K rev) |
54712 | 141 |
|> Unsynchronized.ref |
51260 | 142 |
|
55212 | 143 |
fun get_successors l = Canonical_Label_Tab.lookup_list (!tab) l |
144 |
fun set_successors l refs = tab := Canonical_Label_Tab.update (l, refs) (!tab) |
|
54712 | 145 |
fun replace_successor old new dest = |
146 |
get_successors dest |
|
147 |
|> Ord_List.remove canonical_label_ord old |
|
148 |
|> Ord_List.union canonical_label_ord new |
|
149 |
|> set_successors dest |
|
150 |
in |
|
151 |
(get_successors, replace_successor) |
|
152 |
end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
153 |
|
55243 | 154 |
(* elimination of trivial, one-step subproofs *) |
55309 | 155 |
fun elim_one_subproof time meths_outcomes qs fix l t lfs gfs (meths as meth :: _) comment subs |
156 |
nontriv_subs = |
|
54712 | 157 |
if null subs orelse not (compress_further ()) then |
55264 | 158 |
let |
159 |
val subproofs = List.revAppend (nontriv_subs, subs) |
|
55299 | 160 |
val step = Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths, comment) |
55264 | 161 |
in |
55309 | 162 |
set_preplay_outcomes_of_isar_step ctxt time preplay_data step |
163 |
((meth, Played time) :: meths_outcomes); |
|
55264 | 164 |
step |
165 |
end |
|
54712 | 166 |
else |
167 |
(case subs of |
|
168 |
(sub as Proof (_, assms, sub_steps)) :: subs => |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
169 |
(let |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
170 |
(* trivial subproofs have exactly one "Prove" step *) |
55299 | 171 |
val [Prove (_, [], l', _, [], (lfs', gfs'), meths', _)] = sub_steps |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
172 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
173 |
(* only touch proofs that can be preplayed sucessfully *) |
55272 | 174 |
val Played time' = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l' |
52556
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 |
(* merge steps *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
177 |
val subs'' = subs @ nontriv_subs |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
178 |
val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs') |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
179 |
val gfs'' = union (op =) gfs' gfs |
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
|
180 |
val meths'' as _ :: _ = merge_methods (!preplay_data) (l', meths') (l, meths) |
55299 | 181 |
val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'', comment) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
182 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
183 |
(* check if the modified step can be preplayed fast enough *) |
55271
e78476a99c70
better time slack, to account for ultra-quick proof methods
blanchet
parents:
55270
diff
changeset
|
184 |
val timeout = slackify_merge_timeout (Time.+ (time, time')) |
55309 | 185 |
val (_, Played time'') :: meths_outcomes = preplay_isar_step ctxt timeout step'' |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
186 |
in |
52626 | 187 |
decrement_step_count (); (* l' successfully eliminated! *) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
188 |
map (replace_successor l' [l]) lfs'; |
55309 | 189 |
elim_one_subproof time'' meths_outcomes qs fix l t lfs'' gfs'' meths comment subs |
190 |
nontriv_subs |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
191 |
end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
192 |
handle Bind => |
55309 | 193 |
elim_one_subproof time [] qs fix l t lfs gfs meths comment subs (sub :: nontriv_subs)) |
55264 | 194 |
| _ => raise Fail "Sledgehammer_Isar_Compress: elim_one_subproof") |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
195 |
|
55299 | 196 |
fun elim_subproofs (step as Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths, comment)) = |
54813 | 197 |
if subproofs = [] then |
198 |
step |
|
199 |
else |
|
55272 | 200 |
(case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of |
55309 | 201 |
Played time => elim_one_subproof time [] qs fix l t lfs gfs meths comment subproofs [] |
54826 | 202 |
| _ => step) |
55299 | 203 |
| elim_subproofs step = step |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
204 |
|
54712 | 205 |
fun compress_top_level steps = |
206 |
let |
|
207 |
(* (#successors, (size_of_term t, position)) *) |
|
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
208 |
fun cand_key (i, l, t_size) = (length (get_successors l), (t_size, i)) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
209 |
|
54712 | 210 |
val compression_ord = |
211 |
prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord) |
|
212 |
#> rev_order |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
213 |
|
54712 | 214 |
val cand_ord = pairself cand_key #> compression_ord |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
215 |
|
55298 | 216 |
fun pop_next_candidate [] = (NONE, []) |
217 |
| pop_next_candidate (cands as (cand :: cands')) = |
|
55212 | 218 |
let |
219 |
val best as (i, _, _) = |
|
220 |
fold (fn x => fn y => if cand_ord (x, y) = GREATER then x else y) cands' cand |
|
221 |
in (SOME best, filter_out (fn (j, _, _) => j = i) cands) end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
222 |
|
54712 | 223 |
val candidates = |
224 |
let |
|
55299 | 225 |
fun add_cand (i, Prove (_, _, l, t, _, _, _, _)) = cons (i, l, size_of_term t) |
226 |
| add_cand _ = I |
|
54712 | 227 |
in |
228 |
(steps |
|
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
229 |
|> split_last |> fst (* keep last step *) |
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
230 |
|> fold_index add_cand) [] |
54712 | 231 |
end |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
232 |
|
55264 | 233 |
fun try_eliminate (i, l, _) labels steps = |
54712 | 234 |
let |
55299 | 235 |
val ((cand as Prove (_, _, _, _, _, (lfs, _), _, _)) :: steps') = drop i steps |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
236 |
|
55264 | 237 |
val succs = collect_successors steps' labels |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
238 |
|
55307 | 239 |
(* only touch steps that can be preplayed successfully; FIXME: more generous *) |
55272 | 240 |
val Played time = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
241 |
|
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
|
242 |
val succs' = map (try_merge (!preplay_data) cand #> the) succs |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
243 |
|
55307 | 244 |
(* FIXME: more generous *) |
55269 | 245 |
val times0 = map ((fn Played time => time) o |
55272 | 246 |
forced_intermediate_preplay_outcome_of_isar_step (!preplay_data)) labels |
55264 | 247 |
val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time |
55271
e78476a99c70
better time slack, to account for ultra-quick proof methods
blanchet
parents:
55270
diff
changeset
|
248 |
val timeouts = map (curry Time.+ time_slice #> slackify_merge_timeout) times0 |
55307 | 249 |
(* FIXME: "preplay_timeout" should be an ultimate maximum *) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
250 |
|
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55272
diff
changeset
|
251 |
val meths_outcomess = map2 (preplay_isar_step ctxt) timeouts succs' |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
252 |
|
54712 | 253 |
(* ensure none of the modified successors timed out *) |
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55272
diff
changeset
|
254 |
val times = map (fn (_, Played time) :: _ => time) meths_outcomess |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
255 |
|
55298 | 256 |
val (steps_before, _ :: steps_after) = chop i steps |
54712 | 257 |
(* replace successors with their modified versions *) |
55298 | 258 |
val steps_after = update_steps steps_after succs' |
54712 | 259 |
in |
260 |
decrement_step_count (); (* candidate successfully eliminated *) |
|
55264 | 261 |
map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) times |
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55272
diff
changeset
|
262 |
succs' meths_outcomess; |
55264 | 263 |
map (replace_successor l labels) lfs; |
55243 | 264 |
(* removing the step would mess up the indices; replace with dummy step instead *) |
55298 | 265 |
steps_before @ dummy_isar_step :: steps_after |
54712 | 266 |
end |
267 |
handle Bind => steps |
|
268 |
| Match => steps |
|
269 |
| Option.Option => steps |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
270 |
|
54712 | 271 |
fun compression_loop candidates steps = |
272 |
if not (compress_further ()) then |
|
273 |
steps |
|
274 |
else |
|
55298 | 275 |
(case pop_next_candidate candidates of |
54712 | 276 |
(NONE, _) => steps (* no more candidates for elimination *) |
277 |
| (SOME (cand as (_, l, _)), candidates) => |
|
278 |
let val successors = get_successors l in |
|
279 |
if length successors > compress_degree then steps |
|
280 |
else compression_loop candidates (try_eliminate cand successors steps) |
|
281 |
end) |
|
282 |
in |
|
283 |
compression_loop candidates steps |
|
284 |
|> remove (op =) dummy_isar_step |
|
285 |
end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
286 |
|
55268 | 287 |
(* Proofs are compressed bottom-up, beginning with the innermost subproofs. On the innermost |
288 |
proof level, the proof steps have no subproofs. In the best case, these steps can be merged |
|
289 |
into just one step, resulting in a trivial subproof. Going one level up, trivial subproofs |
|
290 |
can be eliminated. In the best case, this once again leads to a proof whose proof steps do |
|
291 |
not have subproofs. Applying this approach recursively will result in a flat proof in the |
|
292 |
best cast. *) |
|
55263 | 293 |
fun compress_proof (proof as (Proof (fix, assms, steps))) = |
294 |
if compress_further () then Proof (fix, assms, compress_steps steps) else proof |
|
295 |
and compress_steps steps = |
|
54712 | 296 |
(* bottom-up: compress innermost proofs first *) |
55263 | 297 |
steps |> map (fn step => step |> compress_further () ? compress_sub_levels) |
54712 | 298 |
|> compress_further () ? compress_top_level |
55263 | 299 |
and compress_sub_levels (step as Let _) = step |
55299 | 300 |
| compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) = |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
301 |
(* compress subproofs *) |
55299 | 302 |
Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths, comment) |
54712 | 303 |
(* eliminate trivial subproofs *) |
304 |
|> compress_further () ? elim_subproofs |
|
305 |
in |
|
55263 | 306 |
compress_proof proof |
54712 | 307 |
end |
50259 | 308 |
|
54504 | 309 |
end; |