31 (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) = |
31 (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) = |
32 (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of |
32 (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of |
33 Played time => |
33 Played time => |
34 let |
34 let |
35 fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths)) |
35 fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths)) |
36 val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs) |
|
37 |
36 |
38 fun minimize_facts _ time min_facts [] = (time, min_facts) |
37 fun minimize_facts _ time min_facts [] = (time, min_facts) |
39 | minimize_facts mk_step time min_facts (f :: facts) = |
38 | minimize_facts mk_step time min_facts (f :: facts) = |
40 (case preplay_isar_step ctxt (Time.+ (time, slack)) meth |
39 (case preplay_isar_step ctxt (Time.+ (time, slack)) meth |
41 (mk_step (min_facts @ facts)) of |
40 (mk_step (min_facts @ facts)) of |
42 Played time => minimize_facts mk_step time min_facts facts |
41 Played time => minimize_facts mk_step time min_facts facts |
43 | _ => minimize_facts mk_step time (f :: min_facts) facts) |
42 | _ => minimize_facts mk_step time (f :: min_facts) facts) |
44 |
43 |
45 val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs |
44 val (time, min_lfs) = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs) time [] lfs |
46 val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs |
45 val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs |
47 in |
46 in |
48 set_preplay_outcomes_of_isar_step preplay_data l [(meth, Lazy.value (Played time))]; |
47 set_preplay_outcomes_of_isar_step preplay_data l [(meth, Lazy.value (Played time))]; |
49 mk_step_lfs_gfs min_lfs min_gfs |
48 mk_step_lfs_gfs min_lfs min_gfs |
50 end |
49 end |