39 (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of |
39 (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of |
40 Played time => |
40 Played time => |
41 let |
41 let |
42 fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment) |
42 fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment) |
43 |
43 |
44 fun minimize_facts _ time min_facts [] = (time, min_facts) |
44 fun minimize_facts _ min_facts [] time = (min_facts, time) |
45 | minimize_facts mk_step time min_facts (f :: facts) = |
45 | minimize_facts mk_step min_facts (fact :: facts) time = |
46 (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth |
46 (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth |
47 (mk_step (min_facts @ facts)) of |
47 (mk_step (min_facts @ facts)) of |
48 Played time => minimize_facts mk_step time min_facts facts |
48 Played time' => minimize_facts mk_step min_facts facts time' |
49 | _ => minimize_facts mk_step time (f :: min_facts) facts) |
49 | _ => minimize_facts mk_step (fact :: min_facts) facts time) |
50 |
50 |
51 val (time, min_lfs) = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs0) time [] lfs0 |
51 val (min_lfs, time') = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time |
52 val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs0 |
52 val (min_gfs, time'') = minimize_facts (mk_step_lfs_gfs min_lfs) [] gfs0 time' |
53 |
53 |
54 val step' = mk_step_lfs_gfs min_lfs min_gfs |
54 val step' = mk_step_lfs_gfs min_lfs min_gfs |
55 in |
55 in |
56 set_preplay_outcomes_of_isar_step ctxt time preplay_data step' [(meth, Played time)]; |
56 set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step' [(meth, Played time'')]; |
57 step' |
57 step' |
58 end |
58 end |
59 | _ => step (* don't touch steps that time out or fail *)) |
59 | _ => step (* don't touch steps that time out or fail *)) |
60 | minimize_isar_step_dependencies _ _ step = step |
60 | minimize_isar_step_dependencies _ _ step = step |
61 |
61 |