author | blanchet |
Thu, 28 Aug 2014 16:58:27 +0200 | |
changeset 58083 | ca7ec8728348 |
parent 58079 | df0d6ce8fb66 |
child 60305 | 7d278b0617d3 |
permissions | -rw-r--r-- |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML |
54712 | 2 |
Author: Steffen Juilf Smolka, TU Muenchen |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
4 |
|
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
5 |
Minimize dependencies (used facts) of Isar proof steps. |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
6 |
*) |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
7 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
8 |
signature SLEDGEHAMMER_ISAR_MINIMIZE = |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
9 |
sig |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
10 |
type isar_step = Sledgehammer_Isar_Proof.isar_step |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
11 |
type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
55213 | 12 |
type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data |
54712 | 13 |
|
55266 | 14 |
val keep_fastest_method_of_isar_step : isar_preplay_data -> isar_step -> isar_step |
57732 | 15 |
val minimized_isar_step : Proof.context -> Time.time -> isar_step -> Time.time * isar_step |
57054 | 16 |
val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref -> |
17 |
isar_step -> isar_step |
|
58083 | 18 |
val postprocess_isar_proof_remove_show_stuttering : isar_proof -> isar_proof |
55213 | 19 |
val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> |
20 |
isar_proof |
|
54504 | 21 |
end; |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
22 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
23 |
structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE = |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
24 |
struct |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
25 |
|
57675
47336af5d2b2
faster minimization by not adding facts that are already in the simpset
blanchet
parents:
57054
diff
changeset
|
26 |
open Sledgehammer_Util |
55287 | 27 |
open Sledgehammer_Proof_Methods |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
28 |
open Sledgehammer_Isar_Proof |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
29 |
open Sledgehammer_Isar_Preplay |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
30 |
|
55299 | 31 |
fun keep_fastest_method_of_isar_step preplay_data |
32 |
(Prove (qs, xs, l, t, subproofs, facts, meths, comment)) = |
|
55295
b18f65f77fcd
keep all proof methods in data structure until the end, to enhance debugging output
blanchet
parents:
55287
diff
changeset
|
33 |
Prove (qs, xs, l, t, subproofs, facts, |
55299 | 34 |
meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @, |
35 |
comment) |
|
55266 | 36 |
| keep_fastest_method_of_isar_step _ step = step |
37 |
||
55324 | 38 |
val slack = seconds 0.025 |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
39 |
|
57731 | 40 |
fun minimized_isar_step ctxt time |
58079
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
41 |
(Prove (qs, xs, l, t, subproofs, (lfs0, gfs00), meths as meth :: _, comment)) = |
57731 | 42 |
let |
43 |
val gfs0 = filter (thms_influence_proof_method ctxt meth o thms_of_name ctxt) gfs00 |
|
44 |
||
57779 | 45 |
fun mk_step_lfs_gfs lfs gfs = |
58079
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
46 |
Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), meths, comment) |
57731 | 47 |
|
57739 | 48 |
fun minimize_half _ min_facts [] time = (min_facts, time) |
49 |
| minimize_half mk_step min_facts (fact :: facts) time = |
|
57731 | 50 |
(case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth |
51 |
(mk_step (min_facts @ facts)) of |
|
57739 | 52 |
Played time' => minimize_half mk_step min_facts facts time' |
53 |
| _ => minimize_half mk_step (fact :: min_facts) facts time) |
|
57731 | 54 |
|
57739 | 55 |
val (min_lfs, time') = minimize_half (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time |
56 |
val (min_gfs, time'') = minimize_half (mk_step_lfs_gfs min_lfs) [] gfs0 time' |
|
57731 | 57 |
in |
58 |
(time'', mk_step_lfs_gfs min_lfs min_gfs) |
|
59 |
end |
|
60 |
||
57054 | 61 |
fun minimize_isar_step_dependencies ctxt preplay_data |
58079
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
62 |
(step as Prove (_, _, l, _, _, _, meth :: meths, _)) = |
55266 | 63 |
(case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of |
54828 | 64 |
Played time => |
58079
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
65 |
let |
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
66 |
fun old_data_for_method meth' = |
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
67 |
(meth', peek_at_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth')) |
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
68 |
|
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
69 |
val (time', step') = minimized_isar_step ctxt time step |
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
70 |
in |
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
71 |
set_preplay_outcomes_of_isar_step ctxt time' preplay_data step' |
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
72 |
((meth, Played time') :: (if step' = step then map old_data_for_method meths else [])); |
55264 | 73 |
step' |
54826 | 74 |
end |
75 |
| _ => step (* don't touch steps that time out or fail *)) |
|
57054 | 76 |
| minimize_isar_step_dependencies _ _ step = step |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
77 |
|
58083 | 78 |
fun postprocess_isar_proof_remove_show_stuttering (Proof (fix, assms, steps)) = |
79 |
let |
|
80 |
fun process_steps [] = [] |
|
81 |
| process_steps (steps as [Prove ([], [], l1, t1, subs1, facts1, meths1, comment1), |
|
82 |
Prove ([Show], [], l2, t2, _, _, _, comment2)]) = |
|
83 |
if t1 aconv t2 then [Prove ([Show], [], l2, t2, subs1, facts1, meths1, comment1 ^ comment2)] |
|
84 |
else steps |
|
85 |
| process_steps (step :: steps) = step :: process_steps steps |
|
86 |
in |
|
87 |
Proof (fix, assms, process_steps steps) |
|
88 |
end |
|
89 |
||
55213 | 90 |
fun postprocess_isar_proof_remove_unreferenced_steps postproc_step = |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
91 |
let |
55259 | 92 |
fun process_proof (Proof (fix, assms, steps)) = |
55265 | 93 |
process_steps steps ||> (fn steps => Proof (fix, assms, steps)) |
55259 | 94 |
and process_steps [] = ([], []) |
95 |
| process_steps steps = |
|
55212 | 96 |
(* the last step is always implicitly referenced *) |
55265 | 97 |
let val (steps, (used, concl)) = split_last steps ||> process_used_step in |
98 |
fold_rev process_step steps (used, [concl]) |
|
54754 | 99 |
end |
55265 | 100 |
and process_step step (used, accu) = |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
101 |
(case label_of_isar_step step of |
55265 | 102 |
NONE => (used, step :: accu) |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
103 |
| SOME l => |
55265 | 104 |
if Ord_List.member label_ord used l then |
105 |
process_used_step step |>> Ord_List.union label_ord used ||> (fn step => step :: accu) |
|
54813 | 106 |
else |
55265 | 107 |
(used, accu)) |
58083 | 108 |
and process_used_step step = process_used_step_subproofs (postproc_step step) |
55299 | 109 |
and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) = |
55259 | 110 |
let |
55265 | 111 |
val (used, subproofs) = |
55259 | 112 |
map process_proof subproofs |
113 |
|> split_list |
|
114 |
|>> Ord_List.unions label_ord |
|
115 |
|>> fold (Ord_List.insert label_ord) lfs |
|
116 |
in |
|
55299 | 117 |
(used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) |
55259 | 118 |
end |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
119 |
in |
55259 | 120 |
snd o process_proof |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
121 |
end |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
122 |
|
54504 | 123 |
end; |