5 Minimize dependencies (used facts) of Isar proof steps. |
5 Minimize dependencies (used facts) of Isar proof steps. |
6 *) |
6 *) |
7 |
7 |
8 signature SLEDGEHAMMER_ISAR_MINIMIZE = |
8 signature SLEDGEHAMMER_ISAR_MINIMIZE = |
9 sig |
9 sig |
10 type preplay_data = Sledgehammer_Isar_Preplay.preplay_data |
|
11 type isar_step = Sledgehammer_Isar_Proof.isar_step |
10 type isar_step = Sledgehammer_Isar_Proof.isar_step |
12 type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
11 type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
|
12 type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data |
13 |
13 |
14 val minimal_deps_of_step : preplay_data -> isar_step -> isar_step |
14 val minimize_isar_step_dependencies : isar_preplay_data -> isar_step -> isar_step |
15 val postprocess_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof |
15 val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> |
|
16 isar_proof |
16 end; |
17 end; |
17 |
18 |
18 structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE = |
19 structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE = |
19 struct |
20 struct |
20 |
21 |
22 open Sledgehammer_Isar_Proof |
23 open Sledgehammer_Isar_Proof |
23 open Sledgehammer_Isar_Preplay |
24 open Sledgehammer_Isar_Preplay |
24 |
25 |
25 val slack = seconds 0.1 |
26 val slack = seconds 0.1 |
26 |
27 |
27 fun minimal_deps_of_step (_ : preplay_data) (step as Let _) = step |
28 fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step |
28 | minimal_deps_of_step {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} |
29 | minimize_isar_step_dependencies {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} |
29 (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) = |
30 (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) = |
30 (case get_preplay_outcome l of |
31 (case get_preplay_outcome l of |
31 Played time => |
32 Played time => |
32 let |
33 let |
33 fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth)) |
34 fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth)) |
44 in |
45 in |
45 set_preplay_outcome l (Played time); mk_step_lfs_gfs min_lfs min_gfs |
46 set_preplay_outcome l (Played time); mk_step_lfs_gfs min_lfs min_gfs |
46 end |
47 end |
47 | _ => step (* don't touch steps that time out or fail *)) |
48 | _ => step (* don't touch steps that time out or fail *)) |
48 |
49 |
49 fun postprocess_remove_unreferenced_steps postproc_step = |
50 fun postprocess_isar_proof_remove_unreferenced_steps postproc_step = |
50 let |
51 let |
51 val add_lfs = fold (Ord_List.insert label_ord) |
52 val add_lfs = fold (Ord_List.insert label_ord) |
52 |
53 |
53 fun do_proof (Proof (fix, assms, steps)) = |
54 fun do_proof (Proof (fix, assms, steps)) = |
54 let val (refed, steps) = do_steps steps in |
55 let val (refed, steps) = do_steps steps in |