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