9 signature SLEDGEHAMMER_ISAR_COMPRESS = |
9 signature SLEDGEHAMMER_ISAR_COMPRESS = |
10 sig |
10 sig |
11 type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
11 type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
12 type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data |
12 type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data |
13 |
13 |
14 val compress_isar_proof : Proof.context -> real -> Time.time -> |
14 val compress_isar_proof : Proof.context -> bool -> real -> Time.time -> |
15 isar_preplay_data Unsynchronized.ref -> isar_proof -> isar_proof |
15 isar_preplay_data Unsynchronized.ref -> isar_proof -> isar_proof |
16 end; |
16 end; |
17 |
17 |
18 structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS = |
18 structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS = |
19 struct |
19 struct |
107 end |
107 end |
108 |
108 |
109 val compress_degree = 2 |
109 val compress_degree = 2 |
110 |
110 |
111 (* Precondition: The proof must be labeled canonically. *) |
111 (* Precondition: The proof must be labeled canonically. *) |
112 fun compress_isar_proof ctxt compress_isar preplay_timeout preplay_data proof = |
112 fun compress_isar_proof ctxt debug compress_isar preplay_timeout preplay_data proof = |
113 if compress_isar <= 1.0 then |
113 if compress_isar <= 1.0 then |
114 proof |
114 proof |
115 else |
115 else |
116 let |
116 let |
117 val (compress_further, decrement_step_count) = |
117 val (compress_further, decrement_step_count) = |
170 val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'', comment) |
170 val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'', comment) |
171 |
171 |
172 (* check if the modified step can be preplayed fast enough *) |
172 (* check if the modified step can be preplayed fast enough *) |
173 val timeout = adjust_merge_timeout preplay_timeout (Time.+ (time, reference_time l')) |
173 val timeout = adjust_merge_timeout preplay_timeout (Time.+ (time, reference_time l')) |
174 in |
174 in |
175 (case preplay_isar_step ctxt timeout hopeless step'' of |
175 (case preplay_isar_step ctxt debug timeout hopeless step'' of |
176 meths_outcomes as (_, Played time'') :: _ => |
176 meths_outcomes as (_, Played time'') :: _ => |
177 (* l' successfully eliminated *) |
177 (* l' successfully eliminated *) |
178 (decrement_step_count (); |
178 (decrement_step_count (); |
179 set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes; |
179 set_preplay_outcomes_of_isar_step ctxt debug time'' preplay_data step'' |
|
180 meths_outcomes; |
180 map (replace_successor l' [l]) lfs'; |
181 map (replace_successor l' [l]) lfs'; |
181 elim_one_subproof time'' step'' subs nontriv_subs) |
182 elim_one_subproof time'' step'' subs nontriv_subs) |
182 | _ => elim_one_subproof time step subs (sub :: nontriv_subs)) |
183 | _ => elim_one_subproof time step subs (sub :: nontriv_subs)) |
183 end |
184 end |
184 | sub :: subs => elim_one_subproof time step subs (sub :: nontriv_subs)) |
185 | sub :: subs => elim_one_subproof time step subs (sub :: nontriv_subs)) |
213 | SOME times0 => |
214 | SOME times0 => |
214 let |
215 let |
215 val time_slice = time_mult (1.0 / Real.fromInt (length labels)) (reference_time l) |
216 val time_slice = time_mult (1.0 / Real.fromInt (length labels)) (reference_time l) |
216 val timeouts = |
217 val timeouts = |
217 map (adjust_merge_timeout preplay_timeout o curry Time.+ time_slice) times0 |
218 map (adjust_merge_timeout preplay_timeout o curry Time.+ time_slice) times0 |
218 val meths_outcomess = map3 (preplay_isar_step ctxt) timeouts hopelesses succs' |
219 val meths_outcomess = |
|
220 map3 (preplay_isar_step ctxt debug) timeouts hopelesses succs' |
219 in |
221 in |
220 (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of |
222 (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of |
221 NONE => steps |
223 NONE => steps |
222 | SOME times => |
224 | SOME times => |
223 (* candidate successfully eliminated *) |
225 (* candidate successfully eliminated *) |
224 (decrement_step_count (); |
226 (decrement_step_count (); |
225 map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) |
227 map3 (fn time => |
|
228 set_preplay_outcomes_of_isar_step ctxt debug time preplay_data) |
226 times succs' meths_outcomess; |
229 times succs' meths_outcomess; |
227 map (replace_successor l labels) lfs; |
230 map (replace_successor l labels) lfs; |
228 steps_before @ update_steps succs' steps_after)) |
231 steps_before @ update_steps succs' steps_after)) |
229 end) |
232 end) |
230 end |
233 end |