1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML |
|
2 Author: Steffen Juilf Smolka, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 |
|
5 Minimize dependencies (used facts) of Isar proof steps. |
|
6 *) |
|
7 |
|
8 signature SLEDGEHAMMER_MINIMIZE_ISAR = |
|
9 sig |
|
10 type preplay_interface = Sledgehammer_Preplay.preplay_interface |
|
11 type isar_step = Sledgehammer_Proof.isar_step |
|
12 type isar_proof = Sledgehammer_Proof.isar_proof |
|
13 |
|
14 val min_deps_of_step : preplay_interface -> isar_step -> isar_step |
|
15 val postprocess_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof |
|
16 end; |
|
17 |
|
18 structure Sledgehammer_Minimize_Isar : SLEDGEHAMMER_MINIMIZE_ISAR = |
|
19 struct |
|
20 |
|
21 open Sledgehammer_Util |
|
22 open Sledgehammer_Reconstructor |
|
23 open Sledgehammer_Proof |
|
24 open Sledgehammer_Preplay |
|
25 |
|
26 val slack = seconds 0.1 |
|
27 |
|
28 fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step |
|
29 | min_deps_of_step {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} |
|
30 (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) = |
|
31 (case get_preplay_outcome l of |
|
32 Played time => |
|
33 let |
|
34 fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth)) |
|
35 val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs) |
|
36 |
|
37 fun minimize_facts _ time min_facts [] = (time, min_facts) |
|
38 | minimize_facts mk_step time min_facts (f :: facts) = |
|
39 (case preplay_quietly (Time.+ (time, slack)) (mk_step (min_facts @ facts)) of |
|
40 Played time => minimize_facts mk_step time min_facts facts |
|
41 | _ => minimize_facts mk_step time (f :: min_facts) facts) |
|
42 |
|
43 val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs |
|
44 val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs |
|
45 in |
|
46 set_preplay_outcome l (Played time); mk_step_lfs_gfs min_lfs min_gfs |
|
47 end |
|
48 | _ => step (* don't touch steps that time out or fail *)) |
|
49 |
|
50 fun postprocess_remove_unreferenced_steps postproc_step = |
|
51 let |
|
52 val add_lfs = fold (Ord_List.insert label_ord) |
|
53 |
|
54 fun do_proof (Proof (fix, assms, steps)) = |
|
55 let val (refed, steps) = do_steps steps in |
|
56 (refed, Proof (fix, assms, steps)) |
|
57 end |
|
58 and do_steps [] = ([], []) |
|
59 | do_steps steps = |
|
60 let |
|
61 (* the last step is always implicitly referenced *) |
|
62 val (steps, (refed, concl)) = |
|
63 split_last steps |
|
64 ||> do_refed_step |
|
65 in |
|
66 fold_rev do_step steps (refed, [concl]) |
|
67 end |
|
68 and do_step step (refed, accu) = |
|
69 (case label_of_step step of |
|
70 NONE => (refed, step :: accu) |
|
71 | SOME l => |
|
72 if Ord_List.member label_ord refed l then |
|
73 do_refed_step step |
|
74 |>> Ord_List.union label_ord refed |
|
75 ||> (fn x => x :: accu) |
|
76 else |
|
77 (refed, accu)) |
|
78 and do_refed_step step = step |> postproc_step |> do_refed_step' |
|
79 and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar" |
|
80 | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) = |
|
81 let |
|
82 val (refed, subproofs) = |
|
83 map do_proof subproofs |
|
84 |> split_list |
|
85 |>> Ord_List.unions label_ord |
|
86 |>> add_lfs lfs |
|
87 val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m)) |
|
88 in |
|
89 (refed, step) |
|
90 end |
|
91 in |
|
92 snd o do_proof |
|
93 end |
|
94 |
|
95 end; |
|