author | blanchet |
Thu, 19 Dec 2013 18:39:54 +0100 | |
changeset 54827 | 14e2c7616209 |
parent 54826 | 79745ba60a5a |
child 54828 | b2271ad695db |
permissions | -rw-r--r-- |
51130
76d68444cd59
renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents:
51128
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_compress.ML |
54813 | 2 |
Author: Steffen Juilf Smolka, TU Muenchen |
50263 | 3 |
Author: Jasmin Blanchette, TU Muenchen |
4 |
||
52633 | 5 |
Compression of isar proofs by merging steps. |
54712 | 6 |
Only proof steps using the same proof method are merged. |
50263 | 7 |
*) |
8 |
||
51130
76d68444cd59
renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents:
51128
diff
changeset
|
9 |
signature SLEDGEHAMMER_COMPRESS = |
50259 | 10 |
sig |
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
|
11 |
type isar_proof = Sledgehammer_Proof.isar_proof |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
12 |
type preplay_interface = Sledgehammer_Preplay.preplay_interface |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
13 |
|
53763 | 14 |
val compress_proof : real -> preplay_interface -> isar_proof -> isar_proof |
54504 | 15 |
end; |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
16 |
|
51130
76d68444cd59
renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents:
51128
diff
changeset
|
17 |
structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS = |
50259 | 18 |
struct |
19 |
||
50265 | 20 |
open Sledgehammer_Util |
50264
a9ec48b98734
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
smolkas
parents:
50263
diff
changeset
|
21 |
open Sledgehammer_Proof |
50923 | 22 |
open Sledgehammer_Preplay |
50259 | 23 |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
24 |
(* 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
|
25 |
fun collect_successors steps lbls = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
26 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
27 |
fun do_steps _ ([], accu) = ([], accu) |
54712 | 28 |
| do_steps [] accum = accum |
29 |
| do_steps (step :: steps) accum = do_steps steps (do_step step accum) |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
30 |
and do_step (Let _) x = x |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
31 |
| do_step (step as Prove (_, _, l, _, subproofs, _)) x = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
32 |
(case do_subproofs subproofs x of |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
33 |
([], accu) => ([], accu) |
54712 | 34 |
| accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
35 |
and do_subproofs [] x = x |
54712 | 36 |
| do_subproofs (proof :: subproofs) x = |
37 |
(case do_steps (steps_of_proof proof) x of |
|
38 |
accum as ([], _) => accum |
|
39 |
| accum => do_subproofs subproofs accum) |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
40 |
in |
54712 | 41 |
(case do_steps steps (lbls, []) of |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
42 |
([], succs) => rev succs |
54712 | 43 |
| _ => raise Fail "Sledgehammer_Compress: collect_successors") |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
44 |
end |
50259 | 45 |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
46 |
(* 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
|
47 |
fun update_steps steps updates = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
48 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
49 |
fun do_steps [] updates = ([], updates) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
50 |
| do_steps steps [] = (steps, []) |
54712 | 51 |
| do_steps (step :: steps) updates = do_step step (do_steps steps updates) |
52 |
and do_step step (steps, []) = (step :: steps, []) |
|
53 |
| do_step (step as Let _) (steps, updates) = (step :: steps, updates) |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
54 |
| do_step (Prove (qs, xs, l, t, subproofs, by)) |
54712 | 55 |
(steps, updates as Prove (qs', xs', l', t', subproofs', by') :: updates') = |
56 |
let |
|
57 |
val (subproofs, updates) = |
|
58 |
if l = l' then do_subproofs subproofs' updates' else do_subproofs subproofs updates |
|
59 |
in |
|
60 |
if l = l' then (Prove (qs', xs', l', t', subproofs, by') :: steps, updates) |
|
61 |
else (Prove (qs, xs, l, t, subproofs, by) :: steps, updates) |
|
62 |
end |
|
63 |
| do_step _ _ = raise Fail "Sledgehammer_Compress: update_steps (invalid update)" |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
64 |
and do_subproofs [] updates = ([], updates) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
65 |
| do_subproofs steps [] = (steps, []) |
54712 | 66 |
| do_subproofs (proof :: subproofs) updates = |
67 |
do_proof proof (do_subproofs subproofs updates) |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
68 |
and do_proof proof (proofs, []) = (proof :: proofs, []) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
69 |
| do_proof (Proof (fix, assms, steps)) (proofs, updates) = |
54712 | 70 |
let val (steps, updates) = do_steps steps updates in |
71 |
(Proof (fix, assms, steps) :: proofs, updates) |
|
72 |
end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
73 |
in |
54712 | 74 |
(case do_steps steps (rev updates) of |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
75 |
(steps, []) => steps |
54712 | 76 |
| _ => raise Fail "Sledgehammer_Compress: update_steps") |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
77 |
end |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
78 |
|
54752 | 79 |
(* Tries merging the first step into the second step. Arbitrarily picks the second step's method. *) |
80 |
fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), _))) |
|
54712 | 81 |
(Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meth2))) = |
54752 | 82 |
let |
83 |
val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1 |
|
84 |
val gfs = union (op =) gfs1 gfs2 |
|
85 |
in |
|
86 |
SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meth2))) |
|
87 |
end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
88 |
| try_merge _ _ = NONE |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
89 |
|
53763 | 90 |
val compress_degree = 2 |
53762 | 91 |
val merge_timeout_slack = 1.2 |
92 |
||
54712 | 93 |
(* Precondition: The proof must be labeled canonically |
94 |
(cf. "Slegehammer_Proof.relabel_proof_canonically"). *) |
|
53763 | 95 |
fun compress_proof isar_compress |
54826 | 96 |
({get_preplay_result, set_preplay_result, preplay_quietly, ...} : preplay_interface) proof = |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
97 |
if isar_compress <= 1.0 then |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
98 |
proof |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
99 |
else |
54712 | 100 |
let |
101 |
val (compress_further, decrement_step_count) = |
|
102 |
let |
|
103 |
val number_of_steps = add_proof_steps (steps_of_proof proof) 0 |
|
104 |
val target_number_of_steps = Real.round (Real.fromInt number_of_steps / isar_compress) |
|
105 |
val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps) |
|
106 |
in |
|
107 |
(fn () => !delta > 0, fn () => delta := !delta - 1) |
|
108 |
end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
109 |
|
54712 | 110 |
val (get_successors, replace_successor) = |
111 |
let |
|
112 |
fun add_refs (Let _) = I |
|
113 |
| add_refs (Prove (_, _, v, _, _, ((lfs, _), _))) = |
|
114 |
fold (fn key => Canonical_Lbl_Tab.cons_list (key, v)) lfs |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
115 |
|
54712 | 116 |
val tab = |
117 |
Canonical_Lbl_Tab.empty |
|
118 |
|> fold_isar_steps add_refs (steps_of_proof proof) |
|
119 |
(* "rev" should have the same effect as "sort canonical_label_ord" *) |
|
120 |
|> Canonical_Lbl_Tab.map (K rev) |
|
121 |
|> Unsynchronized.ref |
|
51260 | 122 |
|
54712 | 123 |
fun get_successors l = Canonical_Lbl_Tab.lookup_list (!tab) l |
124 |
fun set_successors l refs = tab := Canonical_Lbl_Tab.update (l, refs) (!tab) |
|
125 |
fun replace_successor old new dest = |
|
126 |
get_successors dest |
|
127 |
|> Ord_List.remove canonical_label_ord old |
|
128 |
|> Ord_List.union canonical_label_ord new |
|
129 |
|> set_successors dest |
|
130 |
in |
|
131 |
(get_successors, replace_successor) |
|
132 |
end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
133 |
|
54712 | 134 |
(** elimination of trivial, one-step subproofs **) |
135 |
||
136 |
fun elim_subproofs' time qs fix l t lfs gfs meth subs nontriv_subs = |
|
137 |
if null subs orelse not (compress_further ()) then |
|
54826 | 138 |
(set_preplay_result l (Preplay_Success (false, time)); |
54712 | 139 |
Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meth))) |
140 |
else |
|
141 |
(case subs of |
|
142 |
(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
|
143 |
(let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
144 |
(* trivial subproofs have exactly one Prove step *) |
54712 | 145 |
val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
146 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
147 |
(* only touch proofs that can be preplayed sucessfully *) |
54826 | 148 |
val Preplay_Success (false, time') = get_preplay_result l' |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
149 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
150 |
(* merge steps *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
151 |
val subs'' = subs @ nontriv_subs |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
152 |
val lfs'' = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
153 |
subtract (op =) (map fst assms) lfs' |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
154 |
|> union (op =) lfs |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
155 |
val gfs'' = union (op =) gfs' gfs |
54712 | 156 |
val by = ((lfs'', gfs''), meth) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
157 |
val step'' = Prove (qs, fix, l, t, subs'', by) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
158 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
159 |
(* check if the modified step can be preplayed fast enough *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
160 |
val timeout = time_mult merge_timeout_slack (Time.+(time, time')) |
54827 | 161 |
val Preplay_Success (false, time'') = preplay_quietly timeout step'' |
52556
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 |
in |
52626 | 164 |
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
|
165 |
map (replace_successor l' [l]) lfs'; |
54712 | 166 |
elim_subproofs' time'' qs fix l t lfs'' gfs'' meth subs nontriv_subs |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
167 |
end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
168 |
handle Bind => |
54712 | 169 |
elim_subproofs' time qs fix l t lfs gfs meth subs (sub :: nontriv_subs)) |
170 |
| _ => raise Fail "Sledgehammer_Compress: elim_subproofs'") |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
171 |
|
54712 | 172 |
fun elim_subproofs (step as Let _) = step |
54813 | 173 |
| elim_subproofs (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) = |
174 |
if subproofs = [] then |
|
175 |
step |
|
176 |
else |
|
54826 | 177 |
(case get_preplay_result l of |
178 |
Preplay_Success (false, time) => |
|
179 |
elim_subproofs' time qs fix l t lfs gfs meth subproofs [] |
|
180 |
| _ => step) |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
181 |
|
54712 | 182 |
(** top_level compression: eliminate steps by merging them into their |
183 |
successors **) |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
184 |
|
54712 | 185 |
fun compress_top_level steps = |
186 |
let |
|
187 |
(* (#successors, (size_of_term t, position)) *) |
|
188 |
fun cand_key (i, l, t_size) = (get_successors l |> length, (t_size, i)) |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
189 |
|
54712 | 190 |
val compression_ord = |
191 |
prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord) |
|
192 |
#> rev_order |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
193 |
|
54712 | 194 |
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
|
195 |
|
54712 | 196 |
fun pop_next_cand candidates = |
197 |
(case max_list cand_ord candidates of |
|
198 |
NONE => (NONE, []) |
|
199 |
| cand as SOME (i, _, _) => (cand, filter_out (fn (j, _, _) => j = i) candidates)) |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
200 |
|
54712 | 201 |
val candidates = |
202 |
let |
|
203 |
fun add_cand (_, Let _) = I |
|
204 |
| add_cand (i, Prove (_, _, l, t, _, _)) = cons (i, l, size_of_term t) |
|
205 |
in |
|
206 |
(steps |
|
207 |
|> split_last |> fst (* keep last step *) |
|
208 |
|> fold_index add_cand) [] |
|
209 |
end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
210 |
|
54712 | 211 |
fun try_eliminate (i, l, _) succ_lbls steps = |
212 |
let |
|
213 |
(* only touch steps that can be preplayed successfully *) |
|
54826 | 214 |
val Preplay_Success (false, time) = get_preplay_result l |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
215 |
|
54826 | 216 |
val succ_times = |
217 |
map (get_preplay_result #> (fn Preplay_Success (false, t) => t)) succ_lbls |
|
54712 | 218 |
val timeslice = time_mult (1.0 / (Real.fromInt (length succ_lbls))) time |
219 |
val timeouts = |
|
220 |
map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
221 |
|
54712 | 222 |
val ((cand as Prove (_, _, l, _, _, ((lfs, _), _))) :: steps') = drop i steps |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
223 |
|
54712 | 224 |
(* FIXME: debugging *) |
225 |
val _ = |
|
226 |
if the (label_of_step cand) <> l then |
|
227 |
raise Fail "Sledgehammer_Compress: try_eliminate" |
|
228 |
else |
|
229 |
() |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
230 |
|
54712 | 231 |
val succs = collect_successors steps' succ_lbls |
232 |
val succs' = map (try_merge cand #> the) succs |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
233 |
|
54813 | 234 |
(* TODO: should be lazy: stop preplaying as soon as one step fails/times out *) |
54827 | 235 |
val preplay_results = map2 preplay_quietly timeouts succs' |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
236 |
|
54712 | 237 |
(* ensure none of the modified successors timed out *) |
54827 | 238 |
val true = List.all (fn Preplay_Success _ => true) preplay_results |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
239 |
|
54712 | 240 |
val (steps1, _ :: steps2) = chop i steps |
241 |
(* replace successors with their modified versions *) |
|
242 |
val steps2 = update_steps steps2 succs' |
|
243 |
in |
|
244 |
decrement_step_count (); (* candidate successfully eliminated *) |
|
54827 | 245 |
map2 set_preplay_result succ_lbls preplay_results; |
54712 | 246 |
map (replace_successor l succ_lbls) lfs; |
54813 | 247 |
(* removing the step would mess up the indices -> replace with dummy step instead *) |
54712 | 248 |
steps1 @ dummy_isar_step :: steps2 |
249 |
end |
|
250 |
handle Bind => steps |
|
251 |
| Match => steps |
|
252 |
| Option.Option => steps |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
253 |
|
54712 | 254 |
fun compression_loop candidates steps = |
255 |
if not (compress_further ()) then |
|
256 |
steps |
|
257 |
else |
|
258 |
(case pop_next_cand candidates of |
|
259 |
(NONE, _) => steps (* no more candidates for elimination *) |
|
260 |
| (SOME (cand as (_, l, _)), candidates) => |
|
261 |
let val successors = get_successors l in |
|
262 |
if length successors > compress_degree then steps |
|
263 |
else compression_loop candidates (try_eliminate cand successors steps) |
|
264 |
end) |
|
265 |
in |
|
266 |
compression_loop candidates steps |
|
267 |
|> remove (op =) dummy_isar_step |
|
268 |
end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
269 |
|
54712 | 270 |
(** recusion over the proof tree **) |
271 |
(* |
|
272 |
Proofs are compressed bottom-up, beginning with the innermost |
|
273 |
subproofs. |
|
274 |
On the innermost proof level, the proof steps have no subproofs. |
|
275 |
In the best case, these steps can be merged into just one step, |
|
276 |
resulting in a trivial subproof. Going one level up, trivial subproofs |
|
277 |
can be eliminated. In the best case, this once again leads to a proof |
|
278 |
whose proof steps do not have subproofs. Applying this approach |
|
279 |
recursively will result in a flat proof in the best cast. |
|
280 |
*) |
|
281 |
fun do_proof (proof as (Proof (fix, assms, steps))) = |
|
282 |
if compress_further () then Proof (fix, assms, do_steps steps) else proof |
|
283 |
and do_steps steps = |
|
284 |
(* bottom-up: compress innermost proofs first *) |
|
285 |
steps |> map (fn step => step |> compress_further () ? do_sub_levels) |
|
286 |
|> compress_further () ? compress_top_level |
|
287 |
and do_sub_levels (Let x) = Let x |
|
288 |
| do_sub_levels (Prove (qs, xs, l, t, subproofs, by)) = |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
289 |
(* compress subproofs *) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
290 |
Prove (qs, xs, l, t, map do_proof subproofs, by) |
54712 | 291 |
(* eliminate trivial subproofs *) |
292 |
|> compress_further () ? elim_subproofs |
|
293 |
in |
|
294 |
do_proof proof |
|
295 |
end |
|
50259 | 296 |
|
54504 | 297 |
end; |