author | desharna |
Wed, 21 Oct 2020 17:46:51 +0200 | |
changeset 72583 | e728d3a3d383 |
parent 72582 | b69a3a7655f2 |
child 72584 | 4ea19e5dc67e |
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 |
63097
ee8edbcbb4ad
proper consideration of chained facts in 'try0' minimization
blanchet
parents:
62826
diff
changeset
|
15 |
val minimized_isar_step : Proof.context -> thm list -> Time.time -> isar_step -> |
ee8edbcbb4ad
proper consideration of chained facts in 'try0' minimization
blanchet
parents:
62826
diff
changeset
|
16 |
Time.time * isar_step |
57054 | 17 |
val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref -> |
18 |
isar_step -> isar_step |
|
58083 | 19 |
val postprocess_isar_proof_remove_show_stuttering : isar_proof -> isar_proof |
55213 | 20 |
val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> |
21 |
isar_proof |
|
54504 | 22 |
end; |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
23 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
24 |
structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE = |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
25 |
struct |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
26 |
|
57675
47336af5d2b2
faster minimization by not adding facts that are already in the simpset
blanchet
parents:
57054
diff
changeset
|
27 |
open Sledgehammer_Util |
55287 | 28 |
open Sledgehammer_Proof_Methods |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
29 |
open Sledgehammer_Isar_Proof |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
30 |
open Sledgehammer_Isar_Preplay |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
31 |
|
55299 | 32 |
fun keep_fastest_method_of_isar_step preplay_data |
33 |
(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
|
34 |
Prove (qs, xs, l, t, subproofs, facts, |
55299 | 35 |
meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @, |
36 |
comment) |
|
55266 | 37 |
| keep_fastest_method_of_isar_step _ step = step |
38 |
||
55324 | 39 |
val slack = seconds 0.025 |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
40 |
|
63097
ee8edbcbb4ad
proper consideration of chained facts in 'try0' minimization
blanchet
parents:
62826
diff
changeset
|
41 |
fun minimized_isar_step ctxt chained time |
60305
7d278b0617d3
took out Sledgehammer minimizer optimization that breaks things
blanchet
parents:
58083
diff
changeset
|
42 |
(Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) = |
57731 | 43 |
let |
57779 | 44 |
fun mk_step_lfs_gfs lfs gfs = |
58079
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
45 |
Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), meths, comment) |
57731 | 46 |
|
57739 | 47 |
fun minimize_half _ min_facts [] time = (min_facts, time) |
48 |
| minimize_half mk_step min_facts (fact :: facts) time = |
|
63097
ee8edbcbb4ad
proper consideration of chained facts in 'try0' minimization
blanchet
parents:
62826
diff
changeset
|
49 |
(case preplay_isar_step_for_method ctxt chained (time + slack) meth |
57731 | 50 |
(mk_step (min_facts @ facts)) of |
57739 | 51 |
Played time' => minimize_half mk_step min_facts facts time' |
52 |
| _ => minimize_half mk_step (fact :: min_facts) facts time) |
|
57731 | 53 |
|
57739 | 54 |
val (min_lfs, time') = minimize_half (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time |
55 |
val (min_gfs, time'') = minimize_half (mk_step_lfs_gfs min_lfs) [] gfs0 time' |
|
57731 | 56 |
in |
57 |
(time'', mk_step_lfs_gfs min_lfs min_gfs) |
|
58 |
end |
|
59 |
||
57054 | 60 |
fun minimize_isar_step_dependencies ctxt preplay_data |
58079
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
61 |
(step as Prove (_, _, l, _, _, _, meth :: meths, _)) = |
55266 | 62 |
(case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of |
54828 | 63 |
Played time => |
58079
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
64 |
let |
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
65 |
fun old_data_for_method meth' = |
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
66 |
(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
|
67 |
|
63097
ee8edbcbb4ad
proper consideration of chained facts in 'try0' minimization
blanchet
parents:
62826
diff
changeset
|
68 |
val (time', step') = minimized_isar_step ctxt [] time step |
58079
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
69 |
in |
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
70 |
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
|
71 |
((meth, Played time') :: (if step' = step then map old_data_for_method meths else [])); |
55264 | 72 |
step' |
54826 | 73 |
end |
74 |
| _ => step (* don't touch steps that time out or fail *)) |
|
57054 | 75 |
| minimize_isar_step_dependencies _ _ step = step |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
76 |
|
72583 | 77 |
fun postprocess_isar_proof_remove_show_stuttering (proof as Proof {steps, ...}) = |
58083 | 78 |
let |
79 |
fun process_steps [] = [] |
|
61312
6d779a71086d
further reduced dependency on legacy async thread manager
blanchet
parents:
60305
diff
changeset
|
80 |
| process_steps (steps as [Prove ([], [], _, t1, subs1, facts1, meths1, comment1), |
58083 | 81 |
Prove ([Show], [], l2, t2, _, _, _, comment2)]) = |
82 |
if t1 aconv t2 then [Prove ([Show], [], l2, t2, subs1, facts1, meths1, comment1 ^ comment2)] |
|
83 |
else steps |
|
84 |
| process_steps (step :: steps) = step :: process_steps steps |
|
85 |
in |
|
72583 | 86 |
isar_proof_with_steps proof (process_steps steps) |
58083 | 87 |
end |
88 |
||
55213 | 89 |
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
|
90 |
let |
72583 | 91 |
fun process_proof (proof as Proof {steps, ...}) = |
92 |
process_steps steps ||> isar_proof_with_steps proof |
|
55259 | 93 |
and process_steps [] = ([], []) |
94 |
| process_steps steps = |
|
55212 | 95 |
(* the last step is always implicitly referenced *) |
55265 | 96 |
let val (steps, (used, concl)) = split_last steps ||> process_used_step in |
97 |
fold_rev process_step steps (used, [concl]) |
|
54754 | 98 |
end |
55265 | 99 |
and process_step step (used, accu) = |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
100 |
(case label_of_isar_step step of |
55265 | 101 |
NONE => (used, step :: accu) |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
102 |
| SOME l => |
55265 | 103 |
if Ord_List.member label_ord used l then |
104 |
process_used_step step |>> Ord_List.union label_ord used ||> (fn step => step :: accu) |
|
54813 | 105 |
else |
55265 | 106 |
(used, accu)) |
58083 | 107 |
and process_used_step step = process_used_step_subproofs (postproc_step step) |
55299 | 108 |
and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) = |
55259 | 109 |
let |
55265 | 110 |
val (used, subproofs) = |
55259 | 111 |
map process_proof subproofs |
112 |
|> split_list |
|
113 |
|>> Ord_List.unions label_ord |
|
114 |
|>> fold (Ord_List.insert label_ord) lfs |
|
115 |
in |
|
55299 | 116 |
(used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) |
55259 | 117 |
end |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
118 |
in |
55259 | 119 |
snd o process_proof |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
120 |
end |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
121 |
|
54504 | 122 |
end; |