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