equal
deleted
inserted
replaced
92 SOME (Prove (qs2, fix, l2, t, subproofs, ((lfs, gfs), meths))) |
92 SOME (Prove (qs2, fix, l2, t, subproofs, ((lfs, gfs), meths))) |
93 end) |
93 end) |
94 | try_merge _ _ = NONE |
94 | try_merge _ _ = NONE |
95 |
95 |
96 val compress_degree = 2 |
96 val compress_degree = 2 |
97 val merge_timeout_slack = 1.25 |
97 val merge_timeout_slack_time = seconds 0.005 |
98 |
98 val merge_timeout_slack_factor = 1.5 |
99 (* Precondition: The proof must be labeled canonically |
99 |
100 (cf. "Slegehammer_Isar_Proof.relabel_isar_proof_canonically"). *) |
100 fun slackify_merge_timeout time = |
|
101 time_mult merge_timeout_slack_factor (Time.+ (merge_timeout_slack_time, time)) |
|
102 |
|
103 (* Precondition: The proof must be labeled canonically. *) |
101 fun compress_isar_proof ctxt compress_isar preplay_data proof = |
104 fun compress_isar_proof ctxt compress_isar preplay_data proof = |
102 if compress_isar <= 1.0 then |
105 if compress_isar <= 1.0 then |
103 proof |
106 proof |
104 else |
107 else |
105 let |
108 let |
164 val gfs'' = union (op =) gfs' gfs |
167 val gfs'' = union (op =) gfs' gfs |
165 val by = ((lfs'', gfs''), meths(*FIXME*)) |
168 val by = ((lfs'', gfs''), meths(*FIXME*)) |
166 val step'' = Prove (qs, fix, l, t, subs'', by) |
169 val step'' = Prove (qs, fix, l, t, subs'', by) |
167 |
170 |
168 (* check if the modified step can be preplayed fast enough *) |
171 (* check if the modified step can be preplayed fast enough *) |
169 val timeout = time_mult merge_timeout_slack (Time.+ (time, time')) |
172 val timeout = slackify_merge_timeout (Time.+ (time, time')) |
170 val Played time'' = preplay_isar_step ctxt timeout (hd meths)(*FIXME*) step'' |
173 val Played time'' = preplay_isar_step ctxt timeout (hd meths)(*FIXME*) step'' |
171 in |
174 in |
172 decrement_step_count (); (* l' successfully eliminated! *) |
175 decrement_step_count (); (* l' successfully eliminated! *) |
173 map (replace_successor l' [l]) lfs'; |
176 map (replace_successor l' [l]) lfs'; |
174 elim_one_subproof time'' qs fix l t lfs'' gfs'' meths subs nontriv_subs |
177 elim_one_subproof time'' qs fix l t lfs'' gfs'' meths subs nontriv_subs |
228 val succs' = map (try_merge cand #> the) succs |
231 val succs' = map (try_merge cand #> the) succs |
229 |
232 |
230 val times0 = map ((fn Played time => time) o |
233 val times0 = map ((fn Played time => time) o |
231 forced_preplay_outcome_of_isar_step (!preplay_data)) labels |
234 forced_preplay_outcome_of_isar_step (!preplay_data)) labels |
232 val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time |
235 val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time |
233 val timeouts = map (curry Time.+ time_slice #> time_mult merge_timeout_slack) times0 |
236 val timeouts = map (curry Time.+ time_slice #> slackify_merge_timeout) times0 |
234 |
237 |
235 (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *) |
238 (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *) |
236 val play_outcomes = map3 (preplay_isar_step ctxt) timeouts succ_meths succs' |
239 val play_outcomes = map3 (preplay_isar_step ctxt) timeouts succ_meths succs' |
237 |
240 |
238 (* ensure none of the modified successors timed out *) |
241 (* ensure none of the modified successors timed out *) |