26 val slack = seconds 0.1 |
26 val slack = seconds 0.1 |
27 |
27 |
28 fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step |
28 fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step |
29 | minimize_isar_step_dependencies |
29 | minimize_isar_step_dependencies |
30 {reset_preplay_outcomes, set_preplay_outcome, preplay_outcome, preplay_quietly, ...} |
30 {reset_preplay_outcomes, set_preplay_outcome, preplay_outcome, preplay_quietly, ...} |
31 (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss as (meth :: _) :: _))) = |
31 (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) = |
32 (case Lazy.force (preplay_outcome l meth) of |
32 (case Lazy.force (preplay_outcome 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), methss)) |
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) |
36 val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs) |
37 |
37 |
38 fun minimize_facts _ time min_facts [] = (time, min_facts) |
38 fun minimize_facts _ time min_facts [] = (time, min_facts) |
39 | minimize_facts mk_step time min_facts (f :: facts) = |
39 | minimize_facts mk_step time min_facts (f :: facts) = |
40 (case preplay_quietly (Time.+ (time, slack)) (mk_step (min_facts @ facts)) of |
40 (case preplay_quietly (Time.+ (time, slack)) (mk_step (min_facts @ facts)) of |