author | blanchet |
Fri, 01 Aug 2014 14:43:57 +0200 | |
changeset 57732 | e1b2442dc629 |
parent 57731 | d99080b7f961 |
child 57739 | b6af899a78ac |
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 |
|
55213 | 18 |
val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> |
19 |
isar_proof |
|
54504 | 20 |
end; |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
21 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
22 |
structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE = |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
23 |
struct |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
24 |
|
57675
47336af5d2b2
faster minimization by not adding facts that are already in the simpset
blanchet
parents:
57054
diff
changeset
|
25 |
open Sledgehammer_Util |
55287 | 26 |
open Sledgehammer_Proof_Methods |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
27 |
open Sledgehammer_Isar_Proof |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
28 |
open Sledgehammer_Isar_Preplay |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
29 |
|
55299 | 30 |
fun keep_fastest_method_of_isar_step preplay_data |
31 |
(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
|
32 |
Prove (qs, xs, l, t, subproofs, facts, |
55299 | 33 |
meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @, |
34 |
comment) |
|
55266 | 35 |
| keep_fastest_method_of_isar_step _ step = step |
36 |
||
55324 | 37 |
val slack = seconds 0.025 |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
38 |
|
57731 | 39 |
fun minimized_isar_step ctxt time |
40 |
(Prove (qs, xs, l, t, subproofs, (lfs0, gfs00), meths as meth :: _, comment)) = |
|
41 |
let |
|
42 |
val gfs0 = filter (thms_influence_proof_method ctxt meth o thms_of_name ctxt) gfs00 |
|
43 |
||
44 |
fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment) |
|
45 |
||
46 |
fun minimize_facts _ min_facts [] time = (min_facts, time) |
|
47 |
| minimize_facts mk_step min_facts (fact :: facts) time = |
|
48 |
(case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth |
|
49 |
(mk_step (min_facts @ facts)) of |
|
50 |
Played time' => minimize_facts mk_step min_facts facts time' |
|
51 |
| _ => minimize_facts mk_step (fact :: min_facts) facts time) |
|
52 |
||
53 |
val (min_lfs, time') = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time |
|
54 |
val (min_gfs, time'') = minimize_facts (mk_step_lfs_gfs min_lfs) [] gfs0 time' |
|
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 |
57731 | 60 |
(step as Prove (_, _, l, _, _, _, meth :: _, _)) = |
55266 | 61 |
(case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of |
54828 | 62 |
Played time => |
57731 | 63 |
let val (time', step') = minimized_isar_step ctxt time step in |
64 |
set_preplay_outcomes_of_isar_step ctxt time' preplay_data step' [(meth, Played time')]; |
|
55264 | 65 |
step' |
54826 | 66 |
end |
67 |
| _ => step (* don't touch steps that time out or fail *)) |
|
57054 | 68 |
| minimize_isar_step_dependencies _ _ step = step |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
69 |
|
55213 | 70 |
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
|
71 |
let |
55259 | 72 |
fun process_proof (Proof (fix, assms, steps)) = |
55265 | 73 |
process_steps steps ||> (fn steps => Proof (fix, assms, steps)) |
55259 | 74 |
and process_steps [] = ([], []) |
75 |
| process_steps steps = |
|
55212 | 76 |
(* the last step is always implicitly referenced *) |
55265 | 77 |
let val (steps, (used, concl)) = split_last steps ||> process_used_step in |
78 |
fold_rev process_step steps (used, [concl]) |
|
54754 | 79 |
end |
55265 | 80 |
and process_step step (used, accu) = |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
81 |
(case label_of_isar_step step of |
55265 | 82 |
NONE => (used, step :: accu) |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
83 |
| SOME l => |
55265 | 84 |
if Ord_List.member label_ord used l then |
85 |
process_used_step step |>> Ord_List.union label_ord used ||> (fn step => step :: accu) |
|
54813 | 86 |
else |
55265 | 87 |
(used, accu)) |
88 |
and process_used_step step = step |> postproc_step |> process_used_step_subproofs |
|
55299 | 89 |
and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) = |
55259 | 90 |
let |
55265 | 91 |
val (used, subproofs) = |
55259 | 92 |
map process_proof subproofs |
93 |
|> split_list |
|
94 |
|>> Ord_List.unions label_ord |
|
95 |
|>> fold (Ord_List.insert label_ord) lfs |
|
96 |
in |
|
55299 | 97 |
(used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) |
55259 | 98 |
end |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
99 |
in |
55259 | 100 |
snd o process_proof |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
101 |
end |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
102 |
|
54504 | 103 |
end; |