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_interface = Sledgehammer_Isar_Preplay.preplay_interface |
10 type preplay_data = Sledgehammer_Isar_Preplay.preplay_data |
11 type isar_step = Sledgehammer_Isar_Proof.isar_step |
11 type isar_step = Sledgehammer_Isar_Proof.isar_step |
12 type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
12 type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
13 |
13 |
14 val min_deps_of_step : preplay_interface -> isar_step -> isar_step |
14 val minimal_deps_of_step : preplay_data -> isar_step -> isar_step |
15 val postprocess_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof |
15 val postprocess_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof |
16 end; |
16 end; |
17 |
17 |
18 structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE = |
18 structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE = |
19 struct |
19 struct |
20 |
20 |
21 open Sledgehammer_Util |
|
22 open Sledgehammer_Reconstructor |
21 open Sledgehammer_Reconstructor |
23 open Sledgehammer_Isar_Proof |
22 open Sledgehammer_Isar_Proof |
24 open Sledgehammer_Isar_Preplay |
23 open Sledgehammer_Isar_Preplay |
25 |
24 |
26 val slack = seconds 0.1 |
25 val slack = seconds 0.1 |
27 |
26 |
28 fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step |
27 fun minimal_deps_of_step (_ : preplay_data) (step as Let _) = step |
29 | min_deps_of_step {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} |
28 | minimal_deps_of_step {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} |
30 (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) = |
29 (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) = |
31 (case get_preplay_outcome l of |
30 (case get_preplay_outcome l of |
32 Played time => |
31 Played time => |
33 let |
32 let |
34 fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth)) |
33 fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth)) |
55 let val (refed, steps) = do_steps steps in |
54 let val (refed, steps) = do_steps steps in |
56 (refed, Proof (fix, assms, steps)) |
55 (refed, Proof (fix, assms, steps)) |
57 end |
56 end |
58 and do_steps [] = ([], []) |
57 and do_steps [] = ([], []) |
59 | do_steps steps = |
58 | do_steps steps = |
60 let |
59 (* the last step is always implicitly referenced *) |
61 (* the last step is always implicitly referenced *) |
60 let val (steps, (refed, concl)) = split_last steps ||> do_refed_step in |
62 val (steps, (refed, concl)) = |
|
63 split_last steps |
|
64 ||> do_refed_step |
|
65 in |
|
66 fold_rev do_step steps (refed, [concl]) |
61 fold_rev do_step steps (refed, [concl]) |
67 end |
62 end |
68 and do_step step (refed, accu) = |
63 and do_step step (refed, accu) = |
69 (case label_of_step step of |
64 (case label_of_step step of |
70 NONE => (refed, step :: accu) |
65 NONE => (refed, step :: accu) |