35 | keep_fastest_method_of_isar_step _ step = step |
35 | keep_fastest_method_of_isar_step _ step = step |
36 |
36 |
37 val slack = seconds 0.025 |
37 val slack = seconds 0.025 |
38 |
38 |
39 fun minimized_isar_step ctxt time |
39 fun minimized_isar_step ctxt time |
40 (Prove (qs, xs, l, t, subproofs, (lfs0, gfs00), meth :: _, comment)) = |
40 (Prove (qs, xs, l, t, subproofs, (lfs0, gfs00), meths as meth :: _, comment)) = |
41 let |
41 let |
42 val gfs0 = filter (thms_influence_proof_method ctxt meth o thms_of_name ctxt) gfs00 |
42 val gfs0 = filter (thms_influence_proof_method ctxt meth o thms_of_name ctxt) gfs00 |
43 |
43 |
44 fun mk_step_lfs_gfs lfs gfs = |
44 fun mk_step_lfs_gfs lfs gfs = |
45 Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), [meth], comment) |
45 Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), meths, comment) |
46 |
46 |
47 fun minimize_half _ min_facts [] time = (min_facts, time) |
47 fun minimize_half _ min_facts [] time = (min_facts, time) |
48 | minimize_half mk_step min_facts (fact :: facts) time = |
48 | minimize_half mk_step min_facts (fact :: facts) time = |
49 (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth |
49 (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth |
50 (mk_step (min_facts @ facts)) of |
50 (mk_step (min_facts @ facts)) of |
56 in |
56 in |
57 (time'', mk_step_lfs_gfs min_lfs min_gfs) |
57 (time'', mk_step_lfs_gfs min_lfs min_gfs) |
58 end |
58 end |
59 |
59 |
60 fun minimize_isar_step_dependencies ctxt preplay_data |
60 fun minimize_isar_step_dependencies ctxt preplay_data |
61 (step as Prove (_, _, l, _, _, _, meth :: _, _)) = |
61 (step as Prove (_, _, l, _, _, _, meth :: meths, _)) = |
62 (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of |
62 (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of |
63 Played time => |
63 Played time => |
64 let val (time', step') = minimized_isar_step ctxt time step in |
64 let |
65 set_preplay_outcomes_of_isar_step ctxt time' preplay_data step' [(meth, Played time')]; |
65 fun old_data_for_method meth' = |
|
66 (meth', peek_at_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth')) |
|
67 |
|
68 val (time', step') = minimized_isar_step ctxt time step |
|
69 in |
|
70 set_preplay_outcomes_of_isar_step ctxt time' preplay_data step' |
|
71 ((meth, Played time') :: (if step' = step then map old_data_for_method meths else [])); |
66 step' |
72 step' |
67 end |
73 end |
68 | _ => step (* don't touch steps that time out or fail *)) |
74 | _ => step (* don't touch steps that time out or fail *)) |
69 | minimize_isar_step_dependencies _ _ step = step |
75 | minimize_isar_step_dependencies _ _ step = step |
70 |
76 |