author | blanchet |
Fri, 02 Oct 2015 21:15:25 +0200 | |
changeset 61312 | 6d779a71086d |
parent 60305 | 7d278b0617d3 |
child 62219 | dbac573b27e7 |
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 |
60305
7d278b0617d3
took out Sledgehammer minimizer optimization that breaks things
blanchet
parents:
58083
diff
changeset
|
41 |
(Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) = |
57731 | 42 |
let |
57779 | 43 |
fun mk_step_lfs_gfs lfs gfs = |
58079
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
44 |
Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), meths, comment) |
57731 | 45 |
|
57739 | 46 |
fun minimize_half _ min_facts [] time = (min_facts, time) |
47 |
| minimize_half mk_step min_facts (fact :: facts) time = |
|
57731 | 48 |
(case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth |
49 |
(mk_step (min_facts @ facts)) of |
|
57739 | 50 |
Played time' => minimize_half mk_step min_facts facts time' |
51 |
| _ => minimize_half mk_step (fact :: min_facts) facts time) |
|
57731 | 52 |
|
57739 | 53 |
val (min_lfs, time') = minimize_half (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time |
54 |
val (min_gfs, time'') = minimize_half (mk_step_lfs_gfs min_lfs) [] gfs0 time' |
|
57731 | 55 |
in |
56 |
(time'', mk_step_lfs_gfs min_lfs min_gfs) |
|
57 |
end |
|
58 |
||
57054 | 59 |
fun minimize_isar_step_dependencies ctxt preplay_data |
58079
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
60 |
(step as Prove (_, _, l, _, _, _, meth :: meths, _)) = |
55266 | 61 |
(case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of |
54828 | 62 |
Played time => |
58079
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
63 |
let |
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
64 |
fun old_data_for_method meth' = |
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
65 |
(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
|
66 |
|
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
67 |
val (time', step') = minimized_isar_step ctxt time step |
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
68 |
in |
df0d6ce8fb66
made trace more informative when minimization is enabled
blanchet
parents:
58076
diff
changeset
|
69 |
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
|
70 |
((meth, Played time') :: (if step' = step then map old_data_for_method meths else [])); |
55264 | 71 |
step' |
54826 | 72 |
end |
73 |
| _ => step (* don't touch steps that time out or fail *)) |
|
57054 | 74 |
| minimize_isar_step_dependencies _ _ step = step |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
75 |
|
58083 | 76 |
fun postprocess_isar_proof_remove_show_stuttering (Proof (fix, assms, steps)) = |
77 |
let |
|
78 |
fun process_steps [] = [] |
|
61312
6d779a71086d
further reduced dependency on legacy async thread manager
blanchet
parents:
60305
diff
changeset
|
79 |
| process_steps (steps as [Prove ([], [], _, t1, subs1, facts1, meths1, comment1), |
58083 | 80 |
Prove ([Show], [], l2, t2, _, _, _, comment2)]) = |
81 |
if t1 aconv t2 then [Prove ([Show], [], l2, t2, subs1, facts1, meths1, comment1 ^ comment2)] |
|
82 |
else steps |
|
83 |
| process_steps (step :: steps) = step :: process_steps steps |
|
84 |
in |
|
85 |
Proof (fix, assms, process_steps steps) |
|
86 |
end |
|
87 |
||
55213 | 88 |
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
|
89 |
let |
55259 | 90 |
fun process_proof (Proof (fix, assms, steps)) = |
55265 | 91 |
process_steps steps ||> (fn steps => Proof (fix, assms, steps)) |
55259 | 92 |
and process_steps [] = ([], []) |
93 |
| process_steps steps = |
|
55212 | 94 |
(* the last step is always implicitly referenced *) |
55265 | 95 |
let val (steps, (used, concl)) = split_last steps ||> process_used_step in |
96 |
fold_rev process_step steps (used, [concl]) |
|
54754 | 97 |
end |
55265 | 98 |
and process_step step (used, accu) = |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
99 |
(case label_of_isar_step step of |
55265 | 100 |
NONE => (used, step :: accu) |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
101 |
| SOME l => |
55265 | 102 |
if Ord_List.member label_ord used l then |
103 |
process_used_step step |>> Ord_List.union label_ord used ||> (fn step => step :: accu) |
|
54813 | 104 |
else |
55265 | 105 |
(used, accu)) |
58083 | 106 |
and process_used_step step = process_used_step_subproofs (postproc_step step) |
55299 | 107 |
and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) = |
55259 | 108 |
let |
55265 | 109 |
val (used, subproofs) = |
55259 | 110 |
map process_proof subproofs |
111 |
|> split_list |
|
112 |
|>> Ord_List.unions label_ord |
|
113 |
|>> fold (Ord_List.insert label_ord) lfs |
|
114 |
in |
|
55299 | 115 |
(used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) |
55259 | 116 |
end |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
117 |
in |
55259 | 118 |
snd o process_proof |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
119 |
end |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
120 |
|
54504 | 121 |
end; |